@@ -526,6 +526,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
526526 [ty] -> return ty
527527 pats_in <- mapM (elabClause info (Dictionary `elem` opts))
528528 (zip [0..] cs)
529+ logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in
530+
529531 -- if the return type of 'ty' is collapsible, the optimised version should
530532 -- just do nothing
531533 ist <- getIState
@@ -557,12 +559,25 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
557559 -- show r) pats))
558560 let tcase = opt_typecase (idris_options ist)
559561
560− -- pdef is the compile-time pattern definition with basic
561− -- simplifications applied.
562+ -- Summary of what's about to happen: Definitions go:
563+
564+ -- pats_in -> pats -> optpats
565+ -- pdef comes from pats,
566+ -- optpdef comes from optpats
567+ -- Then pdef' is optpdef with forcing/collapsing applied everywhere
568+
569+ -- addCaseDef builds case trees from <pdef> and <pdef'>
570+
571+ -- pdef is the compile-time pattern definition.
562572 -- This will get further optimised for run-time, and, separately,
563573 -- further inlined to help with totality checking.
564− let pdef = map debind $ map (simpl (tt_ctxt ist)) pats
574+ let pdef = map debind $ map (simple_lhs (tt_ctxt ist)) pats
565575
576+ logLvl 5 $ "Initial typechecked patterns:\n" ++ show pdef
577+
578+ -- TODO: Inlining on initial definition happens here
579+ let pdef_inl = pdef
580+
566581 numArgs <- tclift $ sameLength pdef
567582
568583 -- patterns after collapsing optimisation applied
@@ -572,13 +587,11 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
572587 (take numArgs (repeat Erased)), Erased)]
573588 else stripCollapsed pats
574589
575− logLvl 5 $ "Patterns:\n" ++ show pats_in
576590 case specNames opts of
577591 Just _ -> logLvl 5 $ "Partially evaluated:\n" ++ show pats
578592 _ -> return ()
579− logLvl 3 $ "SIMPLIFIED: \n" ++ show pdef
580593
581− let optpdef = map debind $ map (simpl (tt_ctxt ist)) optpats
594+ let optpdef = map debind $ map (simple_lhs (tt_ctxt ist)) optpats
582595 tree@(CaseDef scargs sc _) <- tclift $
583596 simpleCase tcase False reflect CompileTime fc pdef
584597 cov <- coverage
@@ -600,13 +613,11 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
600613 return (filter (noMatch ist clhs) missing')
601614 else return []
602615 let pcover = null pmissing
603− logLvl 2 $ "Optimising patterns"
604− logLvl 5 $ show optpdef
605616
606617 -- pdef' is the version that gets compiled for run-time
607618 pdef' <- applyOpts optpdef
608− logLvl 2 $ "Optimised patterns"
609− logLvl 5 $ show pdef'
619+ logLvl 5 $ "After data structure transofmrations:\n" ++ show pdef'
620+
610621 ist <- getIState
611622 -- let wf = wellFounded ist n sc
612623 let tot = if pcover || AssertTotal `elem` opts
@@ -642,7 +653,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
642653 reflect
643654 (AssertTotal `elem` opts)
644655 pats
645− pdef pdef' ty)
656+ pdef pdef_inl pdef' ty)
646657 addIBC (IBCDef n)
647658 setTotality n tot
648659 when (not reflect) $ totcheck (fc, n)
@@ -686,9 +697,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
686697
687698 getLHS (_, l, _) = l
688699
689− simpl ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)
690−-- Core.Evaluate.simplify ctxt False [] y)
691− simpl ctxt t = t
700+ simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)
701+ simple_lhs ctxt t = t
692702
693703 specNames [] = Nothing
694704 specNames (Specialise ns : _) = Just ns