summaryrefslogtreecommitdiff
path: root/src/full/Agda/Syntax/Concrete/Definitions.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Syntax/Concrete/Definitions.hs')
-rw-r--r--src/full/Agda/Syntax/Concrete/Definitions.hs232
1 files changed, 136 insertions, 96 deletions
diff --git a/src/full/Agda/Syntax/Concrete/Definitions.hs b/src/full/Agda/Syntax/Concrete/Definitions.hs
index acc46d1..af11faf 100644
--- a/src/full/Agda/Syntax/Concrete/Definitions.hs
+++ b/src/full/Agda/Syntax/Concrete/Definitions.hs
@@ -1,9 +1,13 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE DeriveDataTypeable #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE PatternGuards #-}
-{-# LANGUAGE TupleSections #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+-- GHC 7.4.2 requires this layout for the pragmas. See Issue 1460.
+{-# LANGUAGE CPP,
+ DeriveDataTypeable,
+ FlexibleInstances,
+ PatternGuards,
+ TupleSections #-}
+
+#if __GLASGOW_HASKELL__ >= 710
+{-# LANGUAGE FlexibleContexts #-}
+#endif
-- | Preprocess 'Agda.Syntax.Concrete.Declaration's, producing 'NiceDeclaration's.
--
@@ -39,15 +43,28 @@ module Agda.Syntax.Concrete.Definitions
, Measure
) where
+import Prelude hiding (null)
+
import Control.Arrow ((***))
-import Control.Applicative
+import Control.Applicative hiding (empty)
import Control.Monad.State
-import Data.Foldable hiding (concatMap, mapM_, notElem, elem, all)
+import Data.Foldable hiding
+ ( all
+ , concatMap
+ , elem
+ , mapM_
+ , notElem
+#if MIN_VERSION_base(4,8,0)
+ , null
+#endif
+ )
+
import qualified Data.Map as Map
import Data.Map (Map)
+import Data.Maybe
import Data.Monoid ( Monoid(mappend, mempty) )
-import Data.List as List
+import Data.List as List hiding (null)
import Data.Traversable (traverse)
import Data.Typeable (Typeable)
@@ -63,6 +80,7 @@ import Agda.Utils.Except ( Error(noMsg, strMsg), MonadError(throwError) )
import Agda.Utils.Lens
import Agda.Utils.List (headMaybe, isSublistOf)
import Agda.Utils.Monad
+import Agda.Utils.Null
import Agda.Utils.Pretty
import Agda.Utils.Update
@@ -79,28 +97,32 @@ import Agda.Utils.Impossible
modifiers have been distributed to the individual declarations.
-}
data NiceDeclaration
- = Axiom Range Fixity' Access IsInstance ArgInfo Name Expr
- -- ^ Axioms and functions can be declared irrelevant. (Hiding should be NotHidden)
- | NiceField Range Fixity' Access IsAbstract Name (Arg Expr)
- | PrimitiveFunction Range Fixity' Access IsAbstract Name Expr
- | NiceMutual Range TerminationCheck [NiceDeclaration]
- | NiceModule Range Access IsAbstract QName Telescope [Declaration]
- | NiceModuleMacro Range Access Name ModuleApplication OpenShortHand ImportDirective
- | NiceOpen Range QName ImportDirective
- | NiceImport Range QName (Maybe AsName) OpenShortHand ImportDirective
- | NicePragma Range Pragma
- | NiceRecSig Range Fixity' Access Name [LamBinding] Expr
- | NiceDataSig Range Fixity' Access Name [LamBinding] Expr
- | NiceFunClause Range Access IsAbstract TerminationCheck Declaration
- -- ^ a uncategorized function clause, could be a function clause
- -- without type signature or a pattern lhs (e.g. for irrefutable let)x
- | FunSig Range Fixity' Access IsInstance ArgInfo TerminationCheck Name Expr
- | FunDef Range [Declaration] Fixity' IsAbstract TerminationCheck Name [Clause] -- ^ block of function clauses (we have seen the type signature before)
- | DataDef Range Fixity' IsAbstract Name [LamBinding] [NiceConstructor]
- | RecDef Range Fixity' IsAbstract Name (Maybe (Ranged Induction)) (Maybe (ThingWithFixity Name)) [LamBinding] [NiceDeclaration]
- | NicePatternSyn Range Fixity' Name [Arg Name] Pattern
- | NiceUnquoteDecl Range Fixity' Access IsAbstract TerminationCheck Name Expr
- deriving (Typeable, Show)
+ = Axiom Range Fixity' Access IsInstance ArgInfo Name Expr
+ -- ^ Axioms and functions can be declared irrelevant. (Hiding should be NotHidden)
+ | NiceField Range Fixity' Access IsAbstract Name (Arg Expr)
+ | PrimitiveFunction Range Fixity' Access IsAbstract Name Expr
+ | NiceMutual Range TerminationCheck [NiceDeclaration]
+ | NiceModule Range Access IsAbstract QName Telescope [Declaration]
+ | NiceModuleMacro Range Access Name ModuleApplication OpenShortHand ImportDirective
+ | NiceOpen Range QName ImportDirective
+ | NiceImport Range QName (Maybe AsName) OpenShortHand ImportDirective
+ | NicePragma Range Pragma
+ | NiceRecSig Range Fixity' Access Name [LamBinding] Expr
+ | NiceDataSig Range Fixity' Access Name [LamBinding] Expr
+ | NiceFunClause Range Access IsAbstract TerminationCheck Declaration
+ -- ^ An uncategorized function clause, could be a function clause
+ -- without type signature or a pattern lhs (e.g. for irrefutable let).
+ -- The 'Declaration' is the actual 'FunClause'.
+ | FunSig Range Fixity' Access IsInstance ArgInfo TerminationCheck Name Expr
+ | FunDef Range [Declaration] Fixity' IsAbstract TerminationCheck Name [Clause]
+ -- ^ Block of function clauses (we have seen the type signature before).
+ -- The 'Declaration's are the original declarations that were processed
+ -- into this 'FunDef' and are only used in 'notSoNiceDeclaration'.
+ | DataDef Range Fixity' IsAbstract Name [LamBinding] [NiceConstructor]
+ | RecDef Range Fixity' IsAbstract Name (Maybe (Ranged Induction)) (Maybe (ThingWithFixity Name)) [LamBinding] [NiceDeclaration]
+ | NicePatternSyn Range Fixity' Name [Arg Name] Pattern
+ | NiceUnquoteDecl Range Fixity' Access IsInstance IsAbstract TerminationCheck Name Expr
+ deriving (Typeable, Show)
type TerminationCheck = Common.TerminationCheck Measure
@@ -121,6 +143,8 @@ data Clause = Clause Name LHS RHS WhereClause [Clause]
-- | The exception type.
data DeclarationException
= MultipleFixityDecls [(Name, [Fixity'])]
+ | InvalidName Name
+ | DuplicateDefinition Name
| MissingDefinition Name
| MissingWithClauses Name
| MissingTypeSignature LHS -- Andreas 2012-06-02: currently unused, remove after a while -- Fredrik 2012-09-20: now used, can we keep it?
@@ -147,6 +171,8 @@ data DeclarationException
instance HasRange DeclarationException where
getRange (MultipleFixityDecls xs) = getRange (fst $ head xs)
+ getRange (InvalidName x) = getRange x
+ getRange (DuplicateDefinition x) = getRange x
getRange (MissingDefinition x) = getRange x
getRange (MissingWithClauses x) = getRange x
getRange (MissingTypeSignature x) = getRange x
@@ -184,7 +210,7 @@ instance HasRange NiceDeclaration where
getRange (NiceDataSig r _ _ _ _ _) = r
getRange (NicePatternSyn r _ _ _ _) = r
getRange (NiceFunClause r _ _ _ _) = r
- getRange (NiceUnquoteDecl r _ _ _ _ _ _) = r
+ getRange (NiceUnquoteDecl r _ _ _ _ _ _ _) = r
instance Error DeclarationException where
noMsg = strMsg ""
@@ -192,46 +218,53 @@ instance Error DeclarationException where
-- These error messages can (should) be terminated by a dot ".",
-- there is no error context printed after them.
-instance Show DeclarationException where
- show (MultipleFixityDecls xs) = show $
+instance Pretty DeclarationException where
+ pretty (MultipleFixityDecls xs) =
sep [ fsep $ pwords "Multiple fixity or syntax declarations for"
, vcat $ map f xs
]
where
f (x, fs) = pretty x <> text ": " <+> fsep (map pretty fs)
- show (MissingDefinition x) = show $ fsep $
+ pretty (InvalidName x) = fsep $
+ pwords "Invalid name:" ++ [pretty x]
+ pretty (DuplicateDefinition x) = fsep $
+ pwords "Duplicate definition of" ++ [pretty x]
+ pretty (MissingDefinition x) = fsep $
pwords "Missing definition for" ++ [pretty x]
- show (MissingWithClauses x) = show $ fsep $
+ pretty (MissingWithClauses x) = fsep $
pwords "Missing with-clauses for function" ++ [pretty x]
- show (MissingTypeSignature x) = show $ fsep $
+ pretty (MissingTypeSignature x) = fsep $
pwords "Missing type signature for left hand side" ++ [pretty x]
- show (MissingDataSignature x) = show $ fsep $
+ pretty (MissingDataSignature x) = fsep $
pwords "Missing type signature for " ++ [pretty x]
- show (WrongDefinition x k k') = show $ fsep $ pretty x :
+ pretty (WrongDefinition x k k') = fsep $ pretty x :
pwords ("has been declared as a " ++ show k ++
", but is being defined as a " ++ show k')
- show (WrongParameters x) = show $ fsep $
+ pretty (WrongParameters x) = fsep $
pwords "List of parameters does not match previous signature for" ++ [pretty x]
- show (AmbiguousFunClauses lhs xs) = show $ fsep $
- pwords "More than one matching type signature for left hand side" ++ [pretty lhs] ++
- pwords "it could belong to any of:" ++ map pretty xs
- show (UnknownNamesInFixityDecl xs) = show $ fsep $
+ pretty (AmbiguousFunClauses lhs xs) = sep
+ [ fsep $
+ pwords "More than one matching type signature for left hand side " ++ [pretty lhs] ++
+ pwords "it could belong to any of:"
+ , vcat $ map (pretty . PrintRange) xs
+ ]
+ pretty (UnknownNamesInFixityDecl xs) = fsep $
pwords "The following names are not declared in the same scope as their syntax or fixity declaration (i.e., either not in scope at all, imported from another module, or declared in a super module):" ++ map pretty xs
- show (UselessPrivate _) = show $ fsep $
+ pretty (UselessPrivate _) = fsep $
pwords "Using private here has no effect. Private applies only to declarations that introduce new identifiers into the module, like type signatures and data, record, and module declarations."
- show (UselessAbstract _) = show $ fsep $
+ pretty (UselessAbstract _) = fsep $
pwords "Using abstract here has no effect. Abstract applies only definitions like data definitions, record type definitions and function clauses."
- show (UselessInstance _) = show $ fsep $
+ pretty (UselessInstance _) = fsep $
pwords "Using instance here has no effect. Instance applies only to declarations that introduce new identifiers into the module, like type signatures and axioms."
- show (WrongContentPostulateBlock _) = show $ fsep $
+ pretty (WrongContentPostulateBlock _) = fsep $
pwords "A postulate block can only contain type signatures or instance blocks"
- show (PragmaNoTerminationCheck _) = show $ fsep $
+ pretty (PragmaNoTerminationCheck _) = fsep $
pwords "Pragma {-# NO_TERMINATION_CHECK #-} has been removed. To skip the termination check, label your definitions either as {-# TERMINATING #-} or {-# NON_TERMINATING #-}."
- show (InvalidTerminationCheckPragma _) = show $ fsep $
+ pretty (InvalidTerminationCheckPragma _) = fsep $
pwords "Termination checking pragmas can only precede a mutual block or a function definition."
- show (InvalidMeasureMutual _) = show $ fsep $
+ pretty (InvalidMeasureMutual _) = fsep $
pwords "In a mutual block, either all functions must have the same (or no) termination checking pragma."
- show (NotAllowedInMutual nd) = show $ fsep $
+ pretty (NotAllowedInMutual nd) = fsep $
[text $ decl nd] ++ pwords "are not allowed in mutual blocks"
where
decl Axiom{} = "Postulates"
@@ -252,10 +285,10 @@ instance Show DeclarationException where
decl FunDef{} = __IMPOSSIBLE__
decl RecDef{} = __IMPOSSIBLE__
decl DataDef{} = __IMPOSSIBLE__
- show (Codata _) =
+ pretty (Codata _) = text $
"The codata construction has been removed. " ++
"Use the INFINITY builtin instead."
- show (DeclarationPanic s) = s
+ pretty (DeclarationPanic s) = text s
{--------------------------------------------------------------------------
The niceifier
@@ -336,15 +369,15 @@ data NiceEnv = NiceEnv
, fixs :: Fixities
}
-type LoneSigs = [(DataRecOrFun, Name)]
+type LoneSigs = Map Name DataRecOrFun
type Fixities = Map Name Fixity'
-- | Initial nicifier state.
initNiceEnv :: NiceEnv
initNiceEnv = NiceEnv
- { _loneSigs = []
- , fixs = Map.empty
+ { _loneSigs = empty
+ , fixs = empty
}
-- * Handling the lone signatures, stored to infer mutual blocks.
@@ -356,18 +389,22 @@ loneSigs f e = f (_loneSigs e) <&> \ s -> e { _loneSigs = s }
-- | Adding a lone signature to the state.
-addLoneSig :: DataRecOrFun -> Name -> Nice ()
-addLoneSig k x = loneSigs %= ((k, x) :)
+addLoneSig :: Name -> DataRecOrFun -> Nice ()
+addLoneSig x k = loneSigs %== \ s -> do
+ let (mr, s') = Map.insertLookupWithKey (\ k new old -> new) x k s
+ case mr of
+ Nothing -> return s'
+ Just{} -> throwError $ DuplicateDefinition x
-- | Remove a lone signature from the state.
removeLoneSig :: Name -> Nice ()
-removeLoneSig x = loneSigs %= filter (\ (k', x') -> x /= x')
+removeLoneSig x = loneSigs %= Map.delete x
-- | Search for forward type signature.
getSig :: Name -> Nice (Maybe DataRecOrFun)
-getSig n = fmap fst . List.find (\ (k, x) -> x == n) <$> use loneSigs
+getSig x = Map.lookup x <$> use loneSigs
-- | Check that no lone signatures are left in the state.
@@ -376,15 +413,17 @@ noLoneSigs = null <$> use loneSigs
-- | Ensure that all forward declarations have been given a definition.
-checkLoneSigs :: LoneSigs -> Nice ()
+checkLoneSigs :: [(Name, a)] -> Nice ()
checkLoneSigs xs =
case xs of
[] -> return ()
- (_, x):_ -> throwError $ MissingDefinition x
-
+ (x, _):_ -> throwError $ MissingDefinition x
+-- | Check whether name is not "_" and return its fixity.
getFixity :: Name -> Nice Fixity'
-getFixity x = gets $ Map.findWithDefault defaultFixity' x . fixs
+getFixity x = do
+ when (isUnderscore x) $ throwError $ InvalidName x
+ gets $ Map.findWithDefault defaultFixity' x . fixs
runNice :: Nice a -> Either DeclarationException a
runNice nice = nice `evalStateT` initNiceEnv
@@ -425,7 +464,7 @@ niceDeclarations ds = do
put $ initNiceEnv { fixs = fixs }
ds <- nice ds
-- Check that every signature got its definition.
- checkLoneSigs =<< use loneSigs
+ checkLoneSigs . Map.toList =<< use loneSigs
-- Note that loneSigs is ensured to be empty.
-- (Important, since inferMutualBlocks also uses loneSigs state).
inferMutualBlocks ds
@@ -467,7 +506,7 @@ niceDeclarations ds = do
OtherDecl -> (d :) <$> inferMutualBlocks ds
LoneDef _ x -> __IMPOSSIBLE__
LoneSig k x -> do
- addLoneSig k x
+ addLoneSig x k
(tcs, (ds0, ds1)) <- untilAllDefined [terminationCheck k] ds
tc <- combineTermChecks (getRange d) tcs
@@ -486,9 +525,9 @@ niceDeclarations ds = do
done <- noLoneSigs
if done then return (tc, ([], ds)) else
case ds of
- [] -> __IMPOSSIBLE__ <$ (checkLoneSigs =<< use loneSigs)
+ [] -> __IMPOSSIBLE__ <$ (checkLoneSigs . Map.toList =<< use loneSigs)
d : ds -> case declKind d of
- LoneSig k x -> addLoneSig k x >> cons d (untilAllDefined (terminationCheck k : tc) ds)
+ LoneSig k x -> addLoneSig x k >> cons d (untilAllDefined (terminationCheck k : tc) ds)
LoneDef k x -> removeLoneSig x >> cons d (untilAllDefined (terminationCheck k : tc) ds)
OtherDecl -> cons d (untilAllDefined tc ds)
where
@@ -512,8 +551,8 @@ niceDeclarations ds = do
nice (Pragma (TerminationCheckPragma r tc) : d@FunClause{} : ds) | notMeasure tc =
niceFunClause tc d ds
nice (Pragma (TerminationCheckPragma r tc) : ds@(UnquoteDecl{} : _)) | notMeasure tc = do
- NiceUnquoteDecl r f p a _ x e : ds <- nice ds
- return $ NiceUnquoteDecl r f p a tc x e : ds
+ NiceUnquoteDecl r f p a i _ x e : ds <- nice ds
+ return $ NiceUnquoteDecl r f p a i tc x e : ds
nice (d@TypeSig{} : Pragma (TerminationCheckPragma r (TerminationMeasure _ x)) : ds) =
niceTypeSig (TerminationMeasure r x) d ds
@@ -528,7 +567,7 @@ niceDeclarations ds = do
DataSig r CoInductive x tel t -> throwError (Codata r)
Data r CoInductive x tel t cs -> throwError (Codata r)
DataSig r Inductive x tel t -> do
- addLoneSig (DataName $ parameters tel) x
+ addLoneSig x (DataName $ parameters tel)
(++) <$> dataOrRec DataDef NiceDataSig niceAxioms r x tel (Just t) Nothing
<*> nice ds
Data r Inductive x tel t cs -> do
@@ -536,7 +575,7 @@ niceDeclarations ds = do
(++) <$> dataOrRec DataDef NiceDataSig niceAxioms r x tel t (Just cs)
<*> nice ds
RecordSig r x tel t -> do
- addLoneSig (RecName $ parameters tel) x
+ addLoneSig x (RecName $ parameters tel)
fx <- getFixity x
(NiceRecSig r fx PublicAccess x tel t :) <$> nice ds
Record r x i c tel t cs -> do
@@ -580,7 +619,7 @@ niceDeclarations ds = do
UnquoteDecl r x e -> do
fx <- getFixity x
- (NiceUnquoteDecl r fx PublicAccess ConcreteDef TerminationCheck x e :) <$> nice ds
+ (NiceUnquoteDecl r fx PublicAccess NotInstanceDef ConcreteDef TerminationCheck x e :) <$> nice ds
-- Andreas, AIM XX: do not forbid NO_TERMINATION_CHECK in maintenance version.
-- Pragma (TerminationCheckPragma r NoTerminationCheck) ->
-- throwError $ PragmaNoTerminationCheck r
@@ -590,7 +629,7 @@ niceDeclarations ds = do
niceFunClause :: TerminationCheck -> Declaration -> [Declaration] -> Nice [NiceDeclaration]
niceFunClause termCheck d@(FunClause lhs _ _) ds = do
- xs <- map snd . filter (isFunName . fst) <$> use loneSigs
+ xs <- map fst . filter (isFunName . snd) . Map.toList <$> use loneSigs
-- for each type signature 'x' waiting for clauses, we try
-- if we have some clauses for 'x'
fixs <- gets fixs
@@ -626,14 +665,14 @@ niceDeclarations ds = do
return $ d : ds1
-- case: clauses match more than one sigs (ambiguity)
- l -> throwError $ AmbiguousFunClauses lhs (map fst l) -- "ambiguous function clause; cannot assign it uniquely to one type signature"
+ l -> throwError $ AmbiguousFunClauses lhs $ reverse $ map fst l -- "ambiguous function clause; cannot assign it uniquely to one type signature"
niceFunClause _ _ _ = __IMPOSSIBLE__
niceTypeSig :: TerminationCheck -> Declaration -> [Declaration] -> Nice [NiceDeclaration]
niceTypeSig termCheck d@(TypeSig info x t) ds = do
fx <- getFixity x
-- register x as lone type signature, to recognize clauses later
- addLoneSig (FunName termCheck) x
+ addLoneSig x (FunName termCheck)
ds <- nice ds
return $ FunSig (getRange d) fx PublicAccess NotInstanceDef info termCheck x t : ds
niceTypeSig _ _ _ = __IMPOSSIBLE__
@@ -653,13 +692,15 @@ niceDeclarations ds = do
dataOrRec mkDef mkSig niceD r x tel mt mcs = do
mds <- traverse niceD mcs
f <- getFixity x
- return $
- [mkSig (fuseRange x t) f PublicAccess x tel t | Just t <- [mt] ] ++
- [mkDef (getRange x) f ConcreteDef x (concatMap dropType tel) ds | Just ds <- [mds] ]
+ return $ catMaybes $
+ [ mt <&> \ t -> mkSig (fuseRange x t) f PublicAccess x tel t
+ , mkDef r f ConcreteDef x (concatMap dropType tel) <$> mds
+ ]
where
- dropType (DomainFull (TypedBindings r (Common.Arg i (TBind _ xs _)))) =
- map (DomainFree i) xs
- dropType (DomainFull (TypedBindings _ (Common.Arg _ TLet{}))) = []
+ dropType :: LamBinding -> [LamBinding]
+ dropType (DomainFull (TypedBindings _r (Common.Arg ai (TBind _ xs _)))) =
+ map (mergeHiding . fmap (DomainFree ai)) xs
+ dropType (DomainFull (TypedBindings _r (Common.Arg _ TLet{}))) = []
dropType b@DomainFree{} = [b]
-- Translate axioms
@@ -702,10 +743,10 @@ niceDeclarations ds = do
d : expand p ps ds
where
expand _ _ [] = []
- expand p ps (FunClause (Ellipsis _ ps' eqs []) rhs wh : ds) =
- FunClause (LHS p (ps ++ ps') eqs []) rhs wh : expand p ps ds
- expand p ps (FunClause (Ellipsis _ ps' eqs es) rhs wh : ds) =
- FunClause (LHS p (ps ++ ps') eqs es) rhs wh : expand p (ps ++ ps') ds
+ expand p ps (FunClause (Ellipsis r ps' eqs []) rhs wh : ds) =
+ FunClause (LHS (setRange r p) ((setRange r ps) ++ ps') eqs []) rhs wh : expand p ps ds
+ expand p ps (FunClause (Ellipsis r ps' eqs es) rhs wh : ds) =
+ FunClause (LHS (setRange r p) ((setRange r ps) ++ ps') eqs es) rhs wh : expand p (ps ++ ps') ds
expand p ps (d@(FunClause (LHS _ _ _ []) _ _) : ds) =
d : expand p ps ds
expand _ _ (d@(FunClause (LHS p ps _ (_ : _)) _ _) : ds) =
@@ -807,10 +848,10 @@ niceDeclarations ds = do
isTypeSig d | LoneSig{} <- declKind d = True
isTypeSig _ = False
- sigNames = [ (k, x) | LoneSig k x <- map declKind ds ]
- defNames = [ (k, x) | LoneDef k x <- map declKind ds ]
+ sigNames = [ (x, k) | LoneSig k x <- map declKind ds ]
+ defNames = [ (x, k) | LoneDef k x <- map declKind ds ]
-- compute the set difference with equality just on names
- loneNames = [ (k, x) | (k, x) <- sigNames, List.all ((x /=) . snd) defNames ]
+ loneNames = [ (x, k) | (x, k) <- sigNames, List.all ((x /=) . fst) defNames ]
-- Andreas, 2013-02-28 (issue 804):
-- do not termination check a mutual block if any of its
@@ -818,7 +859,7 @@ niceDeclarations ds = do
termCheck (FunSig _ _ _ _ _ tc _ _) = tc
termCheck (FunDef _ _ _ _ tc _ _) = tc
termCheck (NiceMutual _ tc _) = tc
- termCheck (NiceUnquoteDecl _ _ _ _ tc _ _) = tc
+ termCheck (NiceUnquoteDecl _ _ _ _ _ tc _ _) = tc
termCheck _ = TerminationCheck
-- A mutual block cannot have a measure,
@@ -844,7 +885,7 @@ niceDeclarations ds = do
-- no effect on fields or primitives, the InAbstract field there is unused
NiceField r f p _ x e -> return $ NiceField r f p AbstractDef x e
PrimitiveFunction r f p _ x e -> return $ PrimitiveFunction r f p AbstractDef x e
- NiceUnquoteDecl r f p _ t x e -> return $ NiceUnquoteDecl r f p AbstractDef t x e
+ NiceUnquoteDecl r f p i _ t x e -> return $ NiceUnquoteDecl r f p i AbstractDef t x e
NiceModule{} -> return $ d
NiceModuleMacro{} -> return $ d
Axiom{} -> return $ d
@@ -895,7 +936,7 @@ niceDeclarations ds = do
NiceRecSig r f p x ls t -> (\ p -> NiceRecSig r f p x ls t) <$> setPrivate p
NiceDataSig r f p x ls t -> (\ p -> NiceDataSig r f p x ls t) <$> setPrivate p
NiceFunClause r p a termCheck d -> (\ p -> NiceFunClause r p a termCheck d) <$> setPrivate p
- NiceUnquoteDecl r f p a t x e -> (\ p -> NiceUnquoteDecl r f p a t x e) <$> setPrivate p
+ NiceUnquoteDecl r f p i a t x e -> (\ p -> NiceUnquoteDecl r f p i a t x e) <$> setPrivate p
NicePragma _ _ -> return $ d
NiceOpen _ _ _ -> return $ d
NiceImport _ _ _ _ _ -> return $ d
@@ -933,12 +974,12 @@ niceDeclarations ds = do
case d of
Axiom r f p i rel x e -> (\ i -> Axiom r f p i rel x e) <$> setInstance i
FunSig r f p i rel tc x e -> (\ i -> FunSig r f p i rel tc x e) <$> setInstance i
+ NiceUnquoteDecl r f p i a tc x e -> (\ i -> NiceUnquoteDecl r f p i a tc x e) <$> setInstance i
NiceMutual{} -> return $ d
NiceFunClause{} -> return $ d
FunDef{} -> return $ d
NiceField{} -> return $ d
PrimitiveFunction{} -> return $ d
- NiceUnquoteDecl{} -> return $ d
NiceRecSig{} -> return $ d
NiceDataSig{} -> return $ d
NiceModuleMacro{} -> return $ d
@@ -1055,5 +1096,4 @@ notSoNiceDeclaration d =
RecDef r _ _ x i c bs ds -> Record r x i (unThing <$> c) bs Nothing $ map notSoNiceDeclaration ds
where unThing (ThingWithFixity c _) = c
NicePatternSyn r _ n as p -> PatternSyn r n as p
- NiceUnquoteDecl r _ _ _ _ x e -> UnquoteDecl r x e
-
+ NiceUnquoteDecl r _ _ _ _ _ x e -> UnquoteDecl r x e