0 | module TTImp.Impossible
  1 |
  2 | import Core.Env
  3 | import Core.Value
  4 |
  5 | import TTImp.TTImp
  6 | import TTImp.TTImp.Functor
  7 | import TTImp.Elab.App
  8 |
  9 | import Idris.Syntax
 10 | import Idris.Resugar
 11 |
 12 | %default covering
 13 |
 14 | -- This file contains support for building a guess at the term on the LHS of an
 15 | -- 'impossible' case, in order to help build a tree of covered cases for
 16 | -- coverage checking. Since the LHS by definition won't be well typed, we are
 17 | -- only guessing! But we can still do some type-directed disambiguation of
 18 | -- names.
 19 | -- Constants (fromInteger/fromString etc) won't be supported, because in general
 20 | -- they involve resolving interfaces - they'll just become unmatchable patterns.
 21 |
 22 | match : {auto c : Ref Ctxt Defs} ->
 23 |         ClosedNF -> (Name, Int, ClosedTerm) -> Core Bool
 24 | match nty (n, i, rty)
 25 |     = do defs <- get Ctxt
 26 |          rtynf <- nf defs Env.empty rty
 27 |          sameRet nty rtynf
 28 |   where
 29 |     sameRet : ClosedNF -> ClosedNF -> Core Bool
 30 |     sameRet _ (NApp {}) = pure True
 31 |     sameRet _ (NErased {}) = pure True
 32 |     sameRet (NApp {}) _ = pure True
 33 |     sameRet (NErased {}) _ = pure True
 34 |     sameRet (NTCon _ n _ _) (NTCon _ n' _ _) = pure (n == n')
 35 |     sameRet (NPrimVal _ c) (NPrimVal _ c') = pure (c == c')
 36 |     sameRet (NType {}) (NType {}) = pure True
 37 |     sameRet nf (NBind fc _ (Pi {}) sc)
 38 |         = do defs <- get Ctxt
 39 |              sc' <- sc defs (toClosure defaultOpts Env.empty (Erased fc Placeholder))
 40 |              sameRet nf sc'
 41 |     sameRet _ _ = pure False
 42 |
 43 | dropNoMatch : {auto c : Ref Ctxt Defs} ->
 44 |               Maybe ClosedNF -> List (Name, Int, GlobalDef) ->
 45 |               Core (List (Name, Int, GlobalDef))
 46 | dropNoMatch Nothing ts = pure ts
 47 | dropNoMatch (Just nty) ts
 48 |     = -- if the return type of a thing in ts doesn't match nty, drop it
 49 |       filterM (match nty . map (map type)) ts
 50 |
 51 | nextVar : {auto q : Ref QVar Int} ->
 52 |           FC -> Core ClosedTerm
 53 | nextVar fc
 54 |     = do i <- get QVar
 55 |          put QVar (i + 1)
 56 |          pure (Ref fc Bound (MN "imp" i))
 57 |
 58 | badClause : {auto c : Ref Ctxt Defs} ->
 59 |             ClosedTerm ->
 60 |             List (WithFC RawImp) ->
 61 |             List (WithFC RawImp) ->
 62 |             List (Name, WithFC RawImp) ->
 63 |             Core a
 64 | badClause fn exps autos named
 65 |    = throw (GenericMsg (getLoc fn)
 66 |             ("Badly formed impossible clause "
 67 |                ++ show (!(toFullNames fn),
 68 |                         (.val) <$> exps,
 69 |                         (.val) <$> autos,
 70 |                         mapSnd (.val) <$> named)))
 71 |
 72 | mutual
 73 |   processArgs : {auto c : Ref Ctxt Defs} ->
 74 |                 {auto s : Ref Syn SyntaxInfo} ->
 75 |                 {auto q : Ref QVar Int} ->
 76 |                 Bool -> -- should be fully applied
 77 |                 ClosedTerm -> ClosedNF ->
 78 |                 (expargs : List (WithFC RawImp)) ->
 79 |                 (autoargs : List (WithFC RawImp)) ->
 80 |                 (namedargs : List (Name, WithFC RawImp)) ->
 81 |                 Core ClosedTerm
 82 |   -- unnamed takes priority
 83 |   processArgs con fn (NBind _ x (Pi _ _ Explicit ty) sc) (e :: exps) autos named
 84 |      = do e' <- mkTerm e.val (Just ty)
 85 |           defs <- get Ctxt
 86 |           processArgs con (App e.fc fn e')
 87 |                       !(sc defs (toClosure defaultOpts Env.empty e'))
 88 |                       exps autos named
 89 |   processArgs con fn (NBind _ x (Pi _ _ Explicit ty) sc) [] autos named
 90 |      = do defs <- get Ctxt
 91 |           case findNamed x named of
 92 |             Just ((_, e), named') =>
 93 |                do e' <- mkTerm e.val (Just ty)
 94 |                   processArgs con (App e.fc fn e')
 95 |                               !(sc defs (toClosure defaultOpts Env.empty e'))
 96 |                               [] autos named'
 97 |             Nothing => -- Expected an explicit argument, but only implicits left
 98 |                        do let False = con
 99 |                             | True => throw $ GenericMsg (getLoc fn) $
100 |                                                 "Cannot match on a partially applied constructor: "
101 |                                                 ++ show !(toFullNames fn)
102 |                           let True = null autos && null named
103 |                             | False => badClause fn [] autos named -- unexpected arguments
104 |                           pure fn
105 |   processArgs con fn (NBind _ x (Pi _ _ Implicit ty) sc) exps autos named
106 |      = do defs <- get Ctxt
107 |           case findNamed x named of
108 |             Nothing => do let fc = getLoc fn
109 |                           e' <- nextVar fc
110 |                           processArgs con (App fc fn e')
111 |                                       !(sc defs (toClosure defaultOpts Env.empty e'))
112 |                                       exps autos named
113 |             Just ((_, e), named') =>
114 |                do e' <- mkTerm e.val (Just ty)
115 |                   processArgs con (App e.fc fn e')
116 |                               !(sc defs (toClosure defaultOpts Env.empty e'))
117 |                               exps autos named'
118 |   processArgs con fn (NBind _ x (Pi _ _ AutoImplicit ty) sc) exps autos named
119 |      = do defs <- get Ctxt
120 |           case autos of
121 |                (e :: autos') => -- unnamed takes priority
122 |                    do e' <- mkTerm e.val (Just ty)
123 |                       processArgs con (App e.fc fn e')
124 |                                   !(sc defs (toClosure defaultOpts Env.empty e'))
125 |                                   exps autos' named
126 |                [] =>
127 |                   case findNamed x named of
128 |                      Nothing =>
129 |                         do let fc = getLoc fn
130 |                            e' <- nextVar fc
131 |                            processArgs con (App fc fn e')
132 |                                        !(sc defs (toClosure defaultOpts Env.empty e'))
133 |                                        exps [] named
134 |                      Just ((_, e), named') =>
135 |                         do e' <- mkTerm e.val (Just ty)
136 |                            processArgs con (App e.fc fn e')
137 |                                        !(sc defs (toClosure defaultOpts Env.empty e'))
138 |                                        exps [] named'
139 |   processArgs _ fn _ [] [] [] = pure fn
140 |   processArgs _ fn _ (x :: _) autos named
141 |      = throw $ GenericMsg x.fc "Too many arguments"
142 |   processArgs _ fn _ exps autos named
143 |      = badClause fn exps autos named
144 |
145 |   buildApp : {auto c : Ref Ctxt Defs} ->
146 |              {auto s : Ref Syn SyntaxInfo} ->
147 |              {auto q : Ref QVar Int} ->
148 |              FC -> Name -> Maybe ClosedClosure ->
149 |              (expargs : List (WithFC RawImp)) ->
150 |              (autoargs : List (WithFC RawImp)) ->
151 |              (namedargs : List (Name, WithFC RawImp)) ->
152 |              Core ClosedTerm
153 |   buildApp fc n mty exps autos named
154 |       = do defs <- get Ctxt
155 |            prims <- getPrimitiveNames
156 |            when (n `elem` prims) $
157 |                throw (GenericMsg fc "Can't deal with \{show n} in impossible clauses yet")
158 |
159 |            gdefs <- lookupNameBy id n (gamma defs)
160 |            mty' <- traverseOpt (evalClosure defs) mty
161 |            [(n', i, gdef)] <- dropNoMatch mty' gdefs
162 |               | [] => if length gdefs == 0
163 |                         then undefinedName fc n
164 |                         else throw $ GenericMsg fc "\{show n} does not match expected type"
165 |               | ts => throw $ AmbiguousName fc (map fst ts)
166 |            tynf <- nf defs Env.empty (type gdef)
167 |            -- #899 we need to make sure that type & data constructors are marked
168 |            -- as such so that the coverage checker actually uses the matches in
169 |            -- `impossible` branches to generate parts of the case tree.
170 |            -- When `head` is `Func`, the pattern will be marked as forced and
171 |            -- the coverage checker will considers that all the cases have been
172 |            -- covered!
173 |            let nameType = getDefNameType gdef
174 |            processArgs (isJust $ isCon nameType)
175 |                        (Ref fc nameType (Resolved i))
176 |                        tynf exps autos named
177 |
178 |   mkTerm : {auto c : Ref Ctxt Defs} ->
179 |            {auto s : Ref Syn SyntaxInfo} ->
180 |            {auto q : Ref QVar Int} ->
181 |            RawImp -> Maybe ClosedClosure ->
182 |            Core ClosedTerm
183 |   mkTerm tm mty = go tm [] [] []
184 |     where
185 |       go : RawImp ->
186 |           (expargs : List (WithFC RawImp)) ->
187 |           (autoargs : List (WithFC RawImp)) ->
188 |           (namedargs : List (Name, WithFC RawImp)) ->
189 |           Core ClosedTerm
190 |       go (IVar fc n) exps autos named
191 |         = buildApp fc n mty exps autos named
192 |       go (IAs fc fc' u n pat) exps autos named
193 |         = go pat exps autos named
194 |       go (IApp fc fn arg) exps autos named
195 |         = go fn (MkFCVal fc arg :: exps) autos named
196 |       go (IWithApp fc fn arg) exps autos named
197 |         = go fn (MkFCVal fc arg :: exps) autos named
198 |       go (IAutoApp fc fn arg) exps autos named
199 |         = go fn exps (MkFCVal fc arg :: autos) named
200 |       go (INamedApp fc fn nm arg) exps autos named
201 |         = go fn exps autos ((nm, MkFCVal fc arg) :: named)
202 |       go (IMustUnify fc r tm) exps autos named
203 |         = Erased fc . Dotted <$> go tm exps autos named
204 |       go (IPrimVal fc c) _ _ _
205 |           = do let tm = PrimVal fc c
206 |                True <- isValidPrimType
207 |                  | _ => throw $ GenericMsg fc "\{show tm} does not match expected type"
208 |                pure tm
209 |         where
210 |           isValidPrimType : Core Bool
211 |           isValidPrimType
212 |             = do defs <- get Ctxt
213 |                  Just ty <- traverseOpt (evalClosure defs) mty
214 |                    | _ => pure False
215 |                  case (primType c, ty) of
216 |                       (Nothing, NType {}) => pure True
217 |                       (Just t1, NPrimVal _ (PrT t2)) => pure (t1 == t2)
218 |                       _ => pure False
219 |       go (IType fc) _ _ _
220 |           = do defs <- get Ctxt
221 |                Just (NType {}) <- traverseOpt (evalClosure defs) mty
222 |                  | _ => throw $ GenericMsg fc "Type does not match expected type"
223 |                pure (TType fc $ MN "top" 0)
224 |       -- We're taking UniqueDefault here, _and_ we're falling through to error otherwise, which is sketchy.
225 |       -- One option is to try each and emit an AmbiguousElab? We maybe should respect `UniqueDefault` if there
226 |       -- is no evidence (mty), but we should _try_ to resolve here if there is an mty.
227 |       go (IAlternative _ (UniqueDefault tm) _) exps autos named
228 |         = go tm exps autos named
229 |       go (Implicit fc _) _ _ _ = nextVar fc
230 |       go (IBindVar fc _) _ _ _ = nextVar fc
231 |       go tm _ _ _
232 |         = do tm' <- pterm (map defaultKindedName tm) -- hack
233 |              throw $ GenericMsg (getFC tm) "Unsupported term in impossible clause: \{show tm'}"
234 |
235 | -- Given an LHS that is declared 'impossible', build a term to match from,
236 | -- so that when we build the case tree for checking coverage, we take into
237 | -- account the impossible clauses
238 | export
239 | getImpossibleTerm : {vars : _} ->
240 |                     {auto c : Ref Ctxt Defs} ->
241 |                     {auto s : Ref Syn SyntaxInfo} ->
242 |                     Env Term vars -> NestedNames vars -> RawImp -> Core ClosedTerm
243 | getImpossibleTerm env nest tm
244 |     = do q <- newRef QVar (the Int 0)
245 |          mkTerm (applyEnv tm) Nothing
246 |   where
247 |     addEnv : {vars : _} ->
248 |              FC -> Env Term vars -> List RawImp
249 |     addEnv fc [] = []
250 |     addEnv fc (b :: env) =
251 |        if isLet b
252 |           then addEnv fc env
253 |           else Implicit fc False :: addEnv fc env
254 |
255 |     expandNest : RawImp -> RawImp
256 |     expandNest (IVar fc n)
257 |         = case lookup n (names nest) of
258 |                Just (Just n', _, _) => IVar fc n'
259 |                _ => IVar fc n
260 |     expandNest tm = tm
261 |
262 |     -- Need to apply the function to the surrounding environment, and update
263 |     -- the name to the proper one from the nested names map
264 |     applyEnv : RawImp -> RawImp
265 |     applyEnv (IApp fc fn arg) = IApp fc (applyEnv fn) arg
266 |     applyEnv (IWithApp fc fn arg) = IWithApp fc (applyEnv fn) arg
267 |     applyEnv (IAutoApp fc fn arg) = IAutoApp fc (applyEnv fn) arg
268 |     applyEnv (INamedApp fc fn n arg)
269 |         = INamedApp fc (applyEnv fn) n arg
270 |     applyEnv tm = apply (expandNest tm) (addEnv (getFC tm) env)
271 |