git.iko.soy/Idris-dev
on ccd64c7 help sign in
Idris-dev/src/Evaluate.hs
84 lines 2.9 kB history raw
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
3module Evaluate(normalise) where
5import Debug.Trace
6import Core
8normalise :: Context -> Env -> TT Name -> TT Name
9normalise ctxt env t = quote 0 (eval ctxt (evalEnv env) (hoas [] t))
11type HEnv = [(Name, Binder HTT)]
13evalEnv :: Env -> HEnv
14evalEnv = map (\ (n, b) -> (n, fmap (hoas []) b))
16-- We just evaluate HOAS terms. Any de Bruijn indices will refer to higher
17-- level things, so, if we remove a binder, we need to strengthen the
18-- indices appropriately.
20eval :: Context -> HEnv -> HTT -> HTT
21eval ctxt env t = ev t where
22 ev (HP Ref n ty)
23 | Just v <- lookupVal n ctxt = v -- FIXME! Needs evalling
24 ev (HP nt n ty) = HP nt n (ev ty)
25{-
26 ev (HV i)
27 | i < length env = case env!! i of
28 (n, Let t v) -> ev v
29 _ -> HV i
30 | otherwise = HV i
31-}
32 ev (HApp f t a)
33 = evSpine f [(a, t)]
34 where evSpine (HApp f t a) sp = evSpine f ((a, t):sp)
35 evSpine f sp = evAp f sp
36 ev (HBind n (Let t v) sc) = weaken (-1) (ev (sc (weaken 1 (ev v))))
37 ev (HBind n b sc)
38 = HBind n (evB b) (\x -> ev (sc x))
39 where evB (Lam t) = Lam (ev t)
40 evB (Pi t) = Pi (ev t)
41 evB (Hole t) = Hole (ev t)
42 evB (Guess t v) = Guess (ev t) (ev v)
43 evB (PVar t) = PVar (ev t)
44 ev tm = tm -- Constructors + constants
46 -- TODO:add PE magic here - nothing is evaluated yet
48 evAp f sp = evAp' (ev f) sp
49 evAp' (HBind n (Lam ty) sc) ((a, t):sp)
50 = weaken (-1) (evAp' (sc (weaken 1 (ev a))) sp)
51 evAp' f sp = apply f (map (\ (a, t) -> (ev a, ev t)) sp)
53 apply f [] = f
54 apply f ((a, t):xs) = apply (HApp f t a) xs
56-- Adjust de Bruijn indices across a term
58weaken :: Int -> HTT -> HTT
59weaken w (HV i) = HV (i + w)
60weaken w (HBind n b sc)
61 = HBind n (weakenB b) (\x -> weaken w (sc x))
62 where weakenB (Lam t) = Lam (weaken w t)
63 weakenB (Pi t) = Pi (weaken w t)
64 weakenB (Let t v) = Let (weaken w t) (weaken w v)
65 weakenB (Hole t) = Hole (weaken w t)
66 weakenB (Guess t v) = Guess (weaken w t) (weaken w v)
67 weakenB (PVar t) = PVar (weaken w t)
68weaken w (HApp f t a) = HApp (weaken w f) (weaken w t) (weaken w a)
69weaken w tm = tm
71quote :: Int -> HTT -> TT Name
72quote env (HP nt n t) = P nt n (quote env t)
73quote env (HV i) = V i
74quote env (HBind n b sc)
75 = Bind n (quoteB b) (quote (env+1) (sc (HTmp (env+1))))
76 where quoteB (Lam t) = Lam (quote env t)
77 quoteB (Pi t) = Pi (quote env t)
78 quoteB (Let t v) = Let (quote env t) (quote env v)
79 quoteB (Hole t) = Hole (quote env t)
80 quoteB (Guess t v) = Guess (quote env t) (quote env v)
81 quoteB (PVar t) = PVar (quote env t)
82quote env (HApp f t a) = App (quote env f) (quote env t) (quote env a)
83quote env (HSet i) = Set i
84quote env (HTmp i) = V (env-i)