git.iko.soy/Idris-dev
on 611dd97 help sign in
Idris-dev/src/Core/Evaluate.hs
773 lines 33 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,
2 PatternGuards #-}
4module Core.Evaluate(normalise, normaliseTrace, 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 False 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 False ctxt threshold [] env t [AtREPL]
92 quote 0 val) initEval
94normalise :: Context -> Env -> TT Name -> TT Name
95normalise = normaliseTrace False
97normaliseTrace :: Bool -> Context -> Env -> TT Name -> TT Name
98normaliseTrace tr ctxt env t
99 = evalState (do val <- eval tr ctxt threshold [] (map finalEntry env) (finalise t) []
100 quote 0 val) initEval
102specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name
103specialise ctxt env limits t
104 = evalState (do val <- eval False ctxt threshold limits (map finalEntry env) (finalise t) []
105 quote 0 val) (initEval { limited = limits })
107-- Like normalise, but we only reduce functions that are marked as okay to
108-- inline (and probably shouldn't reduce lets?)
110simplify :: Context -> Env -> TT Name -> TT Name
111simplify ctxt env t
112 = evalState (do val <- eval False ctxt threshold []
113 (map finalEntry env) (finalise t) [Simplify]
114 quote 0 val) initEval
116hnf :: Context -> Env -> TT Name -> TT Name
117hnf ctxt env t
118 = evalState (do val <- eval False ctxt threshold [] (map finalEntry env) (finalise t) [HNF]
119 quote 0 val) initEval
122-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))
124finalEntry :: (Name, Binder (TT Name)) -> (Name, Binder (TT Name))
125finalEntry (n, b) = (n, fmap finalise b)
127bindEnv :: EnvTT n -> TT n -> TT n
128bindEnv [] tm = tm
129bindEnv ((n, Let t v):bs) tm = Bind n (NLet t v) (bindEnv bs tm)
130bindEnv ((n, b):bs) tm = Bind n b (bindEnv bs tm)
132unbindEnv :: EnvTT n -> TT n -> TT n
133unbindEnv [] tm = tm
134unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc
136usable :: Name -> [(Name, Int)] -> (Bool, [(Name, Int)])
137usable n [] = (True, [])
138usable n ns = case lookup n ns of
139 Just 0 -> (False, ns)
140 Just i -> (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns)
141 _ -> (True, (n, 100) : filter (\ (n', _) -> n/=n') ns)
143reduction :: Eval ()
144reduction = do ES ns s <- get
145 put (ES ns (s+1))
147-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,
148-- such as we might have during construction of a proof)
150eval :: Bool -> Context -> Int -> [(Name, Int)] -> Env -> TT Name ->
151 [EvalOpt] -> Eval Value
152eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
153 spec = Spec `elem` opts
154 simpl = Simplify `elem` opts
155 atRepl = AtREPL `elem` opts
157 ev ntimes stk top env (P _ n ty)
158 | Just (Let t v) <- lookup n genv = do when (not atRepl) $ step maxred
159 ev ntimes stk top env v
160 ev ntimes_in stk top env (P Ref n ty)
161 | (True, ntimes) <- usable n ntimes_in
162 = do let val = lookupDefAcc Nothing n atRepl ctxt
163 when (not atRepl) $ step maxred
164 case val of
165 [(Function _ tm, Public)] ->
166 ev ntimes (n:stk) True env tm
167 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty
168 return $ VP nt n vty
169 [(CaseOp inl _ _ [] tree _ _, Public)] -> -- unoptimised version
170 if simpl && (not inl || elem n stk)
171 then liftM (VP Ref n) (ev ntimes stk top env ty)
172 else do c <- evCase ntimes (n:stk) top env [] [] tree
173 case c of
174 (Nothing, _) -> liftM (VP Ref n) (ev ntimes stk top env ty)
175 (Just v, _) -> return v
176 _ -> liftM (VP Ref n) (ev ntimes stk top env ty)
177 ev ntimes stk top env (P nt n ty) = liftM (VP nt n) (ev ntimes stk top env ty)
178 ev ntimes stk top env (V i) | i < length env = return $ env !! i
179 | otherwise = return $ VV i
180 ev ntimes stk top env (Bind n (Let t v) sc)
181 = do v' <- ev ntimes stk top env v --(finalise v)
182 when (not atRepl) $ step maxred
183 sc' <- ev ntimes stk top (v' : env) sc
184 wknV (-1) sc'
185 ev ntimes stk top env (Bind n (NLet t v) sc)
186 = do t' <- ev ntimes stk top env (finalise t)
187 v' <- ev ntimes stk top env (finalise v)
188 when (not atRepl) $ step maxred
189 sc' <- ev ntimes stk top (v' : env) sc
190 return $ VBind n (Let t' v') (\x -> return sc')
191 ev ntimes stk top env (Bind n b sc)
192 = do b' <- vbind env b
193 when (not atRepl) $ step maxred
194 return $ VBind n b' (\x -> ev ntimes stk top (x:env) sc)
195 where vbind env t = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
196-- ev ntimes stk top env (App (App (P _ laz _) _) a)
197-- | laz == UN "lazy"
198-- = trace (showEnvDbg genv a) $ ev ntimes stk top env a
199 ev ntimes stk top env (App f a)
200 = do f' <- ev ntimes stk top env f
201 a' <- ev ntimes stk False env a
202 when (not atRepl) $ step maxred
203 evApply ntimes stk top env [a'] f'
204 ev ntimes stk top env (Constant c) = return $ VConstant c
205 ev ntimes stk top env Erased = return VErased
206 ev ntimes stk top env (Set i) = return $ VSet i
208 evApply ntimes stk top env args (VApp f a) =
209 evApply ntimes stk top env (a:args) f
210 evApply ntimes stk top env args f = do when (not atRepl) $ step maxred
211 apply ntimes stk top env f args
213 apply ntimes stk top env f as
214 | length stk > threshold = return $ unload env f as
215 apply ntimes stk top env (VBind n (Lam t) sc) (a:as)
216 = do a' <- sc a
217 app <- apply ntimes stk top env a' as
218 wknV (-1) app
219-- apply ntimes stk False env f args
220-- | spec = specApply ntimes stk env f args
221 apply ntimes_in stk top env f@(VP Ref n ty) args
222 | (True, ntimes) <- usable n ntimes_in
223 = traceWhen traceon (show stk) $
224 do let val = lookupDefAcc Nothing n atRepl ctxt
225 case val of
226 [(CaseOp inl _ _ ns tree _ _, Public)] ->
227 if simpl && (not inl || elem n stk)
228 then return $ unload env (VP Ref n ty) args
229 else do c <- evCase ntimes (n:stk) top env ns args tree
230 case c of
231 (Nothing, _) -> return $ unload env (VP Ref n ty) args
232 (Just v, rest) -> evApply ntimes stk top env rest v
233 [(Operator _ i op, _)] ->
234 if (i <= length args)
235 then case op (take i args) of
236 Nothing -> return $ unload env (VP Ref n ty) args
237 Just v -> evApply ntimes stk top env (drop i args) v
238 else return $ unload env (VP Ref n ty) args
239 _ -> case args of
240 [] -> return f
241 _ -> return $ unload env f args
242 apply ntimes stk top env f (a:as) = return $ unload env f (a:as)
243 apply ntimes stk top env f [] = return f
245-- specApply stk env f@(VP Ref n ty) args
246-- = case lookupCtxt Nothing n statics of
247-- [as] -> if or as
248-- then trace (show (n, map fst (filter (\ (_, s) -> s) (zip args as)))) $
249-- return $ unload env f args
250-- else return $ unload env f args
251-- _ -> return $ unload env f args
252-- specApply stk env f args = return $ unload env f args
254 unload env f [] = f
255 unload env f (a:as) = unload env (VApp f a) as
257 evCase ntimes stk top env ns args tree
258 | length ns <= length args
259 = do let args' = take (length ns) args
260 let rest = drop (length ns) args
261 t <- evTree ntimes stk top env (zipWith (\n t -> (n, t)) ns args') tree
262 return (t, rest)
263 | otherwise = return (Nothing, args)
265 evTree :: [(Name, Int)] -> [Name] -> Bool ->
266 [Value] -> [(Name, Value)] -> SC -> Eval (Maybe Value)
267 evTree ntimes stk top env amap (UnmatchedCase str) = return Nothing
268 evTree ntimes stk top env amap (STerm tm)
269 = do let etm = pToVs (map fst amap) tm
270 etm' <- ev ntimes stk top (map snd amap ++ env) etm
271 return $ Just etm'
272 evTree ntimes stk top env amap (Case n alts)
273 = case lookup n amap of
274 Just v -> do c <- chooseAlt env v (getValArgs v) alts amap
275 case c of
276 Just (altmap, sc) -> evTree ntimes stk top env altmap sc
277 _ -> do c' <- chooseAlt' ntimes stk env v (getValArgs v) alts amap
278 case c' of
279 Just (altmap, sc) -> evTree ntimes stk top env altmap sc
280 _ -> return Nothing
281 _ -> return Nothing
283 chooseAlt' ntimes stk env _ (f, args) alts amap
284 = do f' <- apply ntimes stk True env f args
285 chooseAlt env f' (getValArgs f') alts amap
287 chooseAlt :: [Value] -> Value -> (Value, [Value]) -> [CaseAlt] -> [(Name, Value)] ->
288 Eval (Maybe ([(Name, Value)], SC))
289 chooseAlt env _ (VP (DCon i a) _ _, args) alts amap
290 | Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)
291 | Just v <- findDefault alts = return $ Just (amap, v)
292 chooseAlt env _ (VP (TCon i a) _ _, args) alts amap
293 | Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)
294 | Just v <- findDefault alts = return $ Just (amap, v)
295 chooseAlt env _ (VConstant c, []) alts amap
296 | Just v <- findConst c alts = return $ Just (amap, v)
297 | Just v <- findDefault alts = return $ Just (amap, v)
298 chooseAlt _ _ _ _ _ = return Nothing
300 -- Replace old variable names in the map with new matches
301 -- (This is possibly unnecessary since we make unique names and don't
302 -- allow repeated variables...?)
303 updateAmap newm amap
304 = newm ++ filter (\ (x, _) -> not (elem x (map fst newm))) amap
305 findTag i [] = Nothing
306 findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
307 findTag i (_ : xs) = findTag i xs
309 findDefault [] = Nothing
310 findDefault (DefaultCase sc : xs) = Just sc
311 findDefault (_ : xs) = findDefault xs
313 findConst c [] = Nothing
314 findConst c (ConstCase c' v : xs) | c == c' = Just v
315 findConst IType (ConCase n 1 [] v : xs) = Just v
316 findConst FlType (ConCase n 2 [] v : xs) = Just v
317 findConst ChType (ConCase n 3 [] v : xs) = Just v
318 findConst StrType (ConCase n 4 [] v : xs) = Just v
319 findConst PtrType (ConCase n 5 [] v : xs) = Just v
320 findConst c (_ : xs) = findConst c xs
322 getValArgs tm = getValArgs' tm []
323 getValArgs' (VApp f a) as = getValArgs' f (a:as)
324 getValArgs' f as = (f, as)
326class Quote a where
327 quote :: Int -> a -> Eval (TT Name)
329instance Quote Value where
330 quote i (VP nt n v) = liftM (P nt n) (quote i v)
331 quote i (VV x) = return $ V x
332 quote i (VBind n b sc) = do sc' <- sc (VTmp i)
333 b' <- quoteB b
334 liftM (Bind n b') (quote (i+1) sc')
335 where quoteB t = fmapMB (quote i) t
336 quote i (VApp f a) = liftM2 App (quote i f) (quote i a)
337 quote i (VSet u) = return $ Set u
338 quote i VErased = return $ Erased
339 quote i (VConstant c) = return $ Constant c
340 quote i (VTmp x) = return $ V (i - x - 1)
342instance Quote HNF where
343 quote i (HP nt n t) = return (P nt n t)
344 quote i (HV x) = return $ V x
345 quote i (HBind n b sc) = do sc' <- sc (HTmp i)
346 b' <- quoteB b
347 liftM (Bind n b') (quote (i+1) sc')
348 where quoteB t = fmapMB (quote i) t
349 quote i (HApp f env as) = do f' <- quote i f
350 as' <- mapM (iEnv env) as
351 return $ mkApp f' as'
352 where iEnv [] a = return a
353 iEnv (x:xs) a = do x' <- quote i x
354 iEnv xs (weakenTm (-1) (instantiate x' a))
355 quote i (HSet u) = return $ Set u
356 quote i (HConstant c) = return $ Constant c
357 quote i (HTmp x) = return $ V (i - x - 1)
359wknV :: Int -> Value -> Eval Value
360wknV i (VV x) = return $ VV (x + i)
361wknV i (VBind n b sc) = do b' <- fmapMB (wknV i) b
362 return $ VBind n b' (\x -> do x' <- sc x
363 wknV i x')
364wknV i (VApp f a) = liftM2 VApp (wknV i f) (wknV i a)
365wknV i t = return t
367wknH :: Int -> HNF -> Eval HNF
368wknH i (HV x) = return $ HV (x + i)
369wknH i (HBind n b sc) = do b' <- fmapMB (wknH i) b
370 return $ HBind n b' (\x -> do x' <- sc x
371 wknH i x')
372wknH i (HApp f env as) = liftM3 HApp (wknH i f) (return env)
373 (return as)
374wknH i t = return t
376-- HEAD NORMAL FORM ---------------------------------------------------------
378eval_hnf :: Context -> Ctxt [Bool] -> Env -> TT Name -> Eval HNF
379eval_hnf ctxt statics genv tm = ev [] tm where
380 ev :: [HNF] -> TT Name -> Eval HNF
381 ev env (P _ n ty)
382 | Just (Let t v) <- lookup n genv = ev env v
383 ev env (P Ref n ty) = case lookupDef Nothing n ctxt of
384 [Function _ t] -> ev env t
385 [TyDecl nt ty] -> return $ HP nt n ty
386 [CaseOp inl _ _ [] tree _ _] ->
387 do c <- evCase env [] [] tree
388 case c of
389 (Nothing, _, _) -> return $ HP Ref n ty
390 (Just v, _, _) -> return v
391 _ -> return $ HP Ref n ty
392 ev env (P nt n ty) = return $ HP nt n ty
393 ev env (V i) | i < length env = return $ env !! i
394 | otherwise = return $ HV i
395 ev env (Bind n (Let t v) sc)
396 = do v' <- ev env (finalise v)
397 sc' <- ev (v' : env) sc
398 wknH (-1) sc'
399 ev env (Bind n b sc)
400 = do b' <- hbind env b
401 return $ HBind n b' (\x -> ev (x : env) sc)
402 where hbind env t = fmapMB (\tm -> ev env (finalise tm)) t
403 ev env (App f a) = evApply env [a] f
404 ev env (Constant c) = return $ HConstant c
405 ev env (Set i) = return $ HSet i
407 evApply env args (App f a) = evApply env (a : args) f
408 evApply env args f = do f' <- ev env f
409 apply env f' args
411 apply env (HBind n (Lam t) sc) (a:as) = do a' <- ev env a
412 sc' <- sc a'
413 app <- apply env sc' as
414 wknH (-1) app
415 apply env (HP Ref n ty) args
416 | [CaseOp _ _ _ ns tree _ _] <- lookupDef Nothing n ctxt
417 = do c <- evCase env ns args tree
418 case c of
419 (Nothing, _, env') -> return $ unload env' (HP Ref n ty) args
420 (Just v, rest, env') -> do v' <- quote 0 v
421 apply env' v rest
422-- | Just (Operator _ i op) <- lookupDef n ctxt
423-- = if (i <= length args)
424-- then case op (take i args) of
425-- Nothing -> return $ unload env (HP Ref n ty) args
426-- Just v -> evApply env (drop i args) v
427-- else return $ unload env (HP Ref n ty) args
428 apply env f (a:as) = return $ unload env f (a:as)
429 apply env f [] = return f
431 unload env f [] = f
432 unload env f as = HApp f env as
434 evCase env ns args tree
435 | length ns <= length args
436 = do let args' = take (length ns) args
437 let rest = drop (length ns) args
438 (t, env') <- evTree env (zipWith (\n t -> (n, t)) ns args') tree
439 return (t, rest, env')
440 | otherwise = return (Nothing, args, env)
442 evTree :: [HNF] -> [(Name, TT Name)] -> SC -> Eval (Maybe HNF, [HNF])
443 evTree env amap (UnmatchedCase str) = return (Nothing, env)
444 evTree env amap (STerm tm)
445 = do let etm = pToVs (map fst amap) tm
446 amap' <- mapM (ev env) (map snd amap)
447 envw <- mapM (wknH (length amap)) env
448 let env' = amap' ++ envw
449 etm' <- trace (show etm) $ ev env' etm
450 etmq <- quote 0 etm'
451 trace ("Ev: " ++ show (etm, etmq)) $ return $ (Just etm', env')
452 evTree env amap (Case n alts)
453 = case lookup n amap of
454 Just v -> do v' <- ev env v
455 case chooseAlt v' (getValArgs v') alts amap of
456 Just (altmap, sc) -> evTree env altmap sc
457 _ -> return (Nothing, env)
459 chooseAlt :: HNF -> (HNF, [HNF], [TT Name]) ->
460 [CaseAlt] -> [(Name, TT Name)] ->
461 Maybe ([(Name, TT Name)], SC)
462 chooseAlt _ (HP (DCon i a) _ _, env, args) alts amap
463 | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)
464 | Just v <- findDefault alts = Just (amap, v)
465 chooseAlt _ (HP (TCon i a) _ _, env, args) alts amap
466 | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)
467 | Just v <- findDefault alts = Just (amap, v)
468 chooseAlt _ (HConstant c, env, []) alts amap
469 | Just v <- findConst c alts = Just (amap, v)
470 | Just v <- findDefault alts = Just (amap, v)
471 chooseAlt _ _ _ _ = Nothing
473 -- Replace old variable names in the map with new matches
474 -- (This is possibly unnecessary since we make unique names and don't
475 -- allow repeated variables...?)
476 updateAmap newm amap
477 = newm ++ filter (\ (x, _) -> not (elem x (map fst newm))) amap
478 findTag i [] = Nothing
479 findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
480 findTag i (_ : xs) = findTag i xs
482 findDefault [] = Nothing
483 findDefault (DefaultCase sc : xs) = Just sc
484 findDefault (_ : xs) = findDefault xs
486 findConst c [] = Nothing
487 findConst c (ConstCase c' v : xs) | c == c' = Just v
488 findConst IType (ConCase n 1 [] v : xs) = Just v
489 findConst FlType (ConCase n 2 [] v : xs) = Just v
490 findConst ChType (ConCase n 3 [] v : xs) = Just v
491 findConst StrType (ConCase n 4 [] v : xs) = Just v
492 findConst PtrType (ConCase n 5 [] v : xs) = Just v
493 findConst c (_ : xs) = findConst c xs
495 getValArgs (HApp t env args) = (t, env, args)
496 getValArgs t = (t, [], [])
498convEq' ctxt x y = evalStateT (convEq ctxt x y) (0, [])
500convEq :: Context -> TT Name -> TT Name -> StateT UCs TC Bool
501convEq ctxt = ceq [] where
502 ceq :: [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
503 ceq ps (P xt x _) (P yt y _)
504 | (xt == yt && x ==y ) || (x, y) `elem` ps || (y,x) `elem` ps = return True
505 | otherwise = sameDefs ps x y
506 ceq ps (V x) (V y) = return (x == y)
507 ceq ps (Bind _ xb xs) (Bind _ yb ys)
508 = liftM2 (&&) (ceqB ps xb yb) (ceq ps xs ys)
509 where
510 ceqB ps (Let v t) (Let v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')
511 ceqB ps (Guess v t) (Guess v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')
512 ceqB ps b b' = ceq ps (binderTy b) (binderTy b')
513 ceq ps (App fx ax) (App fy ay) = liftM2 (&&) (ceq ps fx fy) (ceq ps ax ay)
514 ceq ps (Constant x) (Constant y) = return (x == y)
515 ceq ps (Set x) (Set y) = do (v, cs) <- get
516 put (v, ULE x y : cs)
517 return True
518 ceq ps Erased _ = return True
519 ceq ps _ Erased = return True
520 ceq ps _ _ = return False
522 caseeq ps (Case n cs) (Case n' cs') = caseeqA ((n,n'):ps) cs cs'
523 where
524 caseeqA ps (ConCase x i as sc : rest) (ConCase x' i' as' sc' : rest')
525 = do q1 <- caseeq (zip as as' ++ ps) sc sc'
526 q2 <- caseeqA ps rest rest'
527 return $ x == x' && i == i' && q1 && q2
528 caseeqA ps (ConstCase x sc : rest) (ConstCase x' sc' : rest')
529 = do q1 <- caseeq ps sc sc'
530 q2 <- caseeqA ps rest rest'
531 return $ x == x' && q1 && q2
532 caseeqA ps (DefaultCase sc : rest) (DefaultCase sc' : rest')
533 = liftM2 (&&) (caseeq ps sc sc') (caseeqA ps rest rest')
534 caseeqA ps [] [] = return True
535 caseeqA ps _ _ = return False
536 caseeq ps (STerm x) (STerm y) = ceq ps x y
537 caseeq ps (UnmatchedCase _) (UnmatchedCase _) = return True
538 caseeq ps _ _ = return False
540 sameDefs ps x y = case (lookupDef Nothing x ctxt, lookupDef Nothing y ctxt) of
541 ([Function _ xdef], [Function _ ydef])
542 -> ceq ((x,y):ps) xdef ydef
543 ([CaseOp _ _ _ _ xdef _ _],
544 [CaseOp _ _ _ _ ydef _ _])
545 -> caseeq ((x,y):ps) xdef ydef
546 _ -> return False
548-- SPECIALISATION -----------------------------------------------------------
549-- We need too much control to be able to do this by tweaking the main
550-- evaluator
552spec :: Context -> Ctxt [Bool] -> Env -> TT Name -> Eval (TT Name)
553spec ctxt statics genv tm = error "spec undefined"
555-- CONTEXTS -----------------------------------------------------------------
557{- A definition is either a simple function (just an expression with a type),
558 a constant, which could be a data or type constructor, an axiom or as an
559 yet undefined function, or an Operator.
560 An Operator is a function which explains how to reduce.
561 A CaseOp is a function defined by a simple case tree -}
563data Def = Function Type Term
564 | TyDecl NameType Type
565 | Operator Type Int ([Value] -> Maybe Value)
566 | CaseOp Bool Type [([Name], Term, Term)] -- Bool for inlineable
567 [Name] SC -- Compile time case definition
568 [Name] SC -- Run time cae definitions
569{-!
570deriving instance Binary Def
571!-}
573instance Show Def where
574 show (Function ty tm) = "Function: " ++ show (ty, tm)
575 show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty
576 show (Operator ty _ _) = "Operator: " ++ show ty
577 show (CaseOp _ ty ps ns sc ns' sc')
578 = "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++
579 show ns ++ " " ++ show sc ++ "\n" ++
580 show ns' ++ " " ++ show sc'
581-- We need this for serialising Def. Fortunately, it never gets used because
582-- we'll never serialise a primitive operator
584instance Binary (a -> b) where
585 put x = return ()
586 get = error "Getting a function"
588-------
590-- Frozen => doesn't reduce
591-- Hidden => doesn't reduce and invisible to type checker
593data Accessibility = Public | Frozen | Hidden
594 deriving (Show, Eq)
596data Totality = Total [Int] -- well-founded arguments
597 | Partial PReason
598 | Unchecked
599 deriving Eq
601data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name
602 | Mutual [Name]
603 deriving (Show, Eq)
605instance Show Totality where
606 show (Total args)= "Total" -- ++ show args ++ " decreasing arguments"
607 show Unchecked = "not yet checked for totality"
608 show (Partial Itself) = "possibly not total as it is not well founded"
609 show (Partial NotCovering) = "not total as there are missing cases"
610 show (Partial NotPositive) = "not strictly positive"
611 show (Partial (Other ns)) = "possibly not total due to: " ++ showSep ", " (map show ns)
612 show (Partial (Mutual ns)) = "possibly not total due to mutual recursive path " ++
613 showSep " --> " (map show ns)
615{-!
616deriving instance Binary Accessibility
617!-}
619{-!
620deriving instance Binary Totality
621!-}
623{-!
624deriving instance Binary PReason
625!-}
627data Context = MkContext { uconstraints :: [UConstraint],
628 next_tvar :: Int,
629 definitions :: Ctxt (Def, Accessibility, Totality) }
631initContext = MkContext [] 0 emptyContext
633ctxtAlist :: Context -> [(Name, Def)]
634ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)
636veval ctxt env t = evalState (eval False ctxt threshold [] env t []) initEval
638addToCtxt :: Name -> Term -> Type -> Context -> Context
639addToCtxt n tm ty uctxt
640 = let ctxt = definitions uctxt
641 ctxt' = addDef n (Function ty tm, Public, Unchecked) ctxt in
642 uctxt { definitions = ctxt' }
644setAccess :: Name -> Accessibility -> Context -> Context
645setAccess n a uctxt
646 = let ctxt = definitions uctxt
647 ctxt' = updateDef n (\ (d, _, t) -> (d, a, t)) ctxt in
648 uctxt { definitions = ctxt' }
650setTotal :: Name -> Totality -> Context -> Context
651setTotal n t uctxt
652 = let ctxt = definitions uctxt
653 ctxt' = updateDef n (\ (d, a, _) -> (d, a, t)) ctxt in
654 uctxt { definitions = ctxt' }
656addCtxtDef :: Name -> Def -> Context -> Context
657addCtxtDef n d c = let ctxt = definitions c
658 ctxt' = addDef n (d, Public, Unchecked) ctxt in
659 c { definitions = ctxt' }
661addTyDecl :: Name -> Type -> Context -> Context
662addTyDecl n ty uctxt
663 = let ctxt = definitions uctxt
664 ctxt' = addDef n (TyDecl Ref ty, Public, Unchecked) ctxt in
665 uctxt { definitions = ctxt' }
667addDatatype :: Datatype Name -> Context -> Context
668addDatatype (Data n tag ty cons) uctxt
669 = let ctxt = definitions uctxt
670 ty' = normalise uctxt [] ty
671 ctxt' = addCons 0 cons (addDef n
672 (TyDecl (TCon tag (arity ty')) ty, Public, Unchecked) ctxt) in
673 uctxt { definitions = ctxt' }
674 where
675 addCons tag [] ctxt = ctxt
676 addCons tag ((n, ty) : cons) ctxt
677 = let ty' = normalise uctxt [] ty in
678 addCons (tag+1) cons (addDef n
679 (TyDecl (DCon tag (arity ty')) ty, Public, Unchecked) ctxt)
681addCasedef :: Name -> Bool -> Bool -> Bool ->
682 [([Name], Term, Term)] -> [([Name], Term, Term)] ->
683 Type -> Context -> Context
684addCasedef n alwaysInline tcase covering ps psrt ty uctxt
685 = let ctxt = definitions uctxt
686 ps' = ps -- simpl ps in
687 ctxt' = case (simpleCase tcase covering (FC "" 0) ps',
688 simpleCase tcase covering (FC "" 0) psrt) of
689 (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) ->
690 let inl = alwaysInline in
691 addDef n (CaseOp inl ty ps args sc args' sc',
692 Public, Unchecked) ctxt in
693 uctxt { definitions = ctxt' }
694 where simpl [] = []
695 simpl ((l,r) : xs) = (l, simplify uctxt [] r) : simpl xs
697addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> Context
698addOperator n ty a op uctxt
699 = let ctxt = definitions uctxt
700 ctxt' = addDef n (Operator ty a op, Public, Unchecked) ctxt in
701 uctxt { definitions = ctxt' }
703tfst (a, _, _) = a
705lookupNames :: Maybe [String] -> Name -> Context -> [Name]
706lookupNames root n ctxt
707 = let ns = lookupCtxtName root n (definitions ctxt) in
708 map fst ns
710lookupTy :: Maybe [String] -> Name -> Context -> [Type]
711lookupTy root n ctxt
712 = do def <- lookupCtxt root n (definitions ctxt)
713 case tfst def of
714 (Function ty _) -> return ty
715 (TyDecl _ ty) -> return ty
716 (Operator ty _ _) -> return ty
717 (CaseOp _ ty _ _ _ _ _) -> return ty
719isConName :: Maybe [String] -> Name -> Context -> Bool
720isConName root n ctxt
721 = or $ do def <- lookupCtxt root n (definitions ctxt)
722 case tfst def of
723 (TyDecl (DCon _ _) _) -> return True
724 (TyDecl (TCon _ _) _) -> return True
725 _ -> return False
727isFnName :: Maybe [String] -> Name -> Context -> Bool
728isFnName root n ctxt
729 = or $ do def <- lookupCtxt root n (definitions ctxt)
730 case tfst def of
731 (Function _ _) -> return True
732 (Operator _ _ _) -> return True
733 (CaseOp _ _ _ _ _ _ _) -> return True
734 _ -> return False
736lookupP :: Maybe [String] -> Name -> Context -> [Term]
737lookupP root n ctxt
738 = do def <- lookupCtxt root n (definitions ctxt)
739 p <- case def of
740 (Function ty tm, a, _) -> return (P Ref n ty, a)
741 (TyDecl nt ty, a, _) -> return (P nt n ty, a)
742 (CaseOp _ ty _ _ _ _ _, a, _) -> return (P Ref n ty, a)
743 (Operator ty _ _, a, _) -> return (P Ref n ty, a)
744 case snd p of
745 Hidden -> []
746 _ -> return (fst p)
748lookupDef :: Maybe [String] -> Name -> Context -> [Def]
749lookupDef root n ctxt = map tfst $ lookupCtxt root n (definitions ctxt)
751lookupDefAcc :: Maybe [String] -> Name -> Bool -> Context -> [(Def, Accessibility)]
752lookupDefAcc root n mkpublic ctxt
753 = map mkp $ lookupCtxt root n (definitions ctxt)
754 where mkp (d, a, _) = if mkpublic then (d, Public) else (d, a)
756lookupTotal :: Name -> Context -> [Totality]
757lookupTotal n ctxt = map mkt $ lookupCtxt Nothing n (definitions ctxt)
758 where mkt (d, a, t) = t
760lookupVal :: Maybe [String] -> Name -> Context -> [Value]
761lookupVal root n ctxt
762 = do def <- lookupCtxt root n (definitions ctxt)
763 case tfst def of
764 (Function _ htm) -> return (veval ctxt [] htm)
765 (TyDecl nt ty) -> return (VP nt n (veval ctxt [] ty))
767lookupTyEnv :: Name -> Env -> Maybe (Int, Type)
768lookupTyEnv n env = li n 0 env where
769 li n i [] = Nothing
770 li n i ((x, b): xs)
771 | n == x = Just (i, binderTy b)
772 | otherwise = li n (i+1) xs