git.iko.soy/Idris-dev
on master help sign in
Purge HTT, fix evaluator and contexts
d615021Edwin Brady
src/Core.hs−73
compare with master
unifiedsplit
@@ -161,77 +161,4 @@ weakenEnv env = wk (length env - 1) env
161weakenTmEnv :: Int -> EnvTT n -> EnvTT n
161weakenTmEnv :: Int -> EnvTT n -> EnvTT n
162weakenTmEnv i = map (\ (n, b) -> (n, fmap (weakenTm i) b))
162weakenTmEnv i = map (\ (n, b) -> (n, fmap (weakenTm i) b))
163
163
164−-- WELL TYPED TERMS AS HOAS -------------------------------------------------
165−
166−data HTT = HP NameType Name HTT
167− | HV Int
168− | HBind Name (Binder HTT) (HTT -> HTT)
169− | HApp HTT HTT
170− | HSet Int
171− | HTmp Int
172−
173−instance Show HTT where
174− show h = "<<HOAS>>"
175−
176−hoas :: [HTT] -> TT Name -> HTT
177−hoas env (P nt n ty) = HP nt n (hoas env ty)
178−hoas env (V i) | i < length env = env!!i
179− | otherwise = HV i
180−hoas env (Bind n b sc) = HBind n (hbind b) (\x -> hoas (x:env) sc)
181− where hbind (Lam t) = Lam (hoas env t)
182− hbind (Pi t) = Pi (hoas env t)
183− hbind (Hole t) = Hole (hoas env t)
184− hbind (PVar t) = PVar (hoas env t)
185− hbind (Let v t) = Let (hoas env v) (hoas env t)
186− hbind (Guess v t) = Guess (hoas env v) (hoas env t)
187−hoas env (App f a) = HApp (hoas env f) (hoas env a)
188−hoas env (Set i) = HSet i
189−
190−-- CONTEXTS -----------------------------------------------------------------
191−
192−data Fun = Fun Type HTT Term HTT
193− deriving Show
194−
195−data Def = Function Fun
196− | Constant NameType Type HTT
197− deriving Show
198
164
199−type Context = [(Name, Def)]
200−
201−emptyContext = []
202−
203−addToCtxt :: Name -> Term -> Type -> Context -> Context
204−addToCtxt n tm ty ctxt = (n, Function (Fun ty (hoas [] ty)
205− tm (hoas [] tm))) : ctxt
206−
207−lookupTy :: Name -> Context -> Maybe Type
208−lookupTy n ctxt = do def <- lookup n ctxt
209− case def of
210− (Function (Fun ty _ _ _)) -> return ty
211− (Constant _ ty _) -> return ty
212−
213−lookupP :: Name -> Context -> Maybe Term
214−lookupP n ctxt
215− = do def <- lookup n ctxt
216− case def of
217− (Function (Fun ty _ tm _)) -> return (P Ref n ty)
218− (Constant nt ty hty) -> return (P nt n ty)
219−
220−lookupVal :: Name -> Context -> Maybe HTT
221−lookupVal n ctxt
222− = do def <- lookup n ctxt
223− case def of
224− (Function (Fun _ _ _ htm)) -> return htm
225− (Constant nt ty hty) -> return (HP nt n hty)
226−
227−lookupTyEnv :: Name -> Env -> Maybe (Int, Type)
228−lookupTyEnv n env = li n 0 env where
229− li n i [] = Nothing
230− li n i ((x, b): xs)
231− | n == x = Just (i, binderTy b)
232− | otherwise = li n (i+1) xs
233−
234−
235−x = UN ["x"]
236−xt = UN ["X"]
237−testtm = RBind xt (Lam (RSet 0)) (RBind x (Lam (Var xt)) (Var x))
src/Evaluate.hs+65−87
@@ -1,12 +1,14 @@
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
2
2
3−module Evaluate(normalise) where
3+module Evaluate(normalise,
4+ Fun(..), Def(..), Context,
5+ emptyContext, addToCtxt, addConstant,
6+ lookupTy, lookupP, lookupVal, lookupTyEnv) where
4
7
5import Debug.Trace
8import Debug.Trace
6import Core
9import Core
7
10
8−normalise :: Context -> Env -> TT Name -> TT Name
11+-- VALUES (as HOAS) ---------------------------------------------------------
9−normalise ctxt env t = quote 0 (eval ctxt (weakenEnv env) t)
10
12
11data Value = VP NameType Name Value
13data Value = VP NameType Name Value
12 | VV Int
14 | VV Int
@@ -15,10 +17,18 @@ data Value = VP NameType Name Value
15 | VSet Int
17 | VSet Int
16 | VTmp Int
18 | VTmp Int
17
19
20+instance Show Value where
21+ show = show . quote 0
22+
23+-- THE EVALUATOR ------------------------------------------------------------
24+
25+normalise :: Context -> Env -> TT Name -> TT Name
26+normalise ctxt env t = quote 0 (eval ctxt (weakenEnv env) t)
27+
18eval :: Context -> Env -> TT Name -> Value
28eval :: Context -> Env -> TT Name -> Value
19eval ctxt genv tm = ev [] tm where
29eval ctxt genv tm = ev [] tm where
20−-- ev env (P Ref n ty)
30+ ev env (P Ref n ty)
21−-- | Just v <- lookupP n ctxt = v -- FIXME! Needs evalling
31+ | Just v <- lookupVal n ctxt = v -- FIXME! Needs evalling
22 ev env (P nt n ty) = VP nt n (ev env ty)
32 ev env (P nt n ty) = VP nt n (ev env ty)
23 ev env (V i) | i < length env = env !! i
33 ev env (V i) | i < length env = env !! i
24 | i < length env + length genv
34 | i < length env + length genv
@@ -29,16 +39,12 @@ eval ctxt genv tm = ev [] tm where
29 ev env (Bind n (Let t v) sc)
39 ev env (Bind n (Let t v) sc)
30 = ev (ev env v : env) sc
40 = ev (ev env v : env) sc
31 ev env (Bind n b sc) = VBind n (vbind env b) (\x -> ev (x:env) sc)
41 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)
42+ where vbind env t = fmap (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
43 ev env (App f a) = evApply env [a] f
38 ev env (Set i) = VSet i
44 ev env (Set i) = VSet i
39
45
40 evApply env args (App f a) = evApply env (a:args) f
46 evApply env args (App f a) = evApply env (a:args) f
41− evApply env args f = apply env (ev env f) (reverse args)
47+ evApply env args f = apply env (ev env f) args
42
48
43 apply env (VBind n (Lam t) sc) (a:as) = apply env (sc (ev env a)) as
49 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)
50 apply env f (a:as) = unload env f (a:as)
@@ -56,79 +62,51 @@ quote i (VApp f a) = App (quote i f) (quote i a)
56quote i (VSet u) = Set u
62quote i (VSet u) = Set u
57quote i (VTmp x) = V (i - x)
63quote i (VTmp x) = V (i - x)
58
64
59−-- normalise ctxt env t = quote 0 (eval ctxt (evalEnv env) (hoas [] t))
65+
60−--
66+-- CONTEXTS -----------------------------------------------------------------
67+
68+data Fun = Fun Type Value Term Value
69+ deriving Show
70+
71+data Def = Function Fun
72+ | Constant NameType Type Value
73+ deriving Show
74+
61−-- type HEnv = [(Name, Binder HTT)]
75+type Context = [(Name, Def)]
62−--
76+
63−-- evalEnv :: Env -> HEnv
77+emptyContext = []
64−-- evalEnv = map (\ (n, b) -> (n, fmap (hoas []) b))
78+
65−--
79+addToCtxt :: Name -> Term -> Type -> Context -> Context
66−-- We just evaluate HOAS terms. Any de Bruijn indices will refer to higher
80+addToCtxt n tm ty ctxt = (n, Function (Fun ty (eval ctxt [] ty)
67−-- level things, so, if we remove a binder, we need to strengthen the
81+ tm (eval ctxt [] tm))) : ctxt
68−-- indices appropriately.
82+
69−
83+addConstant :: Name -> Type -> Context -> Context
70−-- eval :: Context -> HEnv -> HTT -> HTT
84+addConstant n ty ctxt = (n, Constant Ref ty (eval ctxt [] ty)) : ctxt
71−-- eval ctxt env t = ev t where
85+
72−-- ev (HP Ref n ty)
86+lookupTy :: Name -> Context -> Maybe Type
73−-- | Just v <- lookupVal n ctxt = v -- FIXME! Needs evalling
87+lookupTy n ctxt = do def <- lookup n ctxt
74−-- ev (HP nt n ty) = HP nt n (ev ty)
88+ case def of
75−-- {-
89+ (Function (Fun ty _ _ _)) -> return ty
76−-- ev (HV i)
90+ (Constant _ ty _) -> return ty
77−-- | i < length env = case env!! i of
91+
78−-- (n, Let t v) -> ev v
92+lookupP :: Name -> Context -> Maybe Term
79−-- _ -> HV i
93+lookupP n ctxt
94+ = do def <- lookup n ctxt
95+ case def of
96+ (Function (Fun ty _ tm _)) -> return (P Ref n ty)
97+ (Constant nt ty hty) -> return (P nt n ty)
98+
99+lookupVal :: Name -> Context -> Maybe Value
100+lookupVal n ctxt
101+ = do def <- lookup n ctxt
102+ case def of
103+ (Function (Fun _ _ _ htm)) -> return htm
104+ (Constant nt ty hty) -> return (VP nt n hty)
105+
106+lookupTyEnv :: Name -> Env -> Maybe (Int, Type)
107+lookupTyEnv n env = li n 0 env where
108+ li n i [] = Nothing
109+ li n i ((x, b): xs)
110+ | n == x = Just (i, binderTy b)
80−-- | otherwise = HV i
111+ | otherwise = li n (i+1) xs
81−-- -}
112+
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)
src/Typecheck.hs+3−3
@@ -133,11 +133,11 @@ checkProgram ctxt [] = return ctxt
133checkProgram ctxt ((n, RConst t):xs)
133checkProgram ctxt ((n, RConst t):xs)
134 = do (t', tt') <- trace (show n) $ check ctxt [] t
134 = do (t', tt') <- trace (show n) $ check ctxt [] t
135 isSet tt'
135 isSet tt'
136− checkProgram ((n, Constant Ref t' (hoas [] t')):ctxt) xs
136+ checkProgram (addConstant n t' ctxt) xs
137checkProgram ctxt ((n, RFunction (RawFun ty val)):xs)
137checkProgram ctxt ((n, RFunction (RawFun ty val)):xs)
138 = do (ty', tyt') <- trace (show n) $ check ctxt [] ty
138 = do (ty', tyt') <- trace (show n) $ check ctxt [] ty
139 (val', valt') <- check ctxt [] val
139 (val', valt') <- check ctxt [] val
140 isSet tyt'
140 isSet tyt'
141 converts ctxt [] ty' valt'
141 converts ctxt [] ty' valt'
142− checkProgram ((n, Function (Fun ty' (hoas [] ty')
142+ checkProgram (addToCtxt n val' ty' ctxt) xs
143− val' (hoas [] val'))):ctxt) xs
143+