-
Notifications
You must be signed in to change notification settings - Fork 337
/
ConcreteToAbstract.hs
1976 lines (1733 loc) · 79 KB
/
ConcreteToAbstract.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
{-# LANGUAGE CPP #-}
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE UndecidableInstances #-}
#if __GLASGOW_HASKELL__ <= 708
{-# LANGUAGE OverlappingInstances #-}
#endif
{-| Translation from "Agda.Syntax.Concrete" to "Agda.Syntax.Abstract". Involves scope analysis,
figuring out infix operator precedences and tidying up definitions.
-}
module Agda.Syntax.Translation.ConcreteToAbstract
( ToAbstract(..), localToAbstract
, concreteToAbstract_
, concreteToAbstract
, NewModuleQName(..)
, OldName(..)
, TopLevel(..)
, TopLevelInfo(..)
, topLevelModuleName
, AbstractRHS
, NewModuleName, OldModuleName
, NewName, OldQName
, LeftHandSide, RightHandSide
, PatName, APatName, LetDef, LetDefs
) where
import Prelude hiding (mapM, null)
import Control.Applicative
import Control.Monad.Reader hiding (mapM)
import Data.Foldable (Foldable, traverse_)
import Data.Traversable (mapM, traverse)
import Data.List ((\\), nub, foldl')
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.Map as Map
import Data.Maybe
import Data.Void
import Agda.Syntax.Concrete as C hiding (topLevelModuleName)
import Agda.Syntax.Concrete.Generic
import Agda.Syntax.Concrete.Operators
import Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Pretty
import qualified Agda.Syntax.Internal as I
import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.Syntax.Common
import Agda.Syntax.Info
import Agda.Syntax.Concrete.Definitions as C
import Agda.Syntax.Fixity
import Agda.Syntax.Notation
import Agda.Syntax.Scope.Base
import Agda.Syntax.Scope.Monad
import Agda.Syntax.Translation.AbstractToConcrete (ToConcrete)
import Agda.TypeChecking.Monad.Base
( TypeError(..) , Call(..) , typeError , genericError , TCErr(..)
, fresh , freshName , freshName_ , freshNoName , extendedLambdaName
, envAbstractMode , AbstractMode(..)
)
import qualified Agda.TypeChecking.Monad.Benchmark as Bench
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.Trace (traceCall, setCurrentRange)
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Monad.MetaVars (registerInteractionPoint)
import Agda.TypeChecking.Monad.Options
import Agda.TypeChecking.Monad.Env (insideDotPattern, isInsideDotPattern)
import Agda.TypeChecking.Rules.Builtin (isUntypedBuiltin, bindUntypedBuiltin)
import Agda.TypeChecking.Pretty hiding (pretty, prettyA)
import Agda.Interaction.FindFile (checkModuleName)
-- import Agda.Interaction.Imports -- for type-checking in ghci
import {-# SOURCE #-} Agda.Interaction.Imports (scopeCheckImport)
import Agda.Interaction.Options
import Agda.Utils.Either
import Agda.Utils.Except ( MonadError(catchError, throwError) )
import Agda.Utils.FileName
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import qualified Agda.Utils.Pretty as P
import Agda.Utils.Pretty (render, Pretty, pretty, prettyShow)
import Agda.Utils.Tuple
#include "undefined.h"
import Agda.Utils.Impossible
import Agda.ImpossibleTest (impossibleTest)
{--------------------------------------------------------------------------
Exceptions
--------------------------------------------------------------------------}
-- notAModuleExpr e = typeError $ NotAModuleExpr e
notAnExpression :: C.Expr -> ScopeM A.Expr
notAnExpression e = typeError $ NotAnExpression e
nothingAppliedToHiddenArg :: C.Expr -> ScopeM A.Expr
nothingAppliedToHiddenArg e = typeError $ NothingAppliedToHiddenArg e
nothingAppliedToInstanceArg :: C.Expr -> ScopeM A.Expr
nothingAppliedToInstanceArg e = typeError $ NothingAppliedToInstanceArg e
notAValidLetBinding :: NiceDeclaration -> ScopeM a
notAValidLetBinding d = typeError $ NotAValidLetBinding d
-- Debugging
printLocals :: Int -> String -> ScopeM ()
printLocals v s = verboseS "scope.top" v $ do
locals <- getLocalVars
reportSLn "scope.top" v $ s ++ " " ++ show locals
{--------------------------------------------------------------------------
Helpers
--------------------------------------------------------------------------}
annotateDecl :: ScopeM A.Declaration -> ScopeM A.Declaration
annotateDecl m = annotateDecls $ (:[]) <$> m
annotateDecls :: ScopeM [A.Declaration] -> ScopeM A.Declaration
annotateDecls m = do
ds <- m
s <- getScope
return $ ScopedDecl s ds
annotateExpr :: ScopeM A.Expr -> ScopeM A.Expr
annotateExpr m = do
e <- m
s <- getScope
return $ ScopedExpr s e
-- | Make sure that each variable occurs only once.
checkPatternLinearity :: [A.Pattern' e] -> ScopeM ()
checkPatternLinearity ps = unlessNull (duplicates xs) $ \ ys -> do
typeError $ RepeatedVariablesInPattern ys
where
xs = concatMap vars ps
vars :: A.Pattern' e -> [C.Name]
vars p = case p of
A.VarP x -> [nameConcrete x]
A.ConP _ _ args -> concatMap (vars . namedArg) args
A.WildP _ -> []
A.AsP _ x p -> nameConcrete x : vars p
A.DotP _ _ -> []
A.AbsurdP _ -> []
A.LitP _ -> []
A.DefP _ _ args -> concatMap (vars . namedArg) args
-- Projection pattern, @args@ should be empty unless we have
-- indexed records.
A.PatternSynP _ _ args -> concatMap (vars . namedArg) args
A.RecP _ fs -> concatMap (vars . (^. exprFieldA)) fs
-- | Make sure that there are no dot patterns (called on pattern synonyms).
noDotPattern :: String -> A.Pattern' e -> ScopeM (A.Pattern' Void)
noDotPattern err = dot
where
dot :: A.Pattern' e -> ScopeM (A.Pattern' Void)
dot p = case p of
A.VarP x -> pure $ A.VarP x
A.ConP i c args -> A.ConP i c <$> (traverse $ traverse $ traverse dot) args
A.WildP i -> pure $ A.WildP i
A.AsP i x p -> A.AsP i x <$> dot p
A.DotP{} -> typeError $ GenericError err
A.AbsurdP i -> pure $ A.AbsurdP i
A.LitP l -> pure $ A.LitP l
A.DefP i f args -> A.DefP i f <$> (traverse $ traverse $ traverse dot) args
A.PatternSynP i c args -> A.PatternSynP i c <$> (traverse $ traverse $ traverse dot) args
A.RecP i fs -> A.RecP i <$> (traverse $ traverse dot) fs
-- | Compute the type of the record constructor (with bogus target type)
recordConstructorType :: [NiceDeclaration] -> C.Expr
recordConstructorType fields = build fs
where
-- drop all declarations after the last field declaration
fs = reverse $ dropWhile notField $ reverse fields
notField NiceField{} = False
notField _ = True
-- Andreas, 2013-11-08
-- Turn @open public@ into just @open@, since we cannot have an
-- @open public@ in a @let@. Fixes issue 532.
build (NiceOpen r m dir@ImportDirective{ publicOpen = True } : fs) =
build (NiceOpen r m dir{ publicOpen = False } : fs)
build (NiceModuleMacro r p x modapp open dir@ImportDirective{ publicOpen = True } : fs) =
build (NiceModuleMacro r p x modapp open dir{ publicOpen = False } : fs)
build (NiceField r f _ _ x (Arg info e) : fs) =
C.Pi [C.TypedBindings r $ Arg info (C.TBind r [pure $ mkBoundName x f] e)] $ build fs
where r = getRange x
build (d : fs) = C.Let (getRange d) [notSoNiceDeclaration d] $
build fs
build [] = C.SetN noRange 0 -- todo: nicer
-- | @checkModuleApplication modapp m0 x dir = return (modapp', renD, renM)@
--
-- @m0@ is the new (abstract) module name and
-- @x@ its concrete form (used for error messages).
checkModuleApplication
:: C.ModuleApplication
-> ModuleName
-> C.Name
-> ImportDirective
-> ScopeM (A.ModuleApplication, Ren A.QName, Ren ModuleName)
checkModuleApplication (C.SectionApp _ tel e) m0 x dir' = do
reportSDoc "scope.decl" 70 $ vcat $
[ text $ "scope checking ModuleApplication " ++ prettyShow x
]
-- For the following, set the current module to be m0.
withCurrentModule m0 $ do
-- Check that expression @e@ is of the form @m args@.
(m, args) <- parseModuleApplication e
-- Scope check the telescope (introduces bindings!).
tel' <- toAbstract tel
-- Scope check the old module name and the module args.
(m1, args') <- toAbstract (OldModuleName m, args)
-- Drop constructors (OnlyQualified) if there are arguments. The record constructor
-- isn't properly in the record module, so copying it will lead to badness.
let noRecConstr | null args = id
| otherwise = removeOnlyQualified
-- Copy the scope associated with m and take the parts actually imported.
s <- applyImportDirectiveM (C.QName x) dir' =<< getNamedScope m1
(s', (renM, renD)) <- copyScope m m0 (noRecConstr s)
-- Set the current scope to @s'@
modifyCurrentScope $ const s'
printScope "mod.inst" 20 "copied source module"
reportSLn "scope.mod.inst" 30 $ "renamings:\n " ++ show renD ++ "\n " ++ show renM
let amodapp = A.SectionApp tel' m1 args'
reportSDoc "scope.decl" 70 $ vcat $
[ text $ "scope checked ModuleApplication " ++ prettyShow x
]
reportSDoc "scope.decl" 70 $ vcat $
[ nest 2 $ prettyA amodapp
]
return (amodapp, renD, renM)
checkModuleApplication (C.RecordModuleIFS _ recN) m0 x dir' =
withCurrentModule m0 $ do
m1 <- toAbstract $ OldModuleName recN
s <- getNamedScope m1
s <- applyImportDirectiveM recN dir' s
(s', (renM, renD)) <- copyScope recN m0 s
modifyCurrentScope $ const s'
printScope "mod.inst" 20 "copied record module"
return ((A.RecordModuleIFS m1), renD, renM)
-- | @checkModuleMacro mkApply range access concreteName modapp open dir@
--
-- Preserves local variables.
checkModuleMacro
:: (Pretty c, ToConcrete a c)
=> (ModuleInfo -> ModuleName -> A.ModuleApplication -> Ren A.QName -> Ren ModuleName -> a)
-> Range
-> Access
-> C.Name
-> C.ModuleApplication
-> OpenShortHand
-> ImportDirective
-> ScopeM [a]
checkModuleMacro apply r p x modapp open dir = do
reportSDoc "scope.decl" 70 $ vcat $
[ text $ "scope checking ModuleMacro " ++ prettyShow x
]
notPublicWithoutOpen open dir
m0 <- toAbstract (NewModuleName x)
reportSDoc "scope.decl" 90 $ text "NewModuleName: m0 =" <+> prettyA m0
printScope "mod.inst" 20 "module macro"
-- If we're opening a /named/ module, the import directive is
-- applied to the "open", otherwise to the module itself. However,
-- "public" is always applied to the "open".
let (moduleDir, openDir) = case (open, isNoName x) of
(DoOpen, False) -> (defaultImportDir, dir)
(DoOpen, True) -> ( dir { publicOpen = False }
, defaultImportDir { publicOpen = publicOpen dir }
)
(DontOpen, _) -> (dir, defaultImportDir)
-- Restore the locals after module application has been checked.
(modapp', renD, renM) <- withLocalVars $ checkModuleApplication modapp m0 x moduleDir
bindModule p x m0
reportSDoc "scope.decl" 90 $ text "after bindMod: m0 =" <+> prettyA m0
printScope "mod.inst.copy.after" 20 "after copying"
-- Andreas, 2014-09-02 openModule_ might shadow some locals!
when (open == DoOpen) $
openModule_ (C.QName x) openDir
printScope "mod.inst" 20 $ show open
reportSDoc "scope.decl" 90 $ text "after open : m0 =" <+> prettyA m0
stripNoNames
printScope "mod.inst" 10 $ "after stripping"
reportSDoc "scope.decl" 90 $ text "after stripNo: m0 =" <+> prettyA m0
let m = m0 `withRangesOf` [x]
adecls = [ apply info m modapp' renD renM ]
reportSDoc "scope.decl" 70 $ vcat $
[ text $ "scope checked ModuleMacro " ++ prettyShow x
]
reportSLn "scope.decl" 90 $ "info = " ++ show info
reportSLn "scope.decl" 90 $ "m = " ++ show m
reportSLn "scope.decl" 90 $ "modapp' = " ++ show modapp'
reportSLn "scope.decl" 90 $ "renD = " ++ show renD
reportSLn "scope.decl" 90 $ "renM = " ++ show renM
reportSDoc "scope.decl" 70 $ vcat $
map (nest 2 . prettyA) adecls
return adecls
where
info = ModuleInfo
{ minfoRange = r
, minfoAsName = Nothing
, minfoAsTo = renamingRange dir
, minfoOpenShort = Just open
, minfoDirective = Just dir
}
-- | The @public@ keyword must only be used together with @open@.
notPublicWithoutOpen :: OpenShortHand -> ImportDirective -> ScopeM ()
notPublicWithoutOpen DoOpen dir = return ()
notPublicWithoutOpen DontOpen dir = when (publicOpen dir) $ typeError $
GenericError
"The public keyword must only be used together with the open keyword"
-- | Computes the range of all the \"to\" keywords used in a renaming
-- directive.
renamingRange :: ImportDirective -> Range
renamingRange = getRange . map renToRange . renaming
{--------------------------------------------------------------------------
Translation
--------------------------------------------------------------------------}
concreteToAbstract_ :: ToAbstract c a => c -> ScopeM a
concreteToAbstract_ x = toAbstract x
concreteToAbstract :: ToAbstract c a => ScopeInfo -> c -> ScopeM a
concreteToAbstract scope x = withScope_ scope (toAbstract x)
-- | Things that can be translated to abstract syntax are instances of this
-- class.
class ToAbstract concrete abstract | concrete -> abstract where
toAbstract :: concrete -> ScopeM abstract
-- | This function should be used instead of 'toAbstract' for things that need
-- to keep track of precedences to make sure that we don't forget about it.
toAbstractCtx :: ToAbstract concrete abstract =>
Precedence -> concrete -> ScopeM abstract
toAbstractCtx ctx c = withContextPrecedence ctx $ toAbstract c
toAbstractTopCtx :: ToAbstract c a => c -> ScopeM a
toAbstractTopCtx = toAbstractCtx TopCtx
toAbstractHiding :: (LensHiding h, ToAbstract c a) => h -> c -> ScopeM a
toAbstractHiding h = toAbstractCtx $ hiddenArgumentCtx $ getHiding h
setContextCPS :: Precedence -> (a -> ScopeM b) ->
((a -> ScopeM b) -> ScopeM b) -> ScopeM b
setContextCPS p ret f = do
p' <- getContextPrecedence
withContextPrecedence p $ f $ withContextPrecedence p' . ret
localToAbstractCtx :: ToAbstract concrete abstract =>
Precedence -> concrete -> (abstract -> ScopeM a) -> ScopeM a
localToAbstractCtx ctx c ret = setContextCPS ctx ret (localToAbstract c)
-- | This operation does not affect the scope, i.e. the original scope
-- is restored upon completion.
localToAbstract :: ToAbstract c a => c -> (a -> ScopeM b) -> ScopeM b
localToAbstract x ret = fst <$> localToAbstract' x ret
-- | Like 'localToAbstract' but returns the scope after the completion of the
-- second argument.
localToAbstract' :: ToAbstract c a => c -> (a -> ScopeM b) -> ScopeM (b, ScopeInfo)
localToAbstract' x ret = do
scope <- getScope
withScope scope $ ret =<< toAbstract x
instance (ToAbstract c1 a1, ToAbstract c2 a2) => ToAbstract (c1,c2) (a1,a2) where
toAbstract (x,y) = (,) <$> toAbstract x <*> toAbstract y
instance (ToAbstract c1 a1, ToAbstract c2 a2, ToAbstract c3 a3) =>
ToAbstract (c1,c2,c3) (a1,a2,a3) where
toAbstract (x,y,z) = flatten <$> toAbstract (x,(y,z))
where
flatten (x,(y,z)) = (x,y,z)
#if __GLASGOW_HASKELL__ >= 710
instance {-# OVERLAPPABLE #-} ToAbstract c a => ToAbstract [c] [a] where
#else
instance ToAbstract c a => ToAbstract [c] [a] where
#endif
toAbstract = mapM toAbstract
instance (ToAbstract c1 a1, ToAbstract c2 a2) =>
ToAbstract (Either c1 c2) (Either a1 a2) where
toAbstract = traverseEither toAbstract toAbstract
instance ToAbstract c a => ToAbstract (Maybe c) (Maybe a) where
toAbstract = traverse toAbstract
-- Names ------------------------------------------------------------------
newtype NewName a = NewName a
data OldQName = OldQName C.QName (Maybe (Set A.Name))
-- ^ If a set is given, then the first name must correspond to one
-- of the names in the set.
newtype OldName = OldName C.Name
data PatName = PatName C.QName (Maybe (Set A.Name))
-- ^ If a set is given, then the first name must correspond to one
-- of the names in the set.
instance ToAbstract (NewName C.Name) A.Name where
toAbstract (NewName x) = do
y <- freshAbstractName_ x
bindVariable x y
return y
instance ToAbstract (NewName C.BoundName) A.Name where
toAbstract (NewName BName{ boundName = x, bnameFixity = fx }) = do
y <- freshAbstractName fx x
bindVariable x y
return y
instance ToAbstract OldQName A.Expr where
toAbstract (OldQName x ns) = do
qx <- resolveName' allKindsOfNames ns x
reportSLn "scope.name" 10 $ "resolved " ++ show x ++ ": " ++ show qx
case qx of
VarName x' -> return $ A.Var x'
DefinedName _ d -> return $ nameExpr d
FieldName d -> return $ nameExpr d
ConstructorName ds -> return $ A.Con $ AmbQ (map anameName ds)
UnknownName -> notInScope x
PatternSynResName d -> return $ nameExpr d
data APatName = VarPatName A.Name
| ConPatName [AbstractName]
| PatternSynPatName AbstractName
instance ToAbstract PatName APatName where
toAbstract (PatName x ns) = do
reportSLn "scope.pat" 10 $ "checking pattern name: " ++ show x
rx <- resolveName' [ConName, PatternSynName] ns x
-- Andreas, 2013-03-21 ignore conflicting names which cannot
-- be meant since we are in a pattern
z <- case (rx, x) of
-- TODO: warn about shadowing
(VarName y, C.QName x) -> return $ Left x -- typeError $ RepeatedVariableInPattern y x
(FieldName d, C.QName x) -> return $ Left x
(DefinedName _ d, C.QName x) | DefName == anameKind d -> return $ Left x
(UnknownName, C.QName x) -> return $ Left x
(ConstructorName ds, _) -> return $ Right (Left ds)
(PatternSynResName d, _) -> return $ Right (Right d)
_ -> genericError $ "Cannot pattern match on non-constructor " ++ prettyShow x
case z of
Left x -> do
reportSLn "scope.pat" 10 $ "it was a var: " ++ show x
p <- VarPatName <$> toAbstract (NewName x)
printLocals 10 "bound it:"
return p
Right (Left ds) -> do
reportSLn "scope.pat" 10 $ "it was a con: " ++ show (map anameName ds)
return $ ConPatName ds
Right (Right d) -> do
reportSLn "scope.pat" 10 $ "it was a pat syn: " ++ show (anameName d)
return $ PatternSynPatName d
-- Should be a defined name.
instance ToAbstract OldName A.QName where
toAbstract (OldName x) = do
rx <- resolveName (C.QName x)
case rx of
DefinedName _ d -> return $ anameName d
-- We can get the cases below for DISPLAY pragmas
ConstructorName (d : _) -> return $ anameName d -- We'll throw out this one, so it doesn't matter which one we pick
ConstructorName [] -> __IMPOSSIBLE__
FieldName d -> return $ anameName d
PatternSynResName d -> return $ anameName d
VarName x -> typeError $ GenericError $ "Not a defined name: " ++ show x
UnknownName -> typeError $ GenericError $ "Not in scope: " ++ show x
newtype NewModuleName = NewModuleName C.Name
newtype NewModuleQName = NewModuleQName C.QName
newtype OldModuleName = OldModuleName C.QName
freshQModule :: A.ModuleName -> C.Name -> ScopeM A.ModuleName
freshQModule m x = A.qualifyM m . mnameFromList . (:[]) <$> freshAbstractName_ x
checkForModuleClash :: C.Name -> ScopeM ()
checkForModuleClash x = do
ms <- scopeLookup (C.QName x) <$> getScope
unless (null ms) $ do
reportSLn "scope.clash" 20 $ "clashing modules ms = " ++ show ms
setCurrentRange x $
typeError $ ShadowedModule x $
map ((`withRangeOf` x) . amodName) ms
instance ToAbstract NewModuleName A.ModuleName where
toAbstract (NewModuleName x) = do
checkForModuleClash x
m <- getCurrentModule
y <- freshQModule m x
createModule False y
return y
instance ToAbstract NewModuleQName A.ModuleName where
toAbstract (NewModuleQName m) = toAbs noModuleName m
where
toAbs m (C.QName x) = do
y <- freshQModule m x
createModule False y
return y
toAbs m (C.Qual x q) = do
m' <- freshQModule m x
toAbs m' q
instance ToAbstract OldModuleName A.ModuleName where
toAbstract (OldModuleName q) = setCurrentRange q $ do
amodName <$> resolveModule q
-- Expressions ------------------------------------------------------------
-- | Peel off 'C.HiddenArg' and represent it as an 'NamedArg'.
mkNamedArg :: C.Expr -> NamedArg C.Expr
mkNamedArg (C.HiddenArg _ e) = Arg (setHiding Hidden defaultArgInfo) e
mkNamedArg (C.InstanceArg _ e) = Arg (setHiding Instance defaultArgInfo) e
mkNamedArg e = Arg defaultArgInfo $ unnamed e
-- | Peel off 'C.HiddenArg' and represent it as an 'Arg', throwing away any name.
mkArg' :: ArgInfo -> C.Expr -> Arg C.Expr
mkArg' info (C.HiddenArg _ e) = Arg (setHiding Hidden info) $ namedThing e
mkArg' info (C.InstanceArg _ e) = Arg (setHiding Instance info) $ namedThing e
mkArg' info e = Arg (setHiding NotHidden info) e
-- | By default, arguments are @Relevant@.
mkArg :: C.Expr -> Arg C.Expr
mkArg e = mkArg' defaultArgInfo e
-- | Parse a possibly dotted C.Expr as A.Expr. Bool = True if dotted.
toAbstractDot :: Precedence -> C.Expr -> ScopeM (A.Expr, Bool)
toAbstractDot prec e = do
reportSLn "scope.irrelevance" 100 $ "toAbstractDot: " ++ (render $ pretty e)
traceCall (ScopeCheckExpr e) $ case e of
C.Dot _ e -> do
e <- toAbstractCtx prec e
return (e, True)
C.RawApp r es -> do
e <- parseApplication es
toAbstractDot prec e
C.Paren _ e -> toAbstractDot TopCtx e
e -> do
e <- toAbstractCtx prec e
return (e, False)
-- | Translate concrete expression under at least one binder into nested
-- lambda abstraction in abstract syntax.
toAbstractLam :: Range -> [C.LamBinding] -> C.Expr -> Precedence -> ScopeM A.Expr
toAbstractLam r bs e ctx = do
-- Translate the binders
localToAbstract (map (C.DomainFull . makeDomainFull) bs) $ \ bs -> do
-- Translate the body
e <- toAbstractCtx ctx e
-- We have at least one binder. Get first @b@ and rest @bs@.
caseList bs __IMPOSSIBLE__ $ \ b bs -> do
return $ A.Lam (ExprRange r) b $ foldr mkLam e bs
where
mkLam b e = A.Lam (ExprRange $ fuseRange b e) b e
-- | Scope check extended lambda expression.
scopeCheckExtendedLam :: Range -> [(C.LHS, C.RHS, WhereClause)] -> ScopeM A.Expr
scopeCheckExtendedLam r cs = do
whenM isInsideDotPattern $
genericError "Extended lambdas are not allowed in dot patterns"
-- Find an unused name for the extended lambda definition.
cname <- nextlamname r 0 extendedLambdaName
name <- freshAbstractName_ cname
reportSLn "scope.extendedLambda" 10 $ "new extended lambda name: " ++ show name
qname <- qualifyName_ name
bindName PrivateAccess DefName cname qname
-- Compose a function definition an scope check it.
a <- aModeToDef <$> asks envAbstractMode
let
insertApp (C.RawAppP r es) = C.RawAppP r $ IdentP (C.QName cname) : es
insertApp (C.IdentP q ) = C.RawAppP r $ IdentP (C.QName cname) : [C.IdentP q]
where r = getRange q
insertApp _ = __IMPOSSIBLE__
d = C.FunDef r [] noFixity' {-'-} a __IMPOSSIBLE__ cname $
for cs $ \ (lhs, rhs, wh) -> -- wh == NoWhere, see parser for more info
C.Clause cname False (mapLhsOriginalPattern insertApp lhs) rhs wh []
scdef <- toAbstract d
-- Create the abstract syntax for the extended lambda.
case scdef of
A.ScopedDecl si [A.FunDef di qname' NotDelayed cs] -> do
setScope si -- This turns into an A.ScopedExpr si $ A.ExtendedLam...
return $ A.ExtendedLam (ExprRange r) di qname' cs
_ -> __IMPOSSIBLE__
where
-- Get a concrete name that is not yet in scope.
nextlamname :: Range -> Int -> String -> ScopeM C.Name
nextlamname r i s = do
let cname = C.Name r [Id $ stringToRawName $ s ++ show i]
rn <- resolveName $ C.QName cname
case rn of
UnknownName -> return cname
_ -> nextlamname r (i+1) s
instance ToAbstract C.Expr A.Expr where
toAbstract e =
traceCall (ScopeCheckExpr e) $ annotateExpr $ case e of
-- Names
Ident x -> toAbstract (OldQName x Nothing)
-- Literals
C.Lit l@(LitInt r n) -> do
let builtin | n < 0 = Just <$> getBuiltin builtinFromNeg -- negative literals are only allowed if FROMNEG is defined
| otherwise = getBuiltin' builtinFromNat
l' = LitInt r (abs n)
info = ExprRange r
conv <- builtin
case conv of
Just (I.Def q _) -> return $ A.App info (A.Def q) $ defaultNamedArg (A.Lit l')
_ -> return $ A.Lit l
C.Lit l -> return $ A.Lit l
-- Meta variables
C.QuestionMark r n -> do
scope <- getScope
-- Andreas, 2014-04-06 create interaction point.
ii <- registerInteractionPoint r n
let info = MetaInfo
{ metaRange = r
, metaScope = scope
, metaNumber = n
, metaNameSuggestion = ""
}
return $ A.QuestionMark info ii
C.Underscore r n -> do
scope <- getScope
return $ A.Underscore $ MetaInfo
{ metaRange = r
, metaScope = scope
, metaNumber = maybe Nothing __IMPOSSIBLE__ n
, metaNameSuggestion = fromMaybe "" n
}
-- Raw application
C.RawApp r es -> do
e <- parseApplication es
toAbstract e
-- Application
C.App r e1 e2 -> do
e1 <- toAbstractCtx FunctionCtx e1
e2 <- toAbstractCtx ArgumentCtx e2
return $ A.App (ExprRange r) e1 e2
-- Operator application
C.OpApp r op ns es -> toAbstractOpApp op ns es
-- With application
C.WithApp r e es -> do
e <- toAbstractCtx WithFunCtx e
es <- mapM (toAbstractCtx WithArgCtx) es
return $ A.WithApp (ExprRange r) e es
-- Misplaced hidden argument
C.HiddenArg _ _ -> nothingAppliedToHiddenArg e
C.InstanceArg _ _ -> nothingAppliedToInstanceArg e
-- Lambda
C.AbsurdLam r h -> return $ A.AbsurdLam (ExprRange r) h
C.Lam r bs e -> toAbstractLam r bs e TopCtx
-- Extended Lambda
C.ExtendedLam r cs -> scopeCheckExtendedLam r cs
-- Relevant and irrelevant non-dependent function type
C.Fun r e1 e2 -> do
Arg info (e0, dotted) <- traverse (toAbstractDot FunctionSpaceDomainCtx) $ mkArg e1
let e1 = Arg ((if dotted then setRelevance Irrelevant else id) info) e0
e2 <- toAbstractCtx TopCtx e2
return $ A.Fun (ExprRange r) e1 e2
-- Dependent function type
e0@(C.Pi tel e) ->
localToAbstract tel $ \tel -> do
e <- toAbstractCtx TopCtx e
let info = ExprRange (getRange e0)
return $ A.Pi info tel e
-- Sorts
C.Set _ -> return $ A.Set (ExprRange $ getRange e) 0
C.SetN _ n -> return $ A.Set (ExprRange $ getRange e) n
C.Prop _ -> return $ A.Prop $ ExprRange $ getRange e
-- Let
e0@(C.Let _ ds e) ->
ifM isInsideDotPattern (genericError $ "Let-expressions are not allowed in dot patterns") $
localToAbstract (LetDefs ds) $ \ds' -> do
e <- toAbstractCtx TopCtx e
let info = ExprRange (getRange e0)
return $ A.Let info ds' e
-- Record construction
C.Rec r fs -> do
fs' <- toAbstractCtx TopCtx fs
let ds' = [ d | Right (_, ds) <- fs', d <- ds ]
fs'' = map (mapRight fst) fs'
i = ExprRange r
return $ A.mkLet i ds' (A.Rec i fs'')
-- Record update
C.RecUpdate r e fs -> do
A.RecUpdate (ExprRange r) <$> toAbstract e <*> toAbstractCtx TopCtx fs
-- Parenthesis
C.Paren _ e -> toAbstractCtx TopCtx e
-- Pattern things
C.Dot _ _ -> notAnExpression e
C.As _ _ _ -> notAnExpression e
C.Absurd _ -> notAnExpression e
-- Impossible things
C.ETel _ -> __IMPOSSIBLE__
C.Equal{} -> genericError "Parse error: unexpected '='"
-- Quoting
C.QuoteGoal _ x e -> do
x' <- toAbstract (NewName x)
e' <- toAbstract e
return $ A.QuoteGoal (ExprRange $ getRange e) x' e'
C.QuoteContext r -> return $ A.QuoteContext (ExprRange r)
C.Quote r -> return $ A.Quote (ExprRange r)
C.QuoteTerm r -> return $ A.QuoteTerm (ExprRange r)
C.Unquote r -> return $ A.Unquote (ExprRange r)
C.Tactic r e es -> do
let AppView e' args = appView e
e' : es <- toAbstract (e' : es)
args <- toAbstract args
return $ A.Tactic (ExprRange r) e' args (map defaultNamedArg es)
-- DontCare
C.DontCare e -> A.DontCare <$> toAbstract e
instance ToAbstract C.ModuleAssignment (A.ModuleName, [A.LetBinding]) where
toAbstract (C.ModuleAssignment m es i)
| null es && isDefaultImportDir i = (\x-> (x, [])) <$> toAbstract (OldModuleName m)
| otherwise = do
x <- C.NoName (getRange m) <$> fresh
r <- checkModuleMacro LetApply (getRange (m, es, i)) PublicAccess x
(C.SectionApp (getRange (m , es)) [] (RawApp (fuseRange m es) (Ident m : es)))
DontOpen i
case r of
(LetApply _ m' _ _ _ : _) -> return (m', r)
_ -> __IMPOSSIBLE__
instance ToAbstract c a => ToAbstract (FieldAssignment' c) (FieldAssignment' a) where
toAbstract = traverse toAbstract
instance ToAbstract C.LamBinding A.LamBinding where
toAbstract (C.DomainFree info x) = A.DomainFree info <$> toAbstract (NewName x)
toAbstract (C.DomainFull tb) = A.DomainFull <$> toAbstract tb
makeDomainFull :: C.LamBinding -> C.TypedBindings
makeDomainFull (C.DomainFull b) = b
makeDomainFull (C.DomainFree info x) =
C.TypedBindings r $ Arg info $ C.TBind r [pure x] $ C.Underscore r Nothing
where r = getRange x
instance ToAbstract C.TypedBindings A.TypedBindings where
toAbstract (C.TypedBindings r bs) = A.TypedBindings r <$> toAbstract bs
instance ToAbstract C.TypedBinding A.TypedBinding where
toAbstract (C.TBind r xs t) = do
t' <- toAbstractCtx TopCtx t
xs' <- toAbstract $ map (fmap NewName) xs
return $ A.TBind r xs' t'
toAbstract (C.TLet r ds) = A.TLet r <$> toAbstract (LetDefs ds)
-- | Scope check a module (top level function).
--
scopeCheckNiceModule
:: Range
-> Access
-> C.Name
-> C.Telescope
-> ScopeM [A.Declaration]
-> ScopeM [A.Declaration]
scopeCheckNiceModule r p name tel checkDs
| telHasOpenStmsOrModuleMacros tel = do
-- Andreas, 2013-12-10:
-- If the module telescope contains open statements
-- or module macros (Issue 1299),
-- add an extra anonymous module around the current one.
-- Otherwise, the open statements would create
-- identifiers in the parent scope of the current module.
-- But open statements in the module telescope should
-- only affect the current module!
scopeCheckNiceModule noRange p noName_ [] $
scopeCheckNiceModule_
| otherwise = do
scopeCheckNiceModule_
where
-- The actual workhorse:
scopeCheckNiceModule_ = do
-- Check whether we are dealing with an anonymous module.
-- This corresponds to a Coq/LEGO section.
(name, p, open) <- do
if isNoName name then do
(i :: NameId) <- fresh
return (C.NoName (getRange name) i, PrivateAccess, True)
else return (name, p, False)
-- Check and bind the module, using the supplied check for its contents.
aname <- toAbstract (NewModuleName name)
ds <- snd <$> do
scopeCheckModule r (C.QName name) aname tel checkDs
bindModule p name aname
-- If the module was anonymous open it public.
when open $
openModule_ (C.QName name) $
defaultImportDir { publicOpen = True }
return ds
-- | Check whether a telescope has open declarations or module macros.
telHasOpenStmsOrModuleMacros :: C.Telescope -> Bool
telHasOpenStmsOrModuleMacros = any yesBinds
where
yesBinds (C.TypedBindings _ tb) = yesBind $ unArg tb
yesBind C.TBind{} = False
yesBind (C.TLet _ ds) = any yes ds
yes C.ModuleMacro{} = True
yes C.Open{} = True
yes C.Import{} = __IMPOSSIBLE__
yes (C.Mutual _ ds) = any yes ds
yes (C.Abstract _ ds) = any yes ds
yes (C.Private _ ds) = any yes ds
yes _ = False
{- UNUSED
telHasLetStms :: C.Telescope -> Bool
telHasLetStms = any isLetBinds
where
isLetBinds (C.TypedBindings _ tb) = isLetBind $ unArg tb
isLetBind C.TBind{} = False
isLetBind C.TLet{} = True
-}
-- | We for now disallow let-bindings in @data@ and @record@ telescopes.
-- This due "nested datatypes"; there is no easy interpretation of
-- @
-- data D (A : Set) (open M A) (b : B) : Set where
-- c : D (A × A) b → D A b
-- @
-- where @B@ is brought in scope by @open M A@.
class EnsureNoLetStms a where
ensureNoLetStms :: a -> ScopeM ()
{- From ghc 7.2, there is LANGUAGE DefaultSignatures
default ensureNoLetStms :: Foldable t => t a -> ScopeM ()
ensureNoLetStms = traverse_ ensureNoLetStms
-}
instance EnsureNoLetStms C.TypedBinding where
ensureNoLetStms tb =
case tb of
C.TLet{} -> typeError $ IllegalLetInTelescope tb
C.TBind{} -> return ()
instance EnsureNoLetStms a => EnsureNoLetStms (LamBinding' a) where
ensureNoLetStms = traverse_ ensureNoLetStms
instance EnsureNoLetStms a => EnsureNoLetStms (TypedBindings' a) where
ensureNoLetStms = traverse_ ensureNoLetStms
instance EnsureNoLetStms a => EnsureNoLetStms [a] where
ensureNoLetStms = traverse_ ensureNoLetStms
-- | Returns the scope inside the checked module.
scopeCheckModule
:: Range
-> C.QName -- ^ The concrete name of the module.
-> A.ModuleName -- ^ The abstract name of the module.
-> C.Telescope -- ^ The module telescope.
-> ScopeM [A.Declaration] -- ^ The code for checking the module contents.
-> ScopeM (ScopeInfo, [A.Declaration])
scopeCheckModule r x qm tel checkDs = do
printScope "module" 20 $ "checking module " ++ show x
-- Andreas, 2013-12-10: Telescope does not live in the new module
-- but its parent, so check it before entering the new module.
-- This is important for Nicolas Pouillard's open parametrized modules
-- statements inside telescopes.
res <- withLocalVars $ do
tel <- toAbstract tel
withCurrentModule qm $ do
-- pushScope m
-- qm <- getCurrentModule
printScope "module" 20 $ "inside module " ++ show x
ds <- checkDs
scope <- getScope
return (scope, [ A.Section info (qm `withRangesOfQ` x) tel ds ])
-- Binding is done by the caller
printScope "module" 20 $ "after module " ++ show x
return res
where
info = ModuleInfo r noRange Nothing Nothing Nothing
-- | Temporary data type to scope check a file.
data TopLevel a = TopLevel
{ topLevelPath :: AbsolutePath
-- ^ The file path from which we loaded this module.
, topLevelTheThing :: a
-- ^ The file content.
}
data TopLevelInfo = TopLevelInfo
{ topLevelDecls :: [A.Declaration]
, topLevelScope :: ScopeInfo -- ^ as seen from inside the module
}
-- | The top-level module name.
topLevelModuleName :: TopLevelInfo -> A.ModuleName
topLevelModuleName topLevel = scopeCurrent (topLevelScope topLevel)
-- | Top-level declarations are always
-- @
-- (import|open)* -- a bunch of possibly opened imports
-- module ThisModule ... -- the top-level module of this file
-- @
instance ToAbstract (TopLevel [C.Declaration]) TopLevelInfo where
toAbstract (TopLevel file ds) =
-- A file is a bunch of preliminary decls (imports etc.)
-- plus a single module decl.
caseMaybe (initLast ds) __IMPOSSIBLE__ $
\ (outsideDecls, C.Module r m0 tel insideDecls) -> do
-- If the module name is _ compute the name from the file path
m <- if isNoName m0
then return $ C.QName $ C.Name noRange [Id $ stringToRawName $ rootName file]
else do
-- Andreas, 2014-03-28 Issue 1078
-- We need to check the module name against the file name here.
-- Otherwise one could sneak in a lie and confuse the scope
-- checker.
checkModuleName (C.toTopLevelModuleName m0) file
return m0
setTopLevelModule m
am <- toAbstract (NewModuleQName m)
-- Scope check the declarations outside
outsideDecls <- toAbstract outsideDecls
(insideScope, insideDecls) <- scopeCheckModule r m am tel $
toAbstract insideDecls
let scope = mapScopeInfo (restrictLocalPrivate am) insideScope