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

src/Core/Elaborate.hs+4−1

@@ -244,6 +244,9 @@ regret = processTactic' Regret

244244compute :: Elab' aux ()

245245compute = processTactic' Compute

246246

247+hnf_compute :: Elab' aux ()

248+hnf_compute = processTactic' HNF_Compute

249+

247250eval_in :: Raw -> Elab' aux ()

248251eval_in t = processTactic' (EvalIn t)

249252

@@ -406,7 +409,7 @@ apply_elab n args =

406409 do ty <- get_type (Var n)

407410 ctxt <- get_context

408411 env <- get_env

409− claims <- doClaims (normalise ctxt env ty) args []

412+ claims <- doClaims (finalise ty) args []

410413 prep_fill n (map fst claims)

411414 let eclaims = sortBy (\ (_, x) (_,y) -> priOrder x y) claims

412415 elabClaims [] False claims

src/Core/Evaluate.hs+19−6

@@ -118,7 +118,9 @@ simplify ctxt runtime env t

118118

119119hnf :: Context -> Env -> TT Name -> TT Name

120120hnf ctxt env t

121− = evalState (do val <- eval False ctxt threshold [] (map finalEntry env) (finalise t) [HNF]

121+ = evalState (do val <- eval False ctxt threshold []

122+ (map finalEntry env)

123+ (finalise t) [HNF]

122124 quote 0 val) initEval

123125

124126

@@ -159,6 +161,7 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

159161 spec = Spec `elem` opts

160162 simpl = Simplify True `elem` opts

161163 atRepl = AtREPL `elem` opts

164+ hnf = HNF `elem` opts

162165

163166 canSimplify inl inr n stk

164167 = (Simplify False `elem` opts && (not inl || elem n stk))

@@ -168,6 +171,7 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

168171 | Just (Let t v) <- lookup n genv = do when (not atRepl) $ step maxred

169172 ev ntimes stk top env v

170173 ev ntimes_in stk top env (P Ref n ty)

174+ | not top && hnf = liftM (VP Ref n) (ev ntimes stk top env ty)

171175 | (True, ntimes) <- usable simpl n ntimes_in

172176 = do let val = lookupDefAcc Nothing n atRepl ctxt

173177 when (not atRepl) $ step maxred

@@ -211,7 +215,7 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

211215 ev ntimes stk top env (Bind n b sc)

212216 = do b' <- vbind env b

213217 when (not atRepl) $ step maxred

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

218+ return $ VBind n b' (\x -> ev ntimes stk False (x:env) sc)

215219 where vbind env t

216220 | simpl

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

@@ -222,7 +226,7 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

222226-- | laz == UN "lazy"

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

224228 ev ntimes stk top env (App f a)

225− = do f' <- ev ntimes stk top env f

229+ = do f' <- ev ntimes stk False env f

226230 a' <- ev ntimes stk False env a

227231 when (not atRepl) $ step maxred

228232 evApply ntimes stk top env [a'] f'

@@ -243,7 +247,10 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

243247 wknV (-1) app

244248-- apply ntimes stk False env f args

245249-- | spec = specApply ntimes stk env f args

246− apply ntimes_in stk top env f@(VP Ref n ty) args

250+ apply ntimes_in stk top env f@(VP Ref n ty) args

251+ | not top && hnf = case args of

252+ [] -> return f

253+ _ -> return $ unload env f args

247254 | (True, ntimes) <- usable simpl n ntimes_in

248255 = traceWhen traceon (show stk) $

249256 do let val = lookupDefAcc Nothing n atRepl ctxt

@@ -284,7 +291,8 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

284291 | length ns <= length args

285292 = do let args' = take (length ns) args

286293 let rest = drop (length ns) args

287− t <- evTree ntimes stk top env (zipWith (\n t -> (n, t)) ns args') tree

294+ t <- evTree ntimes stk top env

295+ (zipWith (\n t -> (n, t)) ns args') tree

288296 return (t, rest)

289297 | otherwise = return (Nothing, args)

290298

@@ -293,7 +301,8 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

293301 evTree ntimes stk top env amap (UnmatchedCase str) = return Nothing

294302 evTree ntimes stk top env amap (STerm tm)

295303 = do let etm = pToVs (map fst amap) tm

296− etm' <- ev ntimes stk top (map snd amap ++ env) etm

304+ etm' <- ev ntimes stk (not (conHeaded tm))

305+ (map snd amap ++ env) etm

297306 return $ Just etm'

298307 evTree ntimes stk top env amap (Case n alts)

299308 = case lookup n amap of

@@ -306,6 +315,10 @@ eval traceon ctxt maxred ntimes genv tm opts = ev ntimes [] True [] tm where

306315 _ -> return Nothing

307316 _ -> return Nothing

308317

318+ conHeaded tm@(App _ _)

319+ | (P (DCon _ _) _ _, args) <- unApply tm = True

320+ conHeaded t = False

321+

309322 chooseAlt' ntimes stk env _ (f, args) alts amap

310323 = do f' <- apply ntimes stk True env f args

311324 chooseAlt env f' (getValArgs f') alts amap

src/Core/ProofState.hs+11−3

@@ -54,6 +54,7 @@ data Tactic = Attack

5454 | StartUnify Name

5555 | EndUnify

5656 | Compute

57+ | HNF_Compute

5758 | EvalIn Raw

5859 | CheckIn Raw

5960 | Intro (Maybe Name)

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

387388 Nothing -> x

388389 let t' = case t of

389390 x@(Bind y (Pi s) _) -> x

390− _ -> normalise ctxt env t

391+ _ -> hnf ctxt env t

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

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

393394 case t' of

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

407408 Nothing -> x

408409 let t' = case t of

409410 x@(Bind y (Pi s) _) -> x

410− _ -> normalise ctxt env t

411+ _ -> hnf ctxt env t

411412 case t' of

412413 Bind y (Pi s) t -> -- trace ("in type " ++ show t') $

413414 let t' = instantiate (P Bound n s) (pToV y t) in

@@ -477,7 +478,7 @@ patbind :: Name -> RunTactic

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

478479 do let t' = case t of

479480 x@(Bind y (PVTy s) t) -> x

480− _ -> normalise ctxt env t

481+ _ -> hnf ctxt env t

481482 case t' of

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

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

@@ -488,6 +489,12 @@ compute :: RunTactic

488489compute ctxt env (Bind x (Hole ty) sc) =

489490 do return $ Bind x (Hole (normalise ctxt env ty)) sc

490491

492+hnf_compute :: RunTactic

493+hnf_compute ctxt env (Bind x (Hole ty) sc) =

494+ do let ty' = hnf ctxt env ty in

495+-- trace ("HNF " ++ show (ty, ty')) $

496+ return $ Bind x (Hole ty') sc

497+

491498check_in :: Raw -> RunTactic

492499check_in t ctxt env tm =

493500 do (val, valty) <- lift $ check ctxt env t

@@ -603,6 +610,7 @@ process t h = tactic (Just h) (mktac t)

603610 mktac Solve = solve

604611 mktac (StartUnify n) = start_unify n

605612 mktac Compute = compute

613+ mktac HNF_Compute = hnf_compute

606614 mktac (Intro n) = intro n

607615 mktac (IntroTy ty n) = introTy ty n

608616 mktac (Forall n t) = forall n t

src/Core/Typecheck.hs+1−1

@@ -67,7 +67,7 @@ check' holes ctxt env top = chk env top where

6767 let fty' = case uniqueBinders (map fst env) (finalise fty) of

6868 ty@(Bind x (Pi s) t) -> ty

6969 _ -> uniqueBinders (map fst env)

70− $ normalise ctxt env fty

70+ $ hnf ctxt env fty

7171 case fty' of

7272 Bind x (Pi s) t ->

7373-- trace ("Converting " ++ show aty ++ " and " ++ show s ++

src/Core/Unify.hs+3−3

@@ -31,7 +31,7 @@ unify ctxt env topx topy =

3131 _ ->

3232 let topxn = normalise ctxt env topx

3333 topyn = normalise ctxt env topy in

34−-- trace ("Unifying " ++ show (topxn, topyn)) $

34+-- trace ("Unifying " ++ show (topx, topy) ++ "\n\n==>\n" ++ show (topxn, topyn) ++ "\n\n") $

3535 case runStateT (un' False [] topxn topyn)

3636 (UI 0 [] []) of

3737 OK (v, UI _ inj fails) ->

@@ -112,7 +112,7 @@ unify ctxt env topx topy =

112112 sc 1

113113 combine bnames hf ha)

114114 where hnormalise [] _ _ t = t

115− hnormalise ns ctxt env t = normalise ctxt env t

115+ hnormalise ns ctxt env t = hnf ctxt env t

116116 checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)

117117 | x /= y = unifyFail appx appy

118118 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)

@@ -200,7 +200,7 @@ unify ctxt env topx topy =

200200 | otherwise = False

201201-- recoverable (P (DCon _ _) x _) (P (TCon _ _) y _) = False

202202-- recoverable (P (TCon _ _) x _) (P (DCon _ _) y _) = False

203− recoverable p@(P _ _ _) (App f a) = recoverable p f

203+ recoverable p@(P _ n _) (App f a) = recoverable p f

204204 recoverable (App f a) p@(P _ _ _) = recoverable f p

205205 recoverable (App f a) (App f' a')

206206 = recoverable f f' && recoverable a a'

src/Idris/Delaborate.hs+6−3

@@ -77,15 +77,18 @@ pshow i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++

7777 "\nThis is probably a bug, or a missing error message.\n" ++

7878 "Please consider reporting at " ++ bugaddr

7979pshow i (CantUnify _ x y e sc s)

80− = "Can't unify " ++ show (delab i x)

81− ++ " with " ++ show (delab i y) ++

80+ = let imps = opt_showimp (idris_options i) in

81+ "Can't unify " ++ showImp imps (delab i x)

82+ ++ " with " ++ showImp imps (delab i y) ++

8283-- " (" ++ show x ++ " and " ++ show y ++ ") " ++

8384 case e of

8485 Msg "" -> ""

8586 _ -> "\n\nSpecifically:\n\t" ++ pshow i e ++

8687 if (opt_errContext (idris_options i)) then showSc i sc else ""

8788pshow i (CantConvert x y env)

88− = "Can't convert " ++ show (delab i x) ++ " with " ++ show (delab i y) ++

89+ = let imps = opt_showimp (idris_options i) in

90+ "Can't convert " ++ showImp imps (delab i x) ++ " with "

91+ ++ showImp imps (delab i y) ++

8992 if (opt_errContext (idris_options i)) then showSc i env else ""

9093pshow i (InfiniteUnify x tm env)

9194 = "Unifying " ++ showbasic x ++ " and " ++ show (delab i tm) ++

src/Idris/ElabDecls.hs+1

@@ -440,6 +440,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

440440

441441 simpl rt ctxt (Right (x, y)) = Right (normalise ctxt [] x,

442442 simplify ctxt rt [] y)

443+-- simpl rt ctxt (Right (x, y)) = Right (x, y)

443444 simpl rt ctxt t = t

444445

445446 sameLength ((_, x, _) : xs)

src/Idris/ElabTerm.hs+3−4

@@ -483,7 +483,7 @@ resolveTC :: Int -> Name -> IState -> ElabD ()

483483resolveTC 0 fn ist = fail $ "Can't resolve type class"

484484resolveTC 1 fn ist = try (trivial ist) (resolveTC 0 fn ist)

485485resolveTC depth fn ist

486− = do compute

486+ = do hnf_compute

487487 try (trivial ist)

488488 (do t <- goal

489489 let insts = findInstances ist t

@@ -647,7 +647,6 @@ runTac autoSolve ist tac = do env <- get_env

647647 (tm', ty') <- get_type_val (Var tacn)

648648 ctxt <- get_context

649649 env <- get_env

650− -- g <- goal

651650 let tactic = normalise ctxt env tm'

652651 runReflected tactic

653652-- p <- get_term

@@ -665,13 +664,13 @@ runTac autoSolve ist tac = do env <- get_env

665664 reify (P _ n _) | n == tacm "Solve" = return Solve

666665 reify f@(App _ _)

667666 | (P _ f _, args) <- unApply f = reifyAp f args

668− reify t = fail "Unknown tactic"

667+ reify t = fail ("Unknown tactic " ++ show t)

669668

670669 reifyAp t [l, r] | t == tacm "Try" = liftM2 Try (reify l) (reify r)

671670 reifyAp t [Constant (Str x)]

672671 | t == tacm "Refine" = return $ Refine (UN x) []

673672 reifyAp t [l, r] | t == tacm "Seq" = liftM2 TSeq (reify l) (reify r)

674− reifyAp f args = fail "Unknown tactic" -- shouldn't happen

673+ reifyAp f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen

675674

676675solveAll = try (do solve; solveAll) (return ())

677676

src/Idris/REPL.hs+1−1

@@ -323,7 +323,7 @@ process fn (Prove n')

323323process fn (HNF t) = do (tm, ty) <- elabVal toplevel False t

324324 ctxt <- getContext

325325 ist <- get

326− let tm' = simplify ctxt True [] tm

326+ let tm' = hnf ctxt [] tm

327327 iputStrLn (show (delab ist tm'))

328328process fn TTShell = do ist <- get

329329 let shst = initState (tt_ctxt ist)