git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/src/Idris/Core/Evaluate.hs
1087 lines 47 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,
2 PatternGuards #-}
4module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
5 rt_simplify, simplify, specialise, hnf, convEq, convEq',
6 Def(..), CaseInfo(..), CaseDefs(..),
7 Accessibility(..), Totality(..), PReason(..), MetaInformation(..),
8 Context, initContext, ctxtAlist, next_tvar,
9 addToCtxt, setAccess, setTotal, setMetaInformation, addCtxtDef, addTyDecl,
10 addDatatype, addCasedef, simplifyCasedef, addOperator,
11 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
12 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
13 mapDefCtxt,
14 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict, isDConName, canBeDConName, isTConName, isConName, isFnName,
15 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,
16 isUniverse) where
18import Debug.Trace
19import Control.Applicative hiding (Const)
20import Control.Monad.State -- not Strict!
21import qualified Data.Binary as B
22import Data.Binary hiding (get, put)
24import Idris.Core.TT
25import Idris.Core.CaseTree
27data EvalState = ES { limited :: [(Name, Int)],
28 nexthole :: Int,
29 blocking :: Bool }
30 deriving Show
32type Eval a = State EvalState a
34data EvalOpt = Spec
35 | HNF
36 | Simplify
37 | AtREPL
38 | RunTT
39 deriving (Show, Eq)
41initEval = ES [] 0 False
43-- VALUES (as HOAS) ---------------------------------------------------------
44-- | A HOAS representation of values
45data Value = VP NameType Name Value
46 | VV Int
47 -- True for Bool indicates safe to reduce
48 | VBind Bool Name (Binder Value) (Value -> Eval Value)
49 -- For frozen let bindings when simplifying
50 | VBLet Int Name Value Value Value
51 | VApp Value Value
52 | VType UExp
53 | VUType Universe
54 | VErased
55 | VImpossible
56 | VConstant Const
57 | VProj Value Int
58-- | VLazy Env [Value] Term
59 | VTmp Int
61instance Show Value where
62 show x = show $ evalState (quote 100 x) initEval
64instance Show (a -> b) where
65 show x = "<<fn>>"
67-- THE EVALUATOR ------------------------------------------------------------
69-- The environment is assumed to be "locally named" - i.e., not de Bruijn
70-- indexed.
71-- i.e. it's an intermediate environment that we have while type checking or
72-- while building a proof.
74-- | Normalise fully type checked terms (so, assume all names/let bindings resolved)
75normaliseC :: Context -> Env -> TT Name -> TT Name
76normaliseC ctxt env t
77 = evalState (do val <- eval False ctxt [] env t []
78 quote 0 val) initEval
80normaliseAll :: Context -> Env -> TT Name -> TT Name
81normaliseAll ctxt env t
82 = evalState (do val <- eval False ctxt [] env t [AtREPL]
83 quote 0 val) initEval
85normalise :: Context -> Env -> TT Name -> TT Name
86normalise = normaliseTrace False
88normaliseTrace :: Bool -> Context -> Env -> TT Name -> TT Name
89normaliseTrace tr ctxt env t
90 = evalState (do val <- eval tr ctxt [] (map finalEntry env) (finalise t) []
91 quote 0 val) initEval
93-- Return a specialised name, and an updated list of reductions available,
94-- so that the caller can tell how much specialisation was achieved.
95specialise :: Context -> Env -> [(Name, Int)] -> TT Name ->
96 (TT Name, [(Name, Int)])
97specialise ctxt env limits t
98 = let (tm, st) =
99 runState (do val <- eval False ctxt []
100 (map finalEntry env) (finalise t)
101 [Spec]
102 quote 0 val) (initEval { limited = limits }) in
103 (tm, limited st)
105-- | Like normalise, but we only reduce functions that are marked as okay to
106-- inline (and probably shouldn't reduce lets?)
107-- 20130908: now only used to reduce for totality checking. Inlining should
108-- be done elsewhere.
110simplify :: Context -> Env -> TT Name -> TT Name
111simplify ctxt env t
112 = evalState (do val <- eval False ctxt [(sUN "lazy", 0),
113 (sUN "force", 0),
114 (sUN "Force", 0),
115 (sUN "assert_smaller", 0),
116 (sUN "assert_total", 0),
117 (sUN "par", 0),
118 (sUN "prim__syntactic_eq", 0),
119 (sUN "fork", 0)]
120 (map finalEntry env) (finalise t)
121 [Simplify]
122 quote 0 val) initEval
124-- | Simplify for run-time (i.e. basic inlining)
125rt_simplify :: Context -> Env -> TT Name -> TT Name
126rt_simplify ctxt env t
127 = evalState (do val <- eval False ctxt [(sUN "lazy", 0),
128 (sUN "force", 0),
129 (sUN "Force", 0),
130 (sUN "par", 0),
131 (sUN "prim__syntactic_eq", 0),
132 (sUN "prim_fork", 0)]
133 (map finalEntry env) (finalise t)
134 [RunTT]
135 quote 0 val) initEval
137-- | Reduce a term to head normal form
138hnf :: Context -> Env -> TT Name -> TT Name
139hnf ctxt env t
140 = evalState (do val <- eval False ctxt []
141 (map finalEntry env)
142 (finalise t) [HNF]
143 quote 0 val) initEval
146-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))
148finalEntry :: (Name, Binder (TT Name)) -> (Name, Binder (TT Name))
149finalEntry (n, b) = (n, fmap finalise b)
151bindEnv :: EnvTT n -> TT n -> TT n
152bindEnv [] tm = tm
153bindEnv ((n, Let t v):bs) tm = Bind n (NLet t v) (bindEnv bs tm)
154bindEnv ((n, b):bs) tm = Bind n b (bindEnv bs tm)
156unbindEnv :: EnvTT n -> TT n -> TT n
157unbindEnv [] tm = tm
158unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc
160usable :: Bool -- specialising
161 -> Name -> [(Name, Int)] -> Eval (Bool, [(Name, Int)])
162-- usable _ _ ns@((MN 0 "STOP", _) : _) = return (False, ns)
163usable False n [] = return (True, [])
164usable True n ns
165 = do ES ls num b <- get
166 if b then return (False, ns)
167 else case lookup n ls of
168 Just 0 -> return (False, ns)
169 Just i -> return (True, ns)
170 _ -> return (False, ns)
171usable False n ns
172 = case lookup n ns of
173 Just 0 -> return (False, ns)
174 Just i -> return $ (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns)
175 _ -> return $ (True, (n, 100) : filter (\ (n', _) -> n/=n') ns)
178fnCount :: Int -> Name -> Eval ()
179fnCount inc n
180 = do ES ls num b <- get
181 case lookup n ls of
182 Just i -> do put $ ES ((n, (i - inc)) :
183 filter (\ (n', _) -> n/=n') ls) num b
184 _ -> return ()
186setBlock :: Bool -> Eval ()
187setBlock b = do ES ls num _ <- get
188 put (ES ls num b)
190deduct = fnCount 1
191reinstate = fnCount (-1)
193-- | Evaluate in a context of locally named things (i.e. not de Bruijn indexed,
194-- such as we might have during construction of a proof)
196-- The (Name, Int) pair in the arguments is the maximum depth of unfolding of
197-- a name. The corresponding pair in the state is the maximum number of
198-- unfoldings overall.
200eval :: Bool -> Context -> [(Name, Int)] -> Env -> TT Name ->
201 [EvalOpt] -> Eval Value
202eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
203 spec = Spec `elem` opts
204 simpl = Simplify `elem` opts
205 runtime = RunTT `elem` opts
206 atRepl = AtREPL `elem` opts
207 hnf = HNF `elem` opts
209 -- returns 'True' if the function should block
210 -- normal evaluation should return false
211 blockSimplify (CaseInfo inl always dict) n stk
212 | RunTT `elem` opts
213 = if always then False
214 else not (inl || dict) || elem n stk
215 | Simplify `elem` opts
216 = (not (inl || dict) || elem n stk)
217 || (n == sUN "prim__syntactic_eq")
218 | otherwise = False
220 getCases cd | simpl = cases_totcheck cd
221 | runtime = cases_runtime cd
222 | otherwise = cases_compiletime cd
224 ev ntimes stk top env (P _ n ty)
225 | Just (Let t v) <- lookup n genv = ev ntimes stk top env v
226 ev ntimes_in stk top env (P Ref n ty)
227 | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)
228 | otherwise
229 = do (u, ntimes) <- usable spec n ntimes_in
230 if u then
231 do let val = lookupDefAcc n (spec || atRepl) ctxt
232 case val of
233 [(Function _ tm, _)] | sUN "assert_total" `elem` stk ->
234 ev ntimes (n:stk) True env tm
235 [(Function _ tm, Public)] ->
236 ev ntimes (n:stk) True env tm
237 [(Function _ tm, Hidden)] ->
238 ev ntimes (n:stk) True env tm
239 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty
240 return $ VP nt n vty
241 [(CaseOp ci _ _ _ _ cd, acc)]
242 | (acc /= Frozen || sUN "assert_total" `elem` stk) &&
243 null (fst (cases_totcheck cd)) -> -- unoptimised version
244 let (ns, tree) = getCases cd in
245 if blockSimplify ci n stk
246 then liftM (VP Ref n) (ev ntimes stk top env ty)
247 else -- traceWhen runtime (show (n, ns, tree)) $
248 do c <- evCase ntimes n (n:stk) top env ns [] tree
249 case c of
250 (Nothing, _) -> liftM (VP Ref n) (ev ntimes stk top env ty)
251 (Just v, _) -> return v
252 _ -> liftM (VP Ref n) (ev ntimes stk top env ty)
253 else liftM (VP Ref n) (ev ntimes stk top env ty)
254 ev ntimes stk top env (P nt n ty)
255 = liftM (VP nt n) (ev ntimes stk top env ty)
256 ev ntimes stk top env (V i)
257 | i < length env && i >= 0 = return $ snd (env !! i)
258 | otherwise = return $ VV i
259 ev ntimes stk top env (Bind n (Let t v) sc)
260 | not runtime || occurrences n sc < 2
261 = do v' <- ev ntimes stk top env v --(finalise v)
262 sc' <- ev ntimes stk top ((n, v') : env) sc
263 wknV (-1) sc'
264 | otherwise
265 = do t' <- ev ntimes stk top env t
266 v' <- ev ntimes stk top env v --(finalise v)
267 -- use Tmp as a placeholder, then make it a variable reference
268 -- again when evaluation finished
269 hs <- get
270 let vd = nexthole hs
271 put (hs { nexthole = vd + 1 })
272 sc' <- ev ntimes stk top ((n, VP Bound (sMN vd "vlet") VErased) : env) sc
273 return $ VBLet vd n t' v' sc'
274 ev ntimes stk top env (Bind n (NLet t v) sc)
275 = do t' <- ev ntimes stk top env (finalise t)
276 v' <- ev ntimes stk top env (finalise v)
277 sc' <- ev ntimes stk top ((n, v') : env) sc
278 return $ VBind True n (Let t' v') (\x -> return sc')
279 ev ntimes stk top env (Bind n b sc)
280 = do b' <- vbind env b
281 let n' = uniqueName n (map fst genv ++ map fst env)
282 return $ VBind True -- (vinstances 0 sc < 2)
283 n' b' (\x -> ev ntimes stk False ((n', x):env) sc)
284 where vbind env t
285 = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
286 -- block reduction immediately under codata (and not forced)
287 ev ntimes stk top env
288 (App (App (App d@(P _ (UN dly) _) l@(P _ (UN lco) _)) t) arg)
289 | dly == txt "Delay" && lco == txt "LazyCodata" && not (simpl || atRepl)
290 = do let (f, _) = unApply arg
291 let ntimes' = case f of
292 P _ fn _ -> (fn, 0) : ntimes
293 _ -> ntimes
294 when spec $ setBlock True
295 d' <- ev ntimes' stk False env d
296 l' <- ev ntimes' stk False env l
297 t' <- ev ntimes' stk False env t
298 arg' <- ev ntimes' stk False env arg
299 when spec $ setBlock False
300 evApply ntimes' stk top env [l',t',arg'] d'
301 -- Treat "assert_total" specially, as long as it's defined!
302 ev ntimes stk top env (App (App (P _ n@(UN at) _) _) arg)
303 | [(CaseOp _ _ _ _ _ _, _)] <- lookupDefAcc n (spec || atRepl) ctxt,
304 at == txt "assert_total" && not simpl
305 = ev ntimes (n : stk) top env arg
306 ev ntimes stk top env (App f a)
307 = do f' <- ev ntimes stk False env f
308 a' <- ev ntimes stk False env a
309 evApply ntimes stk top env [a'] f'
310 ev ntimes stk top env (Proj t i)
311 = do -- evaluate dictionaries if it means the projection works
312 t' <- ev ntimes stk top env t
313-- tfull' <- reapply ntimes stk top env t' []
314 return (doProj t' (getValArgs t'))
315 where doProj t' (VP (DCon _ _ _) _ _, args)
316 | i >= 0 && i < length args = args!!i
317 doProj t' _ = VProj t' i
319 ev ntimes stk top env (Constant c) = return $ VConstant c
320 ev ntimes stk top env Erased = return VErased
321 ev ntimes stk top env Impossible = return VImpossible
322 ev ntimes stk top env (TType i) = return $ VType i
323 ev ntimes stk top env (UType u) = return $ VUType u
325 evApply ntimes stk top env args (VApp f a)
326 = evApply ntimes stk top env (a:args) f
327 evApply ntimes stk top env args f
328 = apply ntimes stk top env f args
330 reapply ntimes stk top env f@(VP Ref n ty) args
331 = let val = lookupDefAcc n (spec || atRepl) ctxt in
332 case val of
333 [(CaseOp ci _ _ _ _ cd, acc)] ->
334 let (ns, tree) = getCases cd in
335 do c <- evCase ntimes n (n:stk) top env ns args tree
336 case c of
337 (Nothing, _) -> return $ unload env (VP Ref n ty) args
338 (Just v, rest) -> evApply ntimes stk top env rest v
339 _ -> case args of
340 (a : as) -> return $ unload env f (a : as)
341 [] -> return f
342 reapply ntimes stk top env (VApp f a) args
343 = reapply ntimes stk top env f (a : args)
344 reapply ntimes stk top env v args = return v
346 apply ntimes stk top env (VBind True n (Lam t) sc) (a:as)
347 = do a' <- sc a
348 app <- apply ntimes stk top env a' as
349 wknV 1 app
350 apply ntimes_in stk top env f@(VP Ref n ty) args
351 | not top && hnf = case args of
352 [] -> return f
353 _ -> return $ unload env f args
354 | otherwise
355 = do (u, ntimes) <- usable spec n ntimes_in
356 if u then
357 do let val = lookupDefAcc n (spec || atRepl) ctxt
358 case val of
359 [(CaseOp ci _ _ _ _ cd, acc)]
360 | acc /= Frozen || sUN "assert_total" `elem` stk ->
361 -- unoptimised version
362 let (ns, tree) = getCases cd in
363 if blockSimplify ci n stk
364 then return $ unload env (VP Ref n ty) args
365 else -- traceWhen runtime (show (n, ns, tree)) $
366 do c <- evCase ntimes n (n:stk) top env ns args tree
367 case c of
368 (Nothing, _) -> return $ unload env (VP Ref n ty) args
369 (Just v, rest) -> evApply ntimes stk top env rest v
370 [(Operator _ i op, _)] ->
371 if (i <= length args)
372 then case op (take i args) of
373 Nothing -> return $ unload env (VP Ref n ty) args
374 Just v -> evApply ntimes stk top env (drop i args) v
375 else return $ unload env (VP Ref n ty) args
376 _ -> case args of
377 [] -> return f
378 _ -> return $ unload env f args
379 else case args of
380 (a : as) -> return $ unload env f (a:as)
381 [] -> return f
382 apply ntimes stk top env f (a:as) = return $ unload env f (a:as)
383 apply ntimes stk top env f [] = return f
385-- specApply stk env f@(VP Ref n ty) args
386-- = case lookupCtxt n statics of
387-- [as] -> if or as
388-- then trace (show (n, map fst (filter (\ (_, s) -> s) (zip args as)))) $
389-- return $ unload env f args
390-- else return $ unload env f args
391-- _ -> return $ unload env f args
392-- specApply stk env f args = return $ unload env f args
394 unload :: [(Name, Value)] -> Value -> [Value] -> Value
395 unload env f [] = f
396 unload env f (a:as) = unload env (VApp f a) as
398 evCase ntimes n stk top env ns args tree
399 | length ns <= length args
400 = do let args' = take (length ns) args
401 let rest = drop (length ns) args
402 when spec $ deduct n
403 t <- evTree ntimes stk top env (zip ns args') tree
404 when spec $ case t of
405 Nothing -> reinstate n -- Blocked, count n again
406 Just _ -> return ()
407-- (zipWith (\n , t) -> (n, t)) ns args') tree
408 return (t, rest)
409 | otherwise = return (Nothing, args)
411 evTree :: [(Name, Int)] -> [Name] -> Bool ->
412 [(Name, Value)] -> [(Name, Value)] -> SC -> Eval (Maybe Value)
413 evTree ntimes stk top env amap (UnmatchedCase str) = return Nothing
414 evTree ntimes stk top env amap (STerm tm)
415 = do let etm = pToVs (map fst amap) tm
416 etm' <- ev ntimes stk (not (conHeaded tm))
417 (amap ++ env) etm
418 return $ Just etm'
419 evTree ntimes stk top env amap (ProjCase t alts)
420 = do t' <- ev ntimes stk top env t
421 doCase ntimes stk top env amap t' alts
422 evTree ntimes stk top env amap (Case _ n alts)
423 = case lookup n amap of
424 Just v -> doCase ntimes stk top env amap v alts
425 _ -> return Nothing
426 evTree ntimes stk top env amap ImpossibleCase = return Nothing
428 doCase ntimes stk top env amap v alts =
429 do c <- chooseAlt env v (getValArgs v) alts amap
430 case c of
431 Just (altmap, sc) -> evTree ntimes stk top env altmap sc
432 _ -> do c' <- chooseAlt' ntimes stk env v (getValArgs v) alts amap
433 case c' of
434 Just (altmap, sc) -> evTree ntimes stk top env altmap sc
435 _ -> return Nothing
437 conHeaded tm@(App _ _)
438 | (P (DCon _ _ _) _ _, args) <- unApply tm = True
439 conHeaded t = False
441 chooseAlt' ntimes stk env _ (f, args) alts amap
442 = do f' <- apply ntimes stk True env f args
443 chooseAlt env f' (getValArgs f')
444 alts amap
446 chooseAlt :: [(Name, Value)] -> Value -> (Value, [Value]) -> [CaseAlt] ->
447 [(Name, Value)] ->
448 Eval (Maybe ([(Name, Value)], SC))
449 chooseAlt env _ (VP (DCon i a _) _ _, args) alts amap
450 | Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)
451 | Just v <- findDefault alts = return $ Just (amap, v)
452 chooseAlt env _ (VP (TCon i a) _ _, args) alts amap
453 | Just (ns, sc) <- findTag i alts
454 = return $ Just (updateAmap (zip ns args) amap, sc)
455 | Just v <- findDefault alts = return $ Just (amap, v)
456 chooseAlt env _ (VConstant c, []) alts amap
457 | Just v <- findConst c alts = return $ Just (amap, v)
458 | Just (n', sub, sc) <- findSuc c alts
459 = return $ Just (updateAmap [(n',sub)] amap, sc)
460 | Just v <- findDefault alts = return $ Just (amap, v)
461 chooseAlt env _ (VP _ n _, args) alts amap
462 | Just (ns, sc) <- findFn n alts = return $ Just (updateAmap (zip ns args) amap, sc)
463 chooseAlt env _ (VBind _ _ (Pi i s k) t, []) alts amap
464 | Just (ns, sc) <- findFn (sUN "->") alts
465 = do t' <- t (VV 0) -- we know it's not in scope or it's not a pattern
466 return $ Just (updateAmap (zip ns [s, t']) amap, sc)
467 chooseAlt _ _ _ alts amap
468 | Just v <- findDefault alts
469 = if (any fnCase alts)
470 then return $ Just (amap, v)
471 else return Nothing
472 | otherwise = return Nothing
474 fnCase (FnCase _ _ _) = True
475 fnCase _ = False
477 -- Replace old variable names in the map with new matches
478 -- (This is possibly unnecessary since we make unique names and don't
479 -- allow repeated variables...?)
480 updateAmap newm amap
481 = newm ++ filter (\ (x, _) -> not (elem x (map fst newm))) amap
482 findTag i [] = Nothing
483 findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
484 findTag i (_ : xs) = findTag i xs
486 findFn fn [] = Nothing
487 findFn fn (FnCase n ns sc : xs) | fn == n = Just (ns, sc)
488 findFn fn (_ : xs) = findFn fn xs
490 findDefault [] = Nothing
491 findDefault (DefaultCase sc : xs) = Just sc
492 findDefault (_ : xs) = findDefault xs
494 findSuc c [] = Nothing
495 findSuc (BI val) (SucCase n sc : _)
496 | val /= 0 = Just (n, VConstant (BI (val - 1)), sc)
497 findSuc c (_ : xs) = findSuc c xs
499 findConst c [] = Nothing
500 findConst c (ConstCase c' v : xs) | c == c' = Just v
501 findConst (AType (ATInt ITNative)) (ConCase n 1 [] v : xs) = Just v
502 findConst (AType ATFloat) (ConCase n 2 [] v : xs) = Just v
503 findConst (AType (ATInt ITChar)) (ConCase n 3 [] v : xs) = Just v
504 findConst StrType (ConCase n 4 [] v : xs) = Just v
505 findConst (AType (ATInt ITBig)) (ConCase n 6 [] v : xs) = Just v
506 findConst (AType (ATInt (ITFixed ity))) (ConCase n tag [] v : xs)
507 | tag == 7 + fromEnum ity = Just v
508 findConst c (_ : xs) = findConst c xs
510 getValArgs tm = getValArgs' tm []
511 getValArgs' (VApp f a) as = getValArgs' f (a:as)
512 getValArgs' f as = (f, as)
514-- tmpToV i vd (VLetHole j) | vd == j = return $ VV i
515-- tmpToV i vd (VP nt n v) = liftM (VP nt n) (tmpToV i vd v)
516-- tmpToV i vd (VBind n b sc) = do b' <- fmapMB (tmpToV i vd) b
517-- let sc' = \x -> do x' <- sc x
518-- tmpToV (i + 1) vd x'
519-- return (VBind n b' sc')
520-- tmpToV i vd (VApp f a) = liftM2 VApp (tmpToV i vd f) (tmpToV i vd a)
521-- tmpToV i vd x = return x
523instance Eq Value where
524 (==) x y = getTT x == getTT y
525 where getTT v = evalState (quote 0 v) initEval
527class Quote a where
528 quote :: Int -> a -> Eval (TT Name)
530instance Quote Value where
531 quote i (VP nt n v) = liftM (P nt n) (quote i v)
532 quote i (VV x) = return $ V x
533 quote i (VBind _ n b sc) = do sc' <- sc (VTmp i)
534 b' <- quoteB b
535 liftM (Bind n b') (quote (i+1) sc')
536 where quoteB t = fmapMB (quote i) t
537 quote i (VBLet vd n t v sc)
538 = do sc' <- quote i sc
539 t' <- quote i t
540 v' <- quote i v
541 let sc'' = pToV (sMN vd "vlet") (addBinder sc')
542 return (Bind n (Let t' v') sc'')
543 quote i (VApp f a) = liftM2 App (quote i f) (quote i a)
544 quote i (VType u) = return $ TType u
545 quote i (VUType u) = return $ UType u
546 quote i VErased = return $ Erased
547 quote i VImpossible = return $ Impossible
548 quote i (VProj v j) = do v' <- quote i v
549 return (Proj v' j)
550 quote i (VConstant c) = return $ Constant c
551 quote i (VTmp x) = return $ V (i - x - 1)
553wknV :: Int -> Value -> Eval Value
554wknV i (VV x) | x >= i = return $ VV (x - 1)
555wknV i (VBind red n b sc) = do b' <- fmapMB (wknV i) b
556 return $ VBind red n b' (\x -> do x' <- sc x
557 wknV (i + 1) x')
558wknV i (VApp f a) = liftM2 VApp (wknV i f) (wknV i a)
559wknV i t = return t
561isUniverse :: Term -> Bool
562isUniverse (TType _) = True
563isUniverse (UType _) = True
564isUniverse _ = False
566isUsableUniverse :: Term -> Bool
567isUsableUniverse (UType NullType) = False
568isUsableUniverse x = isUniverse x
570convEq' ctxt hs x y = evalStateT (convEq ctxt hs x y) (0, [])
572convEq :: Context -> [Name] -> TT Name -> TT Name -> StateT UCs TC Bool
573convEq ctxt holes topx topy = ceq [] topx topy where
574 ceq :: [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
575 ceq ps (P xt x _) (P yt y _)
576 | x `elem` holes || y `elem` holes = return True
577 | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True
578 | otherwise = sameDefs ps x y
579 ceq ps x (Bind n (Lam t) (App y (V 0)))
580 = ceq ps x (substV (P Bound n t) y)
581 ceq ps (Bind n (Lam t) (App x (V 0))) y
582 = ceq ps (substV (P Bound n t) x) y
583 ceq ps x (Bind n (Lam t) (App y (P Bound n' _)))
584 | n == n' = ceq ps x y
585 ceq ps (Bind n (Lam t) (App x (P Bound n' _))) y
586 | n == n' = ceq ps x y
588 ceq ps (Bind n (PVar t) sc) y = ceq ps sc y
589 ceq ps x (Bind n (PVar t) sc) = ceq ps x sc
590 ceq ps (Bind n (PVTy t) sc) y = ceq ps sc y
591 ceq ps x (Bind n (PVTy t) sc) = ceq ps x sc
593 ceq ps (V x) (V y) = return (x == y)
594 ceq ps (V x) (P _ y _)
595 | x >= 0 && length ps > x = return (fst (ps!!x) == y)
596 | otherwise = return False
597 ceq ps (P _ x _) (V y)
598 | y >= 0 && length ps > y = return (x == snd (ps!!y))
599 | otherwise = return False
600 ceq ps (Bind n xb xs) (Bind n' yb ys)
601 = liftM2 (&&) (ceqB ps xb yb) (ceq ((n,n'):ps) xs ys)
602 where
603 ceqB ps (Let v t) (Let v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')
604 ceqB ps (Guess v t) (Guess v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')
605 ceqB ps (Pi i v t) (Pi i' v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')
606 ceqB ps b b' = ceq ps (binderTy b) (binderTy b')
607 ceq ps (App fx ax) (App fy ay) = liftM2 (&&) (ceq ps fx fy) (ceq ps ax ay)
608 ceq ps (Constant x) (Constant y) = return (x == y)
609 ceq ps (TType x) (TType y) = do (v, cs) <- get
610 put (v, ULE x y : cs)
611 return True
612 ceq ps (UType AllTypes) x = return (isUsableUniverse x)
613 ceq ps x (UType AllTypes) = return (isUsableUniverse x)
614 ceq ps (UType u) (UType v) = return (u == v)
615 ceq ps Erased _ = return True
616 ceq ps _ Erased = return True
617 ceq ps x y = return False
619 caseeq ps (Case _ n cs) (Case _ n' cs') = caseeqA ((n,n'):ps) cs cs'
620 where
621 caseeqA ps (ConCase x i as sc : rest) (ConCase x' i' as' sc' : rest')
622 = do q1 <- caseeq (zip as as' ++ ps) sc sc'
623 q2 <- caseeqA ps rest rest'
624 return $ x == x' && i == i' && q1 && q2
625 caseeqA ps (ConstCase x sc : rest) (ConstCase x' sc' : rest')
626 = do q1 <- caseeq ps sc sc'
627 q2 <- caseeqA ps rest rest'
628 return $ x == x' && q1 && q2
629 caseeqA ps (DefaultCase sc : rest) (DefaultCase sc' : rest')
630 = liftM2 (&&) (caseeq ps sc sc') (caseeqA ps rest rest')
631 caseeqA ps [] [] = return True
632 caseeqA ps _ _ = return False
633 caseeq ps (STerm x) (STerm y) = ceq ps x y
634 caseeq ps (UnmatchedCase _) (UnmatchedCase _) = return True
635 caseeq ps _ _ = return False
637 sameDefs ps x y = case (lookupDef x ctxt, lookupDef y ctxt) of
638 ([Function _ xdef], [Function _ ydef])
639 -> ceq ((x,y):ps) xdef ydef
640 ([CaseOp _ _ _ _ _ xd],
641 [CaseOp _ _ _ _ _ yd])
642 -> let (_, xdef) = cases_compiletime xd
643 (_, ydef) = cases_compiletime yd in
644 caseeq ((x,y):ps) xdef ydef
645 _ -> return False
647-- SPECIALISATION -----------------------------------------------------------
648-- We need too much control to be able to do this by tweaking the main
649-- evaluator
651spec :: Context -> Ctxt [Bool] -> Env -> TT Name -> Eval (TT Name)
652spec ctxt statics genv tm = error "spec undefined"
654-- CONTEXTS -----------------------------------------------------------------
656{-| A definition is either a simple function (just an expression with a type),
657 a constant, which could be a data or type constructor, an axiom or as an
658 yet undefined function, or an Operator.
659 An Operator is a function which explains how to reduce.
660 A CaseOp is a function defined by a simple case tree -}
662data Def = Function !Type !Term
663 | TyDecl NameType !Type
664 | Operator Type Int ([Value] -> Maybe Value)
665 | CaseOp CaseInfo
666 !Type
667 ![Type] -- argument types
668 ![Either Term (Term, Term)] -- original definition
669 ![([Name], Term, Term)] -- simplified for totality check definition
670 !CaseDefs
671-- [Name] SC -- Compile time case definition
672-- [Name] SC -- Run time cae definitions
674data CaseDefs = CaseDefs {
675 cases_totcheck :: !([Name], SC),
676 cases_compiletime :: !([Name], SC),
677 cases_inlined :: !([Name], SC),
678 cases_runtime :: !([Name], SC)
679 }
681data CaseInfo = CaseInfo {
682 case_inlinable :: Bool, -- decided by machine
683 case_alwaysinline :: Bool, -- decided by %inline flag
684 tc_dictionary :: Bool
685 }
687{-!
688deriving instance Binary Def
689!-}
690{-!
691deriving instance Binary CaseInfo
692!-}
693{-!
694deriving instance Binary CaseDefs
695!-}
696{-!
697deriving instance NFData Def
698!-}
699{-!
700deriving instance NFData CaseInfo
701!-}
702{-!
703deriving instance NFData CaseDefs
704!-}
706instance Show Def where
707 show (Function ty tm) = "Function: " ++ show (ty, tm)
708 show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty
709 show (Operator ty _ _) = "Operator: " ++ show ty
710 show (CaseOp (CaseInfo inlc inla inlr) ty atys ps_in ps cd)
711 = let (ns, sc) = cases_compiletime cd
712 (ns_t, sc_t) = cases_totcheck cd
713 (ns', sc') = cases_runtime cd in
714 "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++
715 "TOTALITY CHECK TIME:\n\n" ++
716 show ns_t ++ " " ++ show sc_t ++ "\n\n" ++
717 "COMPILE TIME:\n\n" ++
718 show ns ++ " " ++ show sc ++ "\n\n" ++
719 "RUN TIME:\n\n" ++
720 show ns' ++ " " ++ show sc' ++ "\n\n" ++
721 if inlc then "Inlinable" else "Not inlinable" ++
722 if inla then " Aggressively\n" else "\n"
724-------
726-- Frozen => doesn't reduce
727-- Hidden => doesn't reduce and invisible to type checker
729data Accessibility = Public | Frozen | Hidden
730 deriving (Show, Eq)
731{-!
732deriving instance NFData Accessibility
733!-}
735-- | The result of totality checking
736data Totality = Total [Int] -- ^ well-founded arguments
737 | Productive -- ^ productive
738 | Partial PReason
739 | Unchecked
740 deriving Eq
741{-!
742deriving instance NFData Totality
743!-}
745-- | Reasons why a function may not be total
746data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name
747 | ExternalIO | BelieveMe | Mutual [Name] | NotProductive
748 deriving (Show, Eq)
749{-!
750deriving instance NFData PReason
751!-}
753instance Show Totality where
754 show (Total args)= "Total" -- ++ show args ++ " decreasing arguments"
755 show Productive = "Productive" -- ++ show args ++ " decreasing arguments"
756 show Unchecked = "not yet checked for totality"
757 show (Partial Itself) = "possibly not total as it is not well founded"
758 show (Partial NotCovering) = "not total as there are missing cases"
759 show (Partial NotPositive) = "not strictly positive"
760 show (Partial ExternalIO) = "an external IO primitive"
761 show (Partial NotProductive) = "not productive"
762 show (Partial BelieveMe) = "not total due to use of believe_me in proof"
763 show (Partial (Other ns)) = "possibly not total due to: " ++ showSep ", " (map show ns)
764 show (Partial (Mutual ns)) = "possibly not total due to recursive path " ++
765 showSep " --> " (map show ns)
767{-!
768deriving instance Binary Accessibility
769!-}
771{-!
772deriving instance Binary Totality
773!-}
775{-!
776deriving instance Binary PReason
777!-}
779-- Possible attached meta-information for a definition in context
780data MetaInformation =
781 EmptyMI -- ^ No meta-information
782 | DataMI [Int] -- ^ Meta information for a data declaration with position of parameters
783 deriving (Eq, Show)
785-- | Contexts used for global definitions and for proof state. They contain
786-- universe constraints and existing definitions.
787data Context = MkContext {
788 next_tvar :: Int,
789 definitions :: Ctxt (Def, Accessibility, Totality, MetaInformation)
790 } deriving Show
792-- | The initial empty context
793initContext = MkContext 0 emptyContext
795mapDefCtxt :: (Def -> Def) -> Context -> Context
796mapDefCtxt f (MkContext t defs) = MkContext t (mapCtxt f' defs)
797 where f' (d, a, t, m) = f' (f d, a, t, m)
799-- | Get the definitions from a context
800ctxtAlist :: Context -> [(Name, Def)]
801ctxtAlist ctxt = map (\(n, (d, a, t, m)) -> (n, d)) $ toAlist (definitions ctxt)
803veval ctxt env t = evalState (eval False ctxt [] env t []) initEval
805addToCtxt :: Name -> Term -> Type -> Context -> Context
806addToCtxt n tm ty uctxt
807 = let ctxt = definitions uctxt
808 ctxt' = addDef n (Function ty tm, Public, Unchecked, EmptyMI) ctxt in
809 uctxt { definitions = ctxt' }
811setAccess :: Name -> Accessibility -> Context -> Context
812setAccess n a uctxt
813 = let ctxt = definitions uctxt
814 ctxt' = updateDef n (\ (d, _, t, m) -> (d, a, t, m)) ctxt in
815 uctxt { definitions = ctxt' }
817setTotal :: Name -> Totality -> Context -> Context
818setTotal n t uctxt
819 = let ctxt = definitions uctxt
820 ctxt' = updateDef n (\ (d, a, _, m) -> (d, a, t, m)) ctxt in
821 uctxt { definitions = ctxt' }
823setMetaInformation :: Name -> MetaInformation -> Context -> Context
824setMetaInformation n m uctxt
825 = let ctxt = definitions uctxt
826 ctxt' = updateDef n (\ (d, a, t, _) -> (d, a, t, m)) ctxt in
827 uctxt { definitions = ctxt' }
829addCtxtDef :: Name -> Def -> Context -> Context
830addCtxtDef n d c = let ctxt = definitions c
831 ctxt' = addDef n (d, Public, Unchecked, EmptyMI) $! ctxt in
832 c { definitions = ctxt' }
834addTyDecl :: Name -> NameType -> Type -> Context -> Context
835addTyDecl n nt ty uctxt
836 = let ctxt = definitions uctxt
837 ctxt' = addDef n (TyDecl nt ty, Public, Unchecked, EmptyMI) ctxt in
838 uctxt { definitions = ctxt' }
840addDatatype :: Datatype Name -> Context -> Context
841addDatatype (Data n tag ty unique cons) uctxt
842 = let ctxt = definitions uctxt
843 ty' = normalise uctxt [] ty
844 ctxt' = addCons 0 cons (addDef n
845 (TyDecl (TCon tag (arity ty')) ty, Public, Unchecked, EmptyMI) ctxt) in
846 uctxt { definitions = ctxt' }
847 where
848 addCons tag [] ctxt = ctxt
849 addCons tag ((n, ty) : cons) ctxt
850 = let ty' = normalise uctxt [] ty in
851 addCons (tag+1) cons (addDef n
852 (TyDecl (DCon tag (arity ty') unique) ty, Public, Unchecked, EmptyMI) ctxt)
854-- FIXME: Too many arguments! Refactor all these Bools.
855--
856-- Issue #1724 on the issue tracker.
857-- https://github.com/idris-lang/Idris-dev/issues/1724
858addCasedef :: Name -> ErasureInfo -> CaseInfo ->
859 Bool -> SC -> -- default case
860 Bool -> Bool ->
861 [Type] -> -- argument types
862 [Int] -> -- inaccessible arguments
863 [Either Term (Term, Term)] ->
864 [([Name], Term, Term)] -> -- totality
865 [([Name], Term, Term)] -> -- compile time
866 [([Name], Term, Term)] -> -- inlined
867 [([Name], Term, Term)] -> -- run time
868 Type -> Context -> Context
869addCasedef n ei ci@(CaseInfo inline alwaysInline tcdict)
870 tcase covering reflect asserted argtys inacc
871 ps_in ps_tot ps_inl ps_ct ps_rt ty uctxt
872 = let ctxt = definitions uctxt
873 access = case lookupDefAcc n False uctxt of
874 [(_, acc)] -> acc
875 _ -> Public
876 ctxt' = case (simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_tot ei,
877 simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_ct ei,
878 simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_inl ei,
879 simpleCase tcase covering reflect RunTime emptyFC inacc argtys ps_rt ei) of
880 (OK (CaseDef args_tot sc_tot _),
881 OK (CaseDef args_ct sc_ct _),
882 OK (CaseDef args_inl sc_inl _),
883 OK (CaseDef args_rt sc_rt _)) ->
884 let inl = alwaysInline -- tcdict
885 inlc = (inl || small n args_ct sc_ct) && (not asserted)
886 inlr = inl || small n args_rt sc_rt
887 cdef = CaseDefs (args_tot, sc_tot)
888 (args_ct, sc_ct)
889 (args_inl, sc_inl)
890 (args_rt, sc_rt) in
891 addDef n (CaseOp (ci { case_inlinable = inlc })
892 ty argtys ps_in ps_tot cdef,
893 access, Unchecked, EmptyMI) ctxt in
894 uctxt { definitions = ctxt' }
896-- simplify a definition for totality checking
897simplifyCasedef :: Name -> ErasureInfo -> Context -> Context
898simplifyCasedef n ei uctxt
899 = let ctxt = definitions uctxt
900 ctxt' = case lookupCtxt n ctxt of
901 [(CaseOp ci ty atys [] ps _, acc, tot, metainf)] ->
902 ctxt -- nothing to simplify (or already done...)
903 [(CaseOp ci ty atys ps_in ps cd, acc, tot, metainf)] ->
904 let ps_in' = map simpl ps_in
905 pdef = map debind ps_in' in
906 case simpleCase False (STerm Erased) False CompileTime emptyFC [] atys pdef ei of
907 OK (CaseDef args sc _) ->
908 addDef n (CaseOp ci
909 ty atys ps_in' ps (cd { cases_totcheck = (args, sc) }),
910 acc, tot, metainf) ctxt
911 Error err -> error (show err)
912 _ -> ctxt in
913 uctxt { definitions = ctxt' }
914 where
915 depat acc (Bind n (PVar t) sc)
916 = depat (n : acc) (instantiate (P Bound n t) sc)
917 depat acc x = (acc, x)
918 debind (Right (x, y)) = let (vs, x') = depat [] x
919 (_, y') = depat [] y in
920 (vs, x', y')
921 debind (Left x) = let (vs, x') = depat [] x in
922 (vs, x', Impossible)
923 simpl (Right (x, y)) = Right (x, simplify uctxt [] y)
924 simpl t = t
926addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) ->
927 Context -> Context
928addOperator n ty a op uctxt
929 = let ctxt = definitions uctxt
930 ctxt' = addDef n (Operator ty a op, Public, Unchecked, EmptyMI) ctxt in
931 uctxt { definitions = ctxt' }
933tfst (a, _, _, _) = a
935lookupNames :: Name -> Context -> [Name]
936lookupNames n ctxt
937 = let ns = lookupCtxtName n (definitions ctxt) in
938 map fst ns
940-- | Get the list of pairs of fully-qualified names and their types that match some name
941lookupTyName :: Name -> Context -> [(Name, Type)]
942lookupTyName n ctxt = do
943 (name, def) <- lookupCtxtName n (definitions ctxt)
944 ty <- case tfst def of
945 (Function ty _) -> return ty
946 (TyDecl _ ty) -> return ty
947 (Operator ty _ _) -> return ty
948 (CaseOp _ ty _ _ _ _) -> return ty
949 return (name, ty)
951-- | Get the pair of a fully-qualified name and its type, if there is a unique one matching the name used as a key.
952lookupTyNameExact :: Name -> Context -> Maybe (Name, Type)
953lookupTyNameExact n ctxt = case lookupTyName n ctxt of
954 [x] -> Just x
955 _ -> Nothing
957-- | Get the types that match some name
958lookupTy :: Name -> Context -> [Type]
959lookupTy n ctxt = map snd (lookupTyName n ctxt)
961-- | Get the single type that matches some name precisely
962lookupTyExact :: Name -> Context -> Maybe Type
963lookupTyExact n ctxt = case lookupTy n ctxt of
964 [t] -> Just t
965 _ -> Nothing
967isConName :: Name -> Context -> Bool
968isConName n ctxt = isTConName n ctxt || isDConName n ctxt
970isTConName :: Name -> Context -> Bool
971isTConName n ctxt
972 = case lookupDefExact n ctxt of
973 Just (TyDecl (TCon _ _) _) -> True
974 _ -> False
976-- | Check whether a resolved name is certainly a data constructor
977isDConName :: Name -> Context -> Bool
978isDConName n ctxt
979 = case lookupDefExact n ctxt of
980 Just (TyDecl (DCon _ _ _) _) -> True
981 _ -> False
983-- | Check whether any overloading of a name is a data constructor
984canBeDConName :: Name -> Context -> Bool
985canBeDConName n ctxt
986 = or $ do def <- lookupCtxt n (definitions ctxt)
987 case tfst def of
988 (TyDecl (DCon _ _ _) _) -> return True
989 _ -> return False
991isFnName :: Name -> Context -> Bool
992isFnName n ctxt
993 = case lookupDefExact n ctxt of
994 Just (Function _ _) -> True
995 Just (Operator _ _ _) -> True
996 Just (CaseOp _ _ _ _ _ _) -> True
997 _ -> False
999isTCDict :: Name -> Context -> Bool
1000isTCDict n ctxt
1001 = case lookupDefExact n ctxt of
1002 Just (Function _ _) -> False
1003 Just (Operator _ _ _) -> False
1004 Just (CaseOp ci _ _ _ _ _) -> tc_dictionary ci
1005 _ -> False
1007lookupP :: Name -> Context -> [Term]
1008lookupP = lookupP_all False
1010lookupP_all :: Bool -> Name -> Context -> [Term]
1011lookupP_all all n ctxt
1012 = do def <- lookupCtxt n (definitions ctxt)
1013 p <- case def of
1014 (Function ty tm, a, _, _) -> return (P Ref n ty, a)
1015 (TyDecl nt ty, a, _, _) -> return (P nt n ty, a)
1016 (CaseOp _ ty _ _ _ _, a, _, _) -> return (P Ref n ty, a)
1017 (Operator ty _ _, a, _, _) -> return (P Ref n ty, a)
1018 case snd p of
1019 Hidden -> if all then return (fst p) else []
1020 _ -> return (fst p)
1022lookupDefExact :: Name -> Context -> Maybe Def
1023lookupDefExact n ctxt = tfst <$> lookupCtxtExact n (definitions ctxt)
1025lookupDef :: Name -> Context -> [Def]
1026lookupDef n ctxt = tfst <$> lookupCtxt n (definitions ctxt)
1028lookupNameDef :: Name -> Context -> [(Name, Def)]
1029lookupNameDef n ctxt = mapSnd tfst $ lookupCtxtName n (definitions ctxt)
1030 where mapSnd f [] = []
1031 mapSnd f ((x,y):xys) = (x, f y) : mapSnd f xys
1033lookupDefAcc :: Name -> Bool -> Context ->
1034 [(Def, Accessibility)]
1035lookupDefAcc n mkpublic ctxt
1036 = map mkp $ lookupCtxt n (definitions ctxt)
1037 -- io_bind a special case for REPL prettiness
1038 where mkp (d, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_return"))
1039 then (d, Public) else (d, a)
1041lookupDefAccExact :: Name -> Bool -> Context ->
1042 Maybe (Def, Accessibility)
1043lookupDefAccExact n mkpublic ctxt
1044 = fmap mkp $ lookupCtxtExact n (definitions ctxt)
1045 -- io_bind a special case for REPL prettiness
1046 where mkp (d, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_return"))
1047 then (d, Public) else (d, a)
1049lookupTotal :: Name -> Context -> [Totality]
1050lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)
1051 where mkt (d, a, t, m) = t
1053lookupMetaInformation :: Name -> Context -> [MetaInformation]
1054lookupMetaInformation n ctxt = map mkm $ lookupCtxt n (definitions ctxt)
1055 where mkm (d, a, t, m) = m
1057lookupNameTotal :: Name -> Context -> [(Name, Totality)]
1058lookupNameTotal n = map (\(n, (_, _, t, _)) -> (n, t)) . lookupCtxtName n . definitions
1061lookupVal :: Name -> Context -> [Value]
1062lookupVal n ctxt
1063 = do def <- lookupCtxt n (definitions ctxt)
1064 case tfst def of
1065 (Function _ htm) -> return (veval ctxt [] htm)
1066 (TyDecl nt ty) -> return (VP nt n (veval ctxt [] ty))
1068lookupTyEnv :: Name -> Env -> Maybe (Int, Type)
1069lookupTyEnv n env = li n 0 env where
1070 li n i [] = Nothing
1071 li n i ((x, b): xs)
1072 | n == x = Just (i, binderTy b)
1073 | otherwise = li n (i+1) xs
1075-- | Create a unique name given context and other existing names
1076uniqueNameCtxt :: Context -> Name -> [Name] -> Name
1077uniqueNameCtxt ctxt n hs
1078 | n `elem` hs = uniqueNameCtxt ctxt (nextName n) hs
1079 | [_] <- lookupTy n ctxt = uniqueNameCtxt ctxt (nextName n) hs
1080 | otherwise = n
1082uniqueBindersCtxt :: Context -> [Name] -> TT Name -> TT Name
1083uniqueBindersCtxt ctxt ns (Bind n b sc)
1084 = let n' = uniqueNameCtxt ctxt n ns in
1085 Bind n' (fmap (uniqueBindersCtxt ctxt (n':ns)) b) (uniqueBindersCtxt ctxt ns sc)
1086uniqueBindersCtxt ctxt ns (App f a) = App (uniqueBindersCtxt ctxt ns f) (uniqueBindersCtxt ctxt ns a)
1087uniqueBindersCtxt ctxt ns t = t