git.iko.soy/Idris-dev
on 1b71663 help sign in
Idris-dev/src/Idris/Core/Evaluate.hs
1261 lines 55 kB history raw
1{-|
2Module : Idris.Core.Evaluate
3Description : Evaluate Idris expressions.
5License : BSD3
6Maintainer : The Idris Community.
7-}
9{-# LANGUAGE BangPatterns, DeriveGeneric, FlexibleInstances,
10 MultiParamTypeClasses, PatternGuards #-}
11{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
12{-# OPTIONS_GHC -fwarn-unused-imports #-}
14module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,
15 normaliseAll, normaliseBlocking, toValue, quoteTerm,
16 rt_simplify, simplify, inlineSmall,
17 specialise, unfold, convEq, convEq',
18 Def(..), CaseInfo(..), CaseDefs(..),
19 Accessibility(..), Injectivity, Totality(..), TTDecl, PReason(..), MetaInformation(..),
20 Context, initContext, ctxtAlist, next_tvar,
21 addToCtxt, setAccess, setInjective, setTotal, setRigCount,
22 setMetaInformation, addCtxtDef, addTyDecl,
23 addDatatype, addCasedef, simplifyCasedef, addOperator,
24 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
25 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
26 mapDefCtxt, tcReducible,
27 lookupTotal, lookupTotalExact, lookupInjectiveExact,
28 lookupRigCount, lookupRigCountExact,
29 lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict,
30 isCanonical, isDConName, canBeDConName, isTConName, isConName, isFnName,
31 conGuarded,
32 Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions,
33 visibleDefinitions,
34 isUniverse, linearCheck, linearCheckArg) where
36import Idris.Core.CaseTree
37import Idris.Core.TT
39import Control.Monad.State
40import Data.List
41import Data.Maybe (listToMaybe)
42import GHC.Generics (Generic)
44import qualified Data.Map.Strict as Map
46data EvalState = ES { limited :: [(Name, Int)],
47 nexthole :: Int,
48 blocking :: Bool }
49 deriving Show
51type Eval a = State EvalState a
53data EvalOpt = Spec
54 | Simplify Bool -- ^ whether to expand lets or not
55 | AtREPL
56 | RunTT
57 | Unfold
58 deriving (Show, Eq)
60initEval = ES [] 0 False
62-- VALUES (as HOAS) ---------------------------------------------------------
63-- | A HOAS representation of values
64data Value = VP NameType Name Value
65 | VV Int
66 -- True for Bool indicates safe to reduce
67 | VBind Bool Name (Binder Value) (Value -> Eval Value)
68 -- For frozen let bindings when simplifying
69 | VBLet RigCount Int Name Value Value Value
70 | VApp Value Value
71 | VType UExp
72 | VUType Universe
73 | VErased
74 | VImpossible
75 | VConstant Const
76 | VProj Value Int
77-- | VLazy Env [Value] Term
78 | VTmp Int
80canonical :: Value -> Bool
81canonical (VP (DCon _ _ _) _ _) = True
82canonical (VP (TCon _ _) _ _) = True
83canonical (VApp f a) = canonical f
84canonical (VConstant _) = True
85canonical (VType _) = True
86canonical (VUType _) = True
87canonical VErased = True
88canonical _ = False
91instance Show Value where
92 show x = show $ evalState (quote 100 x) initEval
94instance Show (a -> b) where
95 show x = "<<fn>>"
97-- THE EVALUATOR ------------------------------------------------------------
99-- The environment is assumed to be "locally named" - i.e., not de Bruijn
100-- indexed.
101-- i.e. it's an intermediate environment that we have while type checking or
102-- while building a proof.
104-- | Normalise fully type checked terms (so, assume all names/let bindings resolved)
105normaliseC :: Context -> Env -> TT Name -> TT Name
106normaliseC ctxt env t
107 = evalState (do val <- eval False ctxt [] (map finalEntry env) t []
108 quote 0 val) initEval
110-- | Normalise everything, whether abstract, private or public
111normaliseAll :: Context -> Env -> TT Name -> TT Name
112normaliseAll ctxt env t
113 = evalState (do val <- eval False ctxt [] (map finalEntry env) t [AtREPL]
114 quote 0 val) initEval
116-- | As normaliseAll, but with an explicit list of names *not* to reduce
117normaliseBlocking :: Context -> Env -> [Name] -> TT Name -> TT Name
118normaliseBlocking ctxt env blocked t
119 = evalState (do val <- eval False ctxt (map (\n -> (n, 0)) blocked)
120 (map finalEntry env) t [AtREPL]
121 quote 0 val) initEval
123normalise :: Context -> Env -> TT Name -> TT Name
124normalise = normaliseTrace False
126normaliseTrace :: Bool -> Context -> Env -> TT Name -> TT Name
127normaliseTrace tr ctxt env t
128 = evalState (do val <- eval tr ctxt [] (map finalEntry env) (finalise t) []
129 quote 0 val) initEval
131toValue :: Context -> Env -> TT Name -> Value
132toValue ctxt env t
133 = evalState (eval False ctxt [] (map finalEntry env) t []) initEval
135quoteTerm :: Value -> TT Name
136quoteTerm val = evalState (quote 0 val) initEval
138-- Return a specialised name, and an updated list of reductions available,
139-- so that the caller can tell how much specialisation was achieved.
140specialise :: Context -> Env -> [(Name, Int)] -> TT Name ->
141 (TT Name, [(Name, Int)])
142specialise ctxt env limits t
143 = let (tm, st) =
144 runState (do val <- eval False ctxt []
145 (map finalEntry env) (finalise t)
146 [Spec]
147 quote 0 val) (initEval { limited = limits }) in
148 (tm, limited st)
150-- | Like normalise, but we only reduce functions that are marked as okay to
151-- inline, and lets
152simplify :: Context -> Env -> TT Name -> TT Name
153simplify ctxt env t
154 = evalState (do val <- eval False ctxt [(sUN "lazy", 0),
155 (sUN "force", 0),
156 (sUN "Force", 0),
157 (sUN "assert_smaller", 0),
158 (sUN "assert_total", 0),
159 (sUN "par", 0),
160 (sUN "prim__syntactic_eq", 0),
161 (sUN "fork", 0)]
162 (map finalEntry env) (finalise t)
163 [Simplify True]
164 quote 0 val) initEval
166-- | Like simplify, but we only reduce functions that are marked as okay to
167-- inline, and don't reduce lets
168inlineSmall :: Context -> Env -> TT Name -> TT Name
169inlineSmall ctxt env t
170 = evalState (do val <- eval False ctxt []
171 (map finalEntry env) (finalise t)
172 [Simplify False]
173 quote 0 val) initEval
175-- | Simplify for run-time (i.e. basic inlining)
176rt_simplify :: Context -> Env -> TT Name -> TT Name
177rt_simplify ctxt env t
178 = evalState (do val <- eval False ctxt [(sUN "lazy", 0),
179 (sUN "force", 0),
180 (sUN "Force", 0),
181 (sUN "par", 0),
182 (sUN "prim__syntactic_eq", 0),
183 (sUN "prim_fork", 0)]
184 (map finalEntry env) (finalise t)
185 [RunTT]
186 quote 0 val) initEval
188-- | Unfold the given names in a term, the given number of times in a stack.
189-- Preserves 'let'.
190-- This is primarily to support inlining of the given names, and can also
191-- help with partial evaluation by allowing a rescursive definition to be
192-- unfolded once only.
193-- Specifically used to unfold definitions using interfaces before going to
194-- the totality checker (otherwise mutually recursive definitions in
195-- implementations will not work...)
196unfold :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name
197unfold ctxt env ns t
198 = evalState (do val <- eval False ctxt ns
199 (map finalEntry env) (finalise t)
200 [Unfold]
201 quote 0 val) initEval
204-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))
206finalEntry :: (Name, RigCount, Binder (TT Name)) -> (Name, RigCount, Binder (TT Name))
207finalEntry (n, r, b) = (n, r, fmap finalise b)
209usable :: Bool -- specialising
210 -> Bool -- unfolding only
211 -> Int -- Reduction depth limit (when simplifying/at REPL)
212 -> Name -> [(Name, Int)] -> Eval (Bool, [(Name, Int)])
213-- usable _ _ ns@((MN 0 "STOP", _) : _) = return (False, ns)
214usable False uf depthlimit n [] = return (True, [])
215usable True uf depthlimit n ns
216 = do ES ls num b <- get
217 if b then return (False, ns)
218 else case lookup n ls of
219 Just 0 -> return (False, ns)
220 Just i -> return (True, ns)
221 _ -> return (False, ns)
222usable False uf depthlimit n ns
223 = case lookup n ns of
224 Just 0 -> return (False, ns)
225 Just i -> return $ (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns)
226 _ -> return $ if uf
227 then (False, ns)
228 else (True, (n, depthlimit) : filter (\ (n', _) -> n/=n') ns)
231fnCount :: Int -> Name -> Eval ()
232fnCount inc n
233 = do ES ls num b <- get
234 case lookup n ls of
235 Just i -> do put $ ES ((n, (i - inc)) :
236 filter (\ (n', _) -> n/=n') ls) num b
237 _ -> return ()
239setBlock :: Bool -> Eval ()
240setBlock b = do ES ls num _ <- get
241 put (ES ls num b)
243deduct = fnCount 1
244reinstate = fnCount (-1)
246-- | Evaluate in a context of locally named things (i.e. not de Bruijn indexed,
247-- such as we might have during construction of a proof)
249-- The (Name, Int) pair in the arguments is the maximum depth of unfolding of
250-- a name. The corresponding pair in the state is the maximum number of
251-- unfoldings overall.
253eval :: Bool -> Context -> [(Name, Int)] -> Env -> TT Name ->
254 [EvalOpt] -> Eval Value
255eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
256 spec = Spec `elem` opts
257 simpl = Simplify True `elem` opts || Simplify False `elem` opts
258 simpl_inline = Simplify False `elem` opts
259 runtime = RunTT `elem` opts
260 atRepl = AtREPL `elem` opts
261 unfold = Unfold `elem` opts
263 noFree = all canonical . map snd
265 -- returns 'True' if the function should block
266 -- normal evaluation should return false
267 blockSimplify (CaseInfo inl always dict) n stk
268 | runtime
269 = if always then False
270 else not (inl || dict) || elem n stk
271 | simpl
272 = (not inl || elem n stk)
273 || (n == sUN "prim__syntactic_eq")
274 | otherwise = False
276 getCases cd | simpl = cases_compiletime cd
277 | runtime = cases_runtime cd
278 | otherwise = cases_compiletime cd
280 ev ntimes stk top env (P _ n ty)
281 | Just (Let _ t v) <- lookupBinder n genv = ev ntimes stk top env v
282 ev ntimes_in stk top env (P Ref n ty)
283 = do let limit = if simpl then 100 else 10000
284 (u, ntimes) <- usable spec unfold limit n ntimes_in
285 let red = u && (tcReducible n ctxt || spec || (atRepl && noFree env)
286 || runtime || unfold
287 || sUN "assert_total" `elem` stk)
288 if red then
289 do let val = lookupDefAccExact n (spec || unfold || (atRepl && noFree env) || runtime) ctxt
290 case val of
291 Just (Function _ tm, Public) ->
292 ev ntimes (n:stk) True env tm
293 Just (TyDecl nt ty, _) -> do vty <- ev ntimes stk True env ty
294 return $ VP nt n vty
295 Just (CaseOp ci _ _ _ _ cd, acc)
296 | (acc == Public || acc == Hidden) &&
297-- || sUN "assert_total" `elem` stk) &&
298 null (fst (cases_compiletime cd)) -> -- unoptimised version
299 let (ns, tree) = getCases cd in
300 if blockSimplify ci n stk
301 then liftM (VP Ref n) (ev ntimes stk top env ty)
302 else -- traceWhen runtime (show (n, ns, tree)) $
303 do c <- evCase ntimes n (n:stk) top env ns [] tree
304 case c of
305 (Nothing, _) -> liftM (VP Ref n) (ev ntimes stk top env ty)
306 (Just v, _) -> return v
307 _ -> liftM (VP Ref n) (ev ntimes stk top env ty)
308 else liftM (VP Ref n) (ev ntimes stk top env ty)
309 ev ntimes stk top env (P nt n ty)
310 = liftM (VP nt n) (ev ntimes stk top env ty)
311 ev ntimes stk top env (V i)
312 | i < length env && i >= 0 = return $ snd (env !! i)
313 | otherwise = return $ VV i
314 ev ntimes stk top env (Bind n (Let c t v) sc)
315 | (not (runtime || simpl_inline || unfold)) || occurrences n sc < 2
316 = do v' <- ev ntimes stk top env v --(finalise v)
317 sc' <- ev ntimes stk top ((n, v') : env) sc
318 wknV (-1) sc'
319 | otherwise
320 = do t' <- ev ntimes stk top env t
321 v' <- ev ntimes stk top env v --(finalise v)
322 -- use Tmp as a placeholder, then make it a variable reference
323 -- again when evaluation finished
324 hs <- get
325 let vd = nexthole hs
326 put (hs { nexthole = vd + 1 })
327 sc' <- ev ntimes stk top ((n, VP Bound (sMN vd "vlet") VErased) : env) sc
328 return $ VBLet c vd n t' v' sc'
329 ev ntimes stk top env (Bind n (NLet t v) sc)
330 = do t' <- ev ntimes stk top env (finalise t)
331 v' <- ev ntimes stk top env (finalise v)
332 sc' <- ev ntimes stk top ((n, v') : env) sc
333 return $ VBind True n (Let RigW t' v') (\x -> return sc')
334 ev ntimes stk top env (Bind n b sc)
335 = do b' <- vbind env b
336 let n' = uniqueName n (map fstEnv genv ++ map fst env)
337 return $ VBind True -- (vinstances 0 sc < 2)
338 n' b' (\x -> ev ntimes stk False ((n', x):env) sc)
339 where vbind env t
340 = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
341 -- block reduction immediately under codata (and not forced)
342 ev ntimes stk top env
343 (App _ (App _ (App _ d@(P _ (UN dly) _) l@(P _ (UN lco) _)) t) arg)
344 | dly == txt "Delay" && lco == txt "Infinite" && not (unfold || simpl)
345 = do let (f, _) = unApply arg
346 let ntimes' = case f of
347 P _ fn _ -> (fn, 0) : ntimes
348 _ -> ntimes
349 when spec $ setBlock True
350 d' <- ev ntimes' stk False env d
351 l' <- ev ntimes' stk False env l
352 t' <- ev ntimes' stk False env t
353 arg' <- ev ntimes' stk False env arg
354 when spec $ setBlock False
355 evApply ntimes' stk top env [l',t',arg'] d'
356 -- Treat "assert_total" specially, as long as it's defined!
357 ev ntimes stk top env (App _ (App _ (P _ n@(UN at) _) _) arg)
358 | Just (CaseOp _ _ _ _ _ _, _) <- lookupDefAccExact n (spec || (atRepl && noFree env)|| runtime) ctxt,
359 at == txt "assert_total" && not (simpl || unfold)
360 = ev ntimes (n : stk) top env arg
361 ev ntimes stk top env (App _ f a)
362 = do f' <- ev ntimes stk False env f
363 a' <- ev ntimes stk False env a
364 evApply ntimes stk top env [a'] f'
365 ev ntimes stk top env (Proj t i)
366 = do -- evaluate dictionaries if it means the projection works
367 t' <- ev ntimes stk top env t
368-- tfull' <- reapply ntimes stk top env t' []
369 return (doProj t' (getValArgs t'))
370 where doProj t' (VP (DCon _ _ _) _ _, args)
371 | i >= 0 && i < length args = args!!i
372 doProj t' _ = VProj t' i
374 ev ntimes stk top env (Constant c) = return $ VConstant c
375 ev ntimes stk top env Erased = return VErased
376 ev ntimes stk top env Impossible = return VImpossible
377 ev ntimes stk top env (Inferred tm) = ev ntimes stk top env tm
378 ev ntimes stk top env (TType i) = return $ VType i
379 ev ntimes stk top env (UType u) = return $ VUType u
381 evApply ntimes stk top env args (VApp f a)
382 = evApply ntimes stk top env (a:args) f
383 evApply ntimes stk top env args f
384 = apply ntimes stk top env f args
386 apply ntimes stk top env (VBind True n (Lam _ t) sc) (a:as)
387 = do a' <- sc a
388 app <- apply ntimes stk top env a' as
389 wknV 1 app
390 apply ntimes_in stk top env f@(VP Ref n ty) args
391 = do let limit = if simpl then 100 else 10000
392 (u, ntimes) <- usable spec unfold limit n ntimes_in
393 let red = u && (tcReducible n ctxt || spec || (atRepl && noFree env)
394 || unfold || runtime
395 || sUN "assert_total" `elem` stk)
396 if red then
397 do let val = lookupDefAccExact n (spec || unfold || (atRepl && noFree env) || runtime) ctxt
398 case val of
399 Just (CaseOp ci _ _ _ _ cd, acc)
400 | acc == Public || acc == Hidden ->
401 -- unoptimised version
402 let (ns, tree) = getCases cd in
403 if blockSimplify ci n stk
404 then return $ unload env (VP Ref n ty) args
405 else -- traceWhen runtime (show (n, ns, tree)) $
406 do c <- evCase ntimes n (n:stk) top env ns args tree
407 case c of
408 (Nothing, _) -> return $ unload env (VP Ref n ty) args
409 (Just v, rest) -> evApply ntimes stk top env rest v
410 Just (Operator _ i op, _) ->
411 if (i <= length args)
412 then case op (take i args) of
413 Nothing -> return $ unload env (VP Ref n ty) args
414 Just v -> evApply ntimes stk top env (drop i args) v
415 else return $ unload env (VP Ref n ty) args
416 _ -> case args of
417 [] -> return f
418 _ -> return $ unload env f args
419 else case args of
420 (a : as) -> return $ unload env f (a:as)
421 [] -> return f
422 apply ntimes stk top env f (a:as) = return $ unload env f (a:as)
423 apply ntimes stk top env f [] = return f
425-- specApply stk env f@(VP Ref n ty) args
426-- = case lookupCtxt n statics of
427-- [as] -> if or as
428-- then trace (show (n, map fst (filter (\ (_, s) -> s) (zip args as)))) $
429-- return $ unload env f args
430-- else return $ unload env f args
431-- _ -> return $ unload env f args
432-- specApply stk env f args = return $ unload env f args
434 unload :: [(Name, Value)] -> Value -> [Value] -> Value
435 unload env f [] = f
436 unload env f (a:as) = unload env (VApp f a) as
438 evCase ntimes n stk top env ns args tree
439 | length ns <= length args
440 = do let args' = take (length ns) args
441 let rest = drop (length ns) args
442 when spec $ deduct n
443 t <- evTree ntimes stk top env (zip ns args') tree
444 when spec $ case t of
445 Nothing -> reinstate n -- Blocked, count n again
446 Just _ -> return ()
447-- (zipWith (\n , t) -> (n, t)) ns args') tree
448 return (t, rest)
449 | otherwise = return (Nothing, args)
451 evTree :: [(Name, Int)] -> [Name] -> Bool ->
452 [(Name, Value)] -> [(Name, Value)] -> SC -> Eval (Maybe Value)
453 evTree ntimes stk top env amap (UnmatchedCase str) = return Nothing
454 evTree ntimes stk top env amap (STerm tm)
455 = do let etm = pToVs (map fst amap) tm
456 etm' <- ev ntimes stk (not (conHeaded tm))
457 (amap ++ env) etm
458 return $ Just etm'
459 evTree ntimes stk top env amap (ProjCase t alts)
460 = do t' <- ev ntimes stk top env t
461 doCase ntimes stk top env amap t' alts
462 evTree ntimes stk top env amap (Case _ n alts)
463 = case lookup n amap of
464 Just v -> doCase ntimes stk top env amap v alts
465 _ -> return Nothing
466 evTree ntimes stk top env amap ImpossibleCase = return Nothing
468 doCase ntimes stk top env amap v alts =
469 do c <- chooseAlt env v (getValArgs v) alts amap
470 case c of
471 Just (altmap, sc) -> evTree ntimes stk top env altmap sc
472 _ -> do c' <- chooseAlt' ntimes stk env v (getValArgs v) alts amap
473 case c' of
474 Just (altmap, sc) -> evTree ntimes stk top env altmap sc
475 _ -> return Nothing
477 conHeaded tm@(App _ _ _)
478 | (P (DCon _ _ _) _ _, args) <- unApply tm = True
479 conHeaded t = False
481 chooseAlt' ntimes stk env _ (f, args) alts amap
482 = do f' <- apply ntimes stk True env f args
483 chooseAlt env f' (getValArgs f')
484 alts amap
486 chooseAlt :: [(Name, Value)] -> Value -> (Value, [Value]) -> [CaseAlt] ->
487 [(Name, Value)] ->
488 Eval (Maybe ([(Name, Value)], SC))
489 chooseAlt env _ (VP (DCon i a _) _ _, args) alts amap
490 | Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)
491 | Just v <- findDefault alts = return $ Just (amap, v)
492 chooseAlt env _ (VP (TCon i a) _ _, args) alts amap
493 | Just (ns, sc) <- findTag i alts
494 = return $ Just (updateAmap (zip ns args) amap, sc)
495 | Just v <- findDefault alts = return $ Just (amap, v)
496 chooseAlt env _ (VConstant c, []) alts amap
497 | Just v <- findConst c alts = return $ Just (amap, v)
498 | Just (n', sub, sc) <- findSuc c alts
499 = return $ Just (updateAmap [(n',sub)] amap, sc)
500 | Just v <- findDefault alts = return $ Just (amap, v)
501 chooseAlt env _ (VP _ n _, args) alts amap
502 | Just (ns, sc) <- findFn n alts = return $ Just (updateAmap (zip ns args) amap, sc)
503 chooseAlt env _ (VBind _ _ (Pi _ i s k) t, []) alts amap
504 | Just (ns, sc) <- findFn (sUN "->") alts
505 = do t' <- t (VV 0) -- we know it's not in scope or it's not a pattern
506 return $ Just (updateAmap (zip ns [s, t']) amap, sc)
507 chooseAlt _ _ _ alts amap
508 | Just v <- findDefault alts
509 = if (any fnCase alts)
510 then return $ Just (amap, v)
511 else return Nothing
512 | otherwise = return Nothing
514 fnCase (FnCase _ _ _) = True
515 fnCase _ = False
517 -- Replace old variable names in the map with new matches
518 -- (This is possibly unnecessary since we make unique names and don't
519 -- allow repeated variables...?)
520 updateAmap newm amap
521 = newm ++ filter (\ (x, _) -> not (elem x (map fst newm))) amap
522 findTag i [] = Nothing
523 findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
524 findTag i (_ : xs) = findTag i xs
526 findFn fn [] = Nothing
527 findFn fn (FnCase n ns sc : xs) | fn == n = Just (ns, sc)
528 findFn fn (_ : xs) = findFn fn xs
530 findDefault [] = Nothing
531 findDefault (DefaultCase sc : xs) = Just sc
532 findDefault (_ : xs) = findDefault xs
534 findSuc c [] = Nothing
535 findSuc (BI val) (SucCase n sc : _)
536 | val /= 0 = Just (n, VConstant (BI (val - 1)), sc)
537 findSuc c (_ : xs) = findSuc c xs
539 findConst c [] = Nothing
540 findConst c (ConstCase c' v : xs) | c == c' = Just v
541 findConst (AType (ATInt ITNative)) (ConCase n 1 [] v : xs) = Just v
542 findConst (AType ATFloat) (ConCase n 2 [] v : xs) = Just v
543 findConst (AType (ATInt ITChar)) (ConCase n 3 [] v : xs) = Just v
544 findConst StrType (ConCase n 4 [] v : xs) = Just v
545 findConst (AType (ATInt ITBig)) (ConCase n 6 [] v : xs) = Just v
546 findConst (AType (ATInt (ITFixed ity))) (ConCase n tag [] v : xs)
547 | tag == 7 + fromEnum ity = Just v
548 findConst c (_ : xs) = findConst c xs
550 getValArgs tm = getValArgs' tm []
551 getValArgs' (VApp f a) as = getValArgs' f (a:as)
552 getValArgs' f as = (f, as)
554-- tmpToV i vd (VLetHole j) | vd == j = return $ VV i
555-- tmpToV i vd (VP nt n v) = liftM (VP nt n) (tmpToV i vd v)
556-- tmpToV i vd (VBind n b sc) = do b' <- fmapMB (tmpToV i vd) b
557-- let sc' = \x -> do x' <- sc x
558-- tmpToV (i + 1) vd x'
559-- return (VBind n b' sc')
560-- tmpToV i vd (VApp f a) = liftM2 VApp (tmpToV i vd f) (tmpToV i vd a)
561-- tmpToV i vd x = return x
563instance Eq Value where
564 (==) x y = getTT x == getTT y
565 where getTT v = evalState (quote 0 v) initEval
567class Quote a where
568 quote :: Int -> a -> Eval (TT Name)
570instance Quote Value where
571 quote i (VP nt n v) = liftM (P nt n) (quote i v)
572 quote i (VV x) = return $ V x
573 quote i (VBind _ n b sc) = do sc' <- sc (VTmp i)
574 b' <- quoteB b
575 liftM (Bind n b') (quote (i+1) sc')
576 where quoteB t = fmapMB (quote i) t
577 quote i (VBLet c vd n t v sc)
578 = do sc' <- quote i sc
579 t' <- quote i t
580 v' <- quote i v
581 let sc'' = pToV (sMN vd "vlet") (addBinder sc')
582 return (Bind n (Let c t' v') sc'')
583 quote i (VApp f a) = liftM2 (App MaybeHoles) (quote i f) (quote i a)
584 quote i (VType u) = return (TType u)
585 quote i (VUType u) = return (UType u)
586 quote i VErased = return Erased
587 quote i VImpossible = return Impossible
588 quote i (VProj v j) = do v' <- quote i v
589 return (Proj v' j)
590 quote i (VConstant c) = return $ Constant c
591 quote i (VTmp x) = return $ V (i - x - 1)
593wknV :: Int -> Value -> Eval Value
594wknV i (VV x) | x >= i = return $ VV (x - 1)
595wknV i (VBind red n b sc) = do b' <- fmapMB (wknV i) b
596 return $ VBind red n b' (\x -> do x' <- sc x
597 wknV (i + 1) x')
598wknV i (VApp f a) = liftM2 VApp (wknV i f) (wknV i a)
599wknV i t = return t
601isUniverse :: Term -> Bool
602isUniverse (TType _) = True
603isUniverse (UType _) = True
604isUniverse _ = False
606isUsableUniverse :: Term -> Bool
607isUsableUniverse (UType NullType) = False
608isUsableUniverse x = isUniverse x
610convEq' ctxt hs x y = evalStateT (convEq ctxt hs x y) (0, [])
612convEq :: Context -> [Name] -> TT Name -> TT Name -> StateT UCs TC Bool
613convEq ctxt holes topx topy = ceq [] topx topy where
614 ceq :: [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
615 ceq ps (P xt x _) (P yt y _)
616 | x `elem` holes || y `elem` holes = return True
617 | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True
618 | otherwise = sameDefs ps x y
620 ceq ps (Bind n (PVar _ t) sc) y = ceq ps sc y
621 ceq ps x (Bind n (PVar _ t) sc) = ceq ps x sc
622 ceq ps (Bind n (PVTy t) sc) y = ceq ps sc y
623 ceq ps x (Bind n (PVTy t) sc) = ceq ps x sc
625 ceq ps (V x) (V y) = return (x == y)
626 ceq ps (V x) (P _ y _)
627 | x >= 0 && length ps > x = return (fst (ps!!x) == y)
628 | otherwise = return False
629 ceq ps (P _ x _) (V y)
630 | y >= 0 && length ps > y = return (x == snd (ps!!y))
631 | otherwise = return False
632 ceq ps (Bind n xb xs) (Bind n' yb ys)
633 = liftM2 (&&) (ceqB ps xb yb) (ceq ((n,n'):ps) xs ys)
634 where
635 ceqB ps (Let c v t) (Let c' v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')
636 ceqB ps (Guess v t) (Guess v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')
637 ceqB ps (Pi r i v t) (Pi r' i' v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')
638 ceqB ps b b' = ceq ps (binderTy b) (binderTy b')
640 ceq ps x (Bind n (Lam _ t) (App _ y (V 0)))
641 = ceq ps x (substV (P Bound n t) y)
642 ceq ps (Bind n (Lam _ t) (App _ x (V 0))) y
643 = ceq ps (substV (P Bound n t) x) y
644 ceq ps x (Bind n (Lam _ t) (App _ y (P Bound n' _)))
645 | n == n' = ceq ps x y
646 ceq ps (Bind n (Lam _ t) (App _ x (P Bound n' _))) y
647 | n == n' = ceq ps x y
649 -- Special case for 'case' blocks - size of scope causes complications,
650 -- we only want to check the blocks themselves are valid and identical
651 -- in the current scope. So, just check the bodies, and the additional
652 -- arguments the case blocks are applied to.
653 ceq ps x@(App _ _ _) y@(App _ _ _)
654 | (P _ cx _, xargs) <- unApply x,
655 (P _ cy _, yargs) <- unApply y,
656 caseName cx && caseName cy = sameCase ps cx cy xargs yargs
658 ceq ps (App _ fx ax) (App _ fy ay) = liftM2 (&&) (ceq ps fx fy) (ceq ps ax ay)
659 ceq ps (Constant x) (Constant y) = return (x == y)
660 ceq ps (TType x) (TType y) | x == y = return True
661 ceq ps (TType (UVal 0)) (TType y) = return True
662 ceq ps (TType x) (TType y) = do (v, cs) <- get
663 put (v, ULE x y : cs)
664 return True
665 ceq ps (UType AllTypes) x = return (isUsableUniverse x)
666 ceq ps x (UType AllTypes) = return (isUsableUniverse x)
667 ceq ps (UType u) (UType v) = return (u == v)
668 ceq ps Erased _ = return True
669 ceq ps _ Erased = return True
670 ceq ps x y = return False
672 caseeq ps (Case _ n cs) (Case _ n' cs') = caseeqA ((n,n'):ps) cs cs'
673 where
674 caseeqA ps (ConCase x i as sc : rest) (ConCase x' i' as' sc' : rest')
675 = do q1 <- caseeq (zip as as' ++ ps) sc sc'
676 q2 <- caseeqA ps rest rest'
677 return $ x == x' && i == i' && q1 && q2
678 caseeqA ps (ConstCase x sc : rest) (ConstCase x' sc' : rest')
679 = do q1 <- caseeq ps sc sc'
680 q2 <- caseeqA ps rest rest'
681 return $ x == x' && q1 && q2
682 caseeqA ps (DefaultCase sc : rest) (DefaultCase sc' : rest')
683 = liftM2 (&&) (caseeq ps sc sc') (caseeqA ps rest rest')
684 caseeqA ps [] [] = return True
685 caseeqA ps _ _ = return False
686 caseeq ps (STerm x) (STerm y) = ceq ps x y
687 caseeq ps (UnmatchedCase _) (UnmatchedCase _) = return True
688 caseeq ps _ _ = return False
690 sameDefs ps x y = case (lookupDef x ctxt, lookupDef y ctxt) of
691 ([Function _ xdef], [Function _ ydef])
692 -> ceq ((x,y):ps) xdef ydef
693 ([CaseOp _ _ _ _ _ xd],
694 [CaseOp _ _ _ _ _ yd])
695 -> let (_, xdef) = cases_compiletime xd
696 (_, ydef) = cases_compiletime yd in
697 caseeq ((x,y):ps) xdef ydef
698 _ -> return False
700 sameCase :: [(Name, Name)] -> Name -> Name -> [Term] -> [Term] ->
701 StateT UCs TC Bool
702 sameCase ps x y xargs yargs
703 = case (lookupDef x ctxt, lookupDef y ctxt) of
704 ([Function _ xdef], [Function _ ydef])
705 -> ceq ((x,y):ps) xdef ydef
706 ([CaseOp _ _ _ _ _ xd],
707 [CaseOp _ _ _ _ _ yd])
708 -> let (xin, xdef) = cases_compiletime xd
709 (yin, ydef) = cases_compiletime yd in
710 do liftM2 (&&)
711 (do ok <- zipWithM (ceq ps)
712 (drop (length xin) xargs)
713 (drop (length yin) yargs)
714 return (and ok))
715 (caseeq ((x,y):ps) xdef ydef)
716 _ -> return False
718-- CONTEXTS -----------------------------------------------------------------
720{-| A definition is either a simple function (just an expression with a type),
721 a constant, which could be a data or type constructor, an axiom or as an
722 yet undefined function, or an Operator.
723 An Operator is a function which explains how to reduce.
724 A CaseOp is a function defined by a simple case tree -}
726data Def = Function !Type !Term
727 | TyDecl NameType !Type
728 | Operator Type Int ([Value] -> Maybe Value)
729 | CaseOp CaseInfo
730 !Type
731 ![(Type, Bool)] -- argument types, whether canonical
732 ![Either Term (Term, Term)] -- original definition
733 ![([Name], Term, Term)] -- simplified for totality check definition
734 !CaseDefs
735 deriving Generic
736-- [Name] SC -- Compile time case definition
737-- [Name] SC -- Run time cae definitions
739data CaseDefs = CaseDefs {
740 cases_compiletime :: !([Name], SC),
741 cases_runtime :: !([Name], SC)
742 }
743 deriving Generic
745data CaseInfo = CaseInfo {
746 case_inlinable :: Bool, -- decided by machine
747 case_alwaysinline :: Bool, -- decided by %inline flag
748 tc_dictionary :: Bool
749 }
750 deriving Generic
752{-!
753deriving instance Binary Def
754!-}
755{-!
756deriving instance Binary CaseInfo
757!-}
758{-!
759deriving instance Binary CaseDefs
760!-}
762instance Show Def where
763 show (Function ty tm) = "Function: " ++ show (ty, tm)
764 show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty
765 show (Operator ty _ _) = "Operator: " ++ show ty
766 show (CaseOp (CaseInfo inlc inla inlr) ty atys ps_in ps cd)
767 = let (ns, sc) = cases_compiletime cd
768 (ns', sc') = cases_runtime cd in
769 "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++
770 "COMPILE TIME:\n\n" ++
771 show ns ++ " " ++ show sc ++ "\n\n" ++
772 "RUN TIME:\n\n" ++
773 show ns' ++ " " ++ show sc' ++ "\n\n" ++
774 if inlc then "Inlinable" else "Not inlinable" ++
775 if inla then " Aggressively\n" else "\n"
777-------
779-- Hidden => Programs can't access the name at all
780-- Public => Programs can access the name and use at will
781-- Frozen => Programs can access the name, which doesn't reduce
782-- Private => Programs can't access the name, doesn't reduce internally
784data Accessibility = Hidden | Public | Frozen | Private
785 deriving (Eq, Ord, Generic)
787instance Show Accessibility where
788 show Public = "public export"
789 show Frozen = "export"
790 show Private = "private"
791 show Hidden = "hidden"
793type Injectivity = Bool
795-- | The result of totality checking
796data Totality = Total [Int] -- ^ well-founded arguments
797 | Productive -- ^ productive
798 | Partial PReason
799 | Unchecked
800 | Generated
801 deriving (Eq, Generic)
803-- | Reasons why a function may not be total
804data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name
805 | ExternalIO | BelieveMe | Mutual [Name] | NotProductive
806 deriving (Show, Eq, Generic)
808instance Show Totality where
809 show (Total args)= "Total" -- ++ show args ++ " decreasing arguments"
810 show Productive = "Productive" -- ++ show args ++ " decreasing arguments"
811 show Unchecked = "not yet checked for totality"
812 show (Partial Itself) = "possibly not total as it is not well founded"
813 show (Partial NotCovering) = "not total as there are missing cases"
814 show (Partial NotPositive) = "not strictly positive"
815 show (Partial ExternalIO) = "an external IO primitive"
816 show (Partial NotProductive) = "not productive"
817 show (Partial BelieveMe) = "not total due to use of believe_me in proof"
818 show (Partial (Other ns)) = "possibly not total due to: " ++ showSep ", " (map show ns)
819 show (Partial (Mutual ns)) = "possibly not total due to recursive path " ++
820 showSep " --> " (map show ns)
821 show (Partial (UseUndef n)) = "possibly not total because it uses the undefined name " ++ show n
822 show Generated = "auto-generated"
824{-!
825deriving instance Binary Accessibility
826!-}
828{-!
829deriving instance Binary Totality
830!-}
832{-!
833deriving instance Binary PReason
834!-}
836-- Possible attached meta-information for a definition in context
837data MetaInformation =
838 EmptyMI -- ^ No meta-information
839 | DataMI [Int] -- ^ Meta information for a data declaration with position of parameters
840 deriving (Eq, Show, Generic)
842-- | Contexts used for global definitions and for proof state. They contain
843-- universe constraints and existing definitions.
844-- Also store maximum RigCount of the name (can't bind a name at multiplicity
845-- 1 in a RigW, for example)
846data Context = MkContext {
847 next_tvar :: Int,
848 definitions :: Ctxt TTDecl
849 } deriving (Show, Generic)
851type TTDecl = (Def, RigCount, Injectivity, Accessibility, Totality, MetaInformation)
853-- | The initial empty context
854initContext = MkContext 0 emptyContext
857mapDefCtxt :: (Def -> Def) -> Context -> Context
858mapDefCtxt f (MkContext t !defs) = MkContext t (mapCtxt f' defs)
859 where f' (!d, r, i, a, t, m) = f' (f d, r, i, a, t, m)
861-- | Get the definitions from a context
862ctxtAlist :: Context -> [(Name, Def)]
863ctxtAlist ctxt = map (\(n, (d, r, i, a, t, m)) -> (n, d)) $ toAlist (definitions ctxt)
865veval ctxt env t = evalState (eval False ctxt [] env t []) initEval
867addToCtxt :: Name -> Term -> Type -> Context -> Context
868addToCtxt n tm ty uctxt
869 = let ctxt = definitions uctxt
870 !ctxt' = addDef n (Function ty tm, RigW, False, Public, Unchecked, EmptyMI) ctxt in
871 uctxt { definitions = ctxt' }
873setAccess :: Name -> Accessibility -> Context -> Context
874setAccess n a uctxt
875 = let ctxt = definitions uctxt
876 !ctxt' = updateDef n (\ (d, r, i, _, t, m) -> (d, r, i, a, t, m)) ctxt in
877 uctxt { definitions = ctxt' }
879setInjective :: Name -> Injectivity -> Context -> Context
880setInjective n i uctxt
881 = let ctxt = definitions uctxt
882 !ctxt' = updateDef n (\ (d, r, _, a, t, m) -> (d, r, i, a, t, m)) ctxt in
883 uctxt { definitions = ctxt' }
885setTotal :: Name -> Totality -> Context -> Context
886setTotal n t uctxt
887 = let ctxt = definitions uctxt
888 !ctxt' = updateDef n (\ (d, r, i, a, _, m) -> (d, r, i, a, t, m)) ctxt in
889 uctxt { definitions = ctxt' }
891setRigCount :: Name -> RigCount -> Context -> Context
892setRigCount n rc uctxt
893 = let ctxt = definitions uctxt
894 !ctxt' = updateDef n (\ (d, _, i, a, t, m) -> (d, rc, i, a, t, m)) ctxt in
895 uctxt { definitions = ctxt' }
897setMetaInformation :: Name -> MetaInformation -> Context -> Context
898setMetaInformation n m uctxt
899 = let ctxt = definitions uctxt
900 !ctxt' = updateDef n (\ (d, r, i, a, t, _) -> (d, r, i, a, t, m)) ctxt in
901 uctxt { definitions = ctxt' }
903addCtxtDef :: Name -> Def -> Context -> Context
904addCtxtDef n d c = let ctxt = definitions c
905 !ctxt' = addDef n (d, RigW, False, Public, Unchecked, EmptyMI) $! ctxt in
906 c { definitions = ctxt' }
908addTyDecl :: Name -> NameType -> Type -> Context -> Context
909addTyDecl n nt ty uctxt
910 = let ctxt = definitions uctxt
911 !ctxt' = addDef n (TyDecl nt ty, RigW, False, Public, Unchecked, EmptyMI) ctxt in
912 uctxt { definitions = ctxt' }
914addDatatype :: Datatype Name -> Context -> Context
915addDatatype (Data n tag ty unique cons) uctxt
916 = let ctxt = definitions uctxt
917 ty' = normalise uctxt [] ty
918 !ctxt' = addCons 0 cons (addDef n
919 (TyDecl (TCon tag (arity ty')) ty, RigW, True, Public, Unchecked, EmptyMI) ctxt) in
920 uctxt { definitions = ctxt' }
921 where
922 addCons tag [] ctxt = ctxt
923 addCons tag ((n, ty) : cons) ctxt
924 = let ty' = normalise uctxt [] ty in
925 addCons (tag+1) cons (addDef n
926 (TyDecl (DCon tag (arity ty') unique) ty, RigW, True, Public, Unchecked, EmptyMI) ctxt)
928-- FIXME: Too many arguments! Refactor all these Bools.
929--
930-- Issue #1724 on the issue tracker.
931-- https://github.com/idris-lang/Idris-dev/issues/1724
932addCasedef :: Name -> ErasureInfo -> CaseInfo ->
933 Bool -> SC -> -- default case
934 Bool -> Bool ->
935 [(Type, Bool)] -> -- argument types, whether canonical
936 [Int] -> -- inaccessible arguments
937 [Either Term (Term, Term)] ->
938 [([Name], Term, Term)] -> -- compile time
939 [([Name], Term, Term)] -> -- run time
940 Type -> Context -> TC Context
941addCasedef n ei ci@(CaseInfo inline alwaysInline tcdict)
942 tcase covering reflect asserted argtys inacc
943 ps_in ps_ct ps_rt ty uctxt
944 = do let ctxt = definitions uctxt
945 access = case lookupDefAcc n False uctxt of
946 [(_, acc)] -> acc
947 _ -> Public
948 compileTime <- simpleCase tcase covering reflect CompileTime emptyFC inacc argtys ps_ct ei
949 runtime <- simpleCase tcase covering reflect RunTime emptyFC inacc argtys ps_rt ei
950 ctxt' <- case (compileTime, runtime) of
951 ( CaseDef args_ct sc_ct _,
952 CaseDef args_rt sc_rt _) ->
953 let inl = alwaysInline -- tcdict
954 inlc = (inl || small n args_rt sc_rt) && (not asserted)
955 cdef = CaseDefs (args_ct, sc_ct)
956 (args_rt, sc_rt)
957 op = (CaseOp (ci { case_inlinable = inlc })
958 ty argtys ps_in ps_ct cdef,
959 RigW, False, access, Unchecked, EmptyMI)
960 in return $ addDef n op ctxt
961-- other -> tfail (Msg $ "Error adding case def: " ++ show other)
962 return uctxt { definitions = ctxt' }
964-- simplify a definition by unfolding interface methods
965-- We need this for totality checking, because functions which use interfaces
966-- in an implementation definition themselves need to have the implementation
967-- inlined or it'll be treated as a higher order function that will potentially
968-- loop.
969simplifyCasedef :: Name -> [Name] -> [[Name]] -> ErasureInfo -> Context -> TC Context
970simplifyCasedef n ufnames umethss ei uctxt
971 = do let ctxt = definitions uctxt
972 ctxt' <- case lookupCtxt n ctxt of
973 [(CaseOp ci ty atys [] ps _, rc, inj, acc, tot, metainf)] ->
974 return ctxt -- nothing to simplify (or already done...)
975 [(CaseOp ci ty atys ps_in ps cd, rc, inj, acc, tot, metainf)] ->
976 do let ps_in' = map simpl ps_in
977 pdef = map debind ps_in'
978 CaseDef args sc _ <- simpleCase False (STerm Erased) False CompileTime emptyFC [] atys pdef ei
979 return $ addDef n (CaseOp ci
980 ty atys ps_in' ps (cd { cases_compiletime = (args, sc) }),
981 rc, inj, acc, tot, metainf) ctxt
983 _ -> return ctxt
984 return uctxt { definitions = ctxt' }
985 where
986 depat acc (Bind n (PVar _ t) sc)
987 = depat (n : acc) (instantiate (P Bound n t) sc)
988 depat acc x = (acc, x)
989 debind (Right (x, y)) = let (vs, x') = depat [] x
990 (_, y') = depat [] y in
991 (vs, x', y')
992 debind (Left x) = let (vs, x') = depat [] x in
993 (vs, x', Impossible)
994 simpl (Right (x, y))
995 = if null ufnames then Right (x, y)
996 else Right (x, unfold uctxt [] (map (\n -> (n, 1)) (uns y)) y)
997 simpl t = t
999 -- Unfold the given name, interface methdods, and any function which uses it as
1000 -- an argument directly. This is specifically for finding applications of
1001 -- interface dictionaries and inlining them both for totality checking and for
1002 -- a small performance gain.
1003 uns tm = getNamesToUnfold ufnames umethss tm
1005 getNamesToUnfold :: [Name] -> [[Name]] -> Term -> [Name]
1006 getNamesToUnfold inames ms tm = nub $ inames ++ getNames Nothing tm ++ concat ms
1007 where
1008 getNames under fn@(App _ _ _)
1009 | (f, args) <- unApply fn
1010 = let under' = case f of
1011 P _ fn _ -> Just fn
1012 _ -> Nothing
1013 in
1014 getNames under f ++ concatMap (getNames under') args
1015 getNames (Just under) (P _ ref _)
1016 = if ref `elem` inames then [under] else []
1017 getNames under (Bind n (Let c t v) sc)
1018 = getNames Nothing t ++
1019 getNames Nothing v ++
1020 getNames Nothing sc
1021 getNames under (Bind n b sc) = getNames Nothing (binderTy b) ++
1022 getNames Nothing sc
1023 getNames _ _ = []
1025addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) ->
1026 Context -> Context
1027addOperator n ty a op uctxt
1028 = let ctxt = definitions uctxt
1029 ctxt' = addDef n (Operator ty a op, RigW, False, Public, Unchecked, EmptyMI) ctxt in
1030 uctxt { definitions = ctxt' }
1032tfst (a, _, _, _, _, _) = a
1034lookupNames :: Name -> Context -> [Name]
1035lookupNames n ctxt
1036 = let ns = lookupCtxtName n (definitions ctxt) in
1037 map fst ns
1039-- | Get the list of pairs of fully-qualified names and their types that match some name
1040lookupTyName :: Name -> Context -> [(Name, Type)]
1041lookupTyName n ctxt = do
1042 (name, def) <- lookupCtxtName n (definitions ctxt)
1043 ty <- case tfst def of
1044 (Function ty _) -> return ty
1045 (TyDecl _ ty) -> return ty
1046 (Operator ty _ _) -> return ty
1047 (CaseOp _ ty _ _ _ _) -> return ty
1048 return (name, ty)
1050-- | Get the pair of a fully-qualified name and its type, if there is a unique one matching the name used as a key.
1051lookupTyNameExact :: Name -> Context -> Maybe (Name, Type)
1052lookupTyNameExact n ctxt = listToMaybe [ (nm, v) | (nm, v) <- lookupTyName n ctxt, nm == n ]
1054-- | Get the types that match some name
1055lookupTy :: Name -> Context -> [Type]
1056lookupTy n ctxt = map snd (lookupTyName n ctxt)
1058-- | Get the single type that matches some name precisely
1059lookupTyExact :: Name -> Context -> Maybe Type
1060lookupTyExact n ctxt = fmap snd (lookupTyNameExact n ctxt)
1062-- | Return true if the given type is a concrete type familyor primitive
1063-- False it it's a function to compute a type or a variable
1064isCanonical :: Type -> Context -> Bool
1065isCanonical t ctxt
1066 = case unApply t of
1067 (P _ n _, _) -> isConName n ctxt
1068 (Constant _, _) -> True
1069 _ -> False
1071isConName :: Name -> Context -> Bool
1072isConName n ctxt = isTConName n ctxt || isDConName n ctxt
1074isTConName :: Name -> Context -> Bool
1075isTConName n ctxt
1076 = case lookupDefExact n ctxt of
1077 Just (TyDecl (TCon _ _) _) -> True
1078 _ -> False
1080-- | Check whether a resolved name is certainly a data constructor
1081isDConName :: Name -> Context -> Bool
1082isDConName n ctxt
1083 = case lookupDefExact n ctxt of
1084 Just (TyDecl (DCon _ _ _) _) -> True
1085 _ -> False
1087-- | Check whether any overloading of a name is a data constructor
1088canBeDConName :: Name -> Context -> Bool
1089canBeDConName n ctxt
1090 = or $ do def <- lookupCtxt n (definitions ctxt)
1091 case tfst def of
1092 (TyDecl (DCon _ _ _) _) -> return True
1093 _ -> return False
1095isFnName :: Name -> Context -> Bool
1096isFnName n ctxt
1097 = case lookupDefExact n ctxt of
1098 Just (Function _ _) -> True
1099 Just (Operator _ _ _) -> True
1100 Just (CaseOp _ _ _ _ _ _) -> True
1101 _ -> False
1103isTCDict :: Name -> Context -> Bool
1104isTCDict n ctxt
1105 = case lookupDefExact n ctxt of
1106 Just (Function _ _) -> False
1107 Just (Operator _ _ _) -> False
1108 Just (CaseOp ci _ _ _ _ _) -> tc_dictionary ci
1109 _ -> False
1111-- Is the name guarded by constructors in the term?
1112-- We assume the term is normalised, so no looking under 'let' for example.
1113conGuarded :: Context -> Name -> Term -> Bool
1114conGuarded ctxt n tm = guarded n tm
1115 where
1116 guarded n (P _ n' _) = n == n'
1117 guarded n ap@(App _ _ _)
1118 | (P _ f _, as) <- unApply ap,
1119 isConName f ctxt = any (guarded n) as
1120 guarded _ _ = False
1122visibleDefinitions :: Context -> Ctxt TTDecl
1123visibleDefinitions ctxt =
1124 Map.filter (\m -> length m > 0) . Map.map onlyVisible . definitions $ ctxt
1125 where
1126 onlyVisible = Map.filter visible
1127 visible (_def, _rigCount, _injectivity, accessibility, _totality, _metaInformation) =
1128 accessibility `notElem` [Hidden, Private]
1130lookupP :: Name -> Context -> [Term]
1131lookupP = lookupP_all False False
1133lookupP_all :: Bool -> Bool -> Name -> Context -> [Term]
1134lookupP_all all exact n ctxt
1135 = do (n', def) <- names
1136 p <- case def of
1137 (Function ty tm, _, inj, a, _, _) -> return (P Ref n' ty, a)
1138 (TyDecl nt ty, _, _, a, _, _) -> return (P nt n' ty, a)
1139 (CaseOp _ ty _ _ _ _, _, inj, a, _, _) -> return (P Ref n' ty, a)
1140 (Operator ty _ _, _, inj, a, _, _) -> return (P Ref n' ty, a)
1141 case snd p of
1142 Hidden -> if all then return (fst p) else []
1143 Private -> if all then return (fst p) else []
1144 _ -> return (fst p)
1145 where
1146 names = let ns = lookupCtxtName n (definitions ctxt) in
1147 if exact
1148 then filter (\ (n', d) -> n' == n) ns
1149 else ns
1151lookupDefExact :: Name -> Context -> Maybe Def
1152lookupDefExact n ctxt = tfst <$> lookupCtxtExact n (definitions ctxt)
1154lookupDef :: Name -> Context -> [Def]
1155lookupDef n ctxt = tfst <$> lookupCtxt n (definitions ctxt)
1157lookupNameDef :: Name -> Context -> [(Name, Def)]
1158lookupNameDef n ctxt = mapSnd tfst $ lookupCtxtName n (definitions ctxt)
1159 where mapSnd f [] = []
1160 mapSnd f ((x,y):xys) = (x, f y) : mapSnd f xys
1162lookupDefAcc :: Name -> Bool -> Context ->
1163 [(Def, Accessibility)]
1164lookupDefAcc n mkpublic ctxt
1165 = map mkp $ lookupCtxt n (definitions ctxt)
1166 -- io_bind a special case for REPL prettiness
1167 where mkp (d, _, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_pure"))
1168 then (d, Public) else (d, a)
1170lookupDefAccExact :: Name -> Bool -> Context ->
1171 Maybe (Def, Accessibility)
1172lookupDefAccExact n mkpublic ctxt
1173 = fmap mkp $ lookupCtxtExact n (definitions ctxt)
1174 -- io_bind a special case for REPL prettiness
1175 where mkp (d, _, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_pure"))
1176 then (d, Public) else (d, a)
1178lookupTotal :: Name -> Context -> [Totality]
1179lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)
1180 where mkt (d, _, inj, a, t, m) = t
1182lookupTotalExact :: Name -> Context -> Maybe Totality
1183lookupTotalExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)
1184 where mkt (d, _, inj, a, t, m) = t
1186lookupRigCount :: Name -> Context -> [Totality]
1187lookupRigCount n ctxt = map mkt $ lookupCtxt n (definitions ctxt)
1188 where mkt (d, _, inj, a, t, m) = t
1190lookupRigCountExact :: Name -> Context -> Maybe RigCount
1191lookupRigCountExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)
1192 where mkt (d, rc, inj, a, t, m) = rc
1194lookupInjectiveExact :: Name -> Context -> Maybe Injectivity
1195lookupInjectiveExact n ctxt = fmap mkt $ lookupCtxtExact n (definitions ctxt)
1196 where mkt (d, _, inj, a, t, m) = inj
1198-- Assume type is at least in whnfArgs form
1199linearCheck :: Context -> Type -> TC ()
1200linearCheck ctxt t = checkArgs t
1201 where
1202 checkArgs (Bind n (Pi RigW _ ty _) sc)
1203 = do linearCheckArg ctxt ty
1204 checkArgs (substV (P Bound n Erased) sc)
1205 checkArgs (Bind n (Pi _ _ _ _) sc)
1206 = checkArgs (substV (P Bound n Erased) sc)
1207 checkArgs _ = return ()
1209linearCheckArg :: Context -> Type -> TC ()
1210linearCheckArg ctxt ty = mapM_ checkNameOK (allTTNames ty)
1211 where
1212 checkNameOK f
1213 = case lookupRigCountExact f ctxt of
1214 Just Rig1 ->
1215 tfail $ Msg $ show f ++ " can only appear in a linear binding"
1216 _ -> return ()
1218-- Check if a name is reducible in the type checker. Partial definitions
1219-- are not reducible (so treated as a constant)
1220tcReducible :: Name -> Context -> Bool
1221tcReducible n ctxt = case lookupTotalExact n ctxt of
1222 Nothing -> True
1223 Just (Partial _) -> False
1224 _ -> True
1226lookupMetaInformation :: Name -> Context -> [MetaInformation]
1227lookupMetaInformation n ctxt = map mkm $ lookupCtxt n (definitions ctxt)
1228 where mkm (d, _, inj, a, t, m) = m
1230lookupNameTotal :: Name -> Context -> [(Name, Totality)]
1231lookupNameTotal n = map (\(n, (_, _, _, _, t, _)) -> (n, t)) . lookupCtxtName n . definitions
1234lookupVal :: Name -> Context -> [Value]
1235lookupVal n ctxt
1236 = do def <- lookupCtxt n (definitions ctxt)
1237 case tfst def of
1238 (Function _ htm) -> return (veval ctxt [] htm)
1239 (TyDecl nt ty) -> return (VP nt n (veval ctxt [] ty))
1240 _ -> []
1242lookupTyEnv :: Name -> Env -> Maybe (Int, RigCount, Type)
1243lookupTyEnv n env = li n 0 env where
1244 li n i [] = Nothing
1245 li n i ((x, r, b): xs)
1246 | n == x = Just (i, r, binderTy b)
1247 | otherwise = li n (i+1) xs
1249-- | Create a unique name given context and other existing names
1250uniqueNameCtxt :: Context -> Name -> [Name] -> Name
1251uniqueNameCtxt ctxt n hs
1252 | n `elem` hs = uniqueNameCtxt ctxt (nextName n) hs
1253 | [_] <- lookupTy n ctxt = uniqueNameCtxt ctxt (nextName n) hs
1254 | otherwise = n
1256uniqueBindersCtxt :: Context -> [Name] -> TT Name -> TT Name
1257uniqueBindersCtxt ctxt ns (Bind n b sc)
1258 = let n' = uniqueNameCtxt ctxt n ns in
1259 Bind n' (fmap (uniqueBindersCtxt ctxt (n':ns)) b) (uniqueBindersCtxt ctxt ns sc)
1260uniqueBindersCtxt ctxt ns (App s f a) = App s (uniqueBindersCtxt ctxt ns f) (uniqueBindersCtxt ctxt ns a)
1261uniqueBindersCtxt ctxt ns t = t