26
27
import Control.Monad.Reader hiding (mapM)
27
28
import Control.Monad.Error hiding (mapM)
28
29
import Data.Typeable
29
import Data.Traversable (mapM)
30
import Data.List ((\\), nub)
30
import Data.Traversable (mapM, traverse)
31
import Data.List ((\\), nub, foldl')
31
32
import qualified Data.Map as Map
33
34
import Agda.Syntax.Concrete as C hiding (topLevelModuleName)
34
35
import Agda.Syntax.Concrete.Operators
36
-- import qualified Agda.Syntax.Concrete.Copatterns as Cop -- merged into Operators
35
37
import Agda.Syntax.Abstract as A
38
import Agda.Syntax.Abstract.Copatterns
36
39
import Agda.Syntax.Position
37
40
import Agda.Syntax.Common
38
41
import Agda.Syntax.Info
39
42
import Agda.Syntax.Concrete.Definitions as C
40
import Agda.Syntax.Concrete.Operators
41
43
import Agda.Syntax.Concrete.Pretty
42
44
import Agda.Syntax.Abstract.Pretty
43
45
import Agda.Syntax.Fixity
44
46
import Agda.Syntax.Notation
45
47
import Agda.Syntax.Scope.Base
46
48
import Agda.Syntax.Scope.Monad
47
import Agda.Syntax.Strict
49
50
import Agda.TypeChecking.Monad.Base (TypeError(..), Call(..), typeError,
50
TCErr(..), TCErr'(..), extendlambdaname)
51
TCErr(..), extendlambdaname)
51
52
import Agda.TypeChecking.Monad.Trace (traceCall, traceCallCPS, setCurrentRange)
52
53
import Agda.TypeChecking.Monad.State
53
54
import Agda.TypeChecking.Monad.Options
85
86
printScope :: String -> Int -> String -> ScopeM ()
86
87
printScope tag v s = verboseS ("scope." ++ tag) v $ do
88
reportSLn "" 0 $ s ++ " " ++ show scope
89
reportSDoc "" 0 $ return $ vcat [ text s, text $ show scope ]
90
91
{--------------------------------------------------------------------------
92
93
--------------------------------------------------------------------------}
94
lhsArgs :: C.Pattern -> (C.Name, [NamedArg C.Pattern])
95
lhsArgs p = case appView p of
96
Arg _ _ (Named _ (IdentP (C.QName x))) : ps -> (x, ps)
99
mkHead = Arg NotHidden Relevant . unnamed
100
notHidden = Arg NotHidden Relevant . unnamed
101
appView p = case p of
102
AppP p arg -> appView p ++ [arg]
103
OpAppP _ x ps -> mkHead (IdentP $ C.QName x) : map notHidden ps
104
ParenP _ p -> appView p
105
RawAppP _ _ -> __IMPOSSIBLE__
108
95
annotateDecl :: ScopeM A.Declaration -> ScopeM A.Declaration
109
96
annotateDecl m = annotateDecls $ (:[]) <$> m
134
121
xs = concatMap vars ps
135
122
vars :: A.Pattern' e -> [C.Name]
136
123
vars p = case p of
137
A.VarP x -> [nameConcrete x]
138
A.ConP _ _ args -> concatMap (vars . namedThing . unArg) args
140
A.AsP _ x p -> nameConcrete x : vars p
144
A.DefP _ _ args -> __IMPOSSIBLE__
145
A.ImplicitP _ -> __IMPOSSIBLE__
124
A.VarP x -> [nameConcrete x]
125
A.ConP _ _ args -> concatMap (vars . namedArg) args
127
A.AsP _ x p -> nameConcrete x : vars p
131
A.DefP _ _ args -> concatMap (vars . namedArg) args
132
-- Projection pattern, @args@ should be empty unless we have
134
A.ImplicitP _ -> __IMPOSSIBLE__
135
A.PatternSynP _ _ args -> concatMap (vars . namedArg) args
147
137
-- | Compute the type of the record constructor (with bogus target type)
148
138
recordConstructorType :: [NiceDeclaration] -> C.Expr
180
171
printScope "mod.inst" 20 "copied source module"
181
172
reportSLn "scope.mod.inst" 30 $ "renamings:\n " ++ show renD ++ "\n " ++ show renM
182
173
return ((A.SectionApp tel' m1 args'), renD, renM)
183
checkModuleApplication (C.RecordModuleIFS _ rec) m0 x dir' =
174
checkModuleApplication (C.RecordModuleIFS _ recN) m0 x dir' =
184
175
withCurrentModule m0 $ do
185
m1 <- toAbstract $ OldModuleName rec
176
m1 <- toAbstract $ OldModuleName recN
186
177
s <- getNamedScope m1
187
178
(s', (renM, renD)) <- copyScope m0 s
188
s' <- applyImportDirectiveM rec dir' s'
179
s' <- applyImportDirectiveM recN dir' s'
189
180
modifyCurrentScope $ const s'
191
182
printScope "mod.inst" 20 "copied record module"
318
309
nameExpr :: AbstractName -> A.Expr
319
310
nameExpr d = mk (anameKind d) $ anameName d
322
mk ConName = Con . AmbQ . (:[])
314
mk ConName = Con . AmbQ . (:[])
315
mk PatternSynName = A.PatternSyn
324
317
instance ToAbstract OldQName A.Expr where
325
318
toAbstract (OldQName x) = do
326
319
qx <- resolveName x
327
320
reportSLn "scope.name" 10 $ "resolved " ++ show x ++ ": " ++ show qx
329
VarName x' -> return $ A.Var x'
330
DefinedName _ d -> return $ nameExpr d
331
ConstructorName ds -> return $ A.Con $ AmbQ (map anameName ds)
332
UnknownName -> notInScope x
322
VarName x' -> return $ A.Var x'
323
DefinedName _ d -> return $ nameExpr d
324
FieldName d -> return $ nameExpr d
325
ConstructorName ds -> return $ A.Con $ AmbQ (map anameName ds)
326
UnknownName -> notInScope x
327
PatternSynResName d -> return $ nameExpr d
334
329
data APatName = VarPatName A.Name
335
330
| ConPatName [AbstractName]
331
| PatternSynPatName AbstractName
337
333
instance ToAbstract PatName APatName where
338
334
toAbstract (PatName x) = do
341
337
z <- case (rx, x) of
342
338
-- TODO: warn about shadowing
343
339
(VarName y, C.QName x) -> return $ Left x -- typeError $ RepeatedVariableInPattern y x
340
(FieldName d, C.QName x) -> return $ Left x
344
341
(DefinedName _ d, C.QName x) | DefName == anameKind d -> return $ Left x
345
342
(UnknownName, C.QName x) -> return $ Left x
346
(ConstructorName ds, _) -> return $ Right ds
343
(ConstructorName ds, _) -> return $ Right (Left ds)
344
(PatternSynResName d, _) -> return $ Right (Right d)
348
346
typeError $ GenericError $
349
347
"Cannot pattern match on " ++ show x ++ ", because it is not a constructor"
537
542
insertApp _ = __IMPOSSIBLE__
538
543
insertHead (C.LHS p wps eqs with) = C.LHS (insertApp p) wps eqs with
539
544
insertHead (C.Ellipsis r wps eqs with) = C.Ellipsis r wps eqs with
540
scdef <- toAbstract (C.FunDef r [] defaultFixity' ConcreteDef cname
545
scdef <- toAbstract (C.FunDef r [] defaultFixity' ConcreteDef True cname
541
546
(map (\(lhs,rhs,wh) -> -- wh = NoWhere, see parser for more info
542
547
C.Clause cname (insertHead lhs) rhs wh []) cs))
544
(A.ScopedDecl si [A.FunDef di qname' cs]) -> do
549
(A.ScopedDecl si [A.FunDef di qname' NotDelayed cs]) -> do
546
551
return $ A.ExtendedLam (ExprRange r) di qname' cs
547
552
_ -> __IMPOSSIBLE__
698
703
-- | runs Syntax.Concrete.Definitions.niceDeclarations on main module
699
704
niceDecls :: [C.Declaration] -> ScopeM [NiceDeclaration]
700
705
niceDecls ds = case runNice $ niceDeclarations ds of
701
Left e -> throwError $ TCErr Nothing $ Exception (getRange e) (show e)
706
Left e -> throwError $ Exception (getRange e) (show e)
702
707
Right ds -> return ds
704
709
instance ToAbstract [C.Declaration] [A.Declaration] where
705
toAbstract ds = toAbstract =<< niceDecls ds
711
-- don't allow to switch off termination checker in --safe mode
712
ds <- ifM (optSafe <$> commandLineOptions) (mapM noNoTermCheck ds) (return ds)
713
toAbstract =<< niceDecls ds
715
noNoTermCheck (C.Pragma (NoTerminationCheckPragma r)) =
716
typeError $ SafeFlagNoTerminationCheck
717
noNoTermCheck d = return d
707
719
newtype LetDefs = LetDefs [C.Declaration]
708
720
newtype LetDef = LetDef NiceDeclaration
772
802
C.Axiom r f p rel x t -> do
803
-- check that we do not postulate in --safe mode
773
804
clo <- commandLineOptions
774
805
when (optSafe clo) (typeError (SafeFlagPostulate x))
775
t' <- toAbstractCtx TopCtx t
776
y <- freshAbstractQName f x
777
bindName p DefName x y
778
return [ A.Axiom (mkDefInfo x f p ConcreteDef r) rel y t' ]
806
-- check the postulate
807
toAbstractNiceAxiom d
781
810
C.NiceField r f p a x t -> do
811
unless (p == PublicAccess) $ typeError $ GenericError "Record fields can not be private"
782
812
t' <- toAbstractCtx TopCtx t
783
813
y <- freshAbstractQName f x
784
814
irrProj <- optIrrelevantProjections <$> pragmaOptions
820
849
_ -> __IMPOSSIBLE__
821
850
ls' <- toAbstract (map toTypeBinding ls)
822
851
x' <- freshAbstractQName f x
852
{- -- Andreas, 2012-01-16: remember number of parameters
853
bindName a (DataName (length ls)) x x' -}
823
854
bindName a DefName x x'
824
855
t' <- toAbstract t
825
856
return [ A.DataSig (mkDefInfo x f a ConcreteDef r) x' ls' t' ]
826
857
-- Type signatures
827
C.FunSig r f p rel x t -> (:[]) <$> toAbstract (C.Axiom r f p rel x t)
858
C.FunSig r f p rel tc x t -> toAbstractNiceAxiom (C.Axiom r f p rel x t)
828
859
-- Function definitions
829
C.FunDef r ds f a x cs -> do
860
C.FunDef r ds f a tc x cs -> do
830
861
printLocals 10 $ "checking def " ++ show x
831
(x',cs') <- toAbstract (OldName x,cs)
832
return [ A.FunDef (mkDefInfo x f PublicAccess a r) x' cs' ]
862
(x',cs) <- toAbstract (OldName x,cs)
863
(delayed, cs) <- translateCopatternClauses cs
864
return [ A.FunDef (mkDefInfo x f PublicAccess a r) x' delayed cs ]
866
-- Uncategorized function clauses
867
C.NiceFunClause r acc abs termCheck (C.FunClause lhs rhs wcls) ->
868
typeError $ GenericError $
869
"Missing type signature for left hand side " ++ show lhs
870
C.NiceFunClause{} -> __IMPOSSIBLE__
834
872
-- Data definitions
835
873
C.DataDef r f a x pars cons -> withLocalVars $ do
881
919
cm' <- mapM (\(ThingWithFixity c f) -> bindConstructorName m c f a p YesRec) cm
882
920
printScope "rec" 15 "record complete"
883
return [ A.RecDef (mkDefInfo x f PublicAccess a r) x' cm' pars contel afields ]
921
return [ A.RecDef (mkDefInfo x f PublicAccess a r) x' ind cm' pars contel afields ]
923
-- Andreas, 2012-10-30 anonymous modules are like Coq sections
885
924
NiceModule r p a (C.QName name) tel ds ->
886
925
traceCall (ScopeCheckDeclaration $ NiceModule r p a (C.QName name) tel []) $ do
926
(name, p, isSection) <- if not (C.isNoName name)
927
then return (name, p, False)
929
(i :: NameId) <- fresh
930
return (C.NoName (getRange name) i, PrivateAccess, True)
887
931
aname <- toAbstract (NewModuleName name)
888
x <- snd <$> scopeCheckModule r (C.QName name) aname tel ds
932
ds <- snd <$> scopeCheckModule r (C.QName name) aname tel ds
889
933
bindModule p name aname
934
-- if the module was anonymous open it public
936
openModule_ (C.QName name) $
937
defaultImportDir { publicOpen = True }
892
940
NiceModule _ _ _ C.Qual{} _ _ -> __IMPOSSIBLE__
1013
NicePatternSyn r fx n as p -> do
1014
reportSLn "scope.pat" 10 $ "found nice pattern syn: " ++ show r
1016
isparameterised <- not . null <$> getLocalVars
1017
when isparameterised $ typeError $ NotSupported
1018
"pattern synonym in parameterised module"
1020
y <- freshAbstractQName fx n
1021
bindName PublicAccess PatternSynName n y
1022
defn <- withLocalVars $ do
1023
p' <- killRange <$> (toAbstract =<< toAbstract =<< parsePatternSyn p)
1024
as' <- mapM (\a -> unVarName =<< resolveName (C.QName a)) as
1026
modifyPatternSyns (Map.insert y defn)
1028
where unVarName (VarName a) = return a
1029
unVarName _ = typeError $ UnusedVariableInPatternSynonym
1032
-- checking postulate or type sig. without checking safe flag
1033
toAbstractNiceAxiom (C.Axiom r f p rel x t) = do
1034
t' <- toAbstractCtx TopCtx t
1035
y <- freshAbstractQName f x
1036
bindName p DefName x y
1037
return [ A.Axiom (mkDefInfo x f p ConcreteDef r) rel y t' ]
1038
toAbstractNiceAxiom _ = __IMPOSSIBLE__
966
1041
data IsRecordCon = YesRec | NoRec
967
1042
data ConstrDecl = ConstrDecl IsRecordCon A.ModuleName IsAbstract Access C.NiceDeclaration
969
bindConstructorName m x f a p rec = do
1044
bindConstructorName m x f a p record = do
970
1045
-- The abstract name is the qualified one
971
1046
y <- withCurrentModule m $ freshAbstractQName f x
972
1047
-- Bind it twice, once unqualified and once qualified
980
1055
AbstractDef -> PrivateAccess
982
p'' = case (a, rec) of
1057
p'' = case (a, record) of
983
1058
(AbstractDef, _) -> PrivateAccess
984
1059
(_, YesRec) -> OnlyQualified -- record constructors aren't really in the record module
985
1060
_ -> PublicAccess
987
1062
instance ToAbstract ConstrDecl A.Declaration where
988
toAbstract (ConstrDecl rec m a p (C.Axiom r f _ rel x t)) = do -- rel==Relevant
1063
toAbstract (ConstrDecl record m a p (C.Axiom r f _ rel x t)) = do -- rel==Relevant
989
1064
t' <- toAbstractCtx TopCtx t
990
1065
-- The abstract name is the qualified one
991
1066
-- Bind it twice, once unqualified and once qualified
992
y <- bindConstructorName m x f a p rec
1067
y <- bindConstructorName m x f a p record
993
1068
printScope "con" 15 "bound constructor"
994
1069
return $ A.Axiom (mkDefInfo x f p ConcreteDef r) rel y t'
1047
1122
A.Def x -> return [ A.EtaPragma x ]
1048
1123
_ -> fail "Bad ETA pragma"
1124
-- NO_TERMINATION_CHECK is handled by the nicifier
1125
toAbstract (C.NoTerminationCheckPragma _) = __IMPOSSIBLE__
1050
1127
instance ToAbstract C.Clause A.Clause where
1051
1128
toAbstract (C.Clause top C.Ellipsis{} _ _ _) = fail "bad '...'" -- TODO: errors message
1052
1129
toAbstract (C.Clause top lhs@(C.LHS p wps eqs with) rhs wh wcs) = withLocalVars $ do
1053
let wcs' = map (expandEllipsis p wps) wcs
1130
-- WAS: let wcs' = map (expandEllipsis p wps) wcs
1131
-- Andreas, 2012-02-14: need to reset local vars before checking subclauses
1132
vars <- getLocalVars
1133
let wcs' = map (\ c -> setLocalVars vars >> do return $ expandEllipsis p wps c) wcs
1054
1134
lhs' <- toAbstract (LeftHandSide top p wps)
1055
1135
printLocals 10 "after lhs:"
1056
1136
let (whname, whds) = case wh of
1085
1165
bindModule acc m am
1088
data RightHandSide = RightHandSide [C.Expr] [C.Expr] [C.Clause] C.RHS [C.Declaration]
1168
data RightHandSide = RightHandSide
1169
{ rhsRewriteEqn :: [C.RewriteEqn] -- ^ @rewrite e@ (many)
1170
, rhsWithExpr :: [C.WithExpr] -- ^ @with e@ (many)
1171
, rhsSubclauses :: [ScopeM C.Clause] -- ^ the subclauses spawned by a with (monadic because we need to reset the local vars before checking these clauses)
1173
, rhsWhereDecls :: [C.Declaration]
1089
1176
data AbstractRHS = AbsurdRHS'
1090
| WithRHS' [A.Expr] [C.Clause] -- ^ The with clauses haven't been translated yet
1177
| WithRHS' [A.Expr] [ScopeM C.Clause] -- ^ The with clauses haven't been translated yet
1092
1179
| RewriteRHS' [A.Expr] AbstractRHS [A.Declaration]
1139
1226
instance ToAbstract LeftHandSide A.LHS where
1140
1227
toAbstract (LeftHandSide top lhs wps) =
1141
1228
traceCall (ScopeCheckLHS top lhs) $ do
1142
p <- parseLHS (Just top) lhs
1229
lhscore <- parseLHS top lhs
1230
reportSLn "scope.lhs" 5 $ "parsed lhs: " ++ show lhscore
1143
1231
printLocals 10 "before lhs:"
1144
let (x, ps) = lhsArgs p
1232
-- error if copattern parsed but no --copatterns option
1233
haveCoPats <- optCopatterns <$> pragmaOptions
1236
C.LHSHead x ps -> return ()
1237
C.LHSProj{} -> typeError $ NeedOptionCopatterns
1238
-- scope check patterns except for dot patterns
1239
lhscore <- toAbstract lhscore
1240
reportSLn "scope.lhs" 5 $ "parsed lhs patterns: " ++ show lhscore
1241
wps <- toAbstract =<< mapM parsePattern wps
1242
checkPatternLinearity $ lhsCoreAllPatterns lhscore ++ wps
1243
printLocals 10 "checked pattern:"
1244
-- scope check dot patterns
1245
lhscore <- toAbstract lhscore
1246
reportSLn "scope.lhs" 5 $ "parsed lhs dot patterns: " ++ show lhscore
1247
wps <- toAbstract wps
1248
printLocals 10 "checked dots:"
1249
return $ A.LHS (LHSRange $ getRange (lhs, wps)) lhscore wps
1251
-- does not check pattern linearity
1252
instance ToAbstract C.LHSCore (A.LHSCore' C.Expr) where
1253
toAbstract (C.LHSHead x ps) = do
1145
1254
x <- withLocalVars $ setLocalVars [] >> toAbstract (OldName x)
1146
1255
args <- toAbstract ps
1147
wps <- toAbstract =<< mapM (parseLHS Nothing) wps
1148
checkPatternLinearity (map (namedThing . unArg) args ++ wps)
1149
printLocals 10 "checked pattern:"
1150
args <- toAbstract args -- take care of dot patterns
1151
wps <- toAbstract wps
1152
printLocals 10 "checked dots:"
1153
return $ A.LHS (LHSRange $ getRange (lhs, wps)) x args wps
1256
return $ A.LHSHead x args
1257
toAbstract (C.LHSProj d ps1 l ps2) = do
1260
FieldName d -> return $ anameName d
1261
UnknownName -> notInScope d
1262
_ -> typeError $ GenericError $
1263
"head of copattern needs to be a field identifier, but "
1264
++ show d ++ " isn't one"
1265
args1 <- toAbstract ps1
1267
args2 <- toAbstract ps2
1268
return $ A.LHSProj d args1 l args2
1155
1270
instance ToAbstract c a => ToAbstract (Arg c) (Arg a) where
1156
1271
toAbstract (Arg h r e) = Arg h r <$> toAbstractCtx (hiddenArgumentCtx h) e
1158
1273
instance ToAbstract c a => ToAbstract (Named name c) (Named name a) where
1159
1274
toAbstract (Named n e) = Named n <$> toAbstract e
1276
{- DOES NOT WORK ANYMORE with pattern synonyms
1277
instance ToAbstract c a => ToAbstract (A.LHSCore' c) (A.LHSCore' a) where
1278
toAbstract = mapM toAbstract
1281
instance ToAbstract (A.LHSCore' C.Expr) (A.LHSCore' A.Expr) where
1282
toAbstract (A.LHSHead f ps) = A.LHSHead f <$> mapM toAbstract ps
1283
toAbstract (A.LHSProj d ps lhscore ps') = A.LHSProj d <$> mapM toAbstract ps
1284
<*> mapM toAbstract lhscore <*> mapM toAbstract ps'
1161
1286
-- Patterns are done in two phases. First everything but the dot patterns, and
1162
1287
-- then the dot patterns. This is because dot patterns can refer to variables
1163
1288
-- bound anywhere in the pattern.
1165
instance ToAbstract c a => ToAbstract (A.Pattern' c) (A.Pattern' a) where
1166
toAbstract = mapM toAbstract
1290
instance ToAbstract (A.Pattern' C.Expr) (A.Pattern' A.Expr) where
1291
toAbstract (A.VarP x) = return $ A.VarP x
1292
toAbstract (A.ConP i ds as) = A.ConP i ds <$> mapM toAbstract as
1293
toAbstract (A.DefP i x as) = A.DefP i x <$> mapM toAbstract as
1294
toAbstract (A.WildP i) = return $ A.WildP i
1295
toAbstract (A.AsP i x p) = A.AsP i x <$> toAbstract p
1296
toAbstract (A.DotP i e) = A.DotP i <$> toAbstract e
1297
toAbstract (A.AbsurdP i) = return $ A.AbsurdP i
1298
toAbstract (A.LitP l) = return $ A.LitP l
1299
toAbstract (A.ImplicitP i) = return $ A.ImplicitP i
1300
toAbstract (A.PatternSynP i x as) = do
1301
p <- lookupPatternSyn x
1302
as' <- mapM toAbstract as
1303
instPatternSyn p as'
1305
instPatternSyn :: A.PatternSynDefn -> [NamedArg A.Pattern] -> ScopeM A.Pattern
1306
instPatternSyn (ns, p) as
1307
| length ns == length as = return $ substPattern s $ setRange (getRange i) p
1308
| otherwise = typeError $ PatternSynonymArityMismatch x
1310
s = zipWith' (\n a -> (n, namedThing (unArg a))) ns as
1168
1313
instance ToAbstract C.Pattern (A.Pattern' C.Expr) where
1170
1315
toAbstract p@(C.IdentP x) = do
1171
1316
px <- toAbstract (PatName x)
1173
VarPatName y -> return $ VarP y
1174
ConPatName ds -> return $ ConP (PatRange (getRange p))
1175
(AmbQ $ map anameName ds)
1318
VarPatName y -> return $ VarP y
1319
ConPatName ds -> return $ ConP (PatRange (getRange p))
1320
(AmbQ $ map anameName ds)
1322
PatternSynPatName d -> return $ PatternSynP (PatRange (getRange p))
1178
1325
toAbstract p0@(AppP p q) = do
1179
1326
(p', q') <- toAbstract (p,q)
1181
ConP _ x as -> return $ ConP info x (as ++ [q'])
1182
DefP _ x as -> return $ DefP info x (as ++ [q'])
1183
_ -> typeError $ InvalidPattern p0
1328
ConP _ x as -> return $ ConP info x (as ++ [q'])
1329
DefP _ x as -> return $ DefP info x (as ++ [q'])
1330
PatternSynP _ x as -> return $ PatternSynP info x (as ++ [q'])
1331
_ -> typeError $ InvalidPattern p0
1185
1333
r = getRange p0
1186
1334
info = PatSource r $ \pr -> if appBrackets pr then ParenP r p0 else p0
1188
1336
toAbstract p0@(OpAppP r op ps) = do
1189
p <- toAbstract (IdentP $ C.QName op)
1337
p <- toAbstract (IdentP op)
1190
1338
ps <- toAbstract ps
1192
ConP _ x as -> return $ ConP info x (as ++ map (Arg NotHidden Relevant . unnamed) ps)
1193
DefP _ x as -> return $ DefP info x (as ++ map (Arg NotHidden Relevant. unnamed) ps)
1340
ConP _ x as -> return $ ConP info x
1341
(as ++ map (Arg NotHidden Relevant . unnamed) ps)
1342
DefP _ x as -> return $ DefP info x
1343
(as ++ map (Arg NotHidden Relevant . unnamed) ps)
1344
PatternSynP _ x as -> return $ PatternSynP info x
1345
(as ++ map (Arg NotHidden Relevant . unnamed) ps)
1197
1349
info = PatSource r $ \pr -> if appBrackets pr then ParenP r p0 else p0
1199
1351
-- Removed when parsing
1200
toAbstract (HiddenP _ _) = __IMPOSSIBLE__
1352
toAbstract (HiddenP _ _) = __IMPOSSIBLE__
1201
1353
toAbstract (InstanceP _ _) = __IMPOSSIBLE__
1202
toAbstract (RawAppP _ _) = __IMPOSSIBLE__
1354
toAbstract (RawAppP _ _) = __IMPOSSIBLE__
1204
1356
toAbstract p@(C.WildP r) = return $ A.WildP (PatSource r $ const p)
1205
1357
toAbstract (C.ParenP _ p) = toAbstract p
1216
1368
toAbstract p0@(C.DotP r e) = return $ A.DotP info e
1217
1369
where info = PatSource r $ \_ -> p0
1218
1370
toAbstract p0@(C.AbsurdP r) = return $ A.AbsurdP info
1220
info = PatSource r $ \_ -> p0
1371
where info = PatSource r $ \_ -> p0
1222
1373
-- | Turn an operator application into abstract syntax. Make sure to record the
1223
1374
-- right precedences for the various arguments.
1224
toAbstractOpApp :: C.Name -> [OpApp C.Expr] -> ScopeM A.Expr
1225
toAbstractOpApp op@(C.NoName _ _) es = __IMPOSSIBLE__
1226
toAbstractOpApp op@(C.Name _ _) es = do
1227
f <- getFixity (C.QName op)
1375
toAbstractOpApp :: C.QName -> [OpApp C.Expr] -> ScopeM A.Expr
1376
toAbstractOpApp op es = do
1228
1378
let (_,_,parts) = oldToNewNotation $ (op, f)
1229
op <- toAbstract (OldQName $ C.QName op)
1230
foldl app op <$> left (theFixity f) [p | p <- parts, not (isBindingHole p)] es
1379
op <- toAbstract (OldQName op)
1380
foldl' app op <$> left (theFixity f) [p | p <- parts, not (isBindingHole p)] es
1232
1382
app e arg = A.App (ExprRange (fuseRange e arg)) e
1233
1383
$ Arg NotHidden Relevant $ unnamed arg
added
removed
src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs
