151
154
---------------------------------------------------------------------------
154
checkTelescope :: A.Telescope -> Sort -> (Telescope -> TCM a) -> TCM a
155
checkTelescope [] s ret = ret EmptyTel
156
checkTelescope (b : tel) s ret =
157
checkTypedBindings b s $ \tel1 ->
158
checkTelescope tel s $ \tel2 ->
159
ret $ abstract tel1 tel2
161
checkTypedBindings :: A.TypedBindings -> Sort -> (Telescope -> TCM a) -> TCM a
162
checkTypedBindings (A.TypedBindings i (Arg h rel b)) s ret =
163
checkTypedBinding h rel s b $ \bs ->
164
ret $ foldr (\(x,t) -> ExtendTel (Arg h rel t) . Abs x) EmptyTel bs
166
checkTypedBinding :: Hiding -> Relevance -> Sort -> A.TypedBinding -> ([(String,Type)] -> TCM a) -> TCM a
167
checkTypedBinding h rel s (A.TBind i xs e) ret = do
169
addCtxs xs (Arg h rel t) $ ret $ mkTel xs t
172
mkTel (x:xs) t = (show $ nameConcrete x,t) : mkTel xs (raise 1 t)
173
checkTypedBinding h rel s (A.TNoBind e) ret = do
178
156
-- | Type check a telescope. Binds the variables defined by the telescope.
179
157
checkTelescope_ :: A.Telescope -> (Telescope -> TCM a) -> TCM a
180
158
checkTelescope_ [] ret = ret EmptyTel
248
224
-- fresh problem for the check.
249
225
t1 <- addCtxs xs argsT $ workOnTypes newTypeMeta_
250
226
let tel = telFromList $ mkTel xs argsT
251
pid <- newProblem_ $ leqType (telePi tel t1) target
253
-- Now check body : ?t₁
254
v <- addCtxs xs argsT $ checkExpr body t1
256
-- Block on the type comparison
257
blockTermOnProblem target (teleLam tel v) pid
259
useTargetType tel@(ExtendTel arg (Abs _ EmptyTel)) btyp = do
227
-- Do not coerce hidden lambdas
228
if (h /= NotHidden) then do
229
pid <- newProblem_ $ leqType (telePi tel t1) target
230
-- Now check body : ?t₁
231
v <- addCtxs xs argsT $ checkExpr body t1
232
-- Block on the type comparison
233
blockTermOnProblem target (teleLam tel v) pid
235
-- Now check body : ?t₁
236
v <- addCtxs xs argsT $ checkExpr body t1
237
-- Block on the type comparison
238
coerce (teleLam tel v) (telePi tel t1) target
240
useTargetType tel@(ExtendTel arg (Abs y EmptyTel)) btyp = do
260
241
verboseS "tc.term.lambda" 5 $ tick "lambda-with-target-type"
261
unless (argHiding arg == h) $ typeError $ WrongHidingInLambda target
242
unless (domHiding arg == h) $ typeError $ WrongHidingInLambda target
262
243
-- Andreas, 2011-10-01 ignore relevance in lambda if not explicitly given
263
let r' = argRelevance arg -- relevance of function type
244
let r' = domRelevance arg -- relevance of function type
264
245
when (r == Irrelevant && r' /= r) $ typeError $ WrongIrrelevanceInLambda target
265
246
-- unless (argRelevance arg == r) $ typeError $ WrongIrrelevanceInLambda target
266
247
-- We only need to block the final term on the argument type
267
248
-- comparison. The body will be blocked if necessary. We still want to
268
249
-- compare the argument types first, so we spawn a new problem for that
270
(pid, argT) <- newProblem $ isTypeEqualTo typ (unArg arg)
271
v <- addCtx x (Arg h r' argT) $ checkExpr body btyp
251
(pid, argT) <- newProblem $ isTypeEqualTo typ (unDom arg)
252
v <- add x y (Dom h r' argT) $ checkExpr body btyp
272
253
blockTermOnProblem target (Lam h $ Abs (show $ nameConcrete x) v) pid
256
add x y | C.isNoName (nameConcrete x) = addCtxString y
257
| otherwise = addCtx x
275
258
useTargetType _ _ = __IMPOSSIBLE__
424
401
A.Quote _ -> typeError $ GenericError "quote must be applied to a defined name"
425
402
A.QuoteTerm _ -> typeError $ GenericError "quoteTerm must be applied to a term"
426
403
A.Unquote _ -> typeError $ GenericError "unquote must be applied to a term"
428
404
A.AbsurdLam i h -> do
429
t <- reduceB =<< instantiateFull t
431
Blocked{} -> postponeTypeCheckingProblem_ e $ ignoreBlocking t
432
NotBlocked (El _ MetaV{}) -> postponeTypeCheckingProblem_ e $ ignoreBlocking t
433
NotBlocked t' -> case unEl t' of
435
| h == h' && not (null $ foldTerm metas a) ->
436
postponeTypeCheckingProblem e (ignoreBlocking t) $
437
null . foldTerm metas <$> instantiateFull a
405
t <- instantiateFull t
406
ifBlockedType t (\ m t' -> postponeTypeCheckingProblem_ e t') $ \ t' -> do
407
case ignoreSharing $ unEl t' of
408
Pi dom@(Dom h' r a) _
409
| h == h' && not (null $ allMetas a) ->
410
postponeTypeCheckingProblem e t' $
411
null . allMetas <$> instantiateFull a
438
412
| h == h' -> blockTerm t' $ do
413
isEmptyType (getRange i) a
440
414
-- Add helper function
441
415
top <- currentModule
442
416
let name = "absurd"
448
422
[ text "Adding absurd function" <+> prettyTCM rel <> prettyTCM aux
449
423
, nest 2 $ text "of type" <+> prettyTCM t'
451
addConstant aux $ Defn rel aux t' (defaultDisplayForm aux) 0 noCompiledRep
454
[Clause { clauseRange = getRange e
455
, clauseTel = EmptyTel
456
, clausePerm = Perm 0 []
457
, clausePats = [Arg h Relevant $ VarP "()"]
458
, clauseBody = NoBody
462
, funDelayed = NotDelayed
463
, funInv = NotInjective
464
, funAbstr = ConcreteDef
465
, funPolarity = [Covariant]
466
, funArgOccurrences = [Unused]
467
, funProjection = Nothing
426
$ Defn rel aux t' [Nonvariant] [Unused] (defaultDisplayForm aux) 0 noCompiledRep
430
{ clauseRange = getRange e
431
, clauseTel = EmptyTel -- telFromList [fmap ("()",) dom]
432
, clausePerm = Perm 1 [] -- Perm 1 [0]
433
, clausePats = [Arg h r $ VarP "()"]
434
, clauseBody = Bind $ NoAbs "()" NoBody
438
, funDelayed = NotDelayed
439
, funInv = NotInjective
440
, funAbstr = ConcreteDef
442
, funPolarity = [Nonvariant] -- WAS: [Covariant]
443
, funArgOccurrences = [Unused]
446
, funProjection = Nothing
449
, funTerminates = Just True
451
-- Andreas 2012-01-30: since aux is lifted to toplevel
452
-- it needs to be applied to the current telescope (issue 557)
453
tel <- getContextTelescope
454
return $ Def aux $ teleArgs tel
455
-- WAS: return (Def aux [])
471
456
| otherwise -> typeError $ WrongHidingInLambda t'
472
457
_ -> typeError $ ShouldBePi t'
474
metas (MetaV m _) = [m]
476
460
A.ExtendedLam i di qname cs -> do
477
461
t <- reduceB =<< instantiateFull t
462
let isMeta t = case ignoreSharing $ unEl t of { MetaV{} -> True; _ -> False }
479
464
Blocked{} -> postponeTypeCheckingProblem_ e $ ignoreBlocking t
480
NotBlocked (El _ MetaV{}) -> postponeTypeCheckingProblem_ e $ ignoreBlocking t
465
NotBlocked t' | isMeta t' -> postponeTypeCheckingProblem_ e $ ignoreBlocking t
481
466
NotBlocked t -> do
482
j <- currentMutualBlock
483
rel <- asks envRelevance
484
addConstant qname (Defn rel qname t (defaultDisplayForm qname) j noCompiledRep Axiom)
485
reportSDoc "tc.term.exlam" 50 $ text "extended lambda's implementation \"" <> prettyTCM qname <>
486
text "\" has type: " $$ prettyTCM t -- <+>
487
abstract (A.defAbstract di) $ checkFunDef' t rel NotDelayed di qname cs
488
tel <- getContextTelescope
489
addExtLambdaTele qname (counthidden tel , countnothidden tel)
490
reduce $ (Def qname [] `apply` (mkArgs tel))
468
A.ExtendedLam i di qname cs -> do
469
t <- instantiateFull t
470
ifBlockedType t (\ m t' -> postponeTypeCheckingProblem_ e t') $ \ t -> do
471
j <- currentOrFreshMutualBlock
472
rel <- asks envRelevance
474
Defn rel qname t [] [] (defaultDisplayForm qname) j noCompiledRep Axiom
475
reportSDoc "tc.term.exlam" 50 $
476
text "extended lambda's implementation \"" <> prettyTCM qname <>
477
text "\" has type: " $$ prettyTCM t -- <+>
478
-- text " where clauses: " <+> text (show cs)
479
abstract (A.defAbstract di) $ checkFunDef' t rel NotDelayed di qname cs
480
args <- getContextArgs
482
freevars <- getSecFreeVars top
483
let argsNoParam = genericDrop freevars args -- don't count module parameters
484
let (hid, notHid) = partition ((Hidden ==) . argHiding) argsNoParam
485
addExtLambdaTele qname (length hid, length notHid)
486
reduce $ (Def qname [] `apply` args)
492
488
-- Concrete definitions cannot use information about abstract things.
493
489
abstract ConcreteDef = inConcreteMode
494
490
abstract AbstractDef = inAbstractMode
495
mkArgs :: Telescope -> Args
496
mkArgs tel = map arg [n - 1, n - 2..0]
499
arg i = defaultArg (Var i [])
501
metas (MetaV m _) = [m]
504
counthidden :: Telescope -> Int
505
counthidden t = length $ filter (\ (Arg h r a) -> h == Hidden ) $ teleArgs t
507
countnothidden :: Telescope -> Int
508
countnothidden t = length $ filter (\ (Arg h r a) -> h == NotHidden ) $ teleArgs t
511
{- Andreas, 2011-04-27 DOES NOT WORK
512
-- a telescope is not for type checking abstract syn
514
A.Lam i (A.DomainFull b) e -> do
515
-- check the types, get the telescope with unchanged relevance
516
(tel, t1, cs) <- workOnTypes $ checkTypedBindings_ b $ \tel -> do
518
cs <- escapeContext (size tel) $ leqType (telePi tel t1) t
520
-- check the body under the unchanged telescope
521
v <- addCtxTel tel $ do teleLam tel <$> checkExpr e t1
522
blockTerm t v (return cs)
524
492
A.Lam i (A.DomainFull (A.TypedBindings _ b)) e -> checkLambda b e t
526
-- A.Lam i (A.DomainFull b) e -> do
527
-- (v, cs) <- checkTypedBindings LamNotPi b $ \tel -> do
528
-- (t1, cs) <- workOnTypes $ do
529
-- t1 <- newTypeMeta_
530
-- cs <- escapeContext (size tel) $ leqType (telePi tel t1) t
532
-- v <- checkExpr e t1
533
-- return (teleLam tel v, cs)
534
-- blockTerm t v (return cs)
536
494
A.Lam i (A.DomainFree h rel x) e0 -> checkExpr (A.Lam i (domainFree h rel x) e0) t
538
496
A.Lit lit -> checkLiteral lit t
549
506
, nest 2 $ text "t =" <+> prettyTCM t'
550
507
, nest 2 $ text "cxt =" <+> (prettyTCM =<< getContextTelescope)
552
blockTerm t $ unEl t' <$ leqType_ (sort s) t
509
coerce (unEl t') (sort s) t
553
510
A.Fun _ (Arg h r a) b -> do
556
513
s <- reduce $ getSort a' `sLub` getSort b'
557
blockTerm t $ Pi (Arg h r a') (NoAbs "_" b') <$ leqType_ (sort s) t
514
coerce (Pi (Dom h r a') (NoAbs "_" b')) (sort s) t
559
516
n <- ifM typeInType (return 0) (return n)
560
blockTerm t $ Sort (mkType n) <$ leqType_ (sort $ mkType $ n + 1) t
517
coerce (Sort $ mkType n) (sort $ mkType $ n + 1) t
562
519
typeError $ GenericError "Prop is no longer supported"
563
520
-- s <- ifM typeInType (return $ mkType 0) (return Prop)
564
-- blockTerm t (Sort Prop) $ leqType_ (sort $ mkType 1) t
521
-- coerce (Sort Prop) (sort $ mkType 1) t
525
case ignoreSharing $ unEl t of
570
527
axs <- getRecordFieldNames r
571
528
let xs = map unArg axs
636
596
checkExpr (A.Rec ei [ (x, e) | (x, Just e) <- zip xs es' ]) t
638
598
inferred <- inferExpr recexpr >>= reduce . snd
639
case unEl inferred of
599
case ignoreSharing $ unEl inferred of
640
600
MetaV _ _ -> postponeTypeCheckingProblem_ e t
642
602
v <- checkExpr e inferred
643
blockTerm t $ v <$ leqType_ t inferred
644
604
_ -> typeError $ ShouldBeRecordType t
646
606
replaceFields :: Name -> A.ExprInfo -> Arg A.QName -> Maybe A.Expr -> Maybe A.Expr
647
replaceFields n ei (Arg NotHidden _ p) Nothing = Just $ A.App ei (A.Def p) $ defaultArg (unnamed $ A.Var n)
607
replaceFields n ei (Arg NotHidden _ p) Nothing = Just $ A.App ei (A.Def p) $ defaultNamedArg $ A.Var n
648
608
replaceFields _ _ (Arg _ _ _) Nothing = Nothing
649
609
replaceFields _ _ _ (Just e) = Just $ e
651
A.DontCare e -> -- can happen in the context of with functions
653
{- Andreas, 2011-10-03 why do I get an internal error for Issue337?
611
A.DontCare e -> -- resurrect vars
612
ifM ((Irrelevant ==) <$> asks envRelevance)
613
(DontCare <$> do applyRelevanceToContext Irrelevant $ checkExpr e t)
614
(internalError "DontCare may only appear in irrelevant contexts")
616
Andreas, 2011-10-03 why do I get an internal error for Issue337?
654
617
-- except that should be fixed now (issue 337)
719
679
NotBlocked (MetaV _ _) -> return Nothing
720
680
Blocked{} -> return Nothing
721
681
_ -> badCon (ignoreBlocking t1)
722
let unblock = isJust <$> getCon
683
-- Lets look at the target type at this point
685
TelV _ t1 <- telView t
686
reportSDoc "tc.check.term.con" 40 $ nest 2 $
687
text "target type: " <+> prettyTCM t1
688
ifBlocked (unEl t1) (\ m t -> return Nothing) $ \ t' ->
689
(isDataOrRecord t' >>=) $ maybe (badCon t') $ \ d ->
690
case [ c | (d', c) <- dcs, d == d' ] of
692
reportSLn "tc.check.term" 40 $ " decided on: " ++ show c
694
[] -> badCon (Def d [])
695
cs -> typeError $ GenericError $
696
"Can't resolve overloaded constructors targeting the same datatype (" ++ show d ++
697
"): " ++ unwords (map show cs)
698
let unblock = isJust <$> getCon -- to unblock, call getCon later again
725
701
Just c -> checkConstructorApplication e t c args
833
828
ds <- mapM prettyTCM vs
834
829
dx <- prettyTCM x
835
830
dt <- prettyTCM $ defType d
836
liftIO $ LocIO.putStrLn $ "inferred def " ++ unwords (show dx : map show ds) ++ " : " ++ show dt
831
reportSLn "" 0 $ "inferred def " ++ unwords (show dx : map show ds) ++ " : " ++ show dt
837
832
return (mkTerm x vs, defType d)
839
834
-- | Check the type of a constructor application. This is easier than
840
835
-- a general application since the implicit arguments can be inserted
841
836
-- without looking at the arguments to the constructor.
842
837
checkConstructorApplication :: A.Expr -> Type -> QName -> [NamedArg A.Expr] -> TCM Term
843
checkConstructorApplication org t c args
844
| hiddenArg = fallback
838
checkConstructorApplication org t c args = do
839
reportSDoc "tc.term.con" 50 $ vcat
840
[ text "entering checkConstructorApplication"
842
[ text "org =" <+> prettyTCM org
843
, text "t =" <+> prettyTCM t
844
, text "c =" <+> prettyTCM c
845
, text "args =" <+> prettyTCM args
847
let (args', paramsGiven) = checkForParams args
848
if paramsGiven then fallback else do
849
reportSDoc "tc.term.con" 50 $ text "checkConstructorApplication: no parameters explicitly supplied, continuing..."
846
850
cdef <- getConstInfo c
847
851
let Constructor{conData = d} = theDef cdef
848
case unEl t of -- Only fully applied constructors get special treatment
849
Def d' vs | d' == d -> do
850
def <- theDef <$> getConstInfo d
851
let npars = case def of
852
Datatype{ dataPars = n } -> Just n
853
Record{ recPars = n } -> Just n
855
flip (maybe fallback) npars $ \n -> do
856
let ps = genericTake n vs
852
reportSDoc "tc.term.con" 50 $ nest 2 $ text "d =" <+> prettyTCM d
853
-- Issue 661: t maybe an evaluated form of d .., so we evaluate d
854
-- as well and then check wether we deal with the same datatype
855
t0 <- reduce (Def d [])
856
case (ignoreSharing t0, ignoreSharing $ unEl t) of -- Only fully applied constructors get special treatment
857
(Def d0 _, Def d' vs) -> do
858
reportSDoc "tc.term.con" 50 $ nest 2 $ text "d0 =" <+> prettyTCM d0
859
reportSDoc "tc.term.con" 50 $ nest 2 $ text "d' =" <+> prettyTCM d'
860
reportSDoc "tc.term.con" 50 $ nest 2 $ text "vs =" <+> prettyTCM vs
861
if d' /= d0 then fallback else do
862
-- Issue 661: d' may take more parameters than d, in particular
863
-- these additional parameters could be a module parameter telescope.
864
-- Since we get the constructor type ctype from d but the parameters
865
-- from t = Def d' vs, we drop the additional parameters.
866
npars <- getNumberOfParameters d
867
npars' <- getNumberOfParameters d'
868
flip (maybe fallback) (sequenceA $ List2 (npars, npars')) $ \(List2 (n,n')) -> do
869
reportSDoc "tc.term.con" 50 $ nest 2 $ text $ "n = " ++ show n
870
reportSDoc "tc.term.con" 50 $ nest 2 $ text $ "n' = " ++ show n'
871
-- when (n > n') __IMPOSSIBLE__ -- NOT IN SCOPE `__IMPOSSIBLE__' WHY???
873
let ps = genericTake n $ genericDrop (n' - n) vs
857
874
ctype = defType cdef
858
875
reportSDoc "tc.term.con" 20 $ vcat
859
876
[ text "special checking of constructor application of" <+> prettyTCM c
861
878
, text "ctype =" <+> prettyTCM ctype ] ]
862
879
let ctype' = ctype `piApply` ps
863
880
reportSDoc "tc.term.con" 20 $ nest 2 $ text "ctype' =" <+> prettyTCM ctype'
864
checkArguments' ExpandLast (getRange c) args ctype' t org $ \us t' -> do
881
-- check the non-parameter arguments
882
checkArguments' ExpandLast ExpandInstanceArguments (getRange c) args' ctype' t org $ \us t' -> do
865
883
reportSDoc "tc.term.con" 20 $ nest 2 $ vcat
866
884
[ text "us =" <+> prettyTCM us
867
885
, text "t' =" <+> prettyTCM t' ]
868
blockTerm t $ Con c us <$ leqType_ t' t
886
coerce (Con c us) t' t
888
reportSDoc "tc.term.con" 50 $ nest 2 $ text "we are not at a datatype, falling back"
871
891
fallback = checkHeadApplication org t (A.Con (AmbQ [c])) args
873
894
-- Check if there are explicitly given hidden arguments,
874
895
-- in which case we fall back to default type checking.
875
896
-- We could work harder, but let's not for now.
876
hiddenArg = case args of
877
Arg Hidden _ _ : _ -> True
898
-- Andreas, 2012-04-18: if all inital args are underscores, ignore them
899
checkForParams args =
900
let (hargs, rest) = span isHiddenArg args
901
removeScope (A.ScopedExpr _ e) = removeScope e
903
notUnderscore A.Underscore{} = False
904
notUnderscore _ = True
905
in (rest,) $ any notUnderscore $ map (removeScope . namedArg) hargs
907
{- UNUSED CODE, BUT DON'T REMOVE (2012-04-18)
880
909
-- Split the arguments to a constructor into those corresponding
881
910
-- to parameters and those that don't. Dummy underscores are inserted
961
993
-- Add the type signature of the fresh function to the
963
i <- currentMutualBlock
995
i <- currentOrFreshMutualBlock
964
996
tel <- getContextTelescope
965
997
-- If we are in irrelevant position, add definition irrelevantly.
966
998
-- TODO: is this sufficient?
967
999
rel <- asks envRelevance
968
addConstant c' (Defn rel c' t (defaultDisplayForm c') i noCompiledRep $ Axiom)
1000
addConstant c' (Defn rel c' t [] [] (defaultDisplayForm c') i noCompiledRep $ Axiom)
970
1002
-- Define and type check the fresh function.
971
1003
ctx <- getContext
972
1004
let info = A.mkDefInfo (A.nameConcrete $ A.qnameName c') defaultFixity'
973
1005
PublicAccess ConcreteDef noRange
974
pats = map (fmap $ \(n, _) -> Named Nothing (A.VarP n)) $
1006
pats = map (\ (Dom h r (n, _)) -> Arg h r $ Named Nothing $ A.VarP n) $
976
clause = A.Clause (A.LHS (A.LHSRange noRange) c' pats [])
1008
clause = A.Clause (A.LHS (A.LHSRange noRange) (A.LHSHead c' pats) [])
977
1009
(A.RHS $ unAppView (A.Application (A.Con (AmbQ [c])) args))
1028
1058
-- that have to be solved for everything to be well-formed.
1030
1060
-- TODO: doesn't do proper blocking of terms
1031
checkArguments :: ExpandHidden -> Range -> [NamedArg A.Expr] -> Type -> Type ->
1061
checkArguments :: ExpandHidden -> ExpandInstances -> Range -> [NamedArg A.Expr] -> Type -> Type ->
1032
1062
ErrorT Type TCM (Args, Type)
1033
checkArguments DontExpandLast _ [] t0 t1 = return ([], t0)
1034
checkArguments exh r [] t0 t1 =
1063
checkArguments DontExpandLast _ _ [] t0 t1 = return ([], t0)
1064
checkArguments exh expandIFS r [] t0 t1 =
1065
traceCallE (CheckArguments r [] t0 t1) $ lift $ do
1066
t1' <- unEl <$> reduce t1
1067
implicitArgs (-1) (expand t1') t0
1069
expand (Pi (Dom h _ _) _) Hidden = h /= Hidden
1070
expand _ Hidden = True
1071
expand (Pi (Dom h _ _) _) Instance = h /= Instance && expandIFS == ExpandInstanceArguments
1072
expand _ Instance = expandIFS == ExpandInstanceArguments
1073
expand _ NotHidden = False
1076
checkArguments exh expandIFS r [] t0 t1 =
1035
1077
traceCallE (CheckArguments r [] t0 t1) $ do
1036
1078
t0' <- lift $ reduce t0
1037
1079
t1' <- lift $ reduce t1
1039
Pi (Arg Hidden rel a) _ | notHPi Hidden $ unEl t1' -> do
1040
v <- lift $ applyRelevanceToContext rel $ newValueMeta a
1080
case ignoreSharing $ unEl t0' of
1081
Pi (Dom Hidden rel a) _ | notHPi Hidden $ unEl t1' -> do
1082
v <- lift $ applyRelevanceToContext rel $ newValueMeta RunMetaOccursCheck a
1041
1083
let arg = Arg Hidden rel v
1042
(vs, t0'') <- checkArguments exh r [] (piApply t0' [arg]) t1'
1084
(vs, t0'') <- checkArguments exh expandIFS r [] (piApply t0' [arg]) t1'
1043
1085
return (arg : vs, t0'')
1044
Pi (Arg Instance rel a) _ | notHPi Instance $ unEl t1' -> do
1086
Pi (Dom Instance rel a) _ | expandIFS == ExpandInstanceArguments &&
1087
(notHPi Instance $ unEl t1') -> do
1045
1088
lift $ reportSLn "tc.term.args.ifs" 15 $ "inserting implicit meta for type " ++ show a
1046
v <- lift $ applyRelevanceToContext rel $ newIFSMeta a
1089
v <- lift $ applyRelevanceToContext rel $ initializeIFSMeta a
1047
1090
let arg = Arg Instance rel v
1048
(vs, t0'') <- checkArguments exh r [] (piApply t0' [arg]) t1'
1091
(vs, t0'') <- checkArguments exh expandIFS r [] (piApply t0' [arg]) t1'
1049
1092
return (arg : vs, t0'')
1050
1093
_ -> return ([], t0')
1052
notHPi h (Pi (Arg h' _ _) _) | h == h' = False
1095
notHPi h (Pi (Dom h' _ _) _) | h == h' = False
1096
notHPi h (Shared p) = notHPi h $ derefPtr p
1053
1097
notHPi _ _ = True
1055
checkArguments exh r args0@(Arg h _ e : args) t0 t1 =
1100
checkArguments exh expandIFS r args0@(Arg h _ e : args) t0 t1 =
1056
1101
traceCallE (CheckArguments r args0 t0 t1) $ do
1102
lift $ reportSDoc "tc.term.args" 30 $ sep
1103
[ text "checkArguments"
1104
-- , text " args0 =" <+> prettyA args0
1106
[ text "e =" <+> prettyA e
1107
, text "t0 =" <+> prettyTCM t0
1108
, text "t1 =" <+> prettyTCM t1
1057
1111
t0b <- lift $ reduceB t0
1112
let isMeta t = case ignoreSharing $ unEl t of { MetaV{} -> True; _ -> False }
1059
Blocked{} -> throwError $ ignoreBlocking t0b
1060
NotBlocked (El _ MetaV{}) -> throwError $ ignoreBlocking t0b
1114
Blocked{} -> throwError $ ignoreBlocking t0b
1115
NotBlocked t0' | isMeta t0' -> throwError $ ignoreBlocking t0b
1061
1116
NotBlocked t0' -> do
1062
1117
-- (t0', cs) <- forcePi h (name e) t0
1063
1118
e' <- return $ namedThing e
1065
Pi (Arg h' rel a) _ |
1119
case ignoreSharing $ unEl t0' of
1120
Pi (Dom h' rel a) _ |
1066
1121
h == h' && (h == NotHidden || sameName (nameOf e) (nameInPi $ unEl t0')) -> do
1067
1122
u <- lift $ applyRelevanceToContext rel $ checkExpr e' a
1068
1123
let arg = Arg h rel u -- save relevance info in argument
1069
(us, t0'') <- checkArguments exh (fuseRange r e) args (piApply t0' [arg]) t1
1070
return (nukeIfIrrelevant arg : us, t0'')
1124
(us, t0'') <- checkArguments exh expandIFS (fuseRange r e) args (piApply t0' [arg]) t1
1125
return (arg : us, t0'')
1126
{- UNUSED. 2012-04-02 do not insert DontCare (is redundant anyway)
1071
1127
where nukeIfIrrelevant arg =
1072
1128
if argRelevance arg == Irrelevant then
1073
1129
-- Andreas, 2011-09-09 keep irr. args. until after termination checking
1074
1130
arg { unArg = DontCare $ unArg arg }
1076
Pi (Arg Instance rel a) _ -> insertIFSUnderscore rel a
1077
Pi (Arg Hidden rel a) _ -> insertUnderscore rel
1078
Pi (Arg NotHidden _ _) _ -> lift $ typeError $ WrongHidingInApplication t0'
1133
Pi (Dom Instance rel a) b | expandIFS == ExpandInstanceArguments ->
1134
insertIFSUnderscore rel (absName b) a
1135
Pi (Dom Hidden rel a) b -> insertUnderscore rel (absName b)
1136
Pi (Dom NotHidden _ _) _ -> lift $ typeError $ WrongHidingInApplication t0'
1079
1137
_ -> lift $ typeError $ ShouldBePi t0'
1081
insertIFSUnderscore rel a = do v <- lift $ applyRelevanceToContext rel $ newIFSMeta a
1082
lift $ reportSLn "tc.term.args.ifs" 15 $ "inserting implicit meta (2) for type " ++ show a
1083
let arg = Arg Instance rel v
1084
(vs, t0'') <- checkArguments exh r args0 (piApply t0 [arg]) t1
1085
return (arg : vs, t0'')
1086
insertUnderscore rel = do
1139
insertIFSUnderscore rel x a = do
1140
lift $ reportSLn "tc.term.args.ifs" 15 $ "inserting implicit meta (2) for type " ++ show a
1141
v <- lift $ applyRelevanceToContext rel $ initializeIFSMeta x a
1142
let arg = Arg Instance rel v
1143
(vs, t0'') <- checkArguments exh expandIFS r args0 (piApply t0 [arg]) t1
1144
return (arg : vs, t0'')
1146
insertUnderscore rel x = do
1087
1147
scope <- lift $ getScope
1088
1148
let m = A.Underscore $ A.MetaInfo
1089
1149
{ A.metaRange = r
1090
1150
, A.metaScope = scope
1091
1151
, A.metaNumber = Nothing
1152
, A.metaNameSuggestion = x
1093
checkArguments exh r (Arg Hidden rel (unnamed m) : args0) t0 t1
1154
checkArguments exh expandIFS r (Arg Hidden rel (unnamed m) : args0) t0 t1
1095
1156
name (Named _ (A.Var x)) = show x
1096
1157
name (Named (Just x) _) = x
1099
1160
sameName Nothing _ = True
1100
1161
sameName n1 n2 = n1 == n2
1102
nameInPi (Pi _ b) = Just $ absName b
1103
nameInPi _ = __IMPOSSIBLE__
1163
nameInPi (Pi _ b) = Just $ absName b
1164
nameInPi (Shared p) = nameInPi (derefPtr p)
1165
nameInPi _ = __IMPOSSIBLE__
1106
1168
-- | Check that a list of arguments fits a telescope.
1107
1169
checkArguments_ :: ExpandHidden -> Range -> [NamedArg A.Expr] -> Telescope -> TCM Args
1108
1170
checkArguments_ exh r args tel = do
1109
z <- runErrorT $ checkArguments exh r args (telePi tel $ sort Prop) (sort Prop)
1171
z <- runErrorT $ checkArguments exh ExpandInstanceArguments r args (telePi tel $ sort Prop) (sort Prop)
1111
1173
Right (args, _) -> return args
1112
1174
Left _ -> __IMPOSSIBLE__
1115
1177
-- | Infer the type of an expression. Implemented by checking against a meta
1178
-- variable. Except for neutrals, for them a polymorphic type is inferred.
1116
1179
inferExpr :: A.Expr -> TCM (Term, Type)
1118
-- Andreas, 2011-04-27
1119
t <- workOnTypes $ newTypeMeta_
1180
inferExpr e = inferOrCheck e Nothing
1183
_ | Application hd args <- appView e, defOrVar hd -> traceCall (InferExpr e) $ do
1184
(f, t0) <- inferHead hd
1185
res <- runErrorT $ checkArguments DontExpandLast ExpandInstanceArguments (getRange hd) args t0 (sort Prop)
1187
Right (vs, t1) -> return (f vs, t1)
1188
Left t1 -> fallback -- blocked on type t1
1192
t <- workOnTypes $ newTypeMeta_
1197
defOrVar :: A.Expr -> Bool
1198
defOrVar A.Var{} = True
1199
defOrVar A.Def{} = True
1202
inferOrCheck :: A.Expr -> Maybe Type -> TCM (Term, Type)
1203
inferOrCheck e mt = case e of
1204
_ | Application hd args <- appView e, defOrVar hd -> traceCall (InferExpr e) $ do
1205
(f, t0) <- inferHead hd
1206
res <- runErrorT $ checkArguments DontExpandLast ExpandInstanceArguments (getRange hd) args t0 $ maybe (sort Prop) id mt
1208
Right (vs, t1) -> maybe (return (f vs, t1))
1209
(\ t -> (,t) <$> coerce (f vs) t1 t)
1211
Left t1 -> fallback -- blocked on type t1
1215
t <- maybe (workOnTypes $ newTypeMeta_) return mt
1219
-- | Infer the type of an expression, and if it is of the form
1220
-- @{tel} -> D vs@ for some datatype @D@ then insert the hidden
1221
-- arguments. Otherwise, leave the type polymorphic.
1222
inferExprForWith :: A.Expr -> TCM (Term, Type)
1223
inferExprForWith e = do
1224
(v, t) <- inferExpr e
1225
TelV tel t0 <- telViewUpTo' (-1) ((NotHidden /=) . domHiding) t
1226
case ignoreSharing $ unEl t0 of
1228
res <- isDataOrRecordType d
1230
Nothing -> return (v, t)
1232
(args, t1) <- implicitArgs (-1) (NotHidden /=) t
1233
return (v `apply` args, t1)
1123
1236
checkTerm :: Term -> Type -> TCM Term
1124
1237
checkTerm tm ty = do atm <- reify tm
1133
1245
checkLetBindings = foldr (.) id . map checkLetBinding
1135
1247
checkLetBinding :: A.LetBinding -> TCM a -> TCM a
1136
1249
checkLetBinding b@(A.LetBind i rel x t e) ret =
1137
1250
traceCallCPS_ (CheckLetBinding b) ret $ \ret -> do
1139
1252
v <- applyRelevanceToContext rel $ checkExpr e t
1140
1253
addLetBinding rel x v t ret
1255
checkLetBinding b@(A.LetPatBind i p e) ret =
1256
traceCallCPS_ (CheckLetBinding b) ret $ \ret -> do
1257
(v, t) <- inferExpr e
1258
let -- construct a type t -> dummy for use in checkLeftHandSide
1259
t0 = El (getSort t) $ Pi (Dom NotHidden Relevant t) (NoAbs "_" typeDontCare)
1260
p0 = Arg NotHidden Relevant (Named Nothing p)
1261
reportSDoc "tc.term.let.pattern" 10 $ vcat
1262
[ text "let-binding pattern p at type t"
1264
[ text "p (A) =" <+> text (show p) -- prettyTCM p
1265
, text "t =" <+> prettyTCM t
1268
checkLeftHandSide (CheckPattern p EmptyTel t) [p0] t0 $ \ mgamma delta sub xs ps t' perm -> do
1269
-- A single pattern in internal syntax is returned.
1270
let p = case ps of [p] -> unArg p; _ -> __IMPOSSIBLE__
1271
reportSDoc "tc.term.let.pattern" 20 $ nest 2 $ vcat
1272
[ text "p (I) =" <+> text (show p)
1273
, text "delta =" <+> text (show delta)
1275
-- We translate it into a list of projections.
1276
fs <- recordPatternToProjections p
1277
-- We remove the bindings for the pattern variables from the context.
1279
let (binds, cxt) = splitAt (size delta) cxt0
1280
escapeContext (length binds) $ do
1281
reportSDoc "tc.term.let.pattern" 20 $ nest 2 $ vcat
1282
[ text "delta =" <+> prettyTCM delta
1283
, text "binds =" <+> text (show binds) -- prettyTCM binds
1285
{- WE CANNOT USE THIS BINDING
1286
-- We add a first let-binding for the value of e.
1287
x <- freshNoName (getRange e)
1288
addLetBinding Relevant x v t $ do
1290
-- We create a substitution for the let-bound variables
1291
-- (unfortunately, we cannot refer to x in internal syntax
1292
-- so we have to copy v).
1293
let sigma = zipWith ($) fs (repeat v)
1294
-- We apply the types of the let bound-variables to this substitution.
1295
-- The 0th variable in a context is the last one, so we reverse.
1296
-- Further, we need to lower all other de Bruijn indices by
1297
-- the size of delta, so we append the identity substitution.
1298
let sub = parallelS (reverse sigma)
1299
let fdelta = flattenTel delta
1300
reportSDoc "tc.term.let.pattern" 20 $ nest 2 $ vcat
1301
[ text "fdelta =" <+> text (show fdelta)
1303
let tsl = applySubst sub fdelta
1304
-- We get a list of types
1305
let ts = map unDom tsl
1307
let rels = map domRelevance tsl
1308
-- We get list of names of the let-bound vars from the context.
1309
let xs = map (fst . unDom) (reverse binds)
1310
-- We add all the bindings to the context.
1311
foldr (uncurry4 addLetBinding) ret $ zip4 rels xs sigma ts
1141
1313
checkLetBinding (A.LetApply i x modapp rd rm) ret = do
1142
1314
-- Any variables in the context that doesn't belong to the current
1143
1315
-- module should go with the new module.
added
removed
src/full/Agda/TypeChecking/Rules/Term.hs
