a1e3b5b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Revert to normalising from WHNF

We don't get any benefit in any of the useful places from using WHNF, and often it leads to much bigger intermediate terms that slow down type checking too much. Fixes #3566

commita1e3b5b0d9c50ee6ce49052431bd17696d995a04 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 4 Mar 2017, 20:48 (10 years ago) parent1b3ed30

6 files changed+22−22

compare with master

unifiedsplit

src/Idris/Core/Elaborate.hs+3−3 src/Idris/Core/Evaluate.hs+1−1 src/Idris/Elab/Clause.hs+1−1 src/Idris/Elab/Term.hs+14−14 src/Idris/ElabDecls.hs+2−2 test/basic018/expected+1−1

src/Idris/Core/Elaborate.hs+3−3

@@ -578,7 +578,7 @@ prepare_apply fn imps =

578578 -- Count arguments to check if we need to normalise the type

579579 let usety = if argsOK (finalise ty) imps

580580 then finalise ty

581− else whnfArgs ctxt env (finalise ty)

581+ else normalise ctxt env (finalise ty)

582582 claims <- -- trace (show (fn, imps, ty, map fst env, normalise ctxt env (finalise ty))) $

583583 mkClaims usety imps [] (map fstEnv env)

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

@@ -748,7 +748,7 @@ checkPiGoal n

748748 = do g <- goal

749749 ctxt <- get_context

750750 env <- get_env

751− case (whnf ctxt env g) of

751+ case (normalise ctxt env g) of

752752 Bind _ (Pi _ _ _ _) _ -> return ()

753753 _ -> do a <- getNameFrom (sMN 0 "__pargTy")

754754 b <- getNameFrom (sMN 0 "__pretTy")

@@ -823,7 +823,7 @@ dep_app fun arg str =

823823 focus s; attack;

824824 ctxt <- get_context

825825 env <- get_env

826− case whnf ctxt env fty of

826+ case normalise ctxt env fty of

827827 -- if f gives a function type, unify our argument type with

828828 -- f's expected argument type

829829 Bind _ (Pi _ _ argty _) _ -> unifyGoal (forget argty)

src/Idris/Core/Evaluate.hs+1−1

@@ -1020,7 +1020,7 @@ simplifyCasedef n ufnames umethss ei uctxt

10201020 (vs, x', y')

10211021 debind (Left x) = let (vs, x') = depat [] x in

10221022 (vs, x', Impossible)

1023− simpl (Right (x, y))

1023+ simpl (Right (x, y))

10241024 = if null ufnames then Right (x, y)

10251025 else Right (x, unfold uctxt [] (map (\n -> (n, 1)) (uns y)) y)

10261026 simpl t = t

src/Idris/Elab/Clause.hs+1−1

@@ -1108,7 +1108,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

11081108 wb <- mapM (mkAuxC mpn wname lhs (map fst bargs_pre) (map fst bargs_post))

11091109 withblock

11101110 logElab 3 ("with block " ++ show wb)

1111− setFlags wname [Inlinable]

1111+ setFlags wname [Inlinable]

11121112 when (AssertTotal `elem` opts) $

11131113 setFlags wname [Inlinable, AssertTotal]

11141114 i <- getIState

src/Idris/Elab/Term.hs+14−14

@@ -245,7 +245,7 @@ elab :: IState

245245elab ist info emode opts fn tm

246246 = do let loglvl = opt_logLevel (idris_options ist)

247247 when (loglvl > 5) $ unifyLog True

248− whnf_compute_args -- expand type synonyms, etc

248+ compute -- expand type synonyms, etc

249249 let fc = maybe "(unknown)"

250250 elabE initElabCtxt (elabFC info) tm -- (in argument, guarded, in type, in qquote)

251251 est <- getAux

@@ -339,13 +339,13 @@ elab ist info emode opts fn tm

339339 pexp ct]))

340340

341341 forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)

342− | (P _ (UN ht) _, _) <- unApply (whnf (tt_ctxt ist) env t),

342+ | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),

343343 ht == txt "Delayed" = notDelay orig

344344 forceErr orig env (CantUnify _ (t,_) (t',_) _ _ _)

345− | (P _ (UN ht) _, _) <- unApply (whnf (tt_ctxt ist) env t'),

345+ | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t'),

346346 ht == txt "Delayed" = notDelay orig

347347 forceErr orig env (InfiniteUnify _ t _)

348− | (P _ (UN ht) _, _) <- unApply (whnf (tt_ctxt ist) env t),

348+ | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),

349349 ht == txt "Delayed" = notDelay orig

350350 forceErr orig env (Elaborating _ _ _ t) = forceErr orig env t

351351 forceErr orig env (ElaboratingArg _ _ _ t) = forceErr orig env t

@@ -397,7 +397,7 @@ elab ist info emode opts fn tm

397397 highlightSource fc' (AnnConst c)

398398 elab' ina fc (PQuote r) = do fill r; solve

399399 elab' ina _ (PTrue fc _) =

400− do whnf_compute

400+ do compute

401401 g <- goal

402402 case g of

403403 TType _ -> elab' ina (Just fc) (PRef fc [] unitTy)

@@ -431,7 +431,7 @@ elab ist info emode opts fn tm

431431 pexp l, pexp r]))

432432

433433 elab' ina _ (PPair fc hls _ l r)

434− = do whnf_compute

434+ = do compute

435435 g <- goal

436436 let (tc, _) = unApply g

437437 case g of

@@ -454,7 +454,7 @@ elab ist info emode opts fn tm

454454 IsType -> asType

455455 IsTerm -> asValue

456456 TypeOrTerm ->

457− do whnf_compute

457+ do compute

458458 g <- goal

459459 case g of

460460 TType _ -> asType

@@ -544,7 +544,7 @@ elab ist info emode opts fn tm

544544 (trySeq' deferr xs) True

545545 elab' ina fc (PAlternative ms TryImplicit (orig : alts)) = do

546546 env <- get_env

547− whnf_compute

547+ compute

548548 ty <- goal

549549 let doelab = elab' ina fc orig

550550 tryCatch doelab

@@ -576,7 +576,7 @@ elab ist info emode opts fn tm

576576 recoverableErr _ = True

577577

578578 pruneAlts (CantUnify _ (inc, _) (outc, _) _ _ _) alts env

579− = case unApply (whnf (tt_ctxt ist) env inc) of

579+ = case unApply (normalise (tt_ctxt ist) env inc) of

580580 (P (TCon _ _) n _, _) -> filter (hasArg n env) alts

581581 (Constant _, _) -> alts

582582 _ -> filter isLend alts -- special case hack for 'Borrowed'

@@ -668,7 +668,7 @@ elab ist info emode opts fn tm

668668 do fty <- get_type (Var n) -- check for implicits

669669 ctxt <- get_context

670670 env <- get_env

671− let a' = insertScopedImps fc (whnfArgs ctxt env fty) []

671+ let a' = insertScopedImps fc (normalise ctxt env fty) []

672672 if null a'

673673 then erun fc $

674674 do apply (Var n) []

@@ -863,7 +863,7 @@ elab ist info emode opts fn tm

863863 let dataCon = isDConName f ctxt

864864 annot <- findHighlight f

865865 mapM_ checkKnownImplicit args_in

866− let args = insertScopedImps fc (whnfArgs ctxt env fty) args_in

866+ let args = insertScopedImps fc (normalise ctxt env fty) args_in

867867 let unmatchableArgs = if pattern

868868 then getUnmatchable (tt_ctxt ist) f

869869 else []

@@ -925,7 +925,7 @@ elab ist info emode opts fn tm

925925 return []

926926 Just rguess -> do

927927 gty <- get_type rguess

928− let ty_n = whnf ctxt env gty

928+ let ty_n = normalise ctxt env gty

929929 return $ getReqImps ty_n

930930 else return []

931931 -- Now we find out how many implicits we needed at the

@@ -982,7 +982,7 @@ elab ist info emode opts fn tm

982982 case lookupBinder n env of

983983 Nothing -> return ()

984984 Just b ->

985− case unApply (whnf (tt_ctxt ist) env (binderTy b)) of

985+ case unApply (normalise (tt_ctxt ist) env (binderTy b)) of

986986 (P _ c _, args) ->

987987 case lookupCtxtExact c (idris_interfaces ist) of

988988 Nothing -> return ()

@@ -1713,7 +1713,7 @@ pruneByType imp env (P _ n _) goalty ist as

17131713 Just ty -> case unApply (getRetTy ty) of

17141714 (P _ ctyn _, _) | isTConName ctyn ctxt && not (ctyn == f)

17151715 -> False

1716− _ -> let ty' = whnf ctxt [] ty in

1716+ _ -> let ty' = normalise ctxt [] ty in

17171717-- trace ("Trying " ++ show f' ++ " : " ++ show (getRetTy ty') ++ " for " ++ show goalty

17181718-- ++ "\nMATCH: " ++ show (pat, matching (getRetTy ty') goalty)) $

17191719 case unApply (getRetTy ty') of

src/Idris/ElabDecls.hs+2−2

@@ -231,14 +231,14 @@ elabDecl' what info (PMutual f ps)

231231

232232 findTCImpl :: IState -> PDecl -> Maybe (Name, [Name])

233233 findTCImpl ist (PImplementation _ _ _ _ _ _ _ _ n_in _ ps _ _ expn _)

234− = let (n, meths)

234+ = let (n, meths)

235235 = case lookupCtxtName n_in (idris_interfaces ist) of

236236 [(n', ci)] -> (n', map fst (interface_methods ci))

237237 _ -> (n_in, [])

238238 iname = mkiname n (namespace info) ps expn in

239239 Just (iname, meths)

240240 findTCImpl ist _ = Nothing

241−

241+

242242 mkiname n' ns ps' expn' =

243243 case expn' of

244244 Nothing -> case ns of

test/basic018/expected+1−1

@@ -8,7 +8,7 @@ basic018.idr:13:6:When checking right hand side of test with expected type

88Type mismatch between

99 42 = 42 (Type of Refl)

1010and

11− thing = S (fromIntegerNat 41) (Expected type)

11+ thing = 42 (Expected type)

1212

1313Specifically:

1414 Type mismatch between