git.iko.soy/Idris-dev
on d66da21 help sign in
Idris-dev/src/Core/Evaluate.hs
905 lines 39 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,
2 PatternGuards #-}
4module Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
5 rt_simplify, simplify, specialise, hnf, convEq, convEq',
6 Def(..), CaseInfo(..), CaseDefs(..),
7 Accessibility(..), Totality(..), PReason(..),
8 Context, initContext, ctxtAlist, uconstraints, next_tvar,
9 addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl,
10 addDatatype, addCasedef, simplifyCasedef, addOperator,
11 lookupNames, lookupTy, lookupP, lookupDef, lookupDefAcc, lookupVal,
12 lookupTotal, lookupNameTotal, lookupTyEnv, isDConName, isTConName, isConName, isFnName,
13 Value(..), Quote(..), initEval) where
15import Debug.Trace
16import Control.Monad.State
17import qualified Data.Binary as B
18import Data.Binary hiding (get, put)
20import Core.TT
21import Core.CaseTree
23data EvalState = ES { limited :: [(Name, Int)],
24 nexthole :: Int }
25 deriving Show
27type Eval a = State EvalState a
29data EvalOpt = Spec
30 | HNF
31 | Simplify
32 | AtREPL
33 | RunTT
34 deriving (Show, Eq)
36initEval = ES [] 0
38-- VALUES (as HOAS) ---------------------------------------------------------
39-- | A HOAS representation of values
40data Value = VP NameType Name Value
41 | VV Int
42 -- True for Bool indicates safe to reduce
43 | VBind Bool Name (Binder Value) (Value -> Eval Value)
44 -- For frozen let bindings when simplifying
45 | VBLet Int Name Value Value Value
46 | VApp Value Value
47 | VType UExp
48 | VErased
49 | VImpossible
50 | VConstant Const
51 | VProj Value Int
52-- | VLazy Env [Value] Term
53 | VTmp Int
55instance Show Value where
56 show x = show $ evalState (quote 100 x) initEval
58instance Show (a -> b) where
59 show x = "<<fn>>"
61-- THE EVALUATOR ------------------------------------------------------------
63-- The environment is assumed to be "locally named" - i.e., not de Bruijn
64-- indexed.
65-- i.e. it's an intermediate environment that we have while type checking or
66-- while building a proof.
68-- | Normalise fully type checked terms (so, assume all names/let bindings resolved)
69normaliseC :: Context -> Env -> TT Name -> TT Name
70normaliseC ctxt env t
71 = evalState (do val <- eval False ctxt [] env t []
72 quote 0 val) initEval
74normaliseAll :: Context -> Env -> TT Name -> TT Name
75normaliseAll ctxt env t
76 = evalState (do val <- eval False ctxt [] env t [AtREPL]
77 quote 0 val) initEval
79normalise :: Context -> Env -> TT Name -> TT Name
80normalise = normaliseTrace False
82normaliseTrace :: Bool -> Context -> Env -> TT Name -> TT Name
83normaliseTrace tr ctxt env t
84 = evalState (do val <- eval tr ctxt [] (map finalEntry env) (finalise t) []
85 quote 0 val) initEval
87specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name
88specialise ctxt env limits t
89 = evalState (do val <- eval False ctxt []
90 (map finalEntry env) (finalise t)
91 [Spec]
92 quote 0 val) (initEval { limited = limits })
94-- | Like normalise, but we only reduce functions that are marked as okay to
95-- inline (and probably shouldn't reduce lets?)
96-- 20130908: now only used to reduce for totality checking. Inlining should
97-- be done elsewhere.
99simplify :: Context -> Env -> TT Name -> TT Name
100simplify ctxt env t
101 = evalState (do val <- eval False ctxt [(UN "lazy", 0),
102 (UN "assert_smaller", 0),
103 (UN "par", 0),
104 (UN "prim__syntactic_eq", 0),
105 (UN "fork", 0)]
106 (map finalEntry env) (finalise t)
107 [Simplify]
108 quote 0 val) initEval
110-- | Simplify for run-time (i.e. basic inlining)
111rt_simplify :: Context -> Env -> TT Name -> TT Name
112rt_simplify ctxt env t
113 = evalState (do val <- eval False ctxt [(UN "lazy", 0),
114 (UN "assert_smaller", 0),
115 (UN "par", 0),
116 (UN "prim__syntactic_eq", 0),
117 (UN "prim_fork", 0)]
118 (map finalEntry env) (finalise t)
119 [RunTT]
120 quote 0 val) initEval
122-- | Reduce a term to head normal form
123hnf :: Context -> Env -> TT Name -> TT Name
124hnf ctxt env t
125 = evalState (do val <- eval False ctxt []
126 (map finalEntry env)
127 (finalise t) [HNF]
128 quote 0 val) initEval
131-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))
133finalEntry :: (Name, Binder (TT Name)) -> (Name, Binder (TT Name))
134finalEntry (n, b) = (n, fmap finalise b)
136bindEnv :: EnvTT n -> TT n -> TT n
137bindEnv [] tm = tm
138bindEnv ((n, Let t v):bs) tm = Bind n (NLet t v) (bindEnv bs tm)
139bindEnv ((n, b):bs) tm = Bind n b (bindEnv bs tm)
141unbindEnv :: EnvTT n -> TT n -> TT n
142unbindEnv [] tm = tm
143unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc
145usable :: Bool -- specialising
146 -> Name -> [(Name, Int)] -> Eval (Bool, [(Name, Int)])
147-- usable _ _ ns@((MN 0 "STOP", _) : _) = return (False, ns)
148usable False n [] = return (True, [])
149usable True n ns
150 = do ES ls num <- get
151 case lookup n ls of
152 Just 0 -> return (False, ns)
153 Just i -> return (True, ns)
154 _ -> return (False, ns)
155usable False n ns
156 = case lookup n ns of
157 Just 0 -> return (False, ns)
158 Just i -> return $ (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns)
159 _ -> return $ (True, (n, 100) : filter (\ (n', _) -> n/=n') ns)
162deduct :: Name -> Eval ()
163deduct n = do ES ls num <- get
164 case lookup n ls of
165 Just i -> do put $ ES ((n, (i-1)) :
166 filter (\ (n', _) -> n/=n') ls) num
167 _ -> return ()
169-- | Evaluate in a context of locally named things (i.e. not de Bruijn indexed,
170-- such as we might have during construction of a proof)
172-- The (Name, Int) pair in the arguments is the maximum depth of unfolding of
173-- a name. The corresponding pair in the state is the maximum number of
174-- unfoldings overall.
176eval :: Bool -> Context -> [(Name, Int)] -> Env -> TT Name ->
177 [EvalOpt] -> Eval Value
178eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
179 spec = Spec `elem` opts
180 simpl = Simplify `elem` opts
181 runtime = RunTT `elem` opts
182 atRepl = AtREPL `elem` opts
183 hnf = HNF `elem` opts
185 -- returns 'True' if the function should block
186 -- normal evaluation should return false
187 blockSimplify (CaseInfo inl dict) n stk
188 | RunTT `elem` opts
189 = not (inl || dict) || elem n stk
190 | Simplify `elem` opts
191 = (not (inl || dict) || elem n stk)
192 || (n == UN "prim__syntactic_eq")
193 | otherwise = False
195 getCases cd | simpl = cases_totcheck cd
196 | runtime = cases_runtime cd
197 | otherwise = cases_compiletime cd
199 ev ntimes stk top env (P _ n ty)
200 | Just (Let t v) <- lookup n genv = ev ntimes stk top env v
201 ev ntimes_in stk top env (P Ref n ty)
202 | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)
203 | otherwise
204 = do (u, ntimes) <- usable spec n ntimes_in
205 if u then
206 do let val = lookupDefAcc n (spec || atRepl) ctxt
207 case val of
208 [(Function _ tm, Public)] ->
209 ev ntimes (n:stk) True env tm
210 [(Function _ tm, Hidden)] ->
211 ev ntimes (n:stk) True env tm
212 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty
213 return $ VP nt n vty
214 [(CaseOp ci _ _ _ cd, acc)]
215 | (acc /= Frozen) &&
216 null (fst (cases_totcheck cd)) -> -- unoptimised version
217 let (ns, tree) = getCases cd in
218 if blockSimplify ci n stk
219 then liftM (VP Ref n) (ev ntimes stk top env ty)
220 else -- traceWhen runtime (show (n, ns, tree)) $
221 do c <- evCase ntimes n (n:stk) top env ns [] tree
222 case c of
223 (Nothing, _) -> liftM (VP Ref n) (ev ntimes stk top env ty)
224 (Just v, _) -> return v
225 _ -> liftM (VP Ref n) (ev ntimes stk top env ty)
226 else liftM (VP Ref n) (ev ntimes stk top env ty)
227 ev ntimes stk top env (P nt n ty)
228 = liftM (VP nt n) (ev ntimes stk top env ty)
229 ev ntimes stk top env (V i)
230 | i < length env && i >= 0 = return $ env !! i
231 | otherwise = return $ VV i
232 ev ntimes stk top env (Bind n (Let t v) sc)
233 = do v' <- ev ntimes stk top env v --(finalise v)
234 sc' <- ev ntimes stk top (v' : env) sc
235 wknV (-1) sc'
236-- | otherwise
237-- = do t' <- ev ntimes stk top env t
238-- v' <- ev ntimes stk top env v --(finalise v)
239-- -- use Tmp as a placeholder, then make it a variable reference
240-- -- again when evaluation finished
241-- hs <- get
242-- let vd = nexthole hs
243-- put (hs { nexthole = vd + 1 })
244-- sc' <- ev ntimes stk top (VP Bound (MN vd "vlet") VErased : env) sc
245-- return $ VBLet vd n t' v' sc'
246 ev ntimes stk top env (Bind n (NLet t v) sc)
247 = do t' <- ev ntimes stk top env (finalise t)
248 v' <- ev ntimes stk top env (finalise v)
249 sc' <- ev ntimes stk top (v' : env) sc
250 return $ VBind True n (Let t' v') (\x -> return sc')
251 ev ntimes stk top env (Bind n b sc)
252 = do b' <- vbind env b
253 return $ VBind True -- (vinstances 0 sc < 2)
254 n b' (\x -> ev ntimes stk False (x:env) sc)
255 where vbind env t
256-- | simpl
257-- = fmapMB (\tm -> ev ((MN 0 "STOP", 0) : ntimes)
258-- stk top env (finalise tm)) t
259-- | otherwise
260 = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
261 ev ntimes stk top env (App f a)
262 = do f' <- ev ntimes stk False env f
263 a' <- ev ntimes stk False env a
264 evApply ntimes stk top env [a'] f'
265 ev ntimes stk top env (Proj t i)
266 = do -- evaluate dictionaries if it means the projection works
267 t' <- ev ntimes stk top env t
268-- tfull' <- reapply ntimes stk top env t' []
269 return (doProj t' (getValArgs t'))
270 where doProj t' (VP (DCon _ _) _ _, args) | i < length args = args!!i
271 doProj t' _ = VProj t' i
273 ev ntimes stk top env (Constant c) = return $ VConstant c
274 ev ntimes stk top env Erased = return VErased
275 ev ntimes stk top env Impossible = return VImpossible
276 ev ntimes stk top env (TType i) = return $ VType i
278 evApply ntimes stk top env args (VApp f a)
279 = evApply ntimes stk top env (a:args) f
280 evApply ntimes stk top env args f
281 = apply ntimes stk top env f args
283 reapply ntimes stk top env f@(VP Ref n ty) args
284 = let val = lookupDefAcc n (spec || atRepl) ctxt in
285 case val of
286 [(CaseOp ci _ _ _ cd, acc)] ->
287 let (ns, tree) = getCases cd in
288 do c <- evCase ntimes n (n:stk) top env ns args tree
289 case c of
290 (Nothing, _) -> return $ unload env (VP Ref n ty) args
291 (Just v, rest) -> evApply ntimes stk top env rest v
292 _ -> case args of
293 (a : as) -> return $ unload env f (a : as)
294 [] -> return f
295 reapply ntimes stk top env (VApp f a) args
296 = reapply ntimes stk top env f (a : args)
297 reapply ntimes stk top env v args = return v
299 apply ntimes stk top env (VBind True n (Lam t) sc) (a:as)
300 = do a' <- sc a
301 app <- apply ntimes stk top env a' as
302 wknV (-1) app
303 apply ntimes_in stk top env f@(VP Ref n ty) args
304 | not top && hnf = case args of
305 [] -> return f
306 _ -> return $ unload env f args
307 | otherwise
308 = do (u, ntimes) <- usable spec n ntimes_in
309 if u then
310 do let val = lookupDefAcc n (spec || atRepl) ctxt
311 case val of
312 [(CaseOp ci _ _ _ cd, acc)]
313 | acc /= Frozen -> -- unoptimised version
314 let (ns, tree) = getCases cd in
315 if blockSimplify ci n stk
316 then return $ unload env (VP Ref n ty) args
317 else -- traceWhen runtime (show (n, ns, tree)) $
318 do c <- evCase ntimes n (n:stk) top env ns args tree
319 case c of
320 (Nothing, _) -> return $ unload env (VP Ref n ty) args
321 (Just v, rest) -> evApply ntimes stk top env rest v
322 [(Operator _ i op, _)] ->
323 if (i <= length args)
324 then case op (take i args) of
325 Nothing -> return $ unload env (VP Ref n ty) args
326 Just v -> evApply ntimes stk top env (drop i args) v
327 else return $ unload env (VP Ref n ty) args
328 _ -> case args of
329 [] -> return f
330 _ -> return $ unload env f args
331 else case args of
332 (a : as) -> return $ unload env f (a:as)
333 [] -> return f
334 apply ntimes stk top env f (a:as) = return $ unload env f (a:as)
335 apply ntimes stk top env f [] = return f
337-- specApply stk env f@(VP Ref n ty) args
338-- = case lookupCtxt n statics of
339-- [as] -> if or as
340-- then trace (show (n, map fst (filter (\ (_, s) -> s) (zip args as)))) $
341-- return $ unload env f args
342-- else return $ unload env f args
343-- _ -> return $ unload env f args
344-- specApply stk env f args = return $ unload env f args
346 unload :: [Value] -> Value -> [Value] -> Value
347 unload env f [] = f
348 unload env f (a:as) = unload env (VApp f a) as
350 evCase ntimes n stk top env ns args tree
351 | length ns <= length args
352 = do let args' = take (length ns) args
353 let rest = drop (length ns) args
354 when spec $ deduct n -- successful, so deduct usages
355 t <- evTree ntimes stk top env (zip ns args') tree
356-- (zipWith (\n , t) -> (n, t)) ns args') tree
357 return (t, rest)
358 | otherwise = return (Nothing, args)
360 evTree :: [(Name, Int)] -> [Name] -> Bool ->
361 [Value] -> [(Name, Value)] -> SC -> Eval (Maybe Value)
362 evTree ntimes stk top env amap (UnmatchedCase str) = return Nothing
363 evTree ntimes stk top env amap (STerm tm)
364 = do let etm = pToVs (map fst amap) tm
365 etm' <- ev ntimes stk (not (conHeaded tm))
366 (map snd amap ++ env) etm
367 return $ Just etm'
368 evTree ntimes stk top env amap (ProjCase t alts)
369 = do t' <- ev ntimes stk top env t
370 doCase ntimes stk top env amap t' alts
371 evTree ntimes stk top env amap (Case n alts)
372 = case lookup n amap of
373 Just v -> doCase ntimes stk top env amap v alts
374 _ -> return Nothing
375 evTree ntimes stk top env amap ImpossibleCase = return Nothing
377 doCase ntimes stk top env amap v alts =
378 do c <- chooseAlt env v (getValArgs v) alts amap
379 case c of
380 Just (altmap, sc) -> evTree ntimes stk top env altmap sc
381 _ -> do c' <- chooseAlt' ntimes stk env v (getValArgs v) alts amap
382 case c' of
383 Just (altmap, sc) -> evTree ntimes stk top env altmap sc
384 _ -> return Nothing
386 conHeaded tm@(App _ _)
387 | (P (DCon _ _) _ _, args) <- unApply tm = True
388 conHeaded t = False
390 chooseAlt' ntimes stk env _ (f, args) alts amap
391 = do f' <- apply ntimes stk True env f args
392 chooseAlt env f' (getValArgs f')
393 alts amap
395 chooseAlt :: [Value] -> Value -> (Value, [Value]) -> [CaseAlt] ->
396 [(Name, Value)] ->
397 Eval (Maybe ([(Name, Value)], SC))
398 chooseAlt env _ (VP (DCon i a) _ _, args) alts amap
399 | Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)
400 | Just v <- findDefault alts = return $ Just (amap, v)
401 chooseAlt env _ (VP (TCon i a) _ _, args) alts amap
402 | Just (ns, sc) <- findTag i alts
403 = return $ Just (updateAmap (zip ns args) amap, sc)
404 | Just v <- findDefault alts = return $ Just (amap, v)
405 chooseAlt env _ (VConstant c, []) alts amap
406 | Just v <- findConst c alts = return $ Just (amap, v)
407 | Just (n', sub, sc) <- findSuc c alts
408 = return $ Just (updateAmap [(n',sub)] amap, sc)
409 | Just v <- findDefault alts = return $ Just (amap, v)
410 chooseAlt env _ (VP _ n _, args) alts amap
411 | Just (ns, sc) <- findFn n alts = return $ Just (updateAmap (zip ns args) amap, sc)
412 chooseAlt env _ (VBind _ _ (Pi s) t, []) alts amap
413 | Just (ns, sc) <- findFn (UN "->") alts
414 = do t' <- t (VV 0) -- we know it's not in scope or it's not a pattern
415 return $ Just (updateAmap (zip ns [s, t']) amap, sc)
416 chooseAlt _ _ _ alts amap
417 | Just v <- findDefault alts
418 = if (any fnCase alts)
419 then return $ Just (amap, v)
420 else return Nothing
421 | otherwise = return Nothing
423 fnCase (FnCase _ _ _) = True
424 fnCase _ = False
426 -- Replace old variable names in the map with new matches
427 -- (This is possibly unnecessary since we make unique names and don't
428 -- allow repeated variables...?)
429 updateAmap newm amap
430 = newm ++ filter (\ (x, _) -> not (elem x (map fst newm))) amap
431 findTag i [] = Nothing
432 findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
433 findTag i (_ : xs) = findTag i xs
435 findFn fn [] = Nothing
436 findFn fn (FnCase n ns sc : xs) | fn == n = Just (ns, sc)
437 findFn fn (_ : xs) = findFn fn xs
439 findDefault [] = Nothing
440 findDefault (DefaultCase sc : xs) = Just sc
441 findDefault (_ : xs) = findDefault xs
443 findSuc c [] = Nothing
444 findSuc (BI val) (SucCase n sc : _)
445 | val /= 0 = Just (n, VConstant (BI (val - 1)), sc)
446 findSuc c (_ : xs) = findSuc c xs
448 findConst c [] = Nothing
449 findConst c (ConstCase c' v : xs) | c == c' = Just v
450 findConst (AType (ATInt ITNative)) (ConCase n 1 [] v : xs) = Just v
451 findConst (AType ATFloat) (ConCase n 2 [] v : xs) = Just v
452 findConst (AType (ATInt ITChar)) (ConCase n 3 [] v : xs) = Just v
453 findConst StrType (ConCase n 4 [] v : xs) = Just v
454 findConst PtrType (ConCase n 5 [] v : xs) = Just v
455 findConst (AType (ATInt ITBig)) (ConCase n 6 [] v : xs) = Just v
456 findConst (AType (ATInt (ITFixed ity))) (ConCase n tag [] v : xs)
457 | tag == 7 + fromEnum ity = Just v
458 findConst (AType (ATInt (ITVec ity count))) (ConCase n tag [] v : xs)
459 | tag == (fromEnum ity + 1) * 1000 + count = Just v
460 findConst c (_ : xs) = findConst c xs
462 getValArgs tm = getValArgs' tm []
463 getValArgs' (VApp f a) as = getValArgs' f (a:as)
464 getValArgs' f as = (f, as)
466-- tmpToV i vd (VLetHole j) | vd == j = return $ VV i
467-- tmpToV i vd (VP nt n v) = liftM (VP nt n) (tmpToV i vd v)
468-- tmpToV i vd (VBind n b sc) = do b' <- fmapMB (tmpToV i vd) b
469-- let sc' = \x -> do x' <- sc x
470-- tmpToV (i + 1) vd x'
471-- return (VBind n b' sc')
472-- tmpToV i vd (VApp f a) = liftM2 VApp (tmpToV i vd f) (tmpToV i vd a)
473-- tmpToV i vd x = return x
475instance Eq Value where
476 (==) x y = getTT x == getTT y
477 where getTT v = evalState (quote 0 v) initEval
479class Quote a where
480 quote :: Int -> a -> Eval (TT Name)
482instance Quote Value where
483 quote i (VP nt n v) = liftM (P nt n) (quote i v)
484 quote i (VV x) = return $ V x
485 quote i (VBind _ n b sc) = do sc' <- sc (VTmp i)
486 b' <- quoteB b
487 liftM (Bind n b') (quote (i+1) sc')
488 where quoteB t = fmapMB (quote i) t
489 quote i (VBLet vd n t v sc)
490 = do sc' <- quote i sc
491 t' <- quote i t
492 v' <- quote i v
493 let sc'' = pToV (MN vd "vlet") (addBinder sc')
494 return (Bind n (Let t' v') sc'')
495 quote i (VApp f a) = liftM2 App (quote i f) (quote i a)
496 quote i (VType u) = return $ TType u
497 quote i VErased = return $ Erased
498 quote i VImpossible = return $ Impossible
499 quote i (VProj v j) = do v' <- quote i v
500 return (Proj v' j)
501 quote i (VConstant c) = return $ Constant c
502 quote i (VTmp x) = return $ V (i - x - 1)
504wknV :: Int -> Value -> Eval Value
505wknV i (VV x) = return $ VV (x + i)
506wknV i (VBind red n b sc) = do b' <- fmapMB (wknV i) b
507 return $ VBind red n b' (\x -> do x' <- sc x
508 wknV i x')
509wknV i (VApp f a) = liftM2 VApp (wknV i f) (wknV i a)
510wknV i t = return t
512convEq' ctxt x y = evalStateT (convEq ctxt x y) (0, [])
514convEq :: Context -> TT Name -> TT Name -> StateT UCs TC Bool
515convEq ctxt = ceq [] where
516 ceq :: [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
517 ceq ps (P xt x _) (P yt y _)
518 | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True
519 | otherwise = sameDefs ps x y
520 ceq ps x (Bind n (Lam t) (App y (V 0))) = ceq ps x y
521 ceq ps (Bind n (Lam t) (App x (V 0))) y = ceq ps x y
522 ceq ps x (Bind n (Lam t) (App y (P Bound n' _)))
523 | n == n' = ceq ps x y
524 ceq ps (Bind n (Lam t) (App x (P Bound n' _))) y
525 | n == n' = ceq ps x y
526 ceq ps (V x) (V y) = return (x == y)
527 ceq ps (Bind _ xb xs) (Bind _ yb ys)
528 = liftM2 (&&) (ceqB ps xb yb) (ceq ps xs ys)
529 where
530 ceqB ps (Let v t) (Let v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')
531 ceqB ps (Guess v t) (Guess v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')
532 ceqB ps b b' = ceq ps (binderTy b) (binderTy b')
533 ceq ps (App fx ax) (App fy ay) = liftM2 (&&) (ceq ps fx fy) (ceq ps ax ay)
534 ceq ps (Constant x) (Constant y) = return (x == y)
535 ceq ps (TType x) (TType y) = do (v, cs) <- get
536 put (v, ULE x y : cs)
537 return True
538 ceq ps Erased _ = return True
539 ceq ps _ Erased = return True
540 ceq ps _ _ = return False
542 caseeq ps (Case n cs) (Case n' cs') = caseeqA ((n,n'):ps) cs cs'
543 where
544 caseeqA ps (ConCase x i as sc : rest) (ConCase x' i' as' sc' : rest')
545 = do q1 <- caseeq (zip as as' ++ ps) sc sc'
546 q2 <- caseeqA ps rest rest'
547 return $ x == x' && i == i' && q1 && q2
548 caseeqA ps (ConstCase x sc : rest) (ConstCase x' sc' : rest')
549 = do q1 <- caseeq ps sc sc'
550 q2 <- caseeqA ps rest rest'
551 return $ x == x' && q1 && q2
552 caseeqA ps (DefaultCase sc : rest) (DefaultCase sc' : rest')
553 = liftM2 (&&) (caseeq ps sc sc') (caseeqA ps rest rest')
554 caseeqA ps [] [] = return True
555 caseeqA ps _ _ = return False
556 caseeq ps (STerm x) (STerm y) = ceq ps x y
557 caseeq ps (UnmatchedCase _) (UnmatchedCase _) = return True
558 caseeq ps _ _ = return False
560 sameDefs ps x y = case (lookupDef x ctxt, lookupDef y ctxt) of
561 ([Function _ xdef], [Function _ ydef])
562 -> ceq ((x,y):ps) xdef ydef
563 ([CaseOp _ _ _ _ xd],
564 [CaseOp _ _ _ _ yd])
565 -> let (_, xdef) = cases_compiletime xd
566 (_, ydef) = cases_compiletime yd in
567 caseeq ((x,y):ps) xdef ydef
568 _ -> return False
570-- SPECIALISATION -----------------------------------------------------------
571-- We need too much control to be able to do this by tweaking the main
572-- evaluator
574spec :: Context -> Ctxt [Bool] -> Env -> TT Name -> Eval (TT Name)
575spec ctxt statics genv tm = error "spec undefined"
577-- CONTEXTS -----------------------------------------------------------------
579{-| A definition is either a simple function (just an expression with a type),
580 a constant, which could be a data or type constructor, an axiom or as an
581 yet undefined function, or an Operator.
582 An Operator is a function which explains how to reduce.
583 A CaseOp is a function defined by a simple case tree -}
585data Def = Function !Type !Term
586 | TyDecl NameType !Type
587 | Operator Type Int ([Value] -> Maybe Value)
588 | CaseOp CaseInfo
589 !Type
590 ![Either Term (Term, Term)] -- original definition
591 ![([Name], Term, Term)] -- simplified for totality check definition
592 !CaseDefs
593-- [Name] SC -- Compile time case definition
594-- [Name] SC -- Run time cae definitions
596data CaseDefs = CaseDefs {
597 cases_totcheck :: !([Name], SC),
598 cases_compiletime :: !([Name], SC),
599 cases_inlined :: !([Name], SC),
600 cases_runtime :: !([Name], SC)
601 }
603data CaseInfo = CaseInfo {
604 case_inlinable :: Bool,
605 tc_dictionary :: Bool
606 }
608{-!
609deriving instance Binary Def
610!-}
611{-!
612deriving instance Binary CaseInfo
613!-}
614{-!
615deriving instance Binary CaseDefs
616!-}
618instance Show Def where
619 show (Function ty tm) = "Function: " ++ show (ty, tm)
620 show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty
621 show (Operator ty _ _) = "Operator: " ++ show ty
622 show (CaseOp (CaseInfo inlc inlr) ty ps_in ps cd)
623 = let (ns, sc) = cases_compiletime cd
624 (ns_t, sc_t) = cases_totcheck cd
625 (ns', sc') = cases_runtime cd in
626 "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++
627 "TOTALITY CHECK TIME:\n\n" ++
628 show ns_t ++ " " ++ show sc_t ++ "\n\n" ++
629 "COMPILE TIME:\n\n" ++
630 show ns ++ " " ++ show sc ++ "\n\n" ++
631 "RUN TIME:\n\n" ++
632 show ns' ++ " " ++ show sc' ++ "\n\n" ++
633 if inlc then "Inlinable\n" else "Not inlinable\n"
635-- We need this for serialising Def. Fortunately, it never gets used because
636-- we'll never serialise a primitive operator
638instance Binary (a -> b) where
639 put x = return ()
640 get = error "Getting a function"
642-------
644-- Frozen => doesn't reduce
645-- Hidden => doesn't reduce and invisible to type checker
647data Accessibility = Public | Frozen | Hidden
648 deriving (Show, Eq)
650-- | The result of totality checking
651data Totality = Total [Int] -- ^ well-founded arguments
652 | Productive -- ^ productive
653 | Partial PReason
654 | Unchecked
655 deriving Eq
657-- | Reasons why a function may not be total
658data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name
659 | BelieveMe | Mutual [Name] | NotProductive
660 deriving (Show, Eq)
662instance Show Totality where
663 show (Total args)= "Total" -- ++ show args ++ " decreasing arguments"
664 show Productive = "Productive" -- ++ show args ++ " decreasing arguments"
665 show Unchecked = "not yet checked for totality"
666 show (Partial Itself) = "possibly not total as it is not well founded"
667 show (Partial NotCovering) = "not total as there are missing cases"
668 show (Partial NotPositive) = "not strictly positive"
669 show (Partial NotProductive) = "not productive"
670 show (Partial BelieveMe) = "not total due to use of believe_me in proof"
671 show (Partial (Other ns)) = "possibly not total due to: " ++ showSep ", " (map show ns)
672 show (Partial (Mutual ns)) = "possibly not total due to recursive path " ++
673 showSep " --> " (map show ns)
675{-!
676deriving instance Binary Accessibility
677!-}
679{-!
680deriving instance Binary Totality
681!-}
683{-!
684deriving instance Binary PReason
685!-}
687-- | Contexts used for global definitions and for proof state. They contain
688-- universe constraints and existing definitions.
689data Context = MkContext {
690 uconstraints :: [UConstraint],
691 next_tvar :: Int,
692 definitions :: Ctxt (Def, Accessibility, Totality)
693 } deriving Show
695-- | The initial empty context
696initContext = MkContext [] 0 emptyContext
698-- | Get the definitions from a context
699ctxtAlist :: Context -> [(Name, Def)]
700ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)
702veval ctxt env t = evalState (eval False ctxt [] env t []) initEval
704addToCtxt :: Name -> Term -> Type -> Context -> Context
705addToCtxt n tm ty uctxt
706 = let ctxt = definitions uctxt
707 ctxt' = addDef n (Function ty tm, Public, Unchecked) ctxt in
708 uctxt { definitions = ctxt' }
710setAccess :: Name -> Accessibility -> Context -> Context
711setAccess n a uctxt
712 = let ctxt = definitions uctxt
713 ctxt' = updateDef n (\ (d, _, t) -> (d, a, t)) ctxt in
714 uctxt { definitions = ctxt' }
716setTotal :: Name -> Totality -> Context -> Context
717setTotal n t uctxt
718 = let ctxt = definitions uctxt
719 ctxt' = updateDef n (\ (d, a, _) -> (d, a, t)) ctxt in
720 uctxt { definitions = ctxt' }
722addCtxtDef :: Name -> Def -> Context -> Context
723addCtxtDef n d c = let ctxt = definitions c
724 ctxt' = addDef n (d, Public, Unchecked) $! ctxt in
725 c { definitions = ctxt' }
727addTyDecl :: Name -> NameType -> Type -> Context -> Context
728addTyDecl n nt ty uctxt
729 = let ctxt = definitions uctxt
730 ctxt' = addDef n (TyDecl nt ty, Public, Unchecked) ctxt in
731 uctxt { definitions = ctxt' }
733addDatatype :: Datatype Name -> Context -> Context
734addDatatype (Data n tag ty cons) uctxt
735 = let ctxt = definitions uctxt
736 ty' = normalise uctxt [] ty
737 ctxt' = addCons 0 cons (addDef n
738 (TyDecl (TCon tag (arity ty')) ty, Public, Unchecked) ctxt) in
739 uctxt { definitions = ctxt' }
740 where
741 addCons tag [] ctxt = ctxt
742 addCons tag ((n, ty) : cons) ctxt
743 = let ty' = normalise uctxt [] ty in
744 addCons (tag+1) cons (addDef n
745 (TyDecl (DCon tag (arity ty')) ty, Public, Unchecked) ctxt)
747-- FIXME: Too many arguments! Refactor all these Bools.
748addCasedef :: Name -> CaseInfo -> Bool -> Bool -> Bool -> Bool ->
749 [Either Term (Term, Term)] ->
750 [([Name], Term, Term)] -> -- totality
751 [([Name], Term, Term)] -> -- compile time
752 [([Name], Term, Term)] -> -- inlined
753 [([Name], Term, Term)] -> -- run time
754 Type -> Context -> Context
755addCasedef n ci@(CaseInfo alwaysInline tcdict)
756 tcase covering reflect asserted ps_in
757 ps_tot ps_inl ps_ct ps_rt ty uctxt
758 = let ctxt = definitions uctxt
759 access = case lookupDefAcc n False uctxt of
760 [(_, acc)] -> acc
761 _ -> Public
762 ctxt' = case (simpleCase tcase covering reflect CompileTime emptyFC ps_tot,
763 simpleCase tcase covering reflect CompileTime emptyFC ps_ct,
764 simpleCase tcase covering reflect CompileTime emptyFC ps_inl,
765 simpleCase tcase covering reflect RunTime emptyFC ps_rt) of
766 (OK (CaseDef args_tot sc_tot _),
767 OK (CaseDef args_ct sc_ct _),
768 OK (CaseDef args_inl sc_inl _),
769 OK (CaseDef args_rt sc_rt _)) ->
770 let inl = alwaysInline -- tcdict
771 inlc = (inl || small n args_ct sc_ct) && (not asserted)
772 inlr = inl || small n args_rt sc_rt
773 cdef = CaseDefs (args_tot, sc_tot)
774 (args_ct, sc_ct)
775 (args_inl, sc_inl)
776 (args_rt, sc_rt) in
777 addDef n (CaseOp (ci { case_inlinable = inlc })
778 ty ps_in ps_tot cdef,
779 access, Unchecked) ctxt in
780 uctxt { definitions = ctxt' }
782-- simplify a definition for totality checking
783simplifyCasedef :: Name -> Context -> Context
784simplifyCasedef n uctxt
785 = let ctxt = definitions uctxt
786 ctxt' = case lookupCtxt n ctxt of
787 [(CaseOp ci ty [] ps _, acc, tot)] ->
788 ctxt -- nothing to simplify (or already done...)
789 [(CaseOp ci ty ps_in ps cd, acc, tot)] ->
790 let ps_in' = map simpl ps_in
791 pdef = map debind ps_in' in
792 case simpleCase False True False CompileTime emptyFC pdef of
793 OK (CaseDef args sc _) ->
794 addDef n (CaseOp ci
795 ty ps_in' ps (cd { cases_totcheck = (args, sc) }),
796 acc, tot) ctxt
797 Error err -> error (show err)
798 _ -> ctxt in
799 uctxt { definitions = ctxt' }
800 where
801 depat acc (Bind n (PVar t) sc)
802 = depat (n : acc) (instantiate (P Bound n t) sc)
803 depat acc x = (acc, x)
804 debind (Right (x, y)) = let (vs, x') = depat [] x
805 (_, y') = depat [] y in
806 (vs, x', y')
807 debind (Left x) = let (vs, x') = depat [] x in
808 (vs, x', Impossible)
809 simpl (Right (x, y)) = Right (x, simplify uctxt [] y)
810 simpl t = t
812addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) ->
813 Context -> Context
814addOperator n ty a op uctxt
815 = let ctxt = definitions uctxt
816 ctxt' = addDef n (Operator ty a op, Public, Unchecked) ctxt in
817 uctxt { definitions = ctxt' }
819tfst (a, _, _) = a
821lookupNames :: Name -> Context -> [Name]
822lookupNames n ctxt
823 = let ns = lookupCtxtName n (definitions ctxt) in
824 map fst ns
826lookupTy :: Name -> Context -> [Type]
827lookupTy n ctxt
828 = do def <- lookupCtxt n (definitions ctxt)
829 case tfst def of
830 (Function ty _) -> return ty
831 (TyDecl _ ty) -> return ty
832 (Operator ty _ _) -> return ty
833 (CaseOp _ ty _ _ _) -> return ty
835isConName :: Name -> Context -> Bool
836isConName n ctxt = isTConName n ctxt || isDConName n ctxt
838isTConName :: Name -> Context -> Bool
839isTConName n ctxt
840 = or $ do def <- lookupCtxt n (definitions ctxt)
841 case tfst def of
842 (TyDecl (TCon _ _) _) -> return True
843 _ -> return False
845isDConName :: Name -> Context -> Bool
846isDConName n ctxt
847 = or $ do def <- lookupCtxt n (definitions ctxt)
848 case tfst def of
849 (TyDecl (DCon _ _) _) -> return True
850 _ -> return False
852isFnName :: Name -> Context -> Bool
853isFnName n ctxt
854 = or $ do def <- lookupCtxt n (definitions ctxt)
855 case tfst def of
856 (Function _ _) -> return True
857 (Operator _ _ _) -> return True
858 (CaseOp _ _ _ _ _) -> return True
859 _ -> return False
861lookupP :: Name -> Context -> [Term]
862lookupP n ctxt
863 = do def <- lookupCtxt n (definitions ctxt)
864 p <- case def of
865 (Function ty tm, a, _) -> return (P Ref n ty, a)
866 (TyDecl nt ty, a, _) -> return (P nt n ty, a)
867 (CaseOp _ ty _ _ _, a, _) -> return (P Ref n ty, a)
868 (Operator ty _ _, a, _) -> return (P Ref n ty, a)
869 case snd p of
870 Hidden -> []
871 _ -> return (fst p)
873lookupDef :: Name -> Context -> [Def]
874lookupDef n ctxt = map tfst $ lookupCtxt n (definitions ctxt)
876lookupDefAcc :: Name -> Bool -> Context ->
877 [(Def, Accessibility)]
878lookupDefAcc n mkpublic ctxt
879 = map mkp $ lookupCtxt n (definitions ctxt)
880 -- io_bind a special case for REPL prettiness
881 where mkp (d, a, _) = if mkpublic && (not (n == UN "io_bind" || n == UN "io_return"))
882 then (d, Public) else (d, a)
884lookupTotal :: Name -> Context -> [Totality]
885lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)
886 where mkt (d, a, t) = t
888lookupNameTotal :: Name -> Context -> [(Name, Totality)]
889lookupNameTotal n = map (\(n, (_, _, t)) -> (n, t)) . lookupCtxtName n . definitions
892lookupVal :: Name -> Context -> [Value]
893lookupVal n ctxt
894 = do def <- lookupCtxt n (definitions ctxt)
895 case tfst def of
896 (Function _ htm) -> return (veval ctxt [] htm)
897 (TyDecl nt ty) -> return (VP nt n (veval ctxt [] ty))
899lookupTyEnv :: Name -> Env -> Maybe (Int, Type)
900lookupTyEnv n env = li n 0 env where
901 li n i [] = Nothing
902 li n i ((x, b): xs)
903 | n == x = Just (i, binderTy b)
904 | otherwise = li n (i+1) xs