git.iko.soy/Idris-dev
on f29a167 help sign in
Idris-dev/src/Core/Evaluate.hs
844 lines 37 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)] }
24type Eval a = State EvalState a
26data EvalOpt = Spec | HNF | Simplify Bool | AtREPL
27 deriving (Show, Eq)
29initEval = ES []
31-- VALUES (as HOAS) ---------------------------------------------------------
33data Value = VP NameType Name Value
34 | VV Int
35 | VBind Name (Binder Value) (Value -> Eval Value)
36 | VApp Value Value
37 | VType UExp
38 | VErased
39 | VConstant Const
40-- | VLazy Env [Value] Term
41 | VTmp Int
43data HNF = HP NameType Name (TT Name)
44 | HV Int
45 | HBind Name (Binder HNF) (HNF -> Eval HNF)
46 | HApp HNF [HNF] [TT Name]
47 | HType UExp
48 | HConstant Const
49 | HTmp Int
50 deriving Show
52instance Show Value where
53 show x = show $ evalState (quote 100 x) initEval
55instance Show (a -> b) where
56 show x = "<<fn>>"
58-- THE EVALUATOR ------------------------------------------------------------
60-- The environment is assumed to be "locally named" - i.e., not de Bruijn
61-- indexed.
62-- i.e. it's an intermediate environment that we have while type checking or
63-- while building a proof.
65-- Normalise fully type checked terms (so, assume all names/let bindings resolved)
66normaliseC :: Context -> Env -> TT Name -> TT Name
67normaliseC ctxt env t
68 = evalState (do val <- eval False ctxt [] env t []
69 quote 0 val) initEval
71normaliseAll :: Context -> Env -> TT Name -> TT Name
72normaliseAll ctxt env t
73 = evalState (do val <- eval False ctxt [] env t [AtREPL]
74 quote 0 val) initEval
76normalise :: Context -> Env -> TT Name -> TT Name
77normalise = normaliseTrace False
79normaliseTrace :: Bool -> Context -> Env -> TT Name -> TT Name
80normaliseTrace tr ctxt env t
81 = evalState (do val <- eval tr ctxt [] (map finalEntry env) (finalise t) []
82 quote 0 val) initEval
84specialise :: Context -> Env -> [(Name, Int)] -> TT Name -> TT Name
85specialise ctxt env limits t
86 = evalState (do val <- eval False ctxt limits (map finalEntry env) (finalise t) []
87 quote 0 val) (initEval { limited = limits })
89-- Like normalise, but we only reduce functions that are marked as okay to
90-- inline (and probably shouldn't reduce lets?)
92simplify :: Context -> Bool -> Env -> TT Name -> TT Name
93simplify ctxt runtime env t
94 = evalState (do val <- eval False ctxt [(UN "lazy", 0),
95 (UN "par", 0),
96 (UN "fork", 0)]
97 (map finalEntry env) (finalise t)
98 [Simplify runtime]
99 quote 0 val) initEval
101hnf :: Context -> Env -> TT Name -> TT Name
102hnf ctxt env t
103 = evalState (do val <- eval False ctxt []
104 (map finalEntry env)
105 (finalise t) [HNF]
106 quote 0 val) initEval
109-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))
111finalEntry :: (Name, Binder (TT Name)) -> (Name, Binder (TT Name))
112finalEntry (n, b) = (n, fmap finalise b)
114bindEnv :: EnvTT n -> TT n -> TT n
115bindEnv [] tm = tm
116bindEnv ((n, Let t v):bs) tm = Bind n (NLet t v) (bindEnv bs tm)
117bindEnv ((n, b):bs) tm = Bind n b (bindEnv bs tm)
119unbindEnv :: EnvTT n -> TT n -> TT n
120unbindEnv [] tm = tm
121unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc
123usable :: Bool -> Name -> [(Name, Int)] -> (Bool, [(Name, Int)])
124usable _ _ ns@((MN 0 "STOP", _) : _) = (False, ns)
125usable True (UN "io_bind") ns = (False, ns)
126usable s n [] = (True, [])
127usable s n ns = case lookup n ns of
128 Just 0 -> (False, ns)
129 Just i -> (True, (n, abs (i-1)) : filter (\ (n', _) -> n/=n') ns)
130 _ -> if s then (True, (n, 0) : filter (\ (n', _) -> n/=n') ns)
131 else (True, (n, 100) : filter (\ (n', _) -> n/=n') ns)
133-- Evaluate in a context of locally named things (i.e. not de Bruijn indexed,
134-- such as we might have during construction of a proof)
136eval :: Bool -> Context -> [(Name, Int)] -> Env -> TT Name ->
137 [EvalOpt] -> Eval Value
138eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
139 spec = Spec `elem` opts
140 simpl = Simplify True `elem` opts
141 atRepl = AtREPL `elem` opts
142 hnf = HNF `elem` opts
144 canSimplify inl inr n stk
145 = (Simplify False `elem` opts && (not inl || elem n stk))
146 || (Simplify True `elem` opts && (not inr || elem n stk))
148 ev ntimes stk top env (P _ n ty)
149 | Just (Let t v) <- lookup n genv = ev ntimes stk top env v
150 ev ntimes_in stk top env (P Ref n ty)
151 | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)
152 | (True, ntimes) <- usable simpl n ntimes_in
153 = do let val = lookupDefAcc Nothing n atRepl ctxt
154 case val of
155 [(Function _ tm, Public)] ->
156 ev ntimes (n:stk) True env tm
157 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty
158 return $ VP nt n vty
159 [(CaseOp inl inr _ _ _ [] tree _ _, acc)]
160 | acc == Public || simpl -> -- unoptimised version
161 if canSimplify inl inr n stk
162 then liftM (VP Ref n) (ev ntimes stk top env ty)
163 else do c <- evCase ntimes (n:stk) top env [] [] tree
164 case c of
165 (Nothing, _) -> liftM (VP Ref n) (ev ntimes stk top env ty)
166 (Just v, _) -> return v
167 _ -> liftM (VP Ref n) (ev ntimes stk top env ty)
168 ev ntimes stk top env (P nt n ty) = liftM (VP nt n) (ev ntimes stk top env ty)
169 ev ntimes stk top env (V i) | i < length env = return $ env !! i
170 | otherwise = return $ VV i
171 ev ntimes stk top env (Bind n (Let t v) sc)
172-- | not simpl || vinstances 0 sc < 2
173 = do v' <- ev ntimes stk top env v --(finalise v)
174 sc' <- ev ntimes stk top (v' : env) sc
175 wknV (-1) sc'
176{- | otherwise -- put this back when the Bind works properly
177 = do t' <- ev ntimes stk top env t
178 v' <- ev ntimes stk top env v --(finalise v)
179 -- use Tmp as a placeholder, then make it a variable reference
180 -- again when evaluation finished
181 sc' <- ev ntimes stk top (v' : env) sc
182 return $ VBind n (Let t' v') (\x -> return sc') -}
183 ev ntimes stk top env (Bind n (NLet t v) sc)
184 = do t' <- ev ntimes stk top env (finalise t)
185 v' <- ev ntimes stk top env (finalise v)
186 sc' <- ev ntimes stk top (v' : env) sc
187 return $ VBind n (Let t' v') (\x -> return sc')
188 ev ntimes stk top env (Bind n b sc)
189 = do b' <- vbind env b
190 return $ VBind n b' (\x -> ev ntimes stk False (x:env) sc)
191 where vbind env t
192 | simpl
193 = fmapMB (\tm -> ev ((MN 0 "STOP", 0) : ntimes)
194 stk top env (finalise tm)) t
195 | otherwise
196 = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t
197-- ev ntimes stk top env (App (App (P _ laz _) _) a)
198-- | laz == UN "lazy"
199-- = trace (showEnvDbg genv a) $ ev ntimes stk top env a
200 ev ntimes stk top env (App f a)
201 = do f' <- ev ntimes stk False env f
202 a' <- ev ntimes stk False env a
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 (TType i) = return $ VType 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 = apply ntimes stk top env f args
212 apply ntimes stk top env (VBind n (Lam t) sc) (a:as)
213 = do a' <- sc a
214 app <- apply ntimes stk top env a' as
215 wknV (-1) app
216-- apply ntimes stk False env f args
217-- | spec = specApply ntimes stk env f args
218 apply ntimes_in stk top env f@(VP Ref n ty) args
219 | not top && hnf = case args of
220 [] -> return f
221 _ -> return $ unload env f args
222 | (True, ntimes) <- usable simpl n ntimes_in
223 = traceWhen traceon (show stk) $
224 do let val = lookupDefAcc Nothing n atRepl ctxt
225 case val of
226 [(CaseOp inl inr _ _ _ ns tree _ _, acc)]
227 | acc == Public -> -- unoptimised version
228 if canSimplify inl inr n stk
229 then return $ unload env (VP Ref n ty) args
230 else do c <- evCase ntimes (n:stk) top env ns args tree
231 case c of
232 (Nothing, _) -> return $ unload env (VP Ref n ty) args
233 (Just v, rest) -> evApply ntimes stk top env rest v
234 [(Operator _ i op, _)] ->
235 if (i <= length args)
236 then case op (take i args) of
237 Nothing -> return $ unload env (VP Ref n ty) args
238 Just v -> evApply ntimes stk top env (drop i args) v
239 else return $ unload env (VP Ref n ty) args
240 _ -> case args of
241 [] -> return f
242 _ -> return $ unload env f args
243 apply ntimes stk top env f (a:as) = return $ unload env f (a:as)
244 apply ntimes stk top env f [] = return f
246-- specApply stk env f@(VP Ref n ty) args
247-- = case lookupCtxt Nothing n statics of
248-- [as] -> if or as
249-- then trace (show (n, map fst (filter (\ (_, s) -> s) (zip args as)))) $
250-- return $ unload env f args
251-- else return $ unload env f args
252-- _ -> return $ unload env f args
253-- specApply stk env f args = return $ unload env f args
255 unload env f [] = f
256 unload env f (a:as) = unload env (VApp f a) as
258 evCase ntimes stk top env ns args tree
259 | length ns <= length args
260 = do let args' = take (length ns) args
261 let rest = drop (length ns) args
262 t <- evTree ntimes stk top env
263 (zipWith (\n t -> (n, t)) ns args') tree
264 return (t, rest)
265 | otherwise = return (Nothing, args)
267 evTree :: [(Name, Int)] -> [Name] -> Bool ->
268 [Value] -> [(Name, Value)] -> SC -> Eval (Maybe Value)
269 evTree ntimes stk top env amap (UnmatchedCase str) = return Nothing
270 evTree ntimes stk top env amap (STerm tm)
271 = do let etm = pToVs (map fst amap) tm
272 etm' <- ev ntimes stk (not (conHeaded tm))
273 (map snd amap ++ env) etm
274 return $ Just etm'
275 evTree ntimes stk top env amap (Case n alts)
276 = case lookup n amap of
277 Just v -> do c <- chooseAlt env v (getValArgs v) alts amap
278 case c of
279 Just (altmap, sc) -> evTree ntimes stk top env altmap sc
280 _ -> do c' <- chooseAlt' ntimes stk env v (getValArgs v) alts amap
281 case c' of
282 Just (altmap, sc) -> evTree ntimes stk top env altmap sc
283 _ -> return Nothing
284 _ -> return Nothing
286 conHeaded tm@(App _ _)
287 | (P (DCon _ _) _ _, args) <- unApply tm = True
288 conHeaded t = False
290 chooseAlt' ntimes stk env _ (f, args) alts amap
291 = do f' <- apply ntimes stk True env f args
292 chooseAlt env f' (getValArgs f') alts amap
294 chooseAlt :: [Value] -> Value -> (Value, [Value]) -> [CaseAlt] -> [(Name, Value)] ->
295 Eval (Maybe ([(Name, Value)], SC))
296 chooseAlt env _ (VP (DCon i a) _ _, args) alts amap
297 | Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)
298 | Just v <- findDefault alts = return $ Just (amap, v)
299 chooseAlt env _ (VP (TCon i a) _ _, args) alts amap
300 | Just (ns, sc) <- findTag i alts = return $ Just (updateAmap (zip ns args) amap, sc)
301 | Just v <- findDefault alts = return $ Just (amap, v)
302 chooseAlt env _ (VConstant c, []) alts amap
303 | Just v <- findConst c alts = return $ Just (amap, v)
304 | Just v <- findDefault alts = return $ Just (amap, v)
305 chooseAlt _ _ _ _ _ = return Nothing
307 -- Replace old variable names in the map with new matches
308 -- (This is possibly unnecessary since we make unique names and don't
309 -- allow repeated variables...?)
310 updateAmap newm amap
311 = newm ++ filter (\ (x, _) -> not (elem x (map fst newm))) amap
312 findTag i [] = Nothing
313 findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
314 findTag i (_ : xs) = findTag i xs
316 findDefault [] = Nothing
317 findDefault (DefaultCase sc : xs) = Just sc
318 findDefault (_ : xs) = findDefault xs
320 findConst c [] = Nothing
321 findConst c (ConstCase c' v : xs) | c == c' = Just v
322 findConst IType (ConCase n 1 [] v : xs) = Just v
323 findConst FlType (ConCase n 2 [] v : xs) = Just v
324 findConst ChType (ConCase n 3 [] v : xs) = Just v
325 findConst StrType (ConCase n 4 [] v : xs) = Just v
326 findConst PtrType (ConCase n 5 [] v : xs) = Just v
327 findConst c (_ : xs) = findConst c xs
329 getValArgs tm = getValArgs' tm []
330 getValArgs' (VApp f a) as = getValArgs' f (a:as)
331 getValArgs' f as = (f, as)
333tmpToV i (VTmp 0) = return $ VV i
334tmpToV i (VP nt n v) = liftM (VP nt n) (tmpToV i v)
336tmpToV i (VBind n b sc) = do b' <- fmapMB (tmpToV i) b
337 let sc' = \x -> do x' <- sc x
338 tmpToV (i + 1) x'
339 return (VBind n b' sc')
340tmpToV i (VApp f a) = liftM2 VApp (tmpToV i f) (tmpToV i a)
341tmpToV i x = return x
343class Quote a where
344 quote :: Int -> a -> Eval (TT Name)
346instance Quote Value where
347 quote i (VP nt n v) = liftM (P nt n) (quote i v)
348 quote i (VV x) = return $ V x
349 quote i (VBind n b sc) = do sc' <- sc (VTmp i)
350 b' <- quoteB b
351 liftM (Bind n b') (quote (i+1) sc')
352 where quoteB t = fmapMB (quote i) t
353 quote i (VApp f a) = liftM2 App (quote i f) (quote i a)
354 quote i (VType u) = return $ TType u
355 quote i VErased = return $ Erased
356 quote i (VConstant c) = return $ Constant c
357 quote i (VTmp x) = return $ V (i - x - 1)
359instance Quote HNF where
360 quote i (HP nt n t) = return (P nt n t)
361 quote i (HV x) = return $ V x
362 quote i (HBind n b sc) = do sc' <- sc (HTmp i)
363 b' <- quoteB b
364 liftM (Bind n b') (quote (i+1) sc')
365 where quoteB t = fmapMB (quote i) t
366 quote i (HApp f env as) = do f' <- quote i f
367 as' <- mapM (iEnv env) as
368 return $ mkApp f' as'
369 where iEnv [] a = return a
370 iEnv (x:xs) a = do x' <- quote i x
371 iEnv xs (weakenTm (-1) (instantiate x' a))
372 quote i (HType u) = return $ TType u
373 quote i (HConstant c) = return $ Constant c
374 quote i (HTmp x) = return $ V (i - x - 1)
376wknV :: Int -> Value -> Eval Value
377wknV i (VV x) = return $ VV (x + i)
378wknV i (VBind n b sc) = do b' <- fmapMB (wknV i) b
379 return $ VBind n b' (\x -> do x' <- sc x
380 wknV i x')
381wknV i (VApp f a) = liftM2 VApp (wknV i f) (wknV i a)
382wknV i t = return t
384wknH :: Int -> HNF -> Eval HNF
385wknH i (HV x) = return $ HV (x + i)
386wknH i (HBind n b sc) = do b' <- fmapMB (wknH i) b
387 return $ HBind n b' (\x -> do x' <- sc x
388 wknH i x')
389wknH i (HApp f env as) = liftM3 HApp (wknH i f) (return env)
390 (return as)
391wknH i t = return t
393-- HEAD NORMAL FORM ---------------------------------------------------------
395eval_hnf :: Context -> Ctxt [Bool] -> Env -> TT Name -> Eval HNF
396eval_hnf ctxt statics genv tm = ev [] tm where
397 ev :: [HNF] -> TT Name -> Eval HNF
398 ev env (P _ n ty)
399 | Just (Let t v) <- lookup n genv = ev env v
400 ev env (P Ref n ty) = case lookupDef Nothing n ctxt of
401 [Function _ t] -> ev env t
402 [TyDecl nt ty] -> return $ HP nt n ty
403 [CaseOp inl _ _ _ _ [] tree _ _] ->
404 do c <- evCase env [] [] tree
405 case c of
406 (Nothing, _, _) -> return $ HP Ref n ty
407 (Just v, _, _) -> return v
408 _ -> return $ HP Ref n ty
409 ev env (P nt n ty) = return $ HP nt n ty
410 ev env (V i) | i < length env = return $ env !! i
411 | otherwise = return $ HV i
412 ev env (Bind n (Let t v) sc)
413 = do v' <- ev env (finalise v)
414 sc' <- ev (v' : env) sc
415 wknH (-1) sc'
416 ev env (Bind n b sc)
417 = do b' <- hbind env b
418 return $ HBind n b' (\x -> ev (x : env) sc)
419 where hbind env t = fmapMB (\tm -> ev env (finalise tm)) t
420 ev env (App f a) = evApply env [a] f
421 ev env (Constant c) = return $ HConstant c
422 ev env (TType i) = return $ HType i
424 evApply env args (App f a) = evApply env (a : args) f
425 evApply env args f = do f' <- ev env f
426 apply env f' args
428 apply env (HBind n (Lam t) sc) (a:as) = do a' <- ev env a
429 sc' <- sc a'
430 app <- apply env sc' as
431 wknH (-1) app
432 apply env (HP Ref n ty) args
433 | [CaseOp _ _ _ _ _ ns tree _ _] <- lookupDef Nothing n ctxt
434 = do c <- evCase env ns args tree
435 case c of
436 (Nothing, _, env') -> return $ unload env' (HP Ref n ty) args
437 (Just v, rest, env') -> do v' <- quote 0 v
438 apply env' v rest
439-- | Just (Operator _ i op) <- lookupDef n ctxt
440-- = if (i <= length args)
441-- then case op (take i args) of
442-- Nothing -> return $ unload env (HP Ref n ty) args
443-- Just v -> evApply env (drop i args) v
444-- else return $ unload env (HP Ref n ty) args
445 apply env f (a:as) = return $ unload env f (a:as)
446 apply env f [] = return f
448 unload env f [] = f
449 unload env f as = HApp f env as
451 evCase env ns args tree
452 | length ns <= length args
453 = do let args' = take (length ns) args
454 let rest = drop (length ns) args
455 (t, env') <- evTree env (zipWith (\n t -> (n, t)) ns args') tree
456 return (t, rest, env')
457 | otherwise = return (Nothing, args, env)
459 evTree :: [HNF] -> [(Name, TT Name)] -> SC -> Eval (Maybe HNF, [HNF])
460 evTree env amap (UnmatchedCase str) = return (Nothing, env)
461 evTree env amap (STerm tm)
462 = do let etm = pToVs (map fst amap) tm
463 amap' <- mapM (ev env) (map snd amap)
464 envw <- mapM (wknH (length amap)) env
465 let env' = amap' ++ envw
466 etm' <- trace (show etm) $ ev env' etm
467 etmq <- quote 0 etm'
468 trace ("Ev: " ++ show (etm, etmq)) $ return $ (Just etm', env')
469 evTree env amap (Case n alts)
470 = case lookup n amap of
471 Just v -> do v' <- ev env v
472 case chooseAlt v' (getValArgs v') alts amap of
473 Just (altmap, sc) -> evTree env altmap sc
474 _ -> return (Nothing, env)
476 chooseAlt :: HNF -> (HNF, [HNF], [TT Name]) ->
477 [CaseAlt] -> [(Name, TT Name)] ->
478 Maybe ([(Name, TT Name)], SC)
479 chooseAlt _ (HP (DCon i a) _ _, env, args) alts amap
480 | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)
481 | Just v <- findDefault alts = Just (amap, v)
482 chooseAlt _ (HP (TCon i a) _ _, env, args) alts amap
483 | Just (ns, sc) <- findTag i alts = Just (updateAmap (zip ns args) amap, sc)
484 | Just v <- findDefault alts = Just (amap, v)
485 chooseAlt _ (HConstant c, env, []) alts amap
486 | Just v <- findConst c alts = Just (amap, v)
487 | Just v <- findDefault alts = Just (amap, v)
488 chooseAlt _ _ _ _ = Nothing
490 -- Replace old variable names in the map with new matches
491 -- (This is possibly unnecessary since we make unique names and don't
492 -- allow repeated variables...?)
493 updateAmap newm amap
494 = newm ++ filter (\ (x, _) -> not (elem x (map fst newm))) amap
495 findTag i [] = Nothing
496 findTag i (ConCase n j ns sc : xs) | i == j = Just (ns, sc)
497 findTag i (_ : xs) = findTag i xs
499 findDefault [] = Nothing
500 findDefault (DefaultCase sc : xs) = Just sc
501 findDefault (_ : xs) = findDefault xs
503 findConst c [] = Nothing
504 findConst c (ConstCase c' v : xs) | c == c' = Just v
505 findConst IType (ConCase n 1 [] v : xs) = Just v
506 findConst FlType (ConCase n 2 [] v : xs) = Just v
507 findConst ChType (ConCase n 3 [] v : xs) = Just v
508 findConst StrType (ConCase n 4 [] v : xs) = Just v
509 findConst PtrType (ConCase n 5 [] v : xs) = Just v
510 findConst BIType (ConCase n 6 [] v : xs) = Just v
511 findConst B8Type (ConCase n 7 [] v : xs) = Just v
512 findConst B16Type (ConCase n 8 [] v : xs) = Just v
513 findConst B32Type (ConCase n 9 [] v : xs) = Just v
514 findConst B64Type (ConCase n 10 [] v : xs) = Just v
515 findConst c (_ : xs) = findConst c xs
517 getValArgs (HApp t env args) = (t, env, args)
518 getValArgs t = (t, [], [])
520convEq' ctxt x y = evalStateT (convEq ctxt x y) (0, [])
522convEq :: Context -> TT Name -> TT Name -> StateT UCs TC Bool
523convEq ctxt = ceq [] where
524 ceq :: [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool
525 ceq ps (P xt x _) (P yt y _)
526 | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True
527 | otherwise = sameDefs ps x y
528 ceq ps (V x) (V y) = return (x == y)
529 ceq ps (Bind _ xb xs) (Bind _ yb ys)
530 = liftM2 (&&) (ceqB ps xb yb) (ceq ps xs ys)
531 where
532 ceqB ps (Let v t) (Let v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')
533 ceqB ps (Guess v t) (Guess v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')
534 ceqB ps b b' = ceq ps (binderTy b) (binderTy b')
535 ceq ps (App fx ax) (App fy ay) = liftM2 (&&) (ceq ps fx fy) (ceq ps ax ay)
536 ceq ps (Constant x) (Constant y) = return (x == y)
537 ceq ps (TType x) (TType y) = do (v, cs) <- get
538 put (v, ULE x y : cs)
539 return True
540 ceq ps Erased _ = return True
541 ceq ps _ Erased = return True
542 ceq ps _ _ = return False
544 caseeq ps (Case n cs) (Case n' cs') = caseeqA ((n,n'):ps) cs cs'
545 where
546 caseeqA ps (ConCase x i as sc : rest) (ConCase x' i' as' sc' : rest')
547 = do q1 <- caseeq (zip as as' ++ ps) sc sc'
548 q2 <- caseeqA ps rest rest'
549 return $ x == x' && i == i' && q1 && q2
550 caseeqA ps (ConstCase x sc : rest) (ConstCase x' sc' : rest')
551 = do q1 <- caseeq ps sc sc'
552 q2 <- caseeqA ps rest rest'
553 return $ x == x' && q1 && q2
554 caseeqA ps (DefaultCase sc : rest) (DefaultCase sc' : rest')
555 = liftM2 (&&) (caseeq ps sc sc') (caseeqA ps rest rest')
556 caseeqA ps [] [] = return True
557 caseeqA ps _ _ = return False
558 caseeq ps (STerm x) (STerm y) = ceq ps x y
559 caseeq ps (UnmatchedCase _) (UnmatchedCase _) = return True
560 caseeq ps _ _ = return False
562 sameDefs ps x y = case (lookupDef Nothing x ctxt, lookupDef Nothing y ctxt) of
563 ([Function _ xdef], [Function _ ydef])
564 -> ceq ((x,y):ps) xdef ydef
565 ([CaseOp _ _ _ _ _ _ xdef _ _],
566 [CaseOp _ _ _ _ _ _ ydef _ _])
567 -> caseeq ((x,y):ps) xdef ydef
568 _ -> return False
570-- SPECIALISATION -----------------------------------------------------------
571-- We need too much control to be able to do this by tweaking the main
572-- evaluator
574spec :: Context -> Ctxt [Bool] -> Env -> TT Name -> Eval (TT Name)
575spec ctxt statics genv tm = error "spec undefined"
577-- CONTEXTS -----------------------------------------------------------------
579{- A definition is either a simple function (just an expression with a type),
580 a constant, which could be a data or type constructor, an axiom or as an
581 yet undefined function, or an Operator.
582 An Operator is a function which explains how to reduce.
583 A CaseOp is a function defined by a simple case tree -}
585data Def = Function Type Term
586 | TyDecl NameType Type
587 | Operator Type Int ([Value] -> Maybe Value)
588 | CaseOp Bool Bool -- compile-time/run-time inlinable
589 Type
590 [Either Term (Term, Term)] -- original definition
591 [([Name], Term, Term)] -- simplified definition
592 [Name] SC -- Compile time case definition
593 [Name] SC -- Run time cae definitions
594{-!
595deriving instance Binary Def
596!-}
598instance Show Def where
599 show (Function ty tm) = "Function: " ++ show (ty, tm)
600 show (TyDecl nt ty) = "TyDecl: " ++ show nt ++ " " ++ show ty
601 show (Operator ty _ _) = "Operator: " ++ show ty
602 show (CaseOp inlc inlr ty ps_in ps ns sc ns' sc')
603 = "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++
604 show ns ++ " " ++ show sc ++ "\n" ++
605 show ns' ++ " " ++ show sc' ++ "\n" ++
606 if inlc then "Inlinable\n" else "Not inlinable\n"
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!-}
658-- | Contexts used for global definitions and for proof state. They contain
659-- universe constraints and existing definitions.
660data Context = MkContext {
661 uconstraints :: [UConstraint],
662 next_tvar :: Int,
663 definitions :: Ctxt (Def, Accessibility, Totality)
664 }
666-- | The initial empty context
667initContext = MkContext [] 0 emptyContext
669-- | Get the definitions from a context
670ctxtAlist :: Context -> [(Name, Def)]
671ctxtAlist ctxt = map (\(n, (d, a, t)) -> (n, d)) $ toAlist (definitions ctxt)
673veval ctxt env t = evalState (eval False ctxt [] env t []) initEval
675addToCtxt :: Name -> Term -> Type -> Context -> Context
676addToCtxt n tm ty uctxt
677 = let ctxt = definitions uctxt
678 ctxt' = addDef n (Function ty tm, Public, Unchecked) ctxt in
679 uctxt { definitions = ctxt' }
681setAccess :: Name -> Accessibility -> Context -> Context
682setAccess n a uctxt
683 = let ctxt = definitions uctxt
684 ctxt' = updateDef n (\ (d, _, t) -> (d, a, t)) ctxt in
685 uctxt { definitions = ctxt' }
687setTotal :: Name -> Totality -> Context -> Context
688setTotal n t uctxt
689 = let ctxt = definitions uctxt
690 ctxt' = updateDef n (\ (d, a, _) -> (d, a, t)) ctxt in
691 uctxt { definitions = ctxt' }
693addCtxtDef :: Name -> Def -> Context -> Context
694addCtxtDef n d c = let ctxt = definitions c
695 ctxt' = addDef n (d, Public, Unchecked) ctxt in
696 c { definitions = ctxt' }
698addTyDecl :: Name -> Type -> Context -> Context
699addTyDecl n ty uctxt
700 = let ctxt = definitions uctxt
701 ctxt' = addDef n (TyDecl Ref ty, Public, Unchecked) ctxt in
702 uctxt { definitions = ctxt' }
704addDatatype :: Datatype Name -> Context -> Context
705addDatatype (Data n tag ty cons) uctxt
706 = let ctxt = definitions uctxt
707 ty' = normalise uctxt [] ty
708 ctxt' = addCons 0 cons (addDef n
709 (TyDecl (TCon tag (arity ty')) ty, Public, Unchecked) ctxt) in
710 uctxt { definitions = ctxt' }
711 where
712 addCons tag [] ctxt = ctxt
713 addCons tag ((n, ty) : cons) ctxt
714 = let ty' = normalise uctxt [] ty in
715 addCons (tag+1) cons (addDef n
716 (TyDecl (DCon tag (arity ty')) ty, Public, Unchecked) ctxt)
718addCasedef :: Name -> Bool -> Bool -> Bool -> Bool ->
719 [Either Term (Term, Term)] ->
720 [([Name], Term, Term)] ->
721 [([Name], Term, Term)] ->
722 Type -> Context -> Context
723addCasedef n alwaysInline tcase covering asserted ps_in ps psrt ty uctxt
724 = let ctxt = definitions uctxt
725 access = case lookupDefAcc Nothing n False uctxt of
726 [(_, acc)] -> acc
727 _ -> Public
728 ctxt' = case (simpleCase tcase covering CompileTime (FC "" 0) ps,
729 simpleCase tcase covering RunTime (FC "" 0) psrt) of
730 (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) ->
731 let inl = alwaysInline
732 inlc = (inl || small n args sc') && (not asserted)
733 inlr = inl || small n args sc' in
734 addDef n (CaseOp inlc inlr
735 ty ps_in ps args sc args' sc',
736 access, Unchecked) ctxt in
737 uctxt { definitions = ctxt' }
739simplifyCasedef :: Name -> Context -> Context
740simplifyCasedef n uctxt
741 = let ctxt = definitions uctxt
742 ctxt' = case lookupCtxt Nothing n ctxt of
743 [(CaseOp inl inr ty [] ps args sc args' sc', acc, tot)] ->
744 ctxt -- nothing to simplify (or already done...)
745 [(CaseOp inl inr ty ps_in ps args sc args' sc', acc, tot)] ->
746 let pdef = map debind $ map simpl ps_in in
747 case simpleCase False True CompileTime (FC "" 0) pdef of
748 OK (CaseDef args sc _) ->
749 addDef n (CaseOp inl inr
750 ty ps_in ps args sc args' sc',
751 acc, tot) ctxt
752 _ -> ctxt in
753 uctxt { definitions = ctxt' }
754 where
755 depat acc (Bind n (PVar t) sc)
756 = depat (n : acc) (instantiate (P Bound n t) sc)
757 depat acc x = (acc, x)
758 debind (Right (x, y)) = let (vs, x') = depat [] x
759 (_, y') = depat [] y in
760 (vs, x', y')
761 debind (Left x) = let (vs, x') = depat [] x in
762 (vs, x', Impossible)
763 simpl (Right (x, y)) = Right (x, simplify uctxt False [] y)
764 simpl t = t
766addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) ->
767 Context -> Context
768addOperator n ty a op uctxt
769 = let ctxt = definitions uctxt
770 ctxt' = addDef n (Operator ty a op, Public, Unchecked) ctxt in
771 uctxt { definitions = ctxt' }
773tfst (a, _, _) = a
775lookupNames :: Maybe [String] -> Name -> Context -> [Name]
776lookupNames root n ctxt
777 = let ns = lookupCtxtName root n (definitions ctxt) in
778 map fst ns
780lookupTy :: Maybe [String] -> Name -> Context -> [Type]
781lookupTy root n ctxt
782 = do def <- lookupCtxt root n (definitions ctxt)
783 case tfst def of
784 (Function ty _) -> return ty
785 (TyDecl _ ty) -> return ty
786 (Operator ty _ _) -> return ty
787 (CaseOp _ _ ty _ _ _ _ _ _) -> return ty
789isConName :: Maybe [String] -> Name -> Context -> Bool
790isConName root n ctxt
791 = or $ do def <- lookupCtxt root n (definitions ctxt)
792 case tfst def of
793 (TyDecl (DCon _ _) _) -> return True
794 (TyDecl (TCon _ _) _) -> return True
795 _ -> return False
797isFnName :: Maybe [String] -> Name -> Context -> Bool
798isFnName root n ctxt
799 = or $ do def <- lookupCtxt root n (definitions ctxt)
800 case tfst def of
801 (Function _ _) -> return True
802 (Operator _ _ _) -> return True
803 (CaseOp _ _ _ _ _ _ _ _ _) -> return True
804 _ -> return False
806lookupP :: Maybe [String] -> Name -> Context -> [Term]
807lookupP root n ctxt
808 = do def <- lookupCtxt root n (definitions ctxt)
809 p <- case def of
810 (Function ty tm, a, _) -> return (P Ref n ty, a)
811 (TyDecl nt ty, a, _) -> return (P nt n ty, a)
812 (CaseOp _ _ ty _ _ _ _ _ _, a, _) -> return (P Ref n ty, a)
813 (Operator ty _ _, a, _) -> return (P Ref n ty, a)
814 case snd p of
815 Hidden -> []
816 _ -> return (fst p)
818lookupDef :: Maybe [String] -> Name -> Context -> [Def]
819lookupDef root n ctxt = map tfst $ lookupCtxt root n (definitions ctxt)
821lookupDefAcc :: Maybe [String] -> Name -> Bool -> Context ->
822 [(Def, Accessibility)]
823lookupDefAcc root n mkpublic ctxt
824 = map mkp $ lookupCtxt root n (definitions ctxt)
825 where mkp (d, a, _) = if mkpublic then (d, Public) else (d, a)
827lookupTotal :: Name -> Context -> [Totality]
828lookupTotal n ctxt = map mkt $ lookupCtxt Nothing n (definitions ctxt)
829 where mkt (d, a, t) = t
831lookupVal :: Maybe [String] -> Name -> Context -> [Value]
832lookupVal root n ctxt
833 = do def <- lookupCtxt root n (definitions ctxt)
834 case tfst def of
835 (Function _ htm) -> return (veval ctxt [] htm)
836 (TyDecl nt ty) -> return (VP nt n (veval ctxt [] ty))
838lookupTyEnv :: Name -> Env -> Maybe (Int, Type)
839lookupTyEnv n env = li n 0 env where
840 li n i [] = Nothing
841 li n i ((x, b): xs)
842 | n == x = Just (i, binderTy b)
843 | otherwise = li n (i+1) xs