git.iko.soy/Idris-dev
on aa42f71 help sign in
Idris-dev/src/Core/Evaluate.hs
873 lines 38 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(..), Quote(..), evalState, initEval) 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 nexthole :: Int }
25type Eval a = State EvalState a
27data EvalOpt = Spec | HNF | Simplify Bool | AtREPL
28 deriving (Show, Eq)
30initEval = ES [] 0
32-- VALUES (as HOAS) ---------------------------------------------------------
33-- | A HOAS representation of values
34data Value = VP NameType Name Value
35 | VV Int
36 -- True for Bool indicates safe to reduce
37 | VBind Bool Name (Binder Value) (Value -> Eval Value)
38 -- For frozen let bindings when simplifying
39 | VBLet Int Name Value Value Value
40 | VApp Value Value
41 | VType UExp
42 | VErased
43 | VConstant Const
44-- | VLazy Env [Value] Term
45 | VTmp Int
47data HNF = HP NameType Name (TT Name)
48 | HV Int
49 | HBind Name (Binder HNF) (HNF -> Eval HNF)
50 | HApp HNF [HNF] [TT Name]
51 | HType UExp
52 | HConstant Const
53 | HTmp Int
54 deriving Show
56instance Show Value where
57 show x = show $ evalState (quote 100 x) initEval
59instance Show (a -> b) where
60 show x = "<<fn>>"
62-- THE EVALUATOR ------------------------------------------------------------
64-- The environment is assumed to be "locally named" - i.e., not de Bruijn
65-- indexed.
66-- i.e. it's an intermediate environment that we have while type checking or
67-- while building a proof.
69-- | Normalise fully type checked terms (so, assume all names/let bindings resolved)
70normaliseC :: Context -> Env -> TT Name -> TT Name
71normaliseC ctxt env t
72 = evalState (do val <- eval False ctxt [] env t []
73 quote 0 val) initEval
75normaliseAll :: Context -> Env -> TT Name -> TT Name
76normaliseAll ctxt env t
77 = evalState (do val <- eval False ctxt [] env t [AtREPL]
78 quote 0 val) initEval
80normalise :: Context -> Env -> TT Name -> TT Name
81normalise = normaliseTrace False
83normaliseTrace :: Bool -> Context -> Env -> TT Name -> TT Name
84normaliseTrace tr ctxt env t
85 = evalState (do val <- eval tr ctxt [] (map finalEntry env) (finalise t) []
86 quote 0 val) initEval
88specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name
89specialise ctxt env limits t
90 = evalState (do val <- eval False ctxt limits (map finalEntry env) (finalise t) []
91 quote 0 val) (initEval { limited = limits })
93-- | Like normalise, but we only reduce functions that are marked as okay to
94-- inline (and probably shouldn't reduce lets?)
95simplify :: Context -> Bool -> Env -> TT Name -> TT Name
96simplify ctxt runtime env t
97 = evalState (do val <- eval False ctxt [(UN "lazy", 0),
98 (UN "assert_smaller", 0),
99 (UN "par", 0),
100 (UN "fork", 0)]
101 (map finalEntry env) (finalise t)
102 [Simplify runtime]
103 quote 0 val) initEval
105-- | Reduce a term to head normal form
106hnf :: Context -> Env -> TT Name -> TT Name
107hnf ctxt env t
108 = evalState (do val <- eval False ctxt []
109 (map finalEntry env)
110 (finalise t) [HNF]
111 quote 0 val) initEval
114-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))
116finalEntry :: (Name, Binder (TT Name)) -> (Name, Binder (TT Name))
117finalEntry (n, b) = (n, fmap finalise b)
119bindEnv :: EnvTT n -> TT n -> TT n
120bindEnv [] tm = tm
121bindEnv ((n, Let t v):bs) tm = Bind n (NLet t v) (bindEnv bs tm)
122bindEnv ((n, b):bs) tm = Bind n b (bindEnv bs tm)
124unbindEnv :: EnvTT n -> TT n -> TT n
125unbindEnv [] tm = tm
126unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc
128usable :: Bool -> Name -> [(Name, Int)] -> (Bool, [(Name, Int)])
129usable _ _ ns@((MN 0 "STOP", _) : _) = (False, ns)
130usable True (UN "io_bind") ns = (False, ns)
131usable s n [] = (True, [])
132usable s n ns = case lookup n ns of
133 Just 0 -> (False, ns)
134 Just i -> (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns)
135 _ -> if s then (True, (n, 0) : filter (\ (n', _) -> n/=n') ns)
136 else (True, (n, 100) : filter (\ (n', _) -> n/=n') ns)
138-- | Evaluate in a context of locally named things (i.e. not de Bruijn indexed,
139-- such as we might have during construction of a proof)
140eval :: Bool -> Context -> [(Name, Int)] -> Env -> TT Name ->
141 [EvalOpt] -> Eval Value
142eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
143 spec = Spec `elem` opts
144 simpl = Simplify True `elem` opts
145 atRepl = AtREPL `elem` opts
146 hnf = HNF `elem` opts
148 canSimplify inl inr n stk
149 = (Simplify False `elem` opts && (not inl || elem n stk))
150 || (Simplify True `elem` opts && (not inr || elem n stk))
152 ev ntimes stk top env (P _ n ty)
153 | Just (Let t v) <- lookup n genv = ev ntimes stk top env v
154 ev ntimes_in stk top env (P Ref n ty)
155 | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)
156 | (True, ntimes) <- usable simpl n ntimes_in
157 = do let val = lookupDefAcc n atRepl ctxt
158 case val of
159 [(Function _ tm, Public)] ->
160 ev ntimes (n:stk) True env tm
161 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty
162 return $ VP nt n vty
163 [(CaseOp inl inr _ _ _ [] tree _ _, acc)]
164 | acc == Public || simpl -> -- unoptimised version
165 if canSimplify inl inr n stk
166 then liftM (VP Ref n) (ev ntimes stk top env ty)
167 else do c <- evCase ntimes (n:stk) top env [] [] tree
168 case c of
169 (Nothing, _) -> liftM (VP Ref n) (ev ntimes stk top env ty)
170 (Just v, _) -> return v
171 _ -> liftM (VP Ref n) (ev ntimes stk top env ty)
172 ev ntimes stk top env (P nt n ty) = liftM (VP nt n) (ev ntimes stk top env ty)
173 ev ntimes stk top env (V i)
174 | i < length env && i >= 0 = return $ env !! i
175 | otherwise = return $ VV i
176 ev ntimes stk top env (Bind n (Let t v) sc)
177 | not simpl -- - || vinstances 0 sc < 2
178 = do v' <- ev ntimes stk top env v --(finalise v)
179 sc' <- ev ntimes stk top (v' : env) sc
180 wknV (-1) sc'
181 | otherwise
182 = do t' <- ev ntimes stk top env t
183 v' <- ev ntimes stk top env v --(finalise v)
184 -- use Tmp as a placeholder, then make it a variable reference
185 -- again when evaluation finished
186 hs <- get
187 let vd = nexthole hs
188 put (hs { nexthole = vd + 1 })
189 sc' <- ev ntimes stk top (VP Bound (MN vd "vlet") VErased : env) sc
190 return $ VBLet vd n t' v' sc'
191 ev ntimes stk top env (Bind n (NLet t v) sc)
192 = do t' <- ev ntimes stk top env (finalise t)
193 v' <- ev ntimes stk top env (finalise v)
194 sc' <- ev ntimes stk top (v' : env) sc
195 return $ VBind True n (Let t' v') (\x -> return sc')
196 ev ntimes stk top env (Bind n b sc)
197 = do b' <- vbind env b
198 return $ VBind (not simpl || vinstances 0 sc < 2)
199 n b' (\x -> ev ntimes stk False (x:env) sc)
200 where vbind env t
201 | simpl
202 = fmapMB (\tm -> ev ((MN 0 "STOP", 0) : ntimes)
203 stk top env (finalise tm)) t
204 | otherwise
205 = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
206-- ev ntimes stk top env (App (App (P _ laz _) _) a)
207-- | laz == UN "lazy"
208-- = trace (showEnvDbg genv a) $ ev ntimes stk top env a
209 ev ntimes stk top env (App f a)
210 = do f' <- ev ntimes stk False env f
211 a' <- ev ntimes stk False env a
212 evApply ntimes stk top env [a'] f'
213 ev ntimes stk top env (Constant c) = return $ VConstant c
214 ev ntimes stk top env Erased = return VErased
215 ev ntimes stk top env (TType i) = return $ VType i
217 evApply ntimes stk top env args (VApp f a) =
218 evApply ntimes stk top env (a:args) f
219 evApply ntimes stk top env args f = apply ntimes stk top env f args
221 apply ntimes stk top env (VBind True n (Lam t) sc) (a:as)
222 = do a' <- sc a
223 app <- apply ntimes stk top env a' as
224 wknV (-1) app
225-- apply ntimes stk False env f args
226-- | spec = specApply ntimes stk env f args
227 apply ntimes_in stk top env f@(VP Ref n ty) args
228 | not top && hnf = case args of
229 [] -> return f
230 _ -> return $ unload env f args
231 | (True, ntimes) <- usable simpl n ntimes_in
232 = traceWhen traceon (show stk) $
233 do let val = lookupDefAcc n atRepl ctxt
234 case val of
235 [(CaseOp inl inr _ _ _ ns tree _ _, acc)]
236 | acc == Public -> -- unoptimised version
237 if canSimplify inl inr n stk
238 then return $ unload env (VP Ref n ty) args
239 else do c <- evCase ntimes (n:stk) top env ns args tree
240 case c of
241 (Nothing, _) -> return $ unload env (VP Ref n ty) args
242 (Just v, rest) -> evApply ntimes stk top env rest v
243 [(Operator _ i op, _)] ->
244 if (i <= length args)
245 then case op (take i args) of
246 Nothing -> return $ unload env (VP Ref n ty) args
247 Just v -> evApply ntimes stk top env (drop i args) v
248 else return $ unload env (VP Ref n ty) args
249 _ -> case args of
250 [] -> return f
251 _ -> return $ unload env f args
252 apply ntimes stk top env f (a:as) = return $ unload env f (a:as)
253 apply ntimes stk top env f [] = return f
255-- specApply stk env f@(VP Ref n ty) args
256-- = case lookupCtxt n statics of
257-- [as] -> if or as
258-- then trace (show (n, map fst (filter (\ (_, s) -> s) (zip args as)))) $
259-- return $ unload env f args
260-- else return $ unload env f args
261-- _ -> return $ unload env f args
262-- specApply stk env f args = return $ unload env f args
264 unload env f [] = f
265 unload env f (a:as) = unload env (VApp f a) as
267 evCase ntimes stk top env ns args tree
268 | length ns <= length args
269 = do let args' = take (length ns) args
270 let rest = drop (length ns) args
271 t <- evTree ntimes stk top env
272 (zipWith (\n t -> (n, t)) ns args') tree
273 return (t, rest)
274 | otherwise = return (Nothing, args)
276 evTree :: [(Name, Int)] -> [Name] -> Bool ->
277 [Value] -> [(Name, Value)] -> SC -> Eval (Maybe Value)
278 evTree ntimes stk top env amap (UnmatchedCase str) = return Nothing
279 evTree ntimes stk top env amap (STerm tm)
280 = do let etm = pToVs (map fst amap) tm
281 etm' <- ev ntimes stk (not (conHeaded tm))
282 (map snd amap ++ env) etm
283 return $ Just etm'
284 evTree ntimes stk top env amap (Case n alts)
285 = case lookup n amap of
286 Just v -> do c <- chooseAlt env v (getValArgs v) alts amap
287 case c of
288 Just (altmap, sc) -> evTree ntimes stk top env altmap sc
289 _ -> do c' <- chooseAlt' ntimes stk env v (getValArgs v) alts amap
290 case c' of
291 Just (altmap, sc) -> evTree ntimes stk top env altmap sc
292 _ -> return Nothing
293 _ -> return Nothing
294 evTree ntimes stk top env amap ImpossibleCase = return Nothing
296 conHeaded tm@(App _ _)
297 | (P (DCon _ _) _ _, args) <- unApply tm = True
298 conHeaded t = False
300 chooseAlt' ntimes stk env _ (f, args) alts amap
301 = do f' <- apply ntimes stk True env f args
302 chooseAlt env f' (getValArgs f') alts amap
304 chooseAlt :: [Value] -> Value -> (Value, [Value]) -> [CaseAlt] -> [(Name, Value)] ->
305 Eval (Maybe ([(Name, Value)], SC))
306 chooseAlt env _ (VP (DCon i a) _ _, args) alts amap
307 | Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)
308 | Just v <- findDefault alts = return $ Just (amap, v)
309 chooseAlt env _ (VP (TCon i a) _ _, args) alts amap
310 | Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)
311 | Just v <- findDefault alts = return $ Just (amap, v)
312 chooseAlt env _ (VConstant c, []) alts amap
313 | Just v <- findConst c alts = return $ Just (amap, v)
314 | Just v <- findDefault alts = return $ Just (amap, v)
315 chooseAlt _ _ _ _ _ = return Nothing
317 -- Replace old variable names in the map with new matches
318 -- (This is possibly unnecessary since we make unique names and don't
319 -- allow repeated variables...?)
320 updateAmap newm amap
321 = newm ++ filter (\ (x, _) -> not (elem x (map fst newm))) amap
322 findTag i [] = Nothing
323 findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
324 findTag i (_ : xs) = findTag i xs
326 findDefault [] = Nothing
327 findDefault (DefaultCase sc : xs) = Just sc
328 findDefault (_ : xs) = findDefault xs
330 findConst c [] = Nothing
331 findConst c (ConstCase c' v : xs) | c == c' = Just v
332 findConst (AType (ATInt ITNative)) (ConCase n 1 [] v : xs) = Just v
333 findConst (AType ATFloat) (ConCase n 2 [] v : xs) = Just v
334 findConst (AType (ATInt ITChar)) (ConCase n 3 [] v : xs) = Just v
335 findConst StrType (ConCase n 4 [] v : xs) = Just v
336 findConst PtrType (ConCase n 5 [] v : xs) = Just v
337 findConst (AType (ATInt ITBig)) (ConCase n 6 [] v : xs) = Just v
338 findConst (AType (ATInt (ITFixed ity))) (ConCase n tag [] v : xs)
339 | tag == 7 + fromEnum ity = Just v
340 findConst (AType (ATInt (ITVec ity count))) (ConCase n tag [] v : xs)
341 | tag == (fromEnum ity + 1) * 1000 + count = Just v
342 findConst c (_ : xs) = findConst c xs
344 getValArgs tm = getValArgs' tm []
345 getValArgs' (VApp f a) as = getValArgs' f (a:as)
346 getValArgs' f as = (f, as)
348-- tmpToV i vd (VLetHole j) | vd == j = return $ VV i
349-- tmpToV i vd (VP nt n v) = liftM (VP nt n) (tmpToV i vd v)
350-- tmpToV i vd (VBind n b sc) = do b' <- fmapMB (tmpToV i vd) b
351-- let sc' = \x -> do x' <- sc x
352-- tmpToV (i + 1) vd x'
353-- return (VBind n b' sc')
354-- tmpToV i vd (VApp f a) = liftM2 VApp (tmpToV i vd f) (tmpToV i vd a)
355-- tmpToV i vd x = return x
357class Quote a where
358 quote :: Int -> a -> Eval (TT Name)
360instance Quote Value where
361 quote i (VP nt n v) = liftM (P nt n) (quote i v)
362 quote i (VV x) = return $ V x
363 quote i (VBind _ n b sc) = do sc' <- sc (VTmp i)
364 b' <- quoteB b
365 liftM (Bind n b') (quote (i+1) sc')
366 where quoteB t = fmapMB (quote i) t
367 quote i (VBLet vd n t v sc)
368 = do sc' <- quote i sc
369 t' <- quote i t
370 v' <- quote i v
371 let sc'' = pToV (MN vd "vlet") (addBinder sc')
372 return (Bind n (Let t' v') sc'')
373 quote i (VApp f a) = liftM2 App (quote i f) (quote i a)
374 quote i (VType u) = return $ TType u
375 quote i VErased = return $ Erased
376 quote i (VConstant c) = return $ Constant c
377 quote i (VTmp x) = return $ V (i - x - 1)
379instance Quote HNF where
380 quote i (HP nt n t) = return (P nt n t)
381 quote i (HV x) = return $ V x
382 quote i (HBind n b sc) = do sc' <- sc (HTmp i)
383 b' <- quoteB b
384 liftM (Bind n b') (quote (i+1) sc')
385 where quoteB t = fmapMB (quote i) t
386 quote i (HApp f env as) = do f' <- quote i f
387 as' <- mapM (iEnv env) as
388 return $ mkApp f' as'
389 where iEnv [] a = return a
390 iEnv (x:xs) a = do x' <- quote i x
391 iEnv xs (weakenTm (-1) (instantiate x' a))
392 quote i (HType u) = return $ TType u
393 quote i (HConstant c) = return $ Constant c
394 quote i (HTmp x) = return $ V (i - x - 1)
396wknV :: Int -> Value -> Eval Value
397wknV i (VV x) = return $ VV (x + i)
398wknV i (VBind red n b sc) = do b' <- fmapMB (wknV i) b
399 return $ VBind red n b' (\x -> do x' <- sc x
400 wknV i x')
401wknV i (VApp f a) = liftM2 VApp (wknV i f) (wknV i a)
402wknV i t = return t
404wknH :: Int -> HNF -> Eval HNF
405wknH i (HV x) = return $ HV (x + i)
406wknH i (HBind n b sc) = do b' <- fmapMB (wknH i) b
407 return $ HBind n b' (\x -> do x' <- sc x
408 wknH i x')
409wknH i (HApp f env as) = liftM3 HApp (wknH i f) (return env)
410 (return as)
411wknH i t = return t
413-- HEAD NORMAL FORM ---------------------------------------------------------
415eval_hnf :: Context -> Ctxt [Bool] -> Env -> TT Name -> Eval HNF
416eval_hnf ctxt statics genv tm = ev [] tm where
417 ev :: [HNF] -> TT Name -> Eval HNF
418 ev env (P _ n ty)
419 | Just (Let t v) <- lookup n genv = ev env v
420 ev env (P Ref n ty) = case lookupDef n ctxt of
421 [Function _ t] -> ev env t
422 [TyDecl nt ty] -> return $ HP nt n ty
423 [CaseOp inl _ _ _ _ [] tree _ _] ->
424 do c <- evCase env [] [] tree
425 case c of
426 (Nothing, _, _) -> return $ HP Ref n ty
427 (Just v, _, _) -> return v
428 _ -> return $ HP Ref n ty
429 ev env (P nt n ty) = return $ HP nt n ty
430 ev env (V i) | i < length env = return $ env !! i
431 | otherwise = return $ HV i
432 ev env (Bind n (Let t v) sc)
433 = do v' <- ev env (finalise v)
434 sc' <- ev (v' : env) sc
435 wknH (-1) sc'
436 ev env (Bind n b sc)
437 = do b' <- hbind env b
438 return $ HBind n b' (\x -> ev (x : env) sc)
439 where hbind env t = fmapMB (\tm -> ev env (finalise tm)) t
440 ev env (App f a) = evApply env [a] f
441 ev env (Constant c) = return $ HConstant c
442 ev env (TType i) = return $ HType i
444 evApply env args (App f a) = evApply env (a : args) f
445 evApply env args f = do f' <- ev env f
446 apply env f' args
448 apply env (HBind n (Lam t) sc) (a:as) = do a' <- ev env a
449 sc' <- sc a'
450 app <- apply env sc' as
451 wknH (-1) app
452 apply env (HP Ref n ty) args
453 | [CaseOp _ _ _ _ _ ns tree _ _] <- lookupDef n ctxt
454 = do c <- evCase env ns args tree
455 case c of
456 (Nothing, _, env') -> return $ unload env' (HP Ref n ty) args
457 (Just v, rest, env') -> do v' <- quote 0 v
458 apply env' v rest
459-- | Just (Operator _ i op) <- lookupDef n ctxt
460-- = if (i <= length args)
461-- then case op (take i args) of
462-- Nothing -> return $ unload env (HP Ref n ty) args
463-- Just v -> evApply env (drop i args) v
464-- else return $ unload env (HP Ref n ty) args
465 apply env f (a:as) = return $ unload env f (a:as)
466 apply env f [] = return f
468 unload env f [] = f
469 unload env f as = HApp f env as
471 evCase env ns args tree
472 | length ns <= length args
473 = do let args' = take (length ns) args
474 let rest = drop (length ns) args
475 (t, env') <- evTree env (zipWith (\n t -> (n, t)) ns args') tree
476 return (t, rest, env')
477 | otherwise = return (Nothing, args, env)
479 evTree :: [HNF] -> [(Name, TT Name)] -> SC -> Eval (Maybe HNF, [HNF])
480 evTree env amap (UnmatchedCase str) = return (Nothing, env)
481 evTree env amap (STerm tm)
482 = do let etm = pToVs (map fst amap) tm
483 amap' <- mapM (ev env) (map snd amap)
484 envw <- mapM (wknH (length amap)) env
485 let env' = amap' ++ envw
486 etm' <- trace (show etm) $ ev env' etm
487 etmq <- quote 0 etm'
488 trace ("Ev: " ++ show (etm, etmq)) $ return $ (Just etm', env')
489 evTree env amap (Case n alts)
490 = case lookup n amap of
491 Just v -> do v' <- ev env v
492 case chooseAlt v' (getValArgs v') alts amap of
493 Just (altmap, sc) -> evTree env altmap sc
494 _ -> return (Nothing, env)
496 chooseAlt :: HNF -> (HNF, [HNF], [TT Name]) ->
497 [CaseAlt] -> [(Name, TT Name)] ->
498 Maybe ([(Name, TT Name)], SC)
499 chooseAlt _ (HP (DCon i a) _ _, env, args) alts amap
500 | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)
501 | Just v <- findDefault alts = Just (amap, v)
502 chooseAlt _ (HP (TCon i a) _ _, env, args) alts amap
503 | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)
504 | Just v <- findDefault alts = Just (amap, v)
505 chooseAlt _ (HConstant c, env, []) alts amap
506 | Just v <- findConst c alts = Just (amap, v)
507 | Just v <- findDefault alts = Just (amap, v)
508 chooseAlt _ _ _ _ = Nothing
510 -- Replace old variable names in the map with new matches
511 -- (This is possibly unnecessary since we make unique names and don't
512 -- allow repeated variables...?)
513 updateAmap newm amap
514 = newm ++ filter (\ (x, _) -> not (elem x (map fst newm))) amap
515 findTag i [] = Nothing
516 findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
517 findTag i (_ : xs) = findTag i xs
519 findDefault [] = Nothing
520 findDefault (DefaultCase sc : xs) = Just sc
521 findDefault (_ : xs) = findDefault xs
523 findConst c [] = Nothing
524 findConst c (ConstCase c' v : xs) | c == c' = Just v
525 findConst (AType (ATInt ITNative)) (ConCase n 1 [] v : xs) = Just v
526 findConst (AType ATFloat) (ConCase n 2 [] v : xs) = Just v
527 findConst (AType (ATInt ITChar)) (ConCase n 3 [] v : xs) = Just v
528 findConst StrType (ConCase n 4 [] v : xs) = Just v
529 findConst PtrType (ConCase n 5 [] v : xs) = Just v
530 findConst (AType (ATInt ITBig)) (ConCase n 6 [] v : xs) = Just v
531 findConst (AType (ATInt (ITFixed ity))) (ConCase n tag [] v : xs)
532 | tag == 7 + fromEnum ity = Just v
533 findConst (AType (ATInt (ITVec ity count))) (ConCase n tag [] v : xs)
534 | tag == (fromEnum ity + 1) * 1000 + count = Just v
535 findConst c (_ : xs) = findConst c xs
537 getValArgs (HApp t env args) = (t, env, args)
538 getValArgs t = (t, [], [])
540convEq' ctxt x y = evalStateT (convEq ctxt x y) (0, [])
542convEq :: Context -> TT Name -> TT Name -> StateT UCs TC Bool
543convEq ctxt = ceq [] where
544 ceq :: [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
545 ceq ps (P xt x _) (P yt y _)
546 | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True
547 | otherwise = sameDefs ps x y
548 ceq ps x (Bind n (Lam t) (App y (V 0))) = ceq ps x y
549 ceq ps (Bind n (Lam t) (App x (V 0))) y = ceq ps x y
550 ceq ps x (Bind n (Lam t) (App y (P Bound n' _)))
551 | n == n' = ceq ps x y
552 ceq ps (Bind n (Lam t) (App x (P Bound n' _))) y
553 | n == n' = ceq ps x y
554 ceq ps (V x) (V y) = return (x == y)
555 ceq ps (Bind _ xb xs) (Bind _ yb ys)
556 = liftM2 (&&) (ceqB ps xb yb) (ceq ps xs ys)
557 where
558 ceqB ps (Let v t) (Let v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')
559 ceqB ps (Guess v t) (Guess v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')
560 ceqB ps b b' = ceq ps (binderTy b) (binderTy b')
561 ceq ps (App fx ax) (App fy ay) = liftM2 (&&) (ceq ps fx fy) (ceq ps ax ay)
562 ceq ps (Constant x) (Constant y) = return (x == y)
563 ceq ps (TType x) (TType y) = do (v, cs) <- get
564 put (v, ULE x y : cs)
565 return True
566 ceq ps Erased _ = return True
567 ceq ps _ Erased = return True
568 ceq ps _ _ = return False
570 caseeq ps (Case n cs) (Case n' cs') = caseeqA ((n,n'):ps) cs cs'
571 where
572 caseeqA ps (ConCase x i as sc : rest) (ConCase x' i' as' sc' : rest')
573 = do q1 <- caseeq (zip as as' ++ ps) sc sc'
574 q2 <- caseeqA ps rest rest'
575 return $ x == x' && i == i' && q1 && q2
576 caseeqA ps (ConstCase x sc : rest) (ConstCase x' sc' : rest')
577 = do q1 <- caseeq ps sc sc'
578 q2 <- caseeqA ps rest rest'
579 return $ x == x' && q1 && q2
580 caseeqA ps (DefaultCase sc : rest) (DefaultCase sc' : rest')
581 = liftM2 (&&) (caseeq ps sc sc') (caseeqA ps rest rest')
582 caseeqA ps [] [] = return True
583 caseeqA ps _ _ = return False
584 caseeq ps (STerm x) (STerm y) = ceq ps x y
585 caseeq ps (UnmatchedCase _) (UnmatchedCase _) = return True
586 caseeq ps _ _ = return False
588 sameDefs ps x y = case (lookupDef x ctxt, lookupDef y ctxt) of
589 ([Function _ xdef], [Function _ ydef])
590 -> ceq ((x,y):ps) xdef ydef
591 ([CaseOp _ _ _ _ _ _ xdef _ _],
592 [CaseOp _ _ _ _ _ _ ydef _ _])
593 -> caseeq ((x,y):ps) xdef ydef
594 _ -> return False
596-- SPECIALISATION -----------------------------------------------------------
597-- We need too much control to be able to do this by tweaking the main
598-- evaluator
600spec :: Context -> Ctxt [Bool] -> Env -> TT Name -> Eval (TT Name)
601spec ctxt statics genv tm = error "spec undefined"
603-- CONTEXTS -----------------------------------------------------------------
605{-| A definition is either a simple function (just an expression with a type),
606 a constant, which could be a data or type constructor, an axiom or as an
607 yet undefined function, or an Operator.
608 An Operator is a function which explains how to reduce.
609 A CaseOp is a function defined by a simple case tree -}
611data Def = Function Type Term
612 | TyDecl NameType Type
613 | Operator Type Int ([Value] -> Maybe Value)
614 | CaseOp Bool Bool -- compile-time/run-time inlinable
615 Type
616 [Either Term (Term, Term)] -- original definition
617 [([Name], Term, Term)] -- simplified definition
618 [Name] SC -- Compile time case definition
619 [Name] SC -- Run time cae definitions
620{-!
621deriving instance Binary Def
622!-}
624instance Show Def where
625 show (Function ty tm) = "Function: " ++ show (ty, tm)
626 show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty
627 show (Operator ty _ _) = "Operator: " ++ show ty
628 show (CaseOp inlc inlr ty ps_in ps ns sc ns' sc')
629 = "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++
630 show ns ++ " " ++ show sc ++ "\n" ++
631 show ns' ++ " " ++ show sc' ++ "\n" ++
632 if inlc then "Inlinable\n" else "Not inlinable\n"
634-- We need this for serialising Def. Fortunately, it never gets used because
635-- we'll never serialise a primitive operator
637instance Binary (a -> b) where
638 put x = return ()
639 get = error "Getting a function"
641-------
643-- Frozen => doesn't reduce
644-- Hidden => doesn't reduce and invisible to type checker
646data Accessibility = Public | Frozen | Hidden
647 deriving (Show, Eq)
649-- | The result of totality checking
650data Totality = Total [Int] -- ^ well-founded arguments
651 | Productive -- ^ productive
652 | Partial PReason
653 | Unchecked
654 deriving Eq
656-- | Reasons why a function may not be total
657data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name
658 | BelieveMe | Mutual [Name] | NotProductive
659 deriving (Show, Eq)
661instance Show Totality where
662 show (Total args)= "Total" -- ++ show args ++ " decreasing arguments"
663 show Productive = "Productive" -- ++ show args ++ " decreasing arguments"
664 show Unchecked = "not yet checked for totality"
665 show (Partial Itself) = "possibly not total as it is not well founded"
666 show (Partial NotCovering) = "not total as there are missing cases"
667 show (Partial NotPositive) = "not strictly positive"
668 show (Partial NotProductive) = "not productive"
669 show (Partial BelieveMe) = "not total due to use of believe_me in proof"
670 show (Partial (Other ns)) = "possibly not total due to: " ++ showSep ", " (map show ns)
671 show (Partial (Mutual ns)) = "possibly not total due to recursive path " ++
672 showSep " --> " (map show ns)
674{-!
675deriving instance Binary Accessibility
676!-}
678{-!
679deriving instance Binary Totality
680!-}
682{-!
683deriving instance Binary PReason
684!-}
686-- | Contexts used for global definitions and for proof state. They contain
687-- universe constraints and existing definitions.
688data Context = MkContext {
689 uconstraints :: [UConstraint],
690 next_tvar :: Int,
691 definitions :: Ctxt (Def, Accessibility, Totality)
692 } deriving Show
694-- | The initial empty context
695initContext = MkContext [] 0 emptyContext
697-- | Get the definitions from a context
698ctxtAlist :: Context -> [(Name, Def)]
699ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)
701veval ctxt env t = evalState (eval False ctxt [] env t []) initEval
703addToCtxt :: Name -> Term -> Type -> Context -> Context
704addToCtxt n tm ty uctxt
705 = let ctxt = definitions uctxt
706 ctxt' = addDef n (Function ty tm, Public, Unchecked) ctxt in
707 uctxt { definitions = ctxt' }
709setAccess :: Name -> Accessibility -> Context -> Context
710setAccess n a uctxt
711 = let ctxt = definitions uctxt
712 ctxt' = updateDef n (\ (d, _, t) -> (d, a, t)) ctxt in
713 uctxt { definitions = ctxt' }
715setTotal :: Name -> Totality -> Context -> Context
716setTotal n t uctxt
717 = let ctxt = definitions uctxt
718 ctxt' = updateDef n (\ (d, a, _) -> (d, a, t)) ctxt in
719 uctxt { definitions = ctxt' }
721addCtxtDef :: Name -> Def -> Context -> Context
722addCtxtDef n d c = let ctxt = definitions c
723 ctxt' = addDef n (d, Public, Unchecked) ctxt in
724 c { definitions = ctxt' }
726addTyDecl :: Name -> NameType -> Type -> Context -> Context
727addTyDecl n nt ty uctxt
728 = let ctxt = definitions uctxt
729 ctxt' = addDef n (TyDecl nt ty, Public, Unchecked) ctxt in
730 uctxt { definitions = ctxt' }
732addDatatype :: Datatype Name -> Context -> Context
733addDatatype (Data n tag ty cons) uctxt
734 = let ctxt = definitions uctxt
735 ty' = normalise uctxt [] ty
736 ctxt' = addCons 0 cons (addDef n
737 (TyDecl (TCon tag (arity ty')) ty, Public, Unchecked) ctxt) in
738 uctxt { definitions = ctxt' }
739 where
740 addCons tag [] ctxt = ctxt
741 addCons tag ((n, ty) : cons) ctxt
742 = let ty' = normalise uctxt [] ty in
743 addCons (tag+1) cons (addDef n
744 (TyDecl (DCon tag (arity ty')) ty, Public, Unchecked) ctxt)
746addCasedef :: Name -> Bool -> Bool -> Bool -> Bool ->
747 [Either Term (Term, Term)] ->
748 [([Name], Term, Term)] ->
749 [([Name], Term, Term)] ->
750 Type -> Context -> Context
751addCasedef n alwaysInline tcase covering asserted ps_in ps psrt ty uctxt
752 = let ctxt = definitions uctxt
753 access = case lookupDefAcc n False uctxt of
754 [(_, acc)] -> acc
755 _ -> Public
756 ctxt' = case (simpleCase tcase covering CompileTime (FC "" 0) ps,
757 simpleCase tcase covering RunTime (FC "" 0) psrt) of
758 (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) ->
759 let inl = alwaysInline
760 inlc = (inl || small n args sc') && (not asserted)
761 inlr = inl || small n args sc' in
762 addDef n (CaseOp inlc inlr
763 ty ps_in ps args sc args' sc',
764 access, Unchecked) ctxt in
765 uctxt { definitions = ctxt' }
767simplifyCasedef :: Name -> Context -> Context
768simplifyCasedef n uctxt
769 = let ctxt = definitions uctxt
770 ctxt' = case lookupCtxt n ctxt of
771 [(CaseOp inl inr ty [] ps args sc args' sc', acc, tot)] ->
772 ctxt -- nothing to simplify (or already done...)
773 [(CaseOp inl inr ty ps_in ps args sc args' sc', acc, tot)] ->
774 let ps_in' = map simpl ps_in
775 pdef = map debind ps_in' in
776 case simpleCase False True CompileTime (FC "" 0) pdef of
777 OK (CaseDef args sc _) ->
778 addDef n (CaseOp inl inr
779 ty ps_in' ps args sc args' sc',
780 acc, tot) ctxt
781 _ -> ctxt in
782 uctxt { definitions = ctxt' }
783 where
784 depat acc (Bind n (PVar t) sc)
785 = depat (n : acc) (instantiate (P Bound n t) sc)
786 depat acc x = (acc, x)
787 debind (Right (x, y)) = let (vs, x') = depat [] x
788 (_, y') = depat [] y in
789 (vs, x', y')
790 debind (Left x) = let (vs, x') = depat [] x in
791 (vs, x', Impossible)
792 simpl (Right (x, y)) = Right (x, simplify uctxt False [] y)
793 simpl t = t
795addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) ->
796 Context -> Context
797addOperator n ty a op uctxt
798 = let ctxt = definitions uctxt
799 ctxt' = addDef n (Operator ty a op, Public, Unchecked) ctxt in
800 uctxt { definitions = ctxt' }
802tfst (a, _, _) = a
804lookupNames :: Name -> Context -> [Name]
805lookupNames n ctxt
806 = let ns = lookupCtxtName n (definitions ctxt) in
807 map fst ns
809lookupTy :: Name -> Context -> [Type]
810lookupTy n ctxt
811 = do def <- lookupCtxt n (definitions ctxt)
812 case tfst def of
813 (Function ty _) -> return ty
814 (TyDecl _ ty) -> return ty
815 (Operator ty _ _) -> return ty
816 (CaseOp _ _ ty _ _ _ _ _ _) -> return ty
818isConName :: Name -> Context -> Bool
819isConName n ctxt
820 = or $ do def <- lookupCtxt n (definitions ctxt)
821 case tfst def of
822 (TyDecl (DCon _ _) _) -> return True
823 (TyDecl (TCon _ _) _) -> return True
824 _ -> return False
826isFnName :: Name -> Context -> Bool
827isFnName n ctxt
828 = or $ do def <- lookupCtxt n (definitions ctxt)
829 case tfst def of
830 (Function _ _) -> return True
831 (Operator _ _ _) -> return True
832 (CaseOp _ _ _ _ _ _ _ _ _) -> return True
833 _ -> return False
835lookupP :: Name -> Context -> [Term]
836lookupP n ctxt
837 = do def <- lookupCtxt n (definitions ctxt)
838 p <- case def of
839 (Function ty tm, a, _) -> return (P Ref n ty, a)
840 (TyDecl nt ty, a, _) -> return (P nt n ty, a)
841 (CaseOp _ _ ty _ _ _ _ _ _, a, _) -> return (P Ref n ty, a)
842 (Operator ty _ _, a, _) -> return (P Ref n ty, a)
843 case snd p of
844 Hidden -> []
845 _ -> return (fst p)
847lookupDef :: Name -> Context -> [Def]
848lookupDef n ctxt = map tfst $ lookupCtxt n (definitions ctxt)
850lookupDefAcc :: Name -> Bool -> Context ->
851 [(Def, Accessibility)]
852lookupDefAcc n mkpublic ctxt
853 = map mkp $ lookupCtxt n (definitions ctxt)
854 where mkp (d, a, _) = if mkpublic then (d, Public) else (d, a)
856lookupTotal :: Name -> Context -> [Totality]
857lookupTotal n ctxt = map mkt $ lookupCtxt n (definitions ctxt)
858 where mkt (d, a, t) = t
860lookupVal :: Name -> Context -> [Value]
861lookupVal n ctxt
862 = do def <- lookupCtxt n (definitions ctxt)
863 case tfst def of
864 (Function _ htm) -> return (veval ctxt [] htm)
865 (TyDecl nt ty) -> return (VP nt n (veval ctxt [] ty))
867lookupTyEnv :: Name -> Env -> Maybe (Int, Type)
868lookupTyEnv n env = li n 0 env where
869 li n i [] = Nothing
870 li n i ((x, b): xs)
871 | n == x = Just (i, binderTy b)
872 | otherwise = li n (i+1) xs