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

src/Core/Elaborate.hs+2−1

compare with master

unifiedsplit

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

289 ctxt <- get_context

290 env <- get_env

291 -- 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 []

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

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

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

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

295 let n = length (filter not imps)

296 let n = length (filter not imps)

src/Core/Evaluate.hs+7−1

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

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

138

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

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

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

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

141usable s n ns = case lookup n ns of

142usable s n ns = case lookup n ns of

142 Just 0 -> (False, ns)

143 Just 0 -> (False, ns)

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

207 = do b' <- vbind env b

208 = do b' <- vbind env b

208 when (not atRepl) $ step maxred

209 when (not atRepl) $ step maxred

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

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

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

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

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

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

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

212-- | laz == UN "lazy"

218-- | laz == UN "lazy"

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

219-- = 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' =

369 do let n = case mn of

370 Just name -> name

371 Nothing -> x

372+ let t' = case t of

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

372− let t' = normalise ctxt env t

374+ _ -> normalise ctxt env t

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

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

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

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

375 case t' of

377 case t' of

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

387 do let n = case mn of

389 do let n = case mn of

388 Just name -> name

390 Just name -> name

389 Nothing -> x

391 Nothing -> x

392+ let t' = case t of

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

390− let t' = normalise ctxt env t

394+ _ -> normalise ctxt env t

391 case t' of

395 case t' of

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

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

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

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

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

454

458

455patbind :: Name -> RunTactic

459patbind :: Name -> RunTactic

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

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

461+ do let t' = case t of

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

457− do let t' = normalise ctxt env t

463+ _ -> normalise ctxt env t

458 case t' of

464 case t' of

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

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

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

466 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

16

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

18convertsC ctxt env x y

19+ = do c1 <- convEq ctxt x y

20+ if c1 then return ()

21+ else

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

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

20 (finalise (normalise ctxt env y))

23 (finalise (normalise ctxt env y))

21− if c then return ()

24+ if c2 then return ()

22− else lift $ tfail (CantConvert

25+ else lift $ tfail (CantConvert

23− (finalise (normalise ctxt env x))

26+ (finalise (normalise ctxt env x))

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

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

25

28

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

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

30+converts ctxt env x y

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

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

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

28− finalise (normalise ctxt env y))

33+ finalise (normalise ctxt env y))

29− then return ()

34+ then return ()

30− else tfail (CantConvert

35+ else tfail (CantConvert

31− (finalise (normalise ctxt env x))

36+ (finalise (normalise ctxt env x))

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

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

33

38

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

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

35

40

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

59 chk env (RApp f a)

64 chk env (RApp f a)

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

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

61 (av, aty) <- chk env a

66 (av, aty) <- chk env a

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

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

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

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

63 case fty' of

70 case fty' of

64 Bind x (Pi s) t ->

71 Bind x (Pi s) t ->

65 do convertsC ctxt env aty s

72 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)

67 return (App fv av, apty)

77 return (App fv av, apty)

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

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

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

79 -- 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

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

26 Injs, Fails)

27unify ctxt env topx topy

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

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

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

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

30− -- _ ->

30+ _ ->

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

32 let topxn = normalise ctxt env topx

33 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

55 addDeferred ds

56 mapM_ (elabCaseBlock info) is

57 ctxt <- getContext

58+ logLvl 5 $ "Rechecking"

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

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

59 addStatics n cty ty'

60 addStatics n cty ty'

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

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

src/Idris/ElabTerm.hs+1−1

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

280 mkN n = case namespace info of

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

282 _ -> n

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

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

284 elab' ina (PTactics ts)

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

286 | otherwise = elab' ina Placeholder