git.iko.soy/Idris-dev
on aa7262e help sign in
Idris-dev/src/Core/Evaluate.hs
838 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(..), Accessibility(..), Totality(..), PReason(..),
7 Context, initContext, ctxtAlist, uconstraints, next_tvar,
8 addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl,
9 addDatatype, addCasedef, simplifyCasedef, addOperator,
10 lookupNames, lookupTy, lookupP, lookupDef, lookupVal,
11 lookupTotal, 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 Bool | 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 -> Bool -> Env -> TT Name -> TT Name
111simplify ctxt runtime env t
112 = evalState (do val <- eval False ctxt threshold [(UN "lazy", 0),
113 (UN "par", 0),
114 (UN "fork", 0)]
115 (map finalEntry env) (finalise t)
116 [Simplify runtime]
117 quote 0 val) initEval
119hnf :: Context -> Env -> TT Name -> TT Name
120hnf ctxt env t
121 = evalState (do val <- eval False ctxt threshold [] (map finalEntry env) (finalise t) [HNF]
122 quote 0 val) initEval
125-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))
127finalEntry :: (Name, Binder (TT Name)) -> (Name, Binder (TT Name))
128finalEntry (n, b) = (n, fmap finalise b)
130bindEnv :: EnvTT n -> TT n -> TT n
131bindEnv [] tm = tm
132bindEnv ((n, Let t v):bs) tm = Bind n (NLet t v) (bindEnv bs tm)
133bindEnv ((n, b):bs) tm = Bind n b (bindEnv bs tm)
135unbindEnv :: EnvTT n -> TT n -> TT n
136unbindEnv [] tm = tm
137unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc
139usable :: Bool -> Name -> [(Name, Int)] -> (Bool, [(Name, Int)])
140usable _ _ ns@((MN 0 "STOP", _) : _) = (False, ns)
141usable True (UN "io_bind") ns = (False, ns)
142usable s n [] = (True, [])
143usable s n ns = case lookup n ns of
144 Just 0 -> (False, ns)
145 Just i -> (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns)
146 _ -> if s then (True, (n, 0) : filter (\ (n', _) -> n/=n') ns)
147 else (True, (n, 100) : filter (\ (n', _) -> n/=n') ns)
149reduction :: Eval ()
150reduction = do ES ns s <- get
151 put (ES ns (s+1))
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)
156eval :: Bool -> Context -> Int -> [(Name, Int)] -> Env -> TT Name ->
157 [EvalOpt] -> Eval Value
158eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where
159 spec = Spec `elem` opts
160 simpl = Simplify True `elem` opts
161 atRepl = AtREPL `elem` opts
163 canSimplify inl inr n stk
164 = (Simplify False `elem` opts && (not inl || elem n stk))
165 || (Simplify True `elem` opts && (not inr || elem n stk))
167 ev ntimes stk top env (P _ n ty)
168 | Just (Let t v) <- lookup n genv = do when (not atRepl) $ step maxred
169 ev ntimes stk top env v
170 ev ntimes_in stk top env (P Ref n ty)
171 | (True, ntimes) <- usable simpl n ntimes_in
172 = do let val = lookupDefAcc Nothing n atRepl ctxt
173 when (not atRepl) $ step maxred
174 case val of
175 [(Function _ tm, Public)] ->
176 ev ntimes (n:stk) True env tm
177 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty
178 return $ VP nt n vty
179 [(CaseOp inl inr _ _ _ [] tree _ _, acc)]
180 | acc == Public || simpl -> -- unoptimised version
181 if canSimplify inl inr n stk
182 then liftM (VP Ref n) (ev ntimes stk top env ty)
183 else do c <- evCase ntimes (n:stk) top env [] [] tree
184 case c of
185 (Nothing, _) -> liftM (VP Ref n) (ev ntimes stk top env ty)
186 (Just v, _) -> return v
187 _ -> liftM (VP Ref n) (ev ntimes stk top env ty)
188 ev ntimes stk top env (P nt n ty) = liftM (VP nt n) (ev ntimes stk top env ty)
189 ev ntimes stk top env (V i) | i < length env = return $ env !! i
190 | otherwise = return $ VV i
191 ev ntimes stk top env (Bind n (Let t v) sc)
192 | not simpl -- || vinstances 0 sc < 2
193 = do v' <- ev ntimes stk top env v --(finalise v)
194 when (not atRepl) $ step maxred
195 sc' <- ev ntimes stk top (v' : env) sc
196 wknV (-1) sc'
197 | otherwise
198 = do t' <- ev ntimes stk top env t
199 v' <- ev ntimes stk top env v --(finalise v)
200 when (not atRepl) $ step maxred
201 sc' <- ev ntimes stk top (v' : env) sc
202 return $ VBind n (Let t' v') (\x -> return sc')
203 ev ntimes stk top env (Bind n (NLet t v) sc)
204 = do t' <- ev ntimes stk top env (finalise t)
205 v' <- ev ntimes stk top env (finalise v)
206 when (not atRepl) $ step maxred
207 sc' <- ev ntimes stk top (v' : env) sc
208 return $ VBind n (Let t' v') (\x -> return sc')
209 ev ntimes stk top env (Bind n b sc)
210 = do b' <- vbind env b
211 when (not atRepl) $ step maxred
212 return $ VBind n b' (\x -> ev ntimes stk top (x:env) sc)
213 where vbind env t
214 | simpl
215 = fmapMB (\tm -> ev ((MN 0 "STOP", 0) : ntimes)
216 stk top env (finalise tm)) t
217 | otherwise
218 = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
219-- ev ntimes stk top env (App (App (P _ laz _) _) a)
220-- | laz == UN "lazy"
221-- = trace (showEnvDbg genv a) $ ev ntimes stk top env a
222 ev ntimes stk top env (App f a)
223 = do f' <- ev ntimes stk top env f
224 a' <- ev ntimes stk False env a
225 when (not atRepl) $ step maxred
226 evApply ntimes stk top env [a'] f'
227 ev ntimes stk top env (Constant c) = return $ VConstant c
228 ev ntimes stk top env Erased = return VErased
229 ev ntimes stk top env (Set i) = return $ VSet i
231 evApply ntimes stk top env args (VApp f a) =
232 evApply ntimes stk top env (a:args) f
233 evApply ntimes stk top env args f = do when (not atRepl) $ step maxred
234 apply ntimes stk top env f args
236 apply ntimes stk top env f as
237 | length stk > threshold = return $ unload env f as
238 apply ntimes stk top env (VBind n (Lam t) sc) (a:as)
239 = do a' <- sc a
240 app <- apply ntimes stk top env a' as
241 wknV (-1) app
242-- apply ntimes stk False env f args
243-- | spec = specApply ntimes stk env f args
244 apply ntimes_in stk top env f@(VP Ref n ty) args
245 | (True, ntimes) <- usable simpl n ntimes_in
246 = traceWhen traceon (show stk) $
247 do let val = lookupDefAcc Nothing n atRepl ctxt
248 case val of
249 [(CaseOp inl inr _ _ _ ns tree _ _, acc)]
250 | acc == Public || simpl -> -- unoptimised version
251 if canSimplify inl inr n stk
252 then return $ unload env (VP Ref n ty) args
253 else do c <- evCase ntimes (n:stk) top env ns args tree
254 case c of
255 (Nothing, _) -> return $ unload env (VP Ref n ty) args
256 (Just v, rest) -> evApply ntimes stk top env rest v
257 [(Operator _ i op, _)] ->
258 if (i <= length args)
259 then case op (take i args) of
260 Nothing -> return $ unload env (VP Ref n ty) args
261 Just v -> evApply ntimes stk top env (drop i args) v
262 else return $ unload env (VP Ref n ty) args
263 _ -> case args of
264 [] -> return f
265 _ -> return $ unload env f args
266 apply ntimes stk top env f (a:as) = return $ unload env f (a:as)
267 apply ntimes stk top env f [] = return f
269-- specApply stk env f@(VP Ref n ty) args
270-- = case lookupCtxt Nothing n statics of
271-- [as] -> if or as
272-- then trace (show (n, map fst (filter (\ (_, s) -> s) (zip args as)))) $
273-- return $ unload env f args
274-- else return $ unload env f args
275-- _ -> return $ unload env f args
276-- specApply stk env f args = return $ unload env f args
278 unload env f [] = f
279 unload env f (a:as) = unload env (VApp f a) as
281 evCase ntimes stk top env ns args tree
282 | length ns <= length args
283 = do let args' = take (length ns) args
284 let rest = drop (length ns) args
285 t <- evTree ntimes stk top env (zipWith (\n t -> (n, t)) ns args') tree
286 return (t, rest)
287 | otherwise = return (Nothing, args)
289 evTree :: [(Name, Int)] -> [Name] -> Bool ->
290 [Value] -> [(Name, Value)] -> SC -> Eval (Maybe Value)
291 evTree ntimes stk top env amap (UnmatchedCase str) = return Nothing
292 evTree ntimes stk top env amap (STerm tm)
293 = do let etm = pToVs (map fst amap) tm
294 etm' <- ev ntimes stk top (map snd amap ++ env) etm
295 return $ Just etm'
296 evTree ntimes stk top env amap (Case n alts)
297 = case lookup n amap of
298 Just v -> do c <- chooseAlt env v (getValArgs v) alts amap
299 case c of
300 Just (altmap, sc) -> evTree ntimes stk top env altmap sc
301 _ -> do c' <- chooseAlt' ntimes stk env v (getValArgs v) alts amap
302 case c' of
303 Just (altmap, sc) -> evTree ntimes stk top env altmap sc
304 _ -> return Nothing
305 _ -> return Nothing
307 chooseAlt' ntimes stk env _ (f, args) alts amap
308 = do f' <- apply ntimes stk True env f args
309 chooseAlt env f' (getValArgs f') alts amap
311 chooseAlt :: [Value] -> Value -> (Value, [Value]) -> [CaseAlt] -> [(Name, Value)] ->
312 Eval (Maybe ([(Name, Value)], SC))
313 chooseAlt env _ (VP (DCon i a) _ _, args) alts amap
314 | Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)
315 | Just v <- findDefault alts = return $ Just (amap, v)
316 chooseAlt env _ (VP (TCon i a) _ _, args) alts amap
317 | Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)
318 | Just v <- findDefault alts = return $ Just (amap, v)
319 chooseAlt env _ (VConstant c, []) alts amap
320 | Just v <- findConst c alts = return $ Just (amap, v)
321 | Just v <- findDefault alts = return $ Just (amap, v)
322 chooseAlt _ _ _ _ _ = return Nothing
324 -- Replace old variable names in the map with new matches
325 -- (This is possibly unnecessary since we make unique names and don't
326 -- allow repeated variables...?)
327 updateAmap newm amap
328 = newm ++ filter (\ (x, _) -> not (elem x (map fst newm))) amap
329 findTag i [] = Nothing
330 findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
331 findTag i (_ : xs) = findTag i xs
333 findDefault [] = Nothing
334 findDefault (DefaultCase sc : xs) = Just sc
335 findDefault (_ : xs) = findDefault xs
337 findConst c [] = Nothing
338 findConst c (ConstCase c' v : xs) | c == c' = Just v
339 findConst IType (ConCase n 1 [] v : xs) = Just v
340 findConst FlType (ConCase n 2 [] v : xs) = Just v
341 findConst ChType (ConCase n 3 [] v : xs) = Just v
342 findConst StrType (ConCase n 4 [] v : xs) = Just v
343 findConst PtrType (ConCase n 5 [] v : xs) = Just v
344 findConst c (_ : xs) = findConst c xs
346 getValArgs tm = getValArgs' tm []
347 getValArgs' (VApp f a) as = getValArgs' f (a:as)
348 getValArgs' f as = (f, as)
350class Quote a where
351 quote :: Int -> a -> Eval (TT Name)
353instance Quote Value where
354 quote i (VP nt n v) = liftM (P nt n) (quote i v)
355 quote i (VV x) = return $ V x
356 quote i (VBind n b sc) = do sc' <- sc (VTmp i)
357 b' <- quoteB b
358 liftM (Bind n b') (quote (i+1) sc')
359 where quoteB t = fmapMB (quote i) t
360 quote i (VApp f a) = liftM2 App (quote i f) (quote i a)
361 quote i (VSet u) = return $ Set u
362 quote i VErased = return $ Erased
363 quote i (VConstant c) = return $ Constant c
364 quote i (VTmp x) = return $ V (i - x - 1)
366instance Quote HNF where
367 quote i (HP nt n t) = return (P nt n t)
368 quote i (HV x) = return $ V x
369 quote i (HBind n b sc) = do sc' <- sc (HTmp i)
370 b' <- quoteB b
371 liftM (Bind n b') (quote (i+1) sc')
372 where quoteB t = fmapMB (quote i) t
373 quote i (HApp f env as) = do f' <- quote i f
374 as' <- mapM (iEnv env) as
375 return $ mkApp f' as'
376 where iEnv [] a = return a
377 iEnv (x:xs) a = do x' <- quote i x
378 iEnv xs (weakenTm (-1) (instantiate x' a))
379 quote i (HSet u) = return $ Set u
380 quote i (HConstant c) = return $ Constant c
381 quote i (HTmp x) = return $ V (i - x - 1)
383wknV :: Int -> Value -> Eval Value
384wknV i (VV x) = return $ VV (x + i)
385wknV i (VBind n b sc) = do b' <- fmapMB (wknV i) b
386 return $ VBind n b' (\x -> do x' <- sc x
387 wknV i x')
388wknV i (VApp f a) = liftM2 VApp (wknV i f) (wknV i a)
389wknV i t = return t
391wknH :: Int -> HNF -> Eval HNF
392wknH i (HV x) = return $ HV (x + i)
393wknH i (HBind n b sc) = do b' <- fmapMB (wknH i) b
394 return $ HBind n b' (\x -> do x' <- sc x
395 wknH i x')
396wknH i (HApp f env as) = liftM3 HApp (wknH i f) (return env)
397 (return as)
398wknH i t = return t
400-- HEAD NORMAL FORM ---------------------------------------------------------
402eval_hnf :: Context -> Ctxt [Bool] -> Env -> TT Name -> Eval HNF
403eval_hnf ctxt statics genv tm = ev [] tm where
404 ev :: [HNF] -> TT Name -> Eval HNF
405 ev env (P _ n ty)
406 | Just (Let t v) <- lookup n genv = ev env v
407 ev env (P Ref n ty) = case lookupDef Nothing n ctxt of
408 [Function _ t] -> ev env t
409 [TyDecl nt ty] -> return $ HP nt n ty
410 [CaseOp inl _ _ _ _ [] tree _ _] ->
411 do c <- evCase env [] [] tree
412 case c of
413 (Nothing, _, _) -> return $ HP Ref n ty
414 (Just v, _, _) -> return v
415 _ -> return $ HP Ref n ty
416 ev env (P nt n ty) = return $ HP nt n ty
417 ev env (V i) | i < length env = return $ env !! i
418 | otherwise = return $ HV i
419 ev env (Bind n (Let t v) sc)
420 = do v' <- ev env (finalise v)
421 sc' <- ev (v' : env) sc
422 wknH (-1) sc'
423 ev env (Bind n b sc)
424 = do b' <- hbind env b
425 return $ HBind n b' (\x -> ev (x : env) sc)
426 where hbind env t = fmapMB (\tm -> ev env (finalise tm)) t
427 ev env (App f a) = evApply env [a] f
428 ev env (Constant c) = return $ HConstant c
429 ev env (Set i) = return $ HSet i
431 evApply env args (App f a) = evApply env (a : args) f
432 evApply env args f = do f' <- ev env f
433 apply env f' args
435 apply env (HBind n (Lam t) sc) (a:as) = do a' <- ev env a
436 sc' <- sc a'
437 app <- apply env sc' as
438 wknH (-1) app
439 apply env (HP Ref n ty) args
440 | [CaseOp _ _ _ _ _ ns tree _ _] <- lookupDef Nothing n ctxt
441 = do c <- evCase env ns args tree
442 case c of
443 (Nothing, _, env') -> return $ unload env' (HP Ref n ty) args
444 (Just v, rest, env') -> do v' <- quote 0 v
445 apply env' v rest
446-- | Just (Operator _ i op) <- lookupDef n ctxt
447-- = if (i <= length args)
448-- then case op (take i args) of
449-- Nothing -> return $ unload env (HP Ref n ty) args
450-- Just v -> evApply env (drop i args) v
451-- else return $ unload env (HP Ref n ty) args
452 apply env f (a:as) = return $ unload env f (a:as)
453 apply env f [] = return f
455 unload env f [] = f
456 unload env f as = HApp f env as
458 evCase env ns args tree
459 | length ns <= length args
460 = do let args' = take (length ns) args
461 let rest = drop (length ns) args
462 (t, env') <- evTree env (zipWith (\n t -> (n, t)) ns args') tree
463 return (t, rest, env')
464 | otherwise = return (Nothing, args, env)
466 evTree :: [HNF] -> [(Name, TT Name)] -> SC -> Eval (Maybe HNF, [HNF])
467 evTree env amap (UnmatchedCase str) = return (Nothing, env)
468 evTree env amap (STerm tm)
469 = do let etm = pToVs (map fst amap) tm
470 amap' <- mapM (ev env) (map snd amap)
471 envw <- mapM (wknH (length amap)) env
472 let env' = amap' ++ envw
473 etm' <- trace (show etm) $ ev env' etm
474 etmq <- quote 0 etm'
475 trace ("Ev: " ++ show (etm, etmq)) $ return $ (Just etm', env')
476 evTree env amap (Case n alts)
477 = case lookup n amap of
478 Just v -> do v' <- ev env v
479 case chooseAlt v' (getValArgs v') alts amap of
480 Just (altmap, sc) -> evTree env altmap sc
481 _ -> return (Nothing, env)
483 chooseAlt :: HNF -> (HNF, [HNF], [TT Name]) ->
484 [CaseAlt] -> [(Name, TT Name)] ->
485 Maybe ([(Name, TT Name)], SC)
486 chooseAlt _ (HP (DCon i a) _ _, env, args) alts amap
487 | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)
488 | Just v <- findDefault alts = Just (amap, v)
489 chooseAlt _ (HP (TCon i a) _ _, env, args) alts amap
490 | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)
491 | Just v <- findDefault alts = Just (amap, v)
492 chooseAlt _ (HConstant c, env, []) alts amap
493 | Just v <- findConst c alts = Just (amap, v)
494 | Just v <- findDefault alts = Just (amap, v)
495 chooseAlt _ _ _ _ = Nothing
497 -- Replace old variable names in the map with new matches
498 -- (This is possibly unnecessary since we make unique names and don't
499 -- allow repeated variables...?)
500 updateAmap newm amap
501 = newm ++ filter (\ (x, _) -> not (elem x (map fst newm))) amap
502 findTag i [] = Nothing
503 findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
504 findTag i (_ : xs) = findTag i xs
506 findDefault [] = Nothing
507 findDefault (DefaultCase sc : xs) = Just sc
508 findDefault (_ : xs) = findDefault xs
510 findConst c [] = Nothing
511 findConst c (ConstCase c' v : xs) | c == c' = Just v
512 findConst IType (ConCase n 1 [] v : xs) = Just v
513 findConst FlType (ConCase n 2 [] v : xs) = Just v
514 findConst ChType (ConCase n 3 [] v : xs) = Just v
515 findConst StrType (ConCase n 4 [] v : xs) = Just v
516 findConst PtrType (ConCase n 5 [] v : xs) = Just v
517 findConst c (_ : xs) = findConst c xs
519 getValArgs (HApp t env args) = (t, env, args)
520 getValArgs t = (t, [], [])
522convEq' ctxt x y = evalStateT (convEq ctxt x y) (0, [])
524convEq :: Context -> TT Name -> TT Name -> StateT UCs TC Bool
525convEq ctxt = ceq [] where
526 ceq :: [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
527 ceq ps (P xt x _) (P yt y _)
528 | (xt == yt && x ==y ) || (x, y) `elem` ps || (y,x) `elem` ps = return True
529 | otherwise = sameDefs ps x y
530 ceq ps (V x) (V y) = return (x == y)
531 ceq ps (Bind _ xb xs) (Bind _ yb ys)
532 = liftM2 (&&) (ceqB ps xb yb) (ceq ps xs ys)
533 where
534 ceqB ps (Let v t) (Let v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')
535 ceqB ps (Guess v t) (Guess v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')
536 ceqB ps b b' = ceq ps (binderTy b) (binderTy b')
537 ceq ps (App fx ax) (App fy ay) = liftM2 (&&) (ceq ps fx fy) (ceq ps ax ay)
538 ceq ps (Constant x) (Constant y) = return (x == y)
539 ceq ps (Set x) (Set y) = do (v, cs) <- get
540 put (v, ULE x y : cs)
541 return True
542 ceq ps Erased _ = return True
543 ceq ps _ Erased = return True
544 ceq ps _ _ = return False
546 caseeq ps (Case n cs) (Case n' cs') = caseeqA ((n,n'):ps) cs cs'
547 where
548 caseeqA ps (ConCase x i as sc : rest) (ConCase x' i' as' sc' : rest')
549 = do q1 <- caseeq (zip as as' ++ ps) sc sc'
550 q2 <- caseeqA ps rest rest'
551 return $ x == x' && i == i' && q1 && q2
552 caseeqA ps (ConstCase x sc : rest) (ConstCase x' sc' : rest')
553 = do q1 <- caseeq ps sc sc'
554 q2 <- caseeqA ps rest rest'
555 return $ x == x' && q1 && q2
556 caseeqA ps (DefaultCase sc : rest) (DefaultCase sc' : rest')
557 = liftM2 (&&) (caseeq ps sc sc') (caseeqA ps rest rest')
558 caseeqA ps [] [] = return True
559 caseeqA ps _ _ = return False
560 caseeq ps (STerm x) (STerm y) = ceq ps x y
561 caseeq ps (UnmatchedCase _) (UnmatchedCase _) = return True
562 caseeq ps _ _ = return False
564 sameDefs ps x y = case (lookupDef Nothing x ctxt, lookupDef Nothing y ctxt) of
565 ([Function _ xdef], [Function _ ydef])
566 -> ceq ((x,y):ps) xdef ydef
567 ([CaseOp _ _ _ _ _ _ xdef _ _],
568 [CaseOp _ _ _ _ _ _ ydef _ _])
569 -> caseeq ((x,y):ps) xdef ydef
570 _ -> return False
572-- SPECIALISATION -----------------------------------------------------------
573-- We need too much control to be able to do this by tweaking the main
574-- evaluator
576spec :: Context -> Ctxt [Bool] -> Env -> TT Name -> Eval (TT Name)
577spec ctxt statics genv tm = error "spec undefined"
579-- CONTEXTS -----------------------------------------------------------------
581{- A definition is either a simple function (just an expression with a type),
582 a constant, which could be a data or type constructor, an axiom or as an
583 yet undefined function, or an Operator.
584 An Operator is a function which explains how to reduce.
585 A CaseOp is a function defined by a simple case tree -}
587data Def = Function Type Term
588 | TyDecl NameType Type
589 | Operator Type Int ([Value] -> Maybe Value)
590 | CaseOp Bool Bool -- compile-time/run-time inlinable
591 Type
592 [Either Term (Term, Term)] -- original definition
593 [([Name], Term, Term)] -- simplified definition
594 [Name] SC -- Compile time case definition
595 [Name] SC -- Run time cae definitions
596{-!
597deriving instance Binary Def
598!-}
600instance Show Def where
601 show (Function ty tm) = "Function: " ++ show (ty, tm)
602 show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty
603 show (Operator ty _ _) = "Operator: " ++ show ty
604 show (CaseOp _ _ ty ps_in ps ns sc ns' sc')
605 = "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++
606 show ns ++ " " ++ show sc ++ "\n" ++
607 show ns' ++ " " ++ show sc'
608-- We need this for serialising Def. Fortunately, it never gets used because
609-- we'll never serialise a primitive operator
611instance Binary (a -> b) where
612 put x = return ()
613 get = error "Getting a function"
615-------
617-- Frozen => doesn't reduce
618-- Hidden => doesn't reduce and invisible to type checker
620data Accessibility = Public | Frozen | Hidden
621 deriving (Show, Eq)
623data Totality = Total [Int] -- well-founded arguments
624 | Productive
625 | Partial PReason
626 | Unchecked
627 deriving Eq
629data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name
630 | BelieveMe | Mutual [Name] | NotProductive
631 deriving (Show, Eq)
633instance Show Totality where
634 show (Total args)= "Total" -- ++ show args ++ " decreasing arguments"
635 show Productive = "Productive" -- ++ show args ++ " decreasing arguments"
636 show Unchecked = "not yet checked for totality"
637 show (Partial Itself) = "possibly not total as it is not well founded"
638 show (Partial NotCovering) = "not total as there are missing cases"
639 show (Partial NotPositive) = "not strictly positive"
640 show (Partial NotProductive) = "not productive"
641 show (Partial BelieveMe) = "not total due to use of believe_me in proof"
642 show (Partial (Other ns)) = "possibly not total due to: " ++ showSep ", " (map show ns)
643 show (Partial (Mutual ns)) = "possibly not total due to recursive path " ++
644 showSep " --> " (map show ns)
646{-!
647deriving instance Binary Accessibility
648!-}
650{-!
651deriving instance Binary Totality
652!-}
654{-!
655deriving instance Binary PReason
656!-}
658data Context = MkContext {
659 uconstraints :: [UConstraint],
660 next_tvar :: Int,
661 definitions :: Ctxt (Def, Accessibility, Totality)
662 }
664initContext = MkContext [] 0 emptyContext
666ctxtAlist :: Context -> [(Name, Def)]
667ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)
669veval ctxt env t = evalState (eval False ctxt threshold [] env t []) initEval
671addToCtxt :: Name -> Term -> Type -> Context -> Context
672addToCtxt n tm ty uctxt
673 = let ctxt = definitions uctxt
674 ctxt' = addDef n (Function ty tm, Public, Unchecked) ctxt in
675 uctxt { definitions = ctxt' }
677setAccess :: Name -> Accessibility -> Context -> Context
678setAccess n a uctxt
679 = let ctxt = definitions uctxt
680 ctxt' = updateDef n (\ (d, _, t) -> (d, a, t)) ctxt in
681 uctxt { definitions = ctxt' }
683setTotal :: Name -> Totality -> Context -> Context
684setTotal n t uctxt
685 = let ctxt = definitions uctxt
686 ctxt' = updateDef n (\ (d, a, _) -> (d, a, t)) ctxt in
687 uctxt { definitions = ctxt' }
689addCtxtDef :: Name -> Def -> Context -> Context
690addCtxtDef n d c = let ctxt = definitions c
691 ctxt' = addDef n (d, Public, Unchecked) ctxt in
692 c { definitions = ctxt' }
694addTyDecl :: Name -> Type -> Context -> Context
695addTyDecl n ty uctxt
696 = let ctxt = definitions uctxt
697 ctxt' = addDef n (TyDecl Ref ty, Public, Unchecked) ctxt in
698 uctxt { definitions = ctxt' }
700addDatatype :: Datatype Name -> Context -> Context
701addDatatype (Data n tag ty cons) uctxt
702 = let ctxt = definitions uctxt
703 ty' = normalise uctxt [] ty
704 ctxt' = addCons 0 cons (addDef n
705 (TyDecl (TCon tag (arity ty')) ty, Public, Unchecked) ctxt) in
706 uctxt { definitions = ctxt' }
707 where
708 addCons tag [] ctxt = ctxt
709 addCons tag ((n, ty) : cons) ctxt
710 = let ty' = normalise uctxt [] ty in
711 addCons (tag+1) cons (addDef n
712 (TyDecl (DCon tag (arity ty')) ty, Public, Unchecked) ctxt)
714addCasedef :: Name -> Bool -> Bool -> Bool ->
715 [Either Term (Term, Term)] ->
716 [([Name], Term, Term)] ->
717 [([Name], Term, Term)] ->
718 Type -> Context -> Context
719addCasedef n alwaysInline tcase covering ps_in ps psrt ty uctxt
720 = let ctxt = definitions uctxt
721 access = case lookupDefAcc Nothing n False uctxt of
722 [(_, acc)] -> acc
723 _ -> Public
724 ctxt' = case (simpleCase tcase covering CompileTime (FC "" 0) ps,
725 simpleCase tcase covering RunTime (FC "" 0) psrt) of
726 (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) ->
727 let inl = alwaysInline in
728 addDef n (CaseOp inl (inl || small n sc')
729 ty ps_in ps args sc args' sc',
730 access, Unchecked) ctxt in
731 uctxt { definitions = ctxt' }
733simplifyCasedef :: Name -> Context -> Context
734simplifyCasedef n uctxt
735 = let ctxt = definitions uctxt
736 ctxt' = case lookupCtxt Nothing n ctxt of
737 [(CaseOp inl inr ty [] ps args sc args' sc', acc, tot)] ->
738 ctxt -- nothing to simplify (or already done...)
739 [(CaseOp inl inr ty ps_in ps args sc args' sc', acc, tot)] ->
740 let pdef = map debind $ map simpl ps_in in
741 case simpleCase False True CompileTime (FC "" 0) pdef of
742 OK (CaseDef args sc _) ->
743 addDef n (CaseOp inl inr
744 ty ps_in ps args sc args' sc',
745 acc, tot) ctxt
746 _ -> ctxt in
747 uctxt { definitions = ctxt' }
748 where
749 depat acc (Bind n (PVar t) sc)
750 = depat (n : acc) (instantiate (P Bound n t) sc)
751 depat acc x = (acc, x)
752 debind (Right (x, y)) = let (vs, x') = depat [] x
753 (_, y') = depat [] y in
754 (vs, x', y')
755 debind (Left x) = let (vs, x') = depat [] x in
756 (vs, x', Impossible)
757 simpl (Right (x, y)) = Right (x, simplify uctxt False [] y)
758 simpl t = t
760addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) ->
761 Context -> Context
762addOperator n ty a op uctxt
763 = let ctxt = definitions uctxt
764 ctxt' = addDef n (Operator ty a op, Public, Unchecked) ctxt in
765 uctxt { definitions = ctxt' }
767tfst (a, _, _) = a
769lookupNames :: Maybe [String] -> Name -> Context -> [Name]
770lookupNames root n ctxt
771 = let ns = lookupCtxtName root n (definitions ctxt) in
772 map fst ns
774lookupTy :: Maybe [String] -> Name -> Context -> [Type]
775lookupTy root n ctxt
776 = do def <- lookupCtxt root n (definitions ctxt)
777 case tfst def of
778 (Function ty _) -> return ty
779 (TyDecl _ ty) -> return ty
780 (Operator ty _ _) -> return ty
781 (CaseOp _ _ ty _ _ _ _ _ _) -> return ty
783isConName :: Maybe [String] -> Name -> Context -> Bool
784isConName root n ctxt
785 = or $ do def <- lookupCtxt root n (definitions ctxt)
786 case tfst def of
787 (TyDecl (DCon _ _) _) -> return True
788 (TyDecl (TCon _ _) _) -> return True
789 _ -> return False
791isFnName :: Maybe [String] -> Name -> Context -> Bool
792isFnName root n ctxt
793 = or $ do def <- lookupCtxt root n (definitions ctxt)
794 case tfst def of
795 (Function _ _) -> return True
796 (Operator _ _ _) -> return True
797 (CaseOp _ _ _ _ _ _ _ _ _) -> return True
798 _ -> return False
800lookupP :: Maybe [String] -> Name -> Context -> [Term]
801lookupP root n ctxt
802 = do def <- lookupCtxt root n (definitions ctxt)
803 p <- case def of
804 (Function ty tm, a, _) -> return (P Ref n ty, a)
805 (TyDecl nt ty, a, _) -> return (P nt n ty, a)
806 (CaseOp _ _ ty _ _ _ _ _ _, a, _) -> return (P Ref n ty, a)
807 (Operator ty _ _, a, _) -> return (P Ref n ty, a)
808 case snd p of
809 Hidden -> []
810 _ -> return (fst p)
812lookupDef :: Maybe [String] -> Name -> Context -> [Def]
813lookupDef root n ctxt = map tfst $ lookupCtxt root n (definitions ctxt)
815lookupDefAcc :: Maybe [String] -> Name -> Bool -> Context ->
816 [(Def, Accessibility)]
817lookupDefAcc root n mkpublic ctxt
818 = map mkp $ lookupCtxt root n (definitions ctxt)
819 where mkp (d, a, _) = if mkpublic then (d, Public) else (d, a)
821lookupTotal :: Name -> Context -> [Totality]
822lookupTotal n ctxt = map mkt $ lookupCtxt Nothing n (definitions ctxt)
823 where mkt (d, a, t) = t
825lookupVal :: Maybe [String] -> Name -> Context -> [Value]
826lookupVal root n ctxt
827 = do def <- lookupCtxt root n (definitions ctxt)
828 case tfst def of
829 (Function _ htm) -> return (veval ctxt [] htm)
830 (TyDecl nt ty) -> return (VP nt n (veval ctxt [] ty))
832lookupTyEnv :: Name -> Env -> Maybe (Int, Type)
833lookupTyEnv n env = li n 0 env where
834 li n i [] = Nothing
835 li n i ((x, b): xs)
836 | n == x = Just (i, binderTy b)
837 | otherwise = li n (i+1) xs