3
module Agda.TypeChecking.Injectivity where
5
import Prelude hiding (mapM)
6
import Control.Applicative
7
import Control.Monad hiding (mapM)
8
import Control.Monad.Error hiding (mapM)
9
import Control.Monad.State hiding (mapM)
10
import Control.Monad.Reader hiding (mapM)
12
import qualified Data.Map as Map
15
import Data.Traversable
17
import Agda.Syntax.Common
18
import Agda.Syntax.Internal
19
import Agda.TypeChecking.Monad
20
import Agda.TypeChecking.Substitute
21
import Agda.TypeChecking.Reduce
22
import Agda.TypeChecking.Primitive
23
import Agda.TypeChecking.MetaVars
24
import {-# SOURCE #-} Agda.TypeChecking.Conversion
25
import Agda.TypeChecking.Pretty
26
import Agda.TypeChecking.Constraints
27
import Agda.Utils.List
28
import Agda.Utils.Monad
29
import Agda.Utils.Permutation
31
#include "../undefined.h"
32
import Agda.Utils.Impossible
34
-- | Reduce simple (single clause) definitions.
35
reduceHead :: Term -> TCM (Blocked Term)
36
reduceHead v = ignoreAbstractMode $ do
37
v <- constructorForm v
40
def <- theDef <$> getConstInfo f
42
-- Function{ funClauses = [ _ ] } -> unfoldDefinition False reduceHead v f args
43
Datatype{ dataClause = Just _ } -> unfoldDefinition False reduceHead v f args
44
Record{ recClause = Just _ } -> unfoldDefinition False reduceHead v f args
45
_ -> return $ notBlocked v
46
_ -> return $ notBlocked v
48
headSymbol :: Term -> TCM (Maybe TermHead)
49
headSymbol v = ignoreAbstractMode $ do
50
v <- ignoreBlocking <$> reduceHead v
53
def <- theDef <$> getConstInfo f
55
Datatype{} -> return (Just $ ConHead f)
56
Record{} -> return (Just $ ConHead f)
57
Axiom{} -> return (Just $ ConHead f)
59
Con c _ -> return (Just $ ConHead c)
60
Sort _ -> return (Just SortHead)
61
Pi _ _ -> return (Just PiHead)
62
Fun _ _ -> return (Just PiHead)
63
Lit _ -> return Nothing -- handle literal heads as well? can't think of
64
-- any examples where it would be useful...
67
checkInjectivity :: QName -> [Clause] -> TCM FunctionInverse
68
checkInjectivity f cs = do
69
reportSLn "tc.inj.check" 40 $ "Checking injectivity of " ++ show f
70
es <- concat <$> mapM entry cs
71
let (hs, ps) = unzip es
72
reportSLn "tc.inj.check" 40 $ " right hand sides: " ++ show hs
73
if all isJust hs && distinct hs
75
let inv = Map.fromList (map fromJust hs `zip` ps)
76
reportSLn "tc.inj.check" 20 $ show f ++ " is injective."
77
reportSDoc "tc.inj.check" 30 $ nest 2 $ vcat $
78
map (\ (h, c) -> text (show h) <+> text "-->" <+>
79
fsep (punctuate comma $ map (text . show) $ clausePats c)
82
else return NotInjective
85
mv <- rhs (clauseBody c)
92
rhs (NoBind b) = rhs b
93
rhs (Bind b) = underAbstraction_ b rhs
94
rhs (Body v) = return $ Just v
95
rhs NoBody = return Nothing
97
-- | Argument should be on weak head normal form.
98
functionInverse :: Term -> TCM InvView
99
functionInverse v = case v of
101
d <- theDef <$> getConstInfo f
103
Function{ funInv = inv } -> case inv of
104
NotInjective -> return NoInv
105
Inverse m -> return $ Inv f args m
109
data InvView = Inv QName Args (Map TermHead Clause)
112
useInjectivity :: Comparison -> Type -> Term -> Term -> TCM Constraints
113
useInjectivity cmp a u v = do
114
uinv <- functionInverse u
115
vinv <- functionInverse v
117
(Inv f fArgs _, Inv g gArgs _)
119
a <- defType <$> getConstInfo f
120
reportSDoc "tc.inj.use" 20 $ vcat
121
[ fsep (pwords "comparing application of injective function" ++ [prettyTCM f] ++
123
, nest 2 $ fsep $ punctuate comma $ map prettyTCM fArgs
124
, nest 2 $ fsep $ punctuate comma $ map prettyTCM gArgs
125
, nest 2 $ text "and type" <+> prettyTCM a
127
pol <- getPolarity' cmp f
128
compareArgs pol a fArgs gArgs
129
| otherwise -> fallBack
130
(Inv f args inv, NoInv) -> do
131
a <- defType <$> getConstInfo f
132
reportSDoc "tc.inj.use" 20 $ fsep $
133
pwords "inverting injective function" ++
134
[ prettyTCM f, text ":", prettyTCM a, text "for", prettyTCM v
135
, parens $ text "args =" <+> prettyList (map prettyTCM args)
137
invert u f a inv args =<< headSymbol v
138
(NoInv, Inv g args inv) -> do
139
a <- defType <$> getConstInfo g
140
reportSDoc "tc.inj.use" 20 $ fsep $
141
pwords "inverting injective function" ++
142
[ prettyTCM g, text ":", prettyTCM a, text "for", prettyTCM u
143
, parens $ text "args =" <+> prettyList (map prettyTCM args)
145
invert v g a inv args =<< headSymbol u
146
(NoInv, NoInv) -> fallBack
148
fallBack = buildConstraint $ ValueCmp cmp a u v
150
invert _ _ a inv args Nothing = fallBack
151
invert org f ftype inv args (Just h) = case Map.lookup h inv of
152
Nothing -> typeError $ UnequalTerms cmp u v a
153
Just (Clause{ clauseTel = tel
155
, clausePats = ps }) -> do -- instArgs args ps
156
-- These are what dot patterns should be instantiated at
157
ms <- map unArg <$> newTelMeta tel
158
reportSDoc "tc.inj.invert" 20 $ vcat
159
[ text "meta patterns" <+> prettyList (map prettyTCM ms)
160
, text " perm =" <+> text (show perm)
161
, text " tel =" <+> prettyTCM tel
162
, text " ps =" <+> prettyList (map (text . show) ps)
164
-- and this is the order the variables occur in the patterns
165
let ms' = permute (invertP $ compactP perm) ms
166
cxt <- getContextTelescope
167
let sub = (reverse ms ++ idSub cxt)
168
margs <- runReaderT (evalStateT (metaArgs ps) ms') sub
169
reportSDoc "tc.inj.invert" 20 $ vcat
172
[ text "lhs =" <+> prettyTCM margs
173
, text "rhs =" <+> prettyTCM args
174
, text "type =" <+> prettyTCM ftype
177
pol <- getPolarity' cmp f
178
-- The clause might not give as many patterns as there
179
-- are arguments (point-free style definitions).
180
let args' = take (length margs) args
181
cs <- compareArgs pol ftype margs args'
182
unless (null cs) patternViolation
183
-- Check that we made progress, i.e. the head symbol
184
-- of the original term should be a constructor.
185
h <- headSymbol =<< reduce org
187
Just h -> compareTerm cmp a u v
188
Nothing -> patternViolation
189
`catchError` \err -> case err of
190
TypeError _ _ -> throwError err
191
Exception _ _ -> throwError err
192
PatternErr _ -> fallBack
193
AbortAssign _ -> fallBack
202
return $ substs sub v
204
metaArgs args = mapM metaArg args
205
metaArg arg = traverse metaPat arg
207
metaPat (DotP v) = dotP v
208
metaPat (VarP _) = nextMeta
209
metaPat (ConP c args) = Con c <$> metaArgs args
210
metaPat (LitP l) = return $ Lit l
added
removed
src/full/Agda/TypeChecking/Injectivity.hs
