@@ -6,79 +6,129 @@ import Debug.Trace
66import Core
77
88normalise :: Context -> Env -> TT Name -> TT Name
9−normalise ctxt env t = quote 0 (eval ctxt (evalEnv env) (hoas [] t))
10−
11−type HEnv = [(Name, Binder HTT)]
9+normalise ctxt env t = quote 0 (eval ctxt (weakenEnv env) t)
1210
13−evalEnv :: Env -> HEnv
14−evalEnv = map (\ (n, b) -> (n, fmap (hoas []) b))
11+data Value = VP NameType Name Value
12+ | VV Int
13+ | VBind Name (Binder Value) (Value -> Value)
14+ | VApp Value Value
15+ | VSet Int
16+ | VTmp Int
1517
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.
19−
20−eval :: Context -> HEnv -> HTT -> HTT
21−eval 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
18+eval :: Context -> Env -> TT Name -> Value
19+eval ctxt genv tm = ev [] tm where
20+-- ev env (P Ref n ty)
21+-- | Just v <- lookupP n ctxt = v -- FIXME! Needs evalling
22+ ev env (P nt n ty) = VP nt n (ev env ty)
23+ ev env (V i) | i < length env = env !! i
24+ | i < length env + length genv
25+ = case genv !! (i - length env) of
26+ (_, Let t v) -> ev env v
27+ _ -> VV i
28+ | otherwise = error $ "Internal error: V" ++ show i
29+ ev env (Bind n (Let t v) sc)
30+ = ev (ev env v : env) sc
31+ ev env (Bind n b sc) = VBind n (vbind env b) (\x -> ev (x:env) sc)
32+ where vbind env (Lam t) = Lam (ev env t)
33+ vbind env (Pi t) = Pi (ev env t)
34+ vbind env (Hole t) = Hole (ev env t)
35+ vbind env (PVar t) = PVar (ev env t)
36+ vbind env (Guess v t) = Guess (ev env v) (ev env t)
37+ ev env (App f a) = evApply env [a] f
38+ ev env (Set i) = VSet i
39+
40+ evApply env args (App f a) = evApply env (a:args) f
41+ evApply env args f = apply env (ev env f) (reverse args)
4542
46− -- TODO:add PE magic here - nothing is evaluated yet
43+ apply env (VBind n (Lam t) sc) (a:as) = apply env (sc (ev env a)) as
44+ apply env f (a:as) = unload env f (a:as)
45+ apply env f [] = f
4746
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)
47+ unload env f [] = f
48+ unload env f (a:as) = unload env (VApp f (ev env a)) as
5249
53− apply f [] = f
54− apply f ((a, t):xs) = apply (HApp f t a) xs
50+quote :: Int -> Value -> TT Name
51+quote i (VP nt n v) = P nt n (quote i v)
52+quote i (VV x) = V x
53+quote i (VBind n b sc) = Bind n (quoteB b) (quote (i+1) (sc (VTmp (i+1))))
54+ where quoteB t = fmap (quote i) t
55+quote i (VApp f a) = App (quote i f) (quote i a)
56+quote i (VSet u) = Set u
57+quote i (VTmp x) = V (i - x)
5558
56−-- Adjust de Bruijn indices across a term
57−
58−weaken :: Int -> HTT -> HTT
59−weaken w (HV i) = HV (i + w)
60−weaken 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)
68−weaken w (HApp f t a) = HApp (weaken w f) (weaken w t) (weaken w a)
69−weaken w tm = tm
59+-- normalise ctxt env t = quote 0 (eval ctxt (evalEnv env) (hoas [] t))
60+--
61+-- type HEnv = [(Name, Binder HTT)]
62+--
63+-- evalEnv :: Env -> HEnv
64+-- evalEnv = map (\ (n, b) -> (n, fmap (hoas []) b))
65+--
66+-- We just evaluate HOAS terms. Any de Bruijn indices will refer to higher
67+-- level things, so, if we remove a binder, we need to strengthen the
68+-- indices appropriately.
7069
71−quote :: Int -> HTT -> TT Name
72−quote env (HP nt n t) = P nt n (quote env t)
73−quote env (HV i) = V i
74−quote 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)
82−quote env (HApp f t a) = App (quote env f) (quote env t) (quote env a)
83−quote env (HSet i) = Set i
84−quote env (HTmp i) = V (env-i)
70+-- eval :: Context -> HEnv -> HTT -> HTT
71+-- eval ctxt env t = ev t where
72+-- ev (HP Ref n ty)
73+-- | Just v <- lookupVal n ctxt = v -- FIXME! Needs evalling
74+-- ev (HP nt n ty) = HP nt n (ev ty)
75+-- {-
76+-- ev (HV i)
77+-- | i < length env = case env!! i of
78+-- (n, Let t v) -> ev v
79+-- _ -> HV i
80+-- | otherwise = HV i
81+-- -}
82+-- ev (HApp f t a)
83+-- = evSpine f [(a, t)]
84+-- where evSpine (HApp f t a) sp = evSpine f ((a, t):sp)
85+-- evSpine f sp = evAp f sp
86+-- ev (HBind n (Let t v) sc) = weaken (-1) (ev (sc (weaken 1 (ev v))))
87+-- ev (HBind n b sc)
88+-- = HBind n (evB b) (\x -> ev (sc x))
89+-- where evB (Lam t) = Lam (ev t)
90+-- evB (Pi t) = Pi (ev t)
91+-- evB (Hole t) = Hole (ev t)
92+-- evB (Guess t v) = Guess (ev t) (ev v)
93+-- evB (PVar t) = PVar (ev t)
94+-- ev tm = tm -- Constructors + constants
95+--
96+-- -- TODO:add PE magic here - nothing is evaluated yet
97+--
98+-- evAp f sp = evAp' (ev f) sp
99+-- evAp' (HBind n (Lam ty) sc) ((a, t):sp)
100+-- = weaken (-1) (evAp' (sc (weaken 1 (ev a))) sp)
101+-- evAp' f sp = apply f (map (\ (a, t) -> (ev a, ev t)) sp)
102+--
103+-- apply f [] = f
104+-- apply f ((a, t):xs) = apply (HApp f t a) xs
105+--
106+-- -- Adjust de Bruijn indices across a term
107+--
108+-- weaken :: Int -> HTT -> HTT
109+-- weaken w (HV i) = HV (i + w)
110+-- weaken w (HBind n b sc)
111+-- = HBind n (weakenB b) (\x -> weaken w (sc x))
112+-- where weakenB (Lam t) = Lam (weaken w t)
113+-- weakenB (Pi t) = Pi (weaken w t)
114+-- weakenB (Let t v) = Let (weaken w t) (weaken w v)
115+-- weakenB (Hole t) = Hole (weaken w t)
116+-- weakenB (Guess t v) = Guess (weaken w t) (weaken w v)
117+-- weakenB (PVar t) = PVar (weaken w t)
118+-- weaken w (HApp f t a) = HApp (weaken w f) (weaken w t) (weaken w a)
119+-- weaken w tm = tm
120+--
121+-- quote :: Int -> HTT -> TT Name
122+-- quote env (HP nt n t) = P nt n (quote env t)
123+-- quote env (HV i) = V i
124+-- quote env (HBind n b sc)
125+-- = Bind n (quoteB b) (quote (env+1) (sc (HTmp (env+1))))
126+-- where quoteB (Lam t) = Lam (quote env t)
127+-- quoteB (Pi t) = Pi (quote env t)
128+-- quoteB (Let t v) = Let (quote env t) (quote env v)
129+-- quoteB (Hole t) = Hole (quote env t)
130+-- quoteB (Guess t v) = Guess (quote env t) (quote env v)
131+-- quoteB (PVar t) = PVar (quote env t)
132+-- quote env (HApp f t a) = App (quote env f) (quote env t) (quote env a)
133+-- quote env (HSet i) = Set i
134+-- quote env (HTmp i) = V (env-i)