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