git.iko.soy/Idris-dev
on 4e0fe22 help sign in
Idris-dev/src/Core/Evaluate.hs
768 lines 33 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,
2 PatternGuards #-}
4module Core.Evaluate(normalise, normaliseC, normaliseAll,
5 simplify, specialise, hnf, convEq, convEq',
6 Def(..), Accessibility(..), Totality(..), PReason(..),
7 Context, initContext, ctxtAlist, uconstraints, next_tvar,
8 addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl, addDatatype,
9 addCasedef, addOperator,
10 lookupNames, lookupTy, lookupP, lookupDef, lookupVal, lookupTotal,
11 lookupTyEnv, isConName, isFnName,
12 Value(..)) where
14import Debug.Trace
15import Control.Monad.State
16import qualified Data.Binary as B
17import Data.Binary hiding (get, put)
19import Core.TT
20import Core.CaseTree
22data EvalState = ES { limited :: [(Name, Int)],
23 steps :: Int -- number of applications/let reductions
24 }
26-- Evaluation fails if we hit a boredom threshold - in which case, just return
27-- the original (capture the failure in a Maybe)
29type Eval a = State EvalState a
31data EvalOpt = Spec | HNF | Simplify | AtREPL
32 deriving (Show, Eq)
34initEval = ES [] 0
36step :: Int -> Eval ()
37step max = do e <- get
38 put (e { steps = steps e + 1 })
39 if steps e > max then fail "Threshold exceeded"
40 else return ()
42getSteps :: Eval Int
43getSteps = do e <- get
44 return (steps e)
46-- VALUES (as HOAS) ---------------------------------------------------------
48data Value = VP NameType Name Value
49 | VV Int
50 | VBind Name (Binder Value) (Value -> Eval Value)
51 | VApp Value Value
52 | VSet UExp
53 | VErased
54 | VConstant Const
55-- | VLazy Env [Value] Term
56 | VTmp Int
58data HNF = HP NameType Name (TT Name)
59 | HV Int
60 | HBind Name (Binder HNF) (HNF -> Eval HNF)
61 | HApp HNF [HNF] [TT Name]
62 | HSet UExp
63 | HConstant Const
64 | HTmp Int
65 deriving Show
67instance Show Value where
68 show x = show $ evalState (quote 100 x) initEval
70instance Show (a -> b) where
71 show x = "<<fn>>"
73-- THE EVALUATOR ------------------------------------------------------------
75-- The environment is assumed to be "locally named" - i.e., not de Bruijn
76-- indexed.
77-- i.e. it's an intermediate environment that we have while type checking or
78-- while building a proof.
80threshold = 1000 -- boredom threshold for evaluation, to prevent infinite typechecking
81 -- in fact it's a maximum recursion depth
83-- Normalise fully type checked terms (so, assume all names/let bindings resolved)
84normaliseC :: Context -> Env -> TT Name -> TT Name
85normaliseC ctxt env t
86 = evalState (do val <- eval ctxt threshold [] env t []
87 quote 0 val) initEval
89normaliseAll :: Context -> Env -> TT Name -> TT Name
90normaliseAll ctxt env t
91 = evalState (do val <- eval ctxt threshold [] env t [AtREPL]
92 quote 0 val) initEval
94normalise :: Context -> Env -> TT Name -> TT Name
95normalise ctxt env t
96 = evalState (do val <- eval ctxt threshold [] (map finalEntry env) (finalise t) []
97 quote 0 val) initEval
99specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name
100specialise ctxt env limits t
101 = evalState (do val <- eval ctxt threshold limits (map finalEntry env) (finalise t) []
102 quote 0 val) (initEval { limited = limits })
104-- Like normalise, but we only reduce functions that are marked as okay to
105-- inline (and probably shouldn't reduce lets?)
107simplify :: Context -> Env -> TT Name -> TT Name
108simplify ctxt env t
109 = evalState (do val <- eval ctxt threshold []
110 (map finalEntry env) (finalise t) [Simplify]
111 quote 0 val) initEval
113hnf :: Context -> Env -> TT Name -> TT Name
114hnf ctxt env t
115 = evalState (do val <- eval ctxt threshold [] (map finalEntry env) (finalise t) [HNF]
116 quote 0 val) initEval
119-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))
121finalEntry :: (Name, Binder (TT Name)) -> (Name, Binder (TT Name))
122finalEntry (n, b) = (n, fmap finalise b)
124bindEnv :: EnvTT n -> TT n -> TT n
125bindEnv [] tm = tm
126bindEnv ((n, Let t v):bs) tm = Bind n (NLet t v) (bindEnv bs tm)
127bindEnv ((n, b):bs) tm = Bind n b (bindEnv bs tm)
129unbindEnv :: EnvTT n -> TT n -> TT n
130unbindEnv [] tm = tm
131unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc
133usable :: Name -> [(Name, Int)] -> (Bool, [(Name, Int)])
134usable n [] = (True, [])
135usable n ns = case lookup n ns of
136 Just 0 -> (False, ns)
137 Just i -> (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns)
138 _ -> (True, (n, 100) : filter (\ (n', _) -> n/=n') ns)
140reduction :: Eval ()
141reduction = do ES ns s <- get
142 put (ES ns (s+1))
144-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,
145-- such as we might have during construction of a proof)
147eval :: Context -> Int -> [(Name, Int)] -> Env -> TT Name -> [EvalOpt] -> Eval Value
148eval ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
149 spec = Spec `elem` opts
150 simpl = Simplify `elem` opts
151 atRepl = AtREPL `elem` opts
153 ev ntimes stk top env (P _ n ty)
154 | Just (Let t v) <- lookup n genv = do when (not atRepl) $ step maxred
155 ev ntimes stk top env v
156 ev ntimes_in stk top env (P Ref n ty)
157 | (True, ntimes) <- usable n ntimes_in
158 = do let val = lookupDefAcc Nothing n atRepl ctxt
159 when (not atRepl) $ step maxred
160 case val of
161 [(Function _ tm, Public)] ->
162 ev ntimes (n:stk) True env tm
163 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty
164 return $ VP nt n vty
165 [(CaseOp inl _ _ [] tree _ _, Public)] -> -- unoptimised version
166 if simpl && (not inl || elem n stk)
167 then liftM (VP Ref n) (ev ntimes stk top env ty)
168 else do c <- evCase ntimes (n:stk) top env [] [] tree
169 case c of
170 (Nothing, _) -> liftM (VP Ref n) (ev ntimes stk top env ty)
171 (Just v, _) -> return v
172 _ -> liftM (VP Ref n) (ev ntimes stk top env ty)
173 ev ntimes stk top env (P nt n ty) = liftM (VP nt n) (ev ntimes stk top env ty)
174 ev ntimes stk top env (V i) | i < length env = return $ env !! i
175 | otherwise = return $ VV i
176 ev ntimes stk top env (Bind n (Let t v) sc)
177 = do v' <- ev ntimes stk top env v --(finalise v)
178 when (not atRepl) $ step maxred
179 sc' <- ev ntimes stk top (v' : env) sc
180 wknV (-1) sc'
181 ev ntimes stk top env (Bind n (NLet t v) sc)
182 = do t' <- ev ntimes stk top env (finalise t)
183 v' <- ev ntimes stk top env (finalise v)
184 when (not atRepl) $ step maxred
185 sc' <- ev ntimes stk top (v' : env) sc
186 return $ VBind n (Let t' v') (\x -> return sc')
187 ev ntimes stk top env (Bind n b sc)
188 = do b' <- vbind env b
189 when (not atRepl) $ step maxred
190 return $ VBind n b' (\x -> ev ntimes stk top (x:env) sc)
191 where vbind env t = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
192-- ev ntimes stk top env (App (App (P _ laz _) _) a)
193-- | laz == UN "lazy"
194-- = trace (showEnvDbg genv a) $ ev ntimes stk top env a
195 ev ntimes stk top env (App f a)
196 = do f' <- ev ntimes stk top env f
197 a' <- ev ntimes stk False env a
198 when (not atRepl) $ step maxred
199 evApply ntimes stk top env [a'] f'
200 ev ntimes stk top env (Constant c) = return $ VConstant c
201 ev ntimes stk top env Erased = return VErased
202 ev ntimes stk top env (Set i) = return $ VSet i
204 evApply ntimes stk top env args (VApp f a) =
205 evApply ntimes stk top env (a:args) f
206 evApply ntimes stk top env args f = do when (not atRepl) $ step maxred
207 apply ntimes stk top env f args
209 apply ntimes stk top env f as
210 | length stk > threshold = return $ unload env f as
211 apply ntimes stk top env (VBind n (Lam t) sc) (a:as)
212 = do a' <- sc a
213 app <- apply ntimes stk top env a' as
214 wknV (-1) app
215-- apply ntimes stk False env f args
216-- | spec = specApply ntimes stk env f args
217 apply ntimes_in stk top env f@(VP Ref n ty) args
218 | (True, ntimes) <- usable n ntimes_in
219 = do let val = lookupDefAcc Nothing n atRepl ctxt
220 case val of
221 [(CaseOp inl _ _ ns tree _ _, Public)] ->
222 if simpl && (not inl || elem n stk)
223 then return $ unload env (VP Ref n ty) args
224 else do c <- evCase ntimes (n:stk) top env ns args tree
225 case c of
226 (Nothing, _) -> return $ unload env (VP Ref n ty) args
227 (Just v, rest) -> evApply ntimes stk top env rest v
228 [(Operator _ i op, _)] ->
229 if (i <= length args)
230 then case op (take i args) of
231 Nothing -> return $ unload env (VP Ref n ty) args
232 Just v -> evApply ntimes stk top env (drop i args) v
233 else return $ unload env (VP Ref n ty) args
234 _ -> case args of
235 [] -> return f
236 _ -> return $ unload env f args
237 apply ntimes stk top env f (a:as) = return $ unload env f (a:as)
238 apply ntimes stk top env f [] = return f
240-- specApply stk env f@(VP Ref n ty) args
241-- = case lookupCtxt Nothing n statics of
242-- [as] -> if or as
243-- then trace (show (n, map fst (filter (\ (_, s) -> s) (zip args as)))) $
244-- return $ unload env f args
245-- else return $ unload env f args
246-- _ -> return $ unload env f args
247-- specApply stk env f args = return $ unload env f args
249 unload env f [] = f
250 unload env f (a:as) = unload env (VApp f a) as
252 evCase ntimes stk top env ns args tree
253 | length ns <= length args
254 = do let args' = take (length ns) args
255 let rest = drop (length ns) args
256 t <- evTree ntimes stk top env (zipWith (\n t -> (n, t)) ns args') tree
257 return (t, rest)
258 | otherwise = return (Nothing, args)
260 evTree :: [(Name, Int)] -> [Name] -> Bool ->
261 [Value] -> [(Name, Value)] -> SC -> Eval (Maybe Value)
262 evTree ntimes stk top env amap (UnmatchedCase str) = return Nothing
263 evTree ntimes stk top env amap (STerm tm)
264 = do let etm = pToVs (map fst amap) tm
265 etm' <- ev ntimes stk top (map snd amap ++ env) etm
266 return $ Just etm'
267 evTree ntimes stk top env amap (Case n alts)
268 = case lookup n amap of
269 Just v -> do c <- chooseAlt env v (getValArgs v) alts amap
270 case c of
271 Just (altmap, sc) -> evTree ntimes stk top env altmap sc
272 _ -> do c' <- chooseAlt' ntimes stk env v (getValArgs v) alts amap
273 case c' of
274 Just (altmap, sc) -> evTree ntimes stk top env altmap sc
275 _ -> return Nothing
276 _ -> return Nothing
278 chooseAlt' ntimes stk env _ (f, args) alts amap
279 = do f' <- apply ntimes stk True env f args
280 chooseAlt env f' (getValArgs f') alts amap
282 chooseAlt :: [Value] -> Value -> (Value, [Value]) -> [CaseAlt] -> [(Name, Value)] ->
283 Eval (Maybe ([(Name, Value)], SC))
284 chooseAlt env _ (VP (DCon i a) _ _, args) alts amap
285 | Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)
286 | Just v <- findDefault alts = return $ Just (amap, v)
287 chooseAlt env _ (VP (TCon i a) _ _, args) alts amap
288 | Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)
289 | Just v <- findDefault alts = return $ Just (amap, v)
290 chooseAlt env _ (VConstant c, []) alts amap
291 | Just v <- findConst c alts = return $ Just (amap, v)
292 | Just v <- findDefault alts = return $ Just (amap, v)
293 chooseAlt _ _ _ _ _ = return Nothing
295 -- Replace old variable names in the map with new matches
296 -- (This is possibly unnecessary since we make unique names and don't
297 -- allow repeated variables...?)
298 updateAmap newm amap
299 = newm ++ filter (\ (x, _) -> not (elem x (map fst newm))) amap
300 findTag i [] = Nothing
301 findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
302 findTag i (_ : xs) = findTag i xs
304 findDefault [] = Nothing
305 findDefault (DefaultCase sc : xs) = Just sc
306 findDefault (_ : xs) = findDefault xs
308 findConst c [] = Nothing
309 findConst c (ConstCase c' v : xs) | c == c' = Just v
310 findConst IType (ConCase n 1 [] v : xs) = Just v
311 findConst FlType (ConCase n 2 [] v : xs) = Just v
312 findConst ChType (ConCase n 3 [] v : xs) = Just v
313 findConst StrType (ConCase n 4 [] v : xs) = Just v
314 findConst PtrType (ConCase n 5 [] v : xs) = Just v
315 findConst c (_ : xs) = findConst c xs
317 getValArgs tm = getValArgs' tm []
318 getValArgs' (VApp f a) as = getValArgs' f (a:as)
319 getValArgs' f as = (f, as)
321class Quote a where
322 quote :: Int -> a -> Eval (TT Name)
324instance Quote Value where
325 quote i (VP nt n v) = liftM (P nt n) (quote i v)
326 quote i (VV x) = return $ V x
327 quote i (VBind n b sc) = do sc' <- sc (VTmp i)
328 b' <- quoteB b
329 liftM (Bind n b') (quote (i+1) sc')
330 where quoteB t = fmapMB (quote i) t
331 quote i (VApp f a) = liftM2 App (quote i f) (quote i a)
332 quote i (VSet u) = return $ Set u
333 quote i VErased = return $ Erased
334 quote i (VConstant c) = return $ Constant c
335 quote i (VTmp x) = return $ V (i - x - 1)
337instance Quote HNF where
338 quote i (HP nt n t) = return (P nt n t)
339 quote i (HV x) = return $ V x
340 quote i (HBind n b sc) = do sc' <- sc (HTmp i)
341 b' <- quoteB b
342 liftM (Bind n b') (quote (i+1) sc')
343 where quoteB t = fmapMB (quote i) t
344 quote i (HApp f env as) = do f' <- quote i f
345 as' <- mapM (iEnv env) as
346 return $ mkApp f' as'
347 where iEnv [] a = return a
348 iEnv (x:xs) a = do x' <- quote i x
349 iEnv xs (weakenTm (-1) (instantiate x' a))
350 quote i (HSet u) = return $ Set u
351 quote i (HConstant c) = return $ Constant c
352 quote i (HTmp x) = return $ V (i - x - 1)
354wknV :: Int -> Value -> Eval Value
355wknV i (VV x) = return $ VV (x + i)
356wknV i (VBind n b sc) = do b' <- fmapMB (wknV i) b
357 return $ VBind n b' (\x -> do x' <- sc x
358 wknV i x')
359wknV i (VApp f a) = liftM2 VApp (wknV i f) (wknV i a)
360wknV i t = return t
362wknH :: Int -> HNF -> Eval HNF
363wknH i (HV x) = return $ HV (x + i)
364wknH i (HBind n b sc) = do b' <- fmapMB (wknH i) b
365 return $ HBind n b' (\x -> do x' <- sc x
366 wknH i x')
367wknH i (HApp f env as) = liftM3 HApp (wknH i f) (return env)
368 (return as)
369wknH i t = return t
371-- HEAD NORMAL FORM ---------------------------------------------------------
373eval_hnf :: Context -> Ctxt [Bool] -> Env -> TT Name -> Eval HNF
374eval_hnf ctxt statics genv tm = ev [] tm where
375 ev :: [HNF] -> TT Name -> Eval HNF
376 ev env (P _ n ty)
377 | Just (Let t v) <- lookup n genv = ev env v
378 ev env (P Ref n ty) = case lookupDef Nothing n ctxt of
379 [Function _ t] -> ev env t
380 [TyDecl nt ty] -> return $ HP nt n ty
381 [CaseOp inl _ _ [] tree _ _] ->
382 do c <- evCase env [] [] tree
383 case c of
384 (Nothing, _, _) -> return $ HP Ref n ty
385 (Just v, _, _) -> return v
386 _ -> return $ HP Ref n ty
387 ev env (P nt n ty) = return $ HP nt n ty
388 ev env (V i) | i < length env = return $ env !! i
389 | otherwise = return $ HV i
390 ev env (Bind n (Let t v) sc)
391 = do v' <- ev env (finalise v)
392 sc' <- ev (v' : env) sc
393 wknH (-1) sc'
394 ev env (Bind n b sc)
395 = do b' <- hbind env b
396 return $ HBind n b' (\x -> ev (x : env) sc)
397 where hbind env t = fmapMB (\tm -> ev env (finalise tm)) t
398 ev env (App f a) = evApply env [a] f
399 ev env (Constant c) = return $ HConstant c
400 ev env (Set i) = return $ HSet i
402 evApply env args (App f a) = evApply env (a : args) f
403 evApply env args f = do f' <- ev env f
404 apply env f' args
406 apply env (HBind n (Lam t) sc) (a:as) = do a' <- ev env a
407 sc' <- sc a'
408 app <- apply env sc' as
409 wknH (-1) app
410 apply env (HP Ref n ty) args
411 | [CaseOp _ _ _ ns tree _ _] <- lookupDef Nothing n ctxt
412 = do c <- evCase env ns args tree
413 case c of
414 (Nothing, _, env') -> return $ unload env' (HP Ref n ty) args
415 (Just v, rest, env') -> do v' <- quote 0 v
416 apply env' v rest
417-- | Just (Operator _ i op) <- lookupDef n ctxt
418-- = if (i <= length args)
419-- then case op (take i args) of
420-- Nothing -> return $ unload env (HP Ref n ty) args
421-- Just v -> evApply env (drop i args) v
422-- else return $ unload env (HP Ref n ty) args
423 apply env f (a:as) = return $ unload env f (a:as)
424 apply env f [] = return f
426 unload env f [] = f
427 unload env f as = HApp f env as
429 evCase env ns args tree
430 | length ns <= length args
431 = do let args' = take (length ns) args
432 let rest = drop (length ns) args
433 (t, env') <- evTree env (zipWith (\n t -> (n, t)) ns args') tree
434 return (t, rest, env')
435 | otherwise = return (Nothing, args, env)
437 evTree :: [HNF] -> [(Name, TT Name)] -> SC -> Eval (Maybe HNF, [HNF])
438 evTree env amap (UnmatchedCase str) = return (Nothing, env)
439 evTree env amap (STerm tm)
440 = do let etm = pToVs (map fst amap) tm
441 amap' <- mapM (ev env) (map snd amap)
442 envw <- mapM (wknH (length amap)) env
443 let env' = amap' ++ envw
444 etm' <- trace (show etm) $ ev env' etm
445 etmq <- quote 0 etm'
446 trace ("Ev: " ++ show (etm, etmq)) $ return $ (Just etm', env')
447 evTree env amap (Case n alts)
448 = case lookup n amap of
449 Just v -> do v' <- ev env v
450 case chooseAlt v' (getValArgs v') alts amap of
451 Just (altmap, sc) -> evTree env altmap sc
452 _ -> return (Nothing, env)
454 chooseAlt :: HNF -> (HNF, [HNF], [TT Name]) ->
455 [CaseAlt] -> [(Name, TT Name)] ->
456 Maybe ([(Name, TT Name)], SC)
457 chooseAlt _ (HP (DCon i a) _ _, env, args) alts amap
458 | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)
459 | Just v <- findDefault alts = Just (amap, v)
460 chooseAlt _ (HP (TCon i a) _ _, env, args) alts amap
461 | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)
462 | Just v <- findDefault alts = Just (amap, v)
463 chooseAlt _ (HConstant c, env, []) alts amap
464 | Just v <- findConst c alts = Just (amap, v)
465 | Just v <- findDefault alts = Just (amap, v)
466 chooseAlt _ _ _ _ = Nothing
468 -- Replace old variable names in the map with new matches
469 -- (This is possibly unnecessary since we make unique names and don't
470 -- allow repeated variables...?)
471 updateAmap newm amap
472 = newm ++ filter (\ (x, _) -> not (elem x (map fst newm))) amap
473 findTag i [] = Nothing
474 findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
475 findTag i (_ : xs) = findTag i xs
477 findDefault [] = Nothing
478 findDefault (DefaultCase sc : xs) = Just sc
479 findDefault (_ : xs) = findDefault xs
481 findConst c [] = Nothing
482 findConst c (ConstCase c' v : xs) | c == c' = Just v
483 findConst IType (ConCase n 1 [] v : xs) = Just v
484 findConst FlType (ConCase n 2 [] v : xs) = Just v
485 findConst ChType (ConCase n 3 [] v : xs) = Just v
486 findConst StrType (ConCase n 4 [] v : xs) = Just v
487 findConst PtrType (ConCase n 5 [] v : xs) = Just v
488 findConst c (_ : xs) = findConst c xs
490 getValArgs (HApp t env args) = (t, env, args)
491 getValArgs t = (t, [], [])
493convEq' ctxt x y = evalStateT (convEq ctxt x y) (0, [])
495convEq :: Context -> TT Name -> TT Name -> StateT UCs TC Bool
496convEq ctxt = ceq [] where
497 ceq :: [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
498 ceq ps (P xt x _) (P yt y _)
499 | (xt == yt && x ==y ) || (x, y) `elem` ps || (y,x) `elem` ps = return True
500 | otherwise = sameDefs ps x y
501 ceq ps (V x) (V y) = return (x == y)
502 ceq ps (Bind _ xb xs) (Bind _ yb ys)
503 = liftM2 (&&) (ceqB ps xb yb) (ceq ps xs ys)
504 where
505 ceqB ps (Let v t) (Let v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')
506 ceqB ps (Guess v t) (Guess v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')
507 ceqB ps b b' = ceq ps (binderTy b) (binderTy b')
508 ceq ps (App fx ax) (App fy ay) = liftM2 (&&) (ceq ps fx fy) (ceq ps ax ay)
509 ceq ps (Constant x) (Constant y) = return (x == y)
510 ceq ps (Set x) (Set y) = do (v, cs) <- get
511 put (v, ULE x y : cs)
512 return True
513 ceq ps Erased _ = return True
514 ceq ps _ Erased = return True
515 ceq ps _ _ = return False
517 caseeq ps (Case n cs) (Case n' cs') = caseeqA ((n,n'):ps) cs cs'
518 where
519 caseeqA ps (ConCase x i as sc : rest) (ConCase x' i' as' sc' : rest')
520 = do q1 <- caseeq (zip as as' ++ ps) sc sc'
521 q2 <- caseeqA ps rest rest'
522 return $ x == x' && i == i' && q1 && q2
523 caseeqA ps (ConstCase x sc : rest) (ConstCase x' sc' : rest')
524 = do q1 <- caseeq ps sc sc'
525 q2 <- caseeqA ps rest rest'
526 return $ x == x' && q1 && q2
527 caseeqA ps (DefaultCase sc : rest) (DefaultCase sc' : rest')
528 = liftM2 (&&) (caseeq ps sc sc') (caseeqA ps rest rest')
529 caseeqA ps [] [] = return True
530 caseeqA ps _ _ = return False
531 caseeq ps (STerm x) (STerm y) = ceq ps x y
532 caseeq ps (UnmatchedCase _) (UnmatchedCase _) = return True
533 caseeq ps _ _ = return False
535 sameDefs ps x y = case (lookupDef Nothing x ctxt, lookupDef Nothing y ctxt) of
536 ([Function _ xdef], [Function _ ydef])
537 -> ceq ((x,y):ps) xdef ydef
538 ([CaseOp _ _ _ _ xdef _ _],
539 [CaseOp _ _ _ _ ydef _ _])
540 -> caseeq ((x,y):ps) xdef ydef
541 _ -> return False
543-- SPECIALISATION -----------------------------------------------------------
544-- We need too much control to be able to do this by tweaking the main
545-- evaluator
547spec :: Context -> Ctxt [Bool] -> Env -> TT Name -> Eval (TT Name)
548spec ctxt statics genv tm = error "spec undefined"
550-- CONTEXTS -----------------------------------------------------------------
552{- A definition is either a simple function (just an expression with a type),
553 a constant, which could be a data or type constructor, an axiom or as an
554 yet undefined function, or an Operator.
555 An Operator is a function which explains how to reduce.
556 A CaseOp is a function defined by a simple case tree -}
558data Def = Function Type Term
559 | TyDecl NameType Type
560 | Operator Type Int ([Value] -> Maybe Value)
561 | CaseOp Bool Type [([Name], Term, Term)] -- Bool for inlineable
562 [Name] SC -- Compile time case definition
563 [Name] SC -- Run time cae definitions
564{-!
565deriving instance Binary Def
566!-}
568instance Show Def where
569 show (Function ty tm) = "Function: " ++ show (ty, tm)
570 show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty
571 show (Operator ty _ _) = "Operator: " ++ show ty
572 show (CaseOp _ ty ps ns sc ns' sc')
573 = "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++
574 show ns ++ " " ++ show sc ++ "\n" ++
575 show ns' ++ " " ++ show sc'
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)
591data Totality = Total [Int] -- well-founded arguments
592 | Partial PReason
593 | Unchecked
594 deriving Eq
596data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name
597 | Mutual [Name]
598 deriving (Show, Eq)
600instance Show Totality where
601 show (Total args)= "Total" -- ++ show args ++ " decreasing arguments"
602 show Unchecked = "not yet checked for totality"
603 show (Partial Itself) = "possibly not total as it is not well founded"
604 show (Partial NotCovering) = "not total as there are missing cases"
605 show (Partial NotPositive) = "not strictly positive"
606 show (Partial (Other ns)) = "possibly not total due to: " ++ showSep ", " (map show ns)
607 show (Partial (Mutual ns)) = "possibly not total due to mutual recursive path " ++
608 showSep " --> " (map show ns)
610{-!
611deriving instance Binary Accessibility
612!-}
614{-!
615deriving instance Binary Totality
616!-}
618{-!
619deriving instance Binary PReason
620!-}
622data Context = MkContext { uconstraints :: [UConstraint],
623 next_tvar :: Int,
624 definitions :: Ctxt (Def, Accessibility, Totality) }
626initContext = MkContext [] 0 emptyContext
628ctxtAlist :: Context -> [(Name, Def)]
629ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)
631veval ctxt env t = evalState (eval ctxt threshold [] env t []) initEval
633addToCtxt :: Name -> Term -> Type -> Context -> Context
634addToCtxt n tm ty uctxt
635 = let ctxt = definitions uctxt
636 ctxt' = addDef n (Function ty tm, Public, Unchecked) ctxt in
637 uctxt { definitions = ctxt' }
639setAccess :: Name -> Accessibility -> Context -> Context
640setAccess n a uctxt
641 = let ctxt = definitions uctxt
642 ctxt' = updateDef n (\ (d, _, t) -> (d, a, t)) ctxt in
643 uctxt { definitions = ctxt' }
645setTotal :: Name -> Totality -> Context -> Context
646setTotal n t uctxt
647 = let ctxt = definitions uctxt
648 ctxt' = updateDef n (\ (d, a, _) -> (d, a, t)) ctxt in
649 uctxt { definitions = ctxt' }
651addCtxtDef :: Name -> Def -> Context -> Context
652addCtxtDef n d c = let ctxt = definitions c
653 ctxt' = addDef n (d, Public, Unchecked) ctxt in
654 c { definitions = ctxt' }
656addTyDecl :: Name -> Type -> Context -> Context
657addTyDecl n ty uctxt
658 = let ctxt = definitions uctxt
659 ctxt' = addDef n (TyDecl Ref ty, Public, Unchecked) ctxt in
660 uctxt { definitions = ctxt' }
662addDatatype :: Datatype Name -> Context -> Context
663addDatatype (Data n tag ty cons) uctxt
664 = let ctxt = definitions uctxt
665 ty' = normalise uctxt [] ty
666 ctxt' = addCons 0 cons (addDef n
667 (TyDecl (TCon tag (arity ty')) ty, Public, Unchecked) ctxt) in
668 uctxt { definitions = ctxt' }
669 where
670 addCons tag [] ctxt = ctxt
671 addCons tag ((n, ty) : cons) ctxt
672 = let ty' = normalise uctxt [] ty in
673 addCons (tag+1) cons (addDef n
674 (TyDecl (DCon tag (arity ty')) ty, Public, Unchecked) ctxt)
676addCasedef :: Name -> Bool -> Bool -> Bool ->
677 [([Name], Term, Term)] -> [([Name], Term, Term)] ->
678 Type -> Context -> Context
679addCasedef n alwaysInline tcase covering ps psrt ty uctxt
680 = let ctxt = definitions uctxt
681 ps' = ps -- simpl ps in
682 ctxt' = case (simpleCase tcase covering (FC "" 0) ps',
683 simpleCase tcase covering (FC "" 0) psrt) of
684 (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) ->
685 let inl = alwaysInline in
686 addDef n (CaseOp inl ty ps args sc args' sc',
687 Public, Unchecked) ctxt in
688 uctxt { definitions = ctxt' }
689 where simpl [] = []
690 simpl ((l,r) : xs) = (l, simplify uctxt [] r) : simpl xs
692addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> Context
693addOperator n ty a op uctxt
694 = let ctxt = definitions uctxt
695 ctxt' = addDef n (Operator ty a op, Public, Unchecked) ctxt in
696 uctxt { definitions = ctxt' }
698tfst (a, _, _) = a
700lookupNames :: Maybe [String] -> Name -> Context -> [Name]
701lookupNames root n ctxt
702 = let ns = lookupCtxtName root n (definitions ctxt) in
703 map fst ns
705lookupTy :: Maybe [String] -> Name -> Context -> [Type]
706lookupTy root n ctxt
707 = do def <- lookupCtxt root n (definitions ctxt)
708 case tfst def of
709 (Function ty _) -> return ty
710 (TyDecl _ ty) -> return ty
711 (Operator ty _ _) -> return ty
712 (CaseOp _ ty _ _ _ _ _) -> return ty
714isConName :: Maybe [String] -> Name -> Context -> Bool
715isConName root n ctxt
716 = or $ do def <- lookupCtxt root n (definitions ctxt)
717 case tfst def of
718 (TyDecl (DCon _ _) _) -> return True
719 (TyDecl (TCon _ _) _) -> return True
720 _ -> return False
722isFnName :: Maybe [String] -> Name -> Context -> Bool
723isFnName root n ctxt
724 = or $ do def <- lookupCtxt root n (definitions ctxt)
725 case tfst def of
726 (Function _ _) -> return True
727 (Operator _ _ _) -> return True
728 (CaseOp _ _ _ _ _ _ _) -> return True
729 _ -> return False
731lookupP :: Maybe [String] -> Name -> Context -> [Term]
732lookupP root n ctxt
733 = do def <- lookupCtxt root n (definitions ctxt)
734 p <- case def of
735 (Function ty tm, a, _) -> return (P Ref n ty, a)
736 (TyDecl nt ty, a, _) -> return (P nt n ty, a)
737 (CaseOp _ ty _ _ _ _ _, a, _) -> return (P Ref n ty, a)
738 (Operator ty _ _, a, _) -> return (P Ref n ty, a)
739 case snd p of
740 Hidden -> []
741 _ -> return (fst p)
743lookupDef :: Maybe [String] -> Name -> Context -> [Def]
744lookupDef root n ctxt = map tfst $ lookupCtxt root n (definitions ctxt)
746lookupDefAcc :: Maybe [String] -> Name -> Bool -> Context -> [(Def, Accessibility)]
747lookupDefAcc root n mkpublic ctxt
748 = map mkp $ lookupCtxt root n (definitions ctxt)
749 where mkp (d, a, _) = if mkpublic then (d, Public) else (d, a)
751lookupTotal :: Name -> Context -> [Totality]
752lookupTotal n ctxt = map mkt $ lookupCtxt Nothing n (definitions ctxt)
753 where mkt (d, a, t) = t
755lookupVal :: Maybe [String] -> Name -> Context -> [Value]
756lookupVal root n ctxt
757 = do def <- lookupCtxt root n (definitions ctxt)
758 case tfst def of
759 (Function _ htm) -> return (veval ctxt [] htm)
760 (TyDecl nt ty) -> return (VP nt n (veval ctxt [] ty))
762lookupTyEnv :: Name -> Env -> Maybe (Int, Type)
763lookupTyEnv n env = li n 0 env where
764 li n i [] = Nothing
765 li n i ((x, b): xs)
766 | n == x = Just (i, binderTy b)
767 | otherwise = li n (i+1) xs