git.iko.soy/Idris-dev
on master help sign in
Fixing evaluator bugs
9c6ea4aEdwin Brady
src/Core.hs+4−5
compare with master
unifiedsplit
@@ -102,7 +102,8 @@ showEnv env t = showEnv' env t False
102showEnvDbg env t = showEnv' env t True
102showEnvDbg env t = showEnv' env t True
103
103
104showEnv' env t dbg = se 10 env t where
104showEnv' env t dbg = se 10 env t where
105− se p env (P _ n _) = show n
105+ se p env (P nt n t) = show n ++
106+ if dbg then "{" ++ show nt ++ " : " ++ se 10 env t ++ "}" else ""
106 se p env (V i) | i < length env = (show $ fst $ env!!i) ++
107 se p env (V i) | i < length env = (show $ fst $ env!!i) ++
107 if dbg then "{" ++ show i ++ "}" else ""
108 if dbg then "{" ++ show i ++ "}" else ""
108 | otherwise = "!!V " ++ show i ++ "!!"
109 | otherwise = "!!V " ++ show i ++ "!!"
@@ -112,7 +113,7 @@ showEnv' env t dbg = se 10 env t where
112
113
113 sb env n (Lam t) = showb env "\\ " " => " n t
114 sb env n (Lam t) = showb env "\\ " " => " n t
114 sb env n (Hole t) = showb env "? " ". " n t
115 sb env n (Hole t) = showb env "? " ". " n t
115− sb env n (Pi t) = showb env "forall " " -> " n t
116+ sb env n (Pi t) = showb env "(" ") -> " n t
116 sb env n (PVar t) = showb env "! " ". " n t
117 sb env n (PVar t) = showb env "! " ". " n t
117 sb env n (Let t v) = showbv env "let " " in " n t v
118 sb env n (Let t v) = showbv env "let " " in " n t v
118 sb env n (Guess t v) = showbv env "?? " " in " n t v
119 sb env n (Guess t v) = showbv env "?? " " in " n t v
@@ -143,9 +144,7 @@ weakenTm i t = wk i 0 t
143 wk i m (App f a) = App (wk i m f) (wk i m a)
144 wk i m (App f a) = App (wk i m f) (wk i m a)
144 wk i m (Bind x b sc) = Bind x (wkb i m b) (wk i (m + 1) sc)
145 wk i m (Bind x b sc) = Bind x (wkb i m b) (wk i (m + 1) sc)
145 wk i m t = t
146 wk i m t = t
146− wkb i m (Let t v) = Let (wk i m t) (wk i m v)
147+ wkb i m t = fmap (wk i m) t
147− wkb i m (Guess t v) = Guess (wk i m t) (wk i m v)
148− wkb i m t = t { binderTy = wk i m (binderTy t) }
149
148
150-- weaken an environment so that all the de Bruijn indices are correct according
149-- weaken an environment so that all the de Bruijn indices are correct according
151-- to the latest bound variable
150-- to the latest bound variable
src/Evaluate.hs+11−5
@@ -28,7 +28,7 @@ normalise ctxt env t = quote 0 (eval ctxt (weakenEnv env) t)
28eval :: Context -> Env -> TT Name -> Value
28eval :: Context -> Env -> TT Name -> Value
29eval ctxt genv tm = ev [] tm where
29eval ctxt genv tm = ev [] tm where
30 ev env (P Ref n ty)
30 ev env (P Ref n ty)
31− | Just v <- lookupVal n ctxt = v -- FIXME! Needs evalling
31+ | Just v <- lookupVal n ctxt = v
32 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)
33 ev env (V i) | i < length env = env !! i
33 ev env (V i) | i < length env = env !! i
34 | i < length env + length genv
34 | i < length env + length genv
@@ -37,7 +37,7 @@ eval ctxt genv tm = ev [] tm where
37 _ -> VV i
37 _ -> VV i
38 | otherwise = error $ "Internal error: V" ++ show i
38 | otherwise = error $ "Internal error: V" ++ show i
39 ev env (Bind n (Let t v) sc)
39 ev env (Bind n (Let t v) sc)
40− = ev (ev env v : env) sc
40+ = wknV (-1) $ ev (ev env v : env) sc
41 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)
42 where vbind env t = fmap (ev env) t
42 where vbind env t = fmap (ev env) t
43 ev env (App f a) = evApply env [a] f
43 ev env (App f a) = evApply env [a] f
@@ -46,7 +46,7 @@ eval ctxt genv tm = ev [] tm where
46 evApply env args (App f a) = evApply env (a:args) f
46 evApply env args (App f a) = evApply env (a:args) f
47 evApply env args f = apply env (ev env f) args
47 evApply env args f = apply env (ev env f) args
48
48
49− 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) = wknV (-1) $ apply env (sc (ev env a)) as
50 apply env f (a:as) = unload env f (a:as)
50 apply env f (a:as) = unload env f (a:as)
51 apply env f [] = f
51 apply env f [] = f
52
52
@@ -56,13 +56,19 @@ eval ctxt genv tm = ev [] tm where
56quote :: Int -> Value -> TT Name
56quote :: Int -> Value -> TT Name
57quote i (VP nt n v) = P nt n (quote i v)
57quote i (VP nt n v) = P nt n (quote i v)
58quote i (VV x) = V x
58quote i (VV x) = V x
59−quote i (VBind n b sc) = Bind n (quoteB b) (quote (i+1) (sc (VTmp (i+1))))
59+quote i (VBind n b sc) = Bind n (quoteB b) (quote (i+1) (sc (VTmp i)))
60 where quoteB t = fmap (quote i) t
60 where quoteB t = fmap (quote i) t
61quote i (VApp f a) = App (quote i f) (quote i a)
61quote i (VApp f a) = App (quote i f) (quote i a)
62quote i (VSet u) = Set u
62quote i (VSet u) = Set u
63−quote i (VTmp x) = V (i - x)
63+quote i (VTmp x) = V (i - x - 1)
64
64
65
65
66+wknV :: Int -> Value -> Value
67+wknV i (VV x) = VV (x + i)
68+wknV i (VBind n b sc) = VBind n (fmap (wknV i) b) (\x -> (wknV i (sc x)))
69+wknV i (VApp f a) = VApp (wknV i f) (wknV i a)
70+wknV i t = t
71+
66-- CONTEXTS -----------------------------------------------------------------
72-- CONTEXTS -----------------------------------------------------------------
67
73
68data Fun = Fun Type Value Term Value
74data Fun = Fun Type Value Term Value
src/ProofState.hs+32−12
@@ -9,6 +9,7 @@ import Core
9import Control.Monad.State
9import Control.Monad.State
10import Control.Applicative
10import Control.Applicative
11import Data.List
11import Data.List
12+import Debug.Trace
12
13
13data ProofState = PS { thname :: Name,
14data ProofState = PS { thname :: Name,
14 holes :: [Name], -- holes still to be solved
15 holes :: [Name], -- holes still to be solved
@@ -36,11 +37,14 @@ data Tactic = Attack
36 | EvalIn Raw
37 | EvalIn Raw
37 | CheckIn Raw
38 | CheckIn Raw
38 | Intro Name
39 | Intro Name
40+ | Focus Name
39 | ProofState
41 | ProofState
40 | QED
42 | QED
41-- Next: add 'EvalHere' and 'CheckHere' tactics
43-- Next: add 'EvalHere' and 'CheckHere' tactics
42
44
43−data TacticAction = AddGoal Name
45+data TacticAction = AddGoal Name -- add a new goal, solve immediately
46+ | NextGoal Name -- add a new goal, solve it after current one
47+ | FocusGoal Name -- focus on this goal next
44 | Solved Name
48 | Solved Name
45 | Log String
49 | Log String
46
50
@@ -50,21 +54,23 @@ instance Show ProofState where
50 show (PS nm [] _ tm _ _ _) = show nm ++ ": no more goals"
54 show (PS nm [] _ tm _ _ _) = show nm ++ ": no more goals"
51 show (PS nm (h:hs) _ tm _ ctxt _)
55 show (PS nm (h:hs) _ tm _ ctxt _)
52 = let OK g = goal (Just h) tm ctxt
56 = let OK g = goal (Just h) tm ctxt
53− wkenv = weakenEnv (premises g) in
57+ wkenv = premises g in
54 showPs wkenv (reverse wkenv) ++ "\n" ++
58 showPs wkenv (reverse wkenv) ++ "\n" ++
55 "-------------------------------- (" ++ show nm ++
59 "-------------------------------- (" ++ show nm ++
56 ") -------\n" ++
60 ") -------\n" ++
57 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
61 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
58 where showPs env [] = ""
62 where showPs env [] = ""
59 showPs env ((n, b):bs)
63 showPs env ((n, b):bs)
64+ = " " ++ show n ++ " : " ++
60− = " " ++ show n ++ " : " ++ showEnv env (binderTy b) ++
65+ showEnv env (normalise ctxt env (binderTy b)) ++
61 "\n" ++ showPs env bs
66 "\n" ++ showPs env bs
62− showG ps (Guess t v) = showEnv ps t ++ " =?= " ++ showEnv ps v
67+ showG ps (Guess t v) = showEnv ps (normalise ctxt ps t) ++
68+ " =?= " ++ showEnv ps v
63 showG ps b = showEnv ps (binderTy b)
69 showG ps b = showEnv ps (binderTy b)
64
70
65same Nothing n = True
71same Nothing n = True
66same (Just x) n = x == n
72same (Just x) n = x == n
67−
73+
68hole (Hole _) = True
74hole (Hole _) = True
69hole (Guess _ _) = True
75hole (Guess _ _) = True
70hole _ = False
76hole _ = False
@@ -91,7 +97,8 @@ type Hole = Maybe Name -- Nothing = default hole, first in list in proof state
91goal :: Hole -> Term -> Context -> TC Goal
97goal :: Hole -> Term -> Context -> TC Goal
92goal h tm ctxt = g [] tm where
98goal h tm ctxt = g [] tm where
93 g env (Bind n b sc) | hole b && same h n = return $ GD env b
99 g env (Bind n b sc) | hole b && same h n = return $ GD env b
100+ | otherwise
94− | otherwise = gb env b `mplus` g ((n,b):env) sc
101+ = gb env b `mplus` g ((n,fmap (weakenTm 1) b):weakenTmEnv 1 env) sc
95 g env (App f a) = g env f `mplus` g env a
102 g env (App f a) = g env f `mplus` g env a
96 g env t = Error "Can't find hole"
103 g env t = Error "Can't find hole"
97
104
@@ -105,8 +112,10 @@ tactic h ps ctxt f = do let tm = pterm ps
105 return (ps { pterm = tm' })
112 return (ps { pterm = tm' })
106 where
113 where
107 atH env binder@(Bind n b sc)
114 atH env binder@(Bind n b sc)
108− | hole b && same h n = f ctxt (weakenEnv env) binder
115+ | hole b && same h n = f ctxt env binder
116+ | otherwise
109− | otherwise = pure Bind <*> pure n <*> atHb env b <*> atH ((n,b):env) sc
117+ = pure Bind <*> pure n <*> atHb env b <*>
118+ atH ((n,fmap (weakenTm 1) b):weakenTmEnv 1 env) sc
110 atH env (App f a) = pure App <*> atH env f <*> atH env a
119 atH env (App f a) = pure App <*> atH env f <*> atH env a
111 atH env t = return t
120 atH env t = return t
112
121
@@ -125,7 +134,15 @@ attack ctxt env (Bind x (Hole t) sc)
125attack ctxt env _ = fail "Not an attackable hole"
134attack ctxt env _ = fail "Not an attackable hole"
126
135
127claim :: Name -> Raw -> RunTactic
136claim :: Name -> Raw -> RunTactic
128−claim = undefined
137+claim n ty ctxt env t =
138+ do (tyv, tyt) <- lift $ check ctxt env ty
139+ lift $ isSet ctxt env tyt
140+ action (NextGoal n)
141+ return $ Bind n (Hole tyv) t
142+
143+focus :: Name -> RunTactic
144+focus n ctxt env t = do action (FocusGoal n)
145+ return t
129
146
130regret :: RunTactic
147regret :: RunTactic
131regret = undefined
148regret = undefined
@@ -182,9 +199,11 @@ processTactic t ps = case holes ps of
182 logs (_ : xs) = logs xs
199 logs (_ : xs) = logs xs
183
200
184 goals g [] = g
201 goals g [] = g
185− goals g (AddGoal n : xs) = goals (n : g) xs
202+ goals g (AddGoal n : xs) = goals (n : g) xs
186− goals g (Solved n : xs) = goals (g \\ [n]) xs
203+ goals (g:gs) (NextGoal n : xs) = goals (g : n : gs) xs
204+ goals g (FocusGoal n : xs) = goals (n : (g \\ [n])) xs
205+ goals g (Solved n : xs) = goals (g \\ [n]) xs
187− goals g (_ : xs) = goals g xs
206+ goals g (_ : xs) = goals g xs
188
207
189
208
190process :: Tactic -> Name -> ProofState -> StateT TState TC ProofState
209process :: Tactic -> Name -> ProofState -> StateT TState TC ProofState
@@ -197,3 +216,4 @@ process t h ps = tactic (Just h) ps (context ps) (mktac t)
197 mktac (Intro n) = intro n
216 mktac (Intro n) = intro n
198 mktac (CheckIn r) = check_in r
217 mktac (CheckIn r) = check_in r
199 mktac (EvalIn r) = eval_in r
218 mktac (EvalIn r) = eval_in r
219+ mktac (Focus n) = focus n
src/ShellParser.hs+1
@@ -52,6 +52,7 @@ pTactic = do reserved "attack"; return Attack
52 <|> do reserved "intro"; n <- iName; return (Intro n)
52 <|> do reserved "intro"; n <- iName; return (Intro n)
53 <|> do reserved "eval"; t <- pTerm; return (EvalIn t)
53 <|> do reserved "eval"; t <- pTerm; return (EvalIn t)
54 <|> do reserved "check"; t <- pTerm; return (CheckIn t)
54 <|> do reserved "check"; t <- pTerm; return (CheckIn t)
55+ <|> do reserved "focus"; n <- iName; return (Focus n)
55 <|> do reserved "state"; return ProofState
56 <|> do reserved "state"; return ProofState
56 <|> do reserved "qed"; return QED
57 <|> do reserved "qed"; return QED
57
58
src/Typecheck.hs+16−14
@@ -33,15 +33,17 @@ instance MonadPlus TC where
33 err `mplus` _ = err
33 err `mplus` _ = err
34
34
35converts :: Context -> Env -> Term -> Term -> TC ()
35converts :: Context -> Env -> Term -> Term -> TC ()
36−converts ctxt env x y = if (normalise ctxt env (bindEnv env x) ==
36+converts ctxt env x y = if (normalise ctxt env x == normalise ctxt env y)
37− normalise ctxt env (bindEnv env y))
38 then return ()
37 then return ()
39 else fail ("Can't convert between " ++
38 else fail ("Can't convert between " ++
40− show x ++ " and " ++ show y)
39+ showEnv env (normalise ctxt env x) ++ " and " ++
40+ showEnv env (normalise ctxt env y))
41
41
42+isSet :: Context -> Env -> Term -> TC ()
43+isSet ctxt env tm = isSet' (normalise ctxt env tm)
42−isSet :: Term -> TC ()
44+ where isSet' :: Term -> TC ()
43−isSet (Set _) = return ()
45+ isSet' (Set _) = return ()
44−isSet tm = fail (show tm ++ " is not a Set")
46+ isSet' tm = fail (showEnv env tm ++ " is not a Set")
45
47
46check :: Context -> Env -> Raw -> TC (Term, Type)
48check :: Context -> Env -> Raw -> TC (Term, Type)
47check ctxt env (Var n)
49check ctxt env (Var n)
@@ -67,13 +69,13 @@ check ctxt env (RBind n b sc)
67 = do (tv, tt) <- check ctxt env t
69 = do (tv, tt) <- check ctxt env t
68 let tv' = normalise ctxt env tv
70 let tv' = normalise ctxt env tv
69 let tt' = normalise ctxt env tt
71 let tt' = normalise ctxt env tt
70− isSet tt'
72+ isSet ctxt env tt'
71 return (Lam tv')
73 return (Lam tv')
72 checkBinder (Pi t)
74 checkBinder (Pi t)
73 = do (tv, tt) <- check ctxt env t
75 = do (tv, tt) <- check ctxt env t
74 let tv' = normalise ctxt env tv
76 let tv' = normalise ctxt env tv
75 let tt' = normalise ctxt env tt
77 let tt' = normalise ctxt env tt
76− isSet tt'
78+ isSet ctxt env tt'
77 return (Pi tv')
79 return (Pi tv')
78 checkBinder (Let t v)
80 checkBinder (Let t v)
79 = do (tv, tt) <- check ctxt env t
81 = do (tv, tt) <- check ctxt env t
@@ -81,13 +83,13 @@ check ctxt env (RBind n b sc)
81 let tv' = normalise ctxt env tv
83 let tv' = normalise ctxt env tv
82 let tt' = normalise ctxt env tt
84 let tt' = normalise ctxt env tt
83 converts ctxt env tv vt
85 converts ctxt env tv vt
84− isSet tt'
86+ isSet ctxt env tt'
85 return (Let tv' vv)
87 return (Let tv' vv)
86 checkBinder (Hole t)
88 checkBinder (Hole t)
87 = do (tv, tt) <- check ctxt env t
89 = do (tv, tt) <- check ctxt env t
88 let tv' = normalise ctxt env tv
90 let tv' = normalise ctxt env tv
89 let tt' = normalise ctxt env tt
91 let tt' = normalise ctxt env tt
90− isSet tt'
92+ isSet ctxt env tt'
91 return (Hole tv')
93 return (Hole tv')
92 checkBinder (Guess t v)
94 checkBinder (Guess t v)
93 = do (tv, tt) <- check ctxt env t
95 = do (tv, tt) <- check ctxt env t
@@ -95,13 +97,13 @@ check ctxt env (RBind n b sc)
95 let tv' = normalise ctxt env tv
97 let tv' = normalise ctxt env tv
96 let tt' = normalise ctxt env tt
98 let tt' = normalise ctxt env tt
97 converts ctxt env tv vt
99 converts ctxt env tv vt
98− isSet tt'
100+ isSet ctxt env tt'
99 return (Guess tv' vv)
101 return (Guess tv' vv)
100 checkBinder (PVar t)
102 checkBinder (PVar t)
101 = do (tv, tt) <- check ctxt env t
103 = do (tv, tt) <- check ctxt env t
102 let tv' = normalise ctxt env tv
104 let tv' = normalise ctxt env tv
103 let tt' = normalise ctxt env tt
105 let tt' = normalise ctxt env tt
104− isSet tt'
106+ isSet ctxt env tt'
105 return (PVar tv')
107 return (PVar tv')
106
108
107 discharge n (Lam t) scv sct
109 discharge n (Lam t) scv sct
@@ -132,12 +134,12 @@ checkProgram :: Context -> RProgram -> TC Context
132checkProgram ctxt [] = return ctxt
134checkProgram ctxt [] = return ctxt
133checkProgram ctxt ((n, RConst t):xs)
135checkProgram ctxt ((n, RConst t):xs)
134 = do (t', tt') <- trace (show n) $ check ctxt [] t
136 = do (t', tt') <- trace (show n) $ check ctxt [] t
135− isSet tt'
137+ isSet ctxt [] tt'
136 checkProgram (addConstant n t' ctxt) xs
138 checkProgram (addConstant n t' ctxt) xs
137checkProgram ctxt ((n, RFunction (RawFun ty val)):xs)
139checkProgram ctxt ((n, RFunction (RawFun ty val)):xs)
138 = do (ty', tyt') <- trace (show n) $ check ctxt [] ty
140 = do (ty', tyt') <- trace (show n) $ check ctxt [] ty
139 (val', valt') <- check ctxt [] val
141 (val', valt') <- check ctxt [] val
140− isSet tyt'
142+ isSet ctxt [] tyt'
141 converts ctxt [] ty' valt'
143 converts ctxt [] ty' valt'
142 checkProgram (addToCtxt n val' ty' ctxt) xs
144 checkProgram (addToCtxt n val' ty' ctxt) xs
143
145