56223ef · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Don't normalise everywhere!

commit56223ef1e4ed2f0002085c22e6c5f7ac27acfbc2 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 14 Nov 2012, 20:21 (14 years ago) parent449bb27

7 files changed+46−22

compare with master

unifiedsplit

src/Core/Elaborate.hs+2−1 src/Core/Evaluate.hs+7−1 src/Core/ProofState.hs+9−3 src/Core/Typecheck.hs+23−13 src/Core/Unify.hs+3−3 src/Idris/ElabDecls.hs+1 src/Idris/ElabTerm.hs+1−1

src/Core/Elaborate.hs+2−1

@@ -289,7 +289,8 @@ prepare_apply fn imps =

289289 ctxt <- get_context

290290 env <- get_env

291291 -- let claims = getArgs ty imps

292− claims <- mkClaims (normalise ctxt env ty) imps []

292+ -- claims <- mkClaims (normalise ctxt env ty) imps []

293+ claims <- mkClaims (finalise ty) imps []

293294 ES (p, a) s prev <- get

294295 -- reverse the claims we made so that args go left to right

295296 let n = length (filter not imps)

src/Core/Evaluate.hs+7−1

@@ -137,6 +137,7 @@ unbindEnv [] tm = tm

137137unbindEnv (_:bs) (Bind n b sc) = unbindEnv bs sc

138138

139139usable :: Bool -> Name -> [(Name, Int)] -> (Bool, [(Name, Int)])

140+usable _ _ ns@((MN 0 "STOP", _) : _) = (False, ns)

140141usable s n [] = (True, [])

141142usable s n ns = case lookup n ns of

142143 Just 0 -> (False, ns)

@@ -207,7 +208,12 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

207208 = do b' <- vbind env b

208209 when (not atRepl) $ step maxred

209210 return $ VBind n b' (\x -> ev ntimes stk top (x:env) sc)

210− where vbind env t = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t

211+ where vbind env t

212+ | simpl

213+ = fmapMB (\tm -> ev ((MN 0 "STOP", 0) : ntimes)

214+ stk top env (finalise tm)) t

215+ | otherwise

216+ = fmapMB (\tm -> ev ntimes stk top env (finalise tm)) t

211217-- ev ntimes stk top env (App (App (P _ laz _) _) a)

212218-- | laz == UN "lazy"

213219-- = trace (showEnvDbg genv a) $ ev ntimes stk top env a

src/Core/ProofState.hs+9−3

@@ -369,7 +369,9 @@ introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

369369 do let n = case mn of

370370 Just name -> name

371371 Nothing -> x

372− let t' = normalise ctxt env t

372+ let t' = case t of

373+ x@(Bind y (Pi s) _) -> x

374+ _ -> normalise ctxt env t

373375 (tyv, tyt) <- lift $ check ctxt env ty

374376-- ns <- lift $ unify ctxt env tyv t'

375377 case t' of

@@ -387,7 +389,9 @@ intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

387389 do let n = case mn of

388390 Just name -> name

389391 Nothing -> x

390− let t' = normalise ctxt env t

392+ let t' = case t of

393+ x@(Bind y (Pi s) _) -> x

394+ _ -> normalise ctxt env t

391395 case t' of

392396 Bind y (Pi s) t -> let t' = instantiate (P Bound n s) (pToV y t) in

393397 return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))

@@ -454,7 +458,9 @@ rewrite _ _ _ _ = fail "Can't rewrite here"

454458

455459patbind :: Name -> RunTactic

456460patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

457− do let t' = normalise ctxt env t

461+ do let t' = case t of

462+ x@(Bind y (PVTy s) t) -> x

463+ _ -> normalise ctxt env t

458464 case t' of

459465 Bind y (PVTy s) t -> let t' = instantiate (P Bound n s) (pToV y t) in

460466 return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))

src/Core/Typecheck.hs+23−13

@@ -16,20 +16,25 @@ import Core.Evaluate

1616

1717convertsC :: Context -> Env -> Term -> Term -> StateT UCs TC ()

1818convertsC ctxt env x y

19− = do c <- convEq ctxt (finalise (normalise ctxt env x))

19+ = do c1 <- convEq ctxt x y

20+ if c1 then return ()

21+ else

22+ do c2 <- convEq ctxt (finalise (normalise ctxt env x))

2023 (finalise (normalise ctxt env y))

21− if c then return ()

22− else lift $ tfail (CantConvert

23− (finalise (normalise ctxt env x))

24− (finalise (normalise ctxt env y)) (errEnv env))

24+ if c2 then return ()

25+ else lift $ tfail (CantConvert

26+ (finalise (normalise ctxt env x))

27+ (finalise (normalise ctxt env y)) (errEnv env))

2528

2629converts :: Context -> Env -> Term -> Term -> TC ()

27−converts ctxt env x y = if (finalise (normalise ctxt env x) ==

28− finalise (normalise ctxt env y))

29− then return ()

30− else tfail (CantConvert

31− (finalise (normalise ctxt env x))

32− (finalise (normalise ctxt env y)) (errEnv env))

30+converts ctxt env x y

31+ = if x == y then return () else

32+ if (finalise (normalise ctxt env x) ==

33+ finalise (normalise ctxt env y))

34+ then return ()

35+ else tfail (CantConvert

36+ (finalise (normalise ctxt env x))

37+ (finalise (normalise ctxt env y)) (errEnv env))

3338

3439errEnv = map (\(x, b) -> (x, binderTy b))

3540

@@ -59,11 +64,16 @@ check' holes ctxt env top = chk env top where

5964 chk env (RApp f a)

6065 = do (fv, fty) <- chk env f

6166 (av, aty) <- chk env a

62− let fty' = renameBinders 0 $ normalise ctxt env fty

67+ let fty' = case renameBinders 0 (finalise fty) of

68+ ty@(Bind x (Pi s) t) -> ty

69+ _ -> renameBinders 0 $ normalise ctxt env fty

6370 case fty' of

6471 Bind x (Pi s) t ->

6572 do convertsC ctxt env aty s

66− let apty = normalise initContext env (Bind x (Let aty av) t)

73+ -- let apty = normalise initContext env

74+ -- (Bind x (Let aty av) t)

75+ let apty = simplify initContext False env

76+ (Bind x (Let aty av) t)

6777 return (App fv av, apty)

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

6979 -- This rather unpleasant hack is needed because during incomplete

src/Core/Unify.hs+3−3

@@ -25,9 +25,9 @@ data UInfo = UI Int Injs Fails

2525unify :: Context -> Env -> TT Name -> TT Name -> TC ([(Name, TT Name)],

2626 Injs, Fails)

2727unify ctxt env topx topy

28− = -- case runStateT (un' False [] topx topy) (UI 0 [] []) of

29− -- OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])

30− -- _ ->

28+ = case runStateT (un' False [] topx topy) (UI 0 [] []) of

29+ OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])

30+ _ ->

3131-- trace ("Unifying " ++ show (topx, topy)) $

3232 let topxn = normalise ctxt env topx

3333 topyn = normalise ctxt env topy in

src/Idris/ElabDecls.hs+1

@@ -55,6 +55,7 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

5555 addDeferred ds

5656 mapM_ (elabCaseBlock info) is

5757 ctxt <- getContext

58+ logLvl 5 $ "Rechecking"

5859 (cty, _) <- recheckC fc [] tyT

5960 addStatics n cty ty'

6061 logLvl 6 $ "Elaborated to " ++ showEnvDbg [] tyT

src/Idris/ElabTerm.hs+1−1

@@ -280,7 +280,7 @@ elab ist info pattern tcgen fn tm

280280 mkN n = case namespace info of

281281 Just xs@(_:_) -> NS n xs

282282 _ -> n

283− elab' ina (PProof ts) = do mapM_ (runTac True ist) ts

283+ elab' ina (PProof ts) = do compute; mapM_ (runTac True ist) ts

284284 elab' ina (PTactics ts)

285285 | not pattern = do mapM_ (runTac False ist) ts

286286 | otherwise = elab' ina Placeholder