7b1336b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fixed naming problem in type checking of application

commit7b1336bfce95bd0256e9cba591b510c90e46cf3b authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateMon 31 Oct 2011, 16:55 (15 years ago) parent58bd7c4

6 files changed+29−16

compare with master

unifiedsplit

lib/builtins.idr+3 src/Core/Evaluate.hs+7−2 src/Core/ProofState.hs+5−5 src/Core/TT.hs+1−1 src/Core/Typecheck.hs+10−5 src/Idris/REPL.hs+3−3

lib/builtins.idr+3

@@ -11,6 +11,9 @@ getSigVal (Exists a v) = v;

1111replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Set} -> x = y -> P x -> P y;

1212replace refl prf = prf;

1313

14+sym : {x:a} -> {y:a} -> x = y -> y = x;

15+sym refl = refl;

16+

1417lazy : a -> a;

1518lazy x = x; -- compiled specially

1619

src/Core/Evaluate.hs+7−2

@@ -1,7 +1,7 @@

11{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,

22 PatternGuards #-}

4−module Core.Evaluate(normalise, specialise, hnf,

4+module Core.Evaluate(normalise, normaliseC, specialise, hnf,

55 Fun(..), Def(..), Context,

66 addToCtxt, addTyDecl, addDatatype, addCasedef, addOperator,

77 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv,

@@ -51,6 +51,11 @@ instance Show (a -> b) where

5151-- i.e. it's an intermediate environment that we have while type checking or

5252-- while building a proof.

5353

54+normaliseC :: Context -> Env -> TT Name -> TT Name

55+normaliseC ctxt env t

56+ = evalState (do val <- eval ctxt emptyContext env t []

57+ quote 0 val) ()

58+

5459normalise :: Context -> Env -> TT Name -> TT Name

5560normalise ctxt env t

5661 = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) []

@@ -103,7 +108,7 @@ eval ctxt statics genv tm opts = ev True [] tm where

103108 ev top env (V i) | i < length env = return $ env !! i

104109 | otherwise = return $ VV i

105110 ev top env (Bind n (Let t v) sc)

106− = do v' <- ev top env (finalise v)

111+ = do v' <- ev top env v --(finalise v)

107112 sc' <- ev top (v' : env) sc

108113 wknV (-1) sc'

109114 ev top env (Bind n (NLet t v) sc)

src/Core/ProofState.hs+5−5

@@ -288,11 +288,11 @@ rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =

288288 (P _ (UN ["="]) _, [lt,rt,l,r]) ->

289289 do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)

290290 let newt = mkP l r l t

291− return (Bind x (Hole newt)

292− (mkApp (P Ref (UN ["replace"]) (Set 0))

293− [lt, l, r, p, tmv, xp]))

294− -- fail $ "Rewrite " ++ show l ++ " to " ++ show r ++ " in " ++

295− -- show t ++ " with " ++ show (p, newt) ++ " not done yet"

291+ let sc = forget $ (Bind x (Hole newt)

292+ (mkApp (P Ref (UN ["replace"]) (Set 0))

293+ [lt, l, r, p, tmv, xp]))

294+ (scv, sct) <- lift $ check ctxt env sc

295+ return scv

296296 _ -> fail "Not an equality type"

297297 where

298298 -- to make the P for rewrite, replace syntactic occurrences of l in ty with

src/Core/TT.hs+1−1

@@ -329,7 +329,7 @@ showEnvDbg env t = showEnv' env t True

329329

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

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

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

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

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

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

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

src/Core/Typecheck.hs+10−5

@@ -39,15 +39,20 @@ check ctxt env (Var n)

3939check ctxt env (RApp f a)

4040 = do (fv, fty) <- check ctxt env f

4141 (av, aty) <- check ctxt env a

42− let fty' = normalise ctxt env fty

43−-- trace (showEnv env fty ++ " ===> " ++ showEnv env fty') $

42+ let fty' = renameBinders 0 $ normalise ctxt env fty

4443 case fty' of

4544 Bind x (Pi s) t ->

4645 do converts ctxt env s aty

47− return (App fv av,

48−-- normalise ctxt env (subst x av t))

49− normalise ctxt env (Bind x (Let aty av) t))

46+ let apty = {- normalise ctxt env -} (Bind x (Let aty av) t)

47+ return (App fv av, apty)

5048 t -> fail "Can't apply a non-function type"

49+ -- This rather unpleasant hack is needed because during incomplete

50+ -- proofs, variables are locally bound with an explicit name. If we just

51+ -- make sure bound names in function types are locally unique, machine

52+ -- generated names, we'll be fine.

53+ where renameBinders i (Bind x (Pi s) t) = Bind (MN i "binder") (Pi s)

54+ (renameBinders (i+1) t)

55+ renameBinders i sc = sc

5156check ctxt env (RSet i) = return (Set i, Set i) -- LATER: (i+1))

5257check ctxt env (RConstant c) = return (Constant c, constType c)

5358 where constType (I _) = Constant IType

src/Idris/REPL.hs+3−3

@@ -46,9 +46,9 @@ process Help

4646process (Eval t) = do (tm, ty) <- elabVal toplevel t

4747 ctxt <- getContext

4848 ist <- get

49− let tm' = normalise ctxt [] tm

50− let ty' = normalise ctxt [] ty

51− logLvl 3 $ "Raw: " ++ show tm'

49+ let tm' = normaliseC ctxt [] tm

50+ let ty' = normaliseC ctxt [] ty

51+ logLvl 3 $ "Raw: " ++ show (tm', ty')

5252 iputStrLn (show (delab ist tm') ++ " : " ++

5353 show (delab ist ty'))

5454process (Spec t) = do (tm, ty) <- elabVal toplevel t