5dadd08 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

QED now rechecks the term, instead of just finalise. *bites fingernails*

5dadd08Edwin Brady15 years ago

src/Core.hs+12−4

compare with master

unifiedsplit

@@ -110,7 +110,7 @@ data TT n = P NameType n (TT n) -- embed type

110 | Bind n (Binder (TT n)) (TT n)

111 | App (TT n) (TT n) -- function, function type, arg

112 | Set Int

113− deriving (Functor, Eq)

113+ deriving Functor

114

115type EnvTT n = [(n, Binder (TT n))]

116

@@ -119,6 +119,14 @@ data Datatype n = Data { d_typename :: n,

119 d_cons :: [(n, TT n)] }

120 deriving (Show, Functor, Eq)

121

122+instance Eq n => Eq (TT n) where

123+ (==) (P xt x _) (P yt y _) = xt == yt && x == y

124+ (==) (V x) (V y) = x == y

125+ (==) (Bind _ xb xs) (Bind _ yb ys) = xb == yb && xs == ys

126+ (==) (App fx ax) (App fy ay) = fx == fy && ax == ay

127+ (==) (Set x) (Set y) = x == y

128+ (==) _ _ = False

129+

122-- A few handy operations on well typed terms:

130-- A few handy operations on well typed terms:

123

131

124-- Returns true if V 0 and bound name n do not occur in the term

132-- Returns true if V 0 and bound name n do not occur in the term

@@ -177,12 +185,12 @@ showEnvDbg env t = showEnv' env t True

177

185

178showEnv' env t dbg = se 10 env t where

186showEnv' env t dbg = se 10 env t where

179 se p env (P nt n t) = show n

187 se p env (P nt n t) = show n

180−-- ++ if dbg then "{" ++ show nt ++ " : " ++ se 10 env t ++ "}" else ""

188+ ++ if dbg then "{" ++ show nt ++ " : " ++ se 10 env t ++ "}" else ""

181 se p env (V i) | i < length env = (show $ fst $ env!!i) ++

189 se p env (V i) | i < length env = (show $ fst $ env!!i) ++

182 if dbg then "{" ++ show i ++ "}" else ""

190 if dbg then "{" ++ show i ++ "}" else ""

183 | otherwise = "!!V " ++ show i ++ "!!"

191 | otherwise = "!!V " ++ show i ++ "!!"

184− se p env (Bind n b@(Pi t) sc)

192+ se p env (Bind n b@(Pi t) sc)

185− | noOccurrence n sc = bracket p 2 $ se 10 env t ++ " -> " ++ se 10 ((n,b):env) sc

193+ | noOccurrence n sc && not dbg = bracket p 2 $ se 10 env t ++ " -> " ++ se 10 ((n,b):env) sc

186 se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc

194 se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc

187 se p env (App f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a

195 se p env (App f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a

188 se p env (Set i) = "Set" ++ show i

196 se p env (Set i) = "Set" ++ show i

src/ProofState.hs+4−3

@@ -254,9 +254,10 @@ eval_in t ctxt env tm =

254

255processTactic :: Tactic -> ProofState -> TC (ProofState, String)

256processTactic QED ps = case holes ps of

257− [] -> let tm = finalise (pterm ps) in

257+ [] -> do let tm = pterm ps

258+ (tm', ty') <- recheck (context ps) [] tm

258− return (ps { done = True, pterm = tm },

259+ return (ps { done = True, pterm = tm' },

259− "Proof complete: " ++ showEnv [] tm)

260+ "Proof complete: " ++ showEnv [] tm')

260 _ -> Error "Still holes to fill."

261 _ -> Error "Still holes to fill."

261processTactic ProofState ps = return (ps, showEnv [] (pterm ps))

262processTactic ProofState ps = return (ps, showEnv [] (pterm ps))

262processTactic Undo ps = case previous ps of

263processTactic Undo ps = case previous ps of

src/Typecheck.hs+5−2

@@ -18,8 +18,8 @@ converts ctxt env x y = if (finalise (normalise ctxt env x) ==

18 finalise (normalise ctxt env y))

19 then return ()

20 else fail ("Can't convert between " ++

21− showEnv env (normalise ctxt env x) ++ " and " ++

21+ showEnv env (finalise (normalise ctxt env x)) ++ " and " ++

22− showEnv env (normalise ctxt env y))

22+ showEnv env (finalise (normalise ctxt env y)))

24isSet :: Context -> Env -> Term -> TC ()

25isSet ctxt env tm = isSet' (normalise ctxt env tm)

@@ -27,6 +27,9 @@ isSet ctxt env tm = isSet' (normalise ctxt env tm)

27 isSet' (Set _) = return ()

28 isSet' tm = fail (showEnv env tm ++ " is not a Set")

30+recheck :: Context -> Env -> Term -> TC (Term, Type)

31+recheck ctxt env tm = check ctxt env (forget tm)

32+

30check :: Context -> Env -> Raw -> TC (Term, Type)

33check :: Context -> Env -> Raw -> TC (Term, Type)

31check ctxt env (Var n)

34check ctxt env (Var n)

32 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)

35 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)