3fcbff5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

A little reorganisation of clauses elaboration

3fcbff5Edwin Brady13 years ago

src/Core/Evaluate.hs+16−10

compare with master

unifiedsplit

@@ -674,24 +674,30 @@ addDatatype (Data n tag ty cons) uctxt

674-- FIXME: Too many arguments! Refactor all these Bools.

675addCasedef :: Name -> CaseInfo -> Bool -> Bool -> Bool -> Bool ->

676 [Either Term (Term, Term)] ->

677− [([Name], Term, Term)] ->

677+ [([Name], Term, Term)] -> -- totality

678+ [([Name], Term, Term)] -> -- compile time

678− [([Name], Term, Term)] ->

679+ [([Name], Term, Term)] -> -- run time

679 Type -> Context -> Context

680 Type -> Context -> Context

680addCasedef n ci@(CaseInfo alwaysInline tcdict)

681addCasedef n ci@(CaseInfo alwaysInline tcdict)

681− tcase covering reflect asserted ps_in ps psrt ty uctxt

682+ tcase covering reflect asserted ps_in ps_tot ps_ct ps_rt ty uctxt

682 = let ctxt = definitions uctxt

683 = let ctxt = definitions uctxt

683 access = case lookupDefAcc n False uctxt of

684 access = case lookupDefAcc n False uctxt of

684 [(_, acc)] -> acc

685 [(_, acc)] -> acc

685 _ -> Public

686 _ -> Public

686− ctxt' = case (simpleCase tcase covering reflect CompileTime (FC "" 0) ps,

687+ ctxt' = case (simpleCase tcase covering reflect CompileTime (FC "" 0) ps_tot,

688+ simpleCase tcase covering reflect CompileTime (FC "" 0) ps_ct,

687− simpleCase tcase covering reflect RunTime (FC "" 0) psrt) of

689+ simpleCase tcase covering reflect RunTime (FC "" 0) ps_rt) of

688− (OK (CaseDef args sc _), OK (CaseDef args' sc' _)) ->

690+ (OK (CaseDef args_tot sc_tot _),

691+ OK (CaseDef args_ct sc_ct _),

692+ OK (CaseDef args_rt sc_rt _)) ->

689 let inl = alwaysInline -- || tcdict

693 let inl = alwaysInline -- || tcdict

690− inlc = (inl || small n args sc') && (not asserted)

694+ inlc = (inl || small n args_ct sc_ct) && (not asserted)

691− inlr = inl || small n args sc'

695+ inlr = inl || small n args_rt sc_rt

692− cdef = CaseDefs (args, sc) (args, sc) (args', sc') in

696+ cdef = CaseDefs (args_tot, sc_tot)

697+ (args_ct, sc_ct)

698+ (args_rt, sc_rt) in

693 addDef n (CaseOp (ci { case_inlinable = inlc })

699 addDef n (CaseOp (ci { case_inlinable = inlc })

694− ty ps_in ps cdef,

700+ ty ps_in ps_tot cdef,

695 access, Unchecked) ctxt in

701 access, Unchecked) ctxt in

696 uctxt { definitions = ctxt' }

702 uctxt { definitions = ctxt' }

697

703

src/Idris/ElabDecls.hs+24−14

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

526 [ty] -> return ty

527 pats_in <- mapM (elabClause info (Dictionary `elem` opts))

528 (zip [0..] cs)

529+ logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in

530+

529 -- if the return type of 'ty' is collapsible, the optimised version should

531 -- if the return type of 'ty' is collapsible, the optimised version should

530 -- just do nothing

532 -- just do nothing

531 ist <- getIState

533 ist <- getIState

@@ -557,12 +559,25 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

557 -- show r) pats))

559 -- show r) pats))

558 let tcase = opt_typecase (idris_options ist)

560 let tcase = opt_typecase (idris_options ist)

559

561

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+

560− -- pdef is the compile-time pattern definition with basic

571+ -- pdef is the compile-time pattern definition.

561− -- simplifications applied.

562 -- This will get further optimised for run-time, and, separately,

572 -- This will get further optimised for run-time, and, separately,

563 -- further inlined to help with totality checking.

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

565

575

576+ logLvl 5 $ "Initial typechecked patterns:\n" ++ show pdef

577+

578+ -- TODO: Inlining on initial definition happens here

579+ let pdef_inl = pdef

580+

566 numArgs <- tclift $ sameLength pdef

581 numArgs <- tclift $ sameLength pdef

567

582

568 -- patterns after collapsing optimisation applied

583 -- patterns after collapsing optimisation applied

@@ -572,13 +587,11 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

572 (take numArgs (repeat Erased)), Erased)]

587 (take numArgs (repeat Erased)), Erased)]

573 else stripCollapsed pats

588 else stripCollapsed pats

574

589

575− logLvl 5 $ "Patterns:\n" ++ show pats_in

576 case specNames opts of

590 case specNames opts of

577 Just _ -> logLvl 5 $ "Partially evaluated:\n" ++ show pats

591 Just _ -> logLvl 5 $ "Partially evaluated:\n" ++ show pats

578 _ -> return ()

592 _ -> return ()

579− logLvl 3 $ "SIMPLIFIED: \n" ++ show pdef

580

593

581− let optpdef = map debind $ map (simpl (tt_ctxt ist)) optpats

594+ let optpdef = map debind $ map (simple_lhs (tt_ctxt ist)) optpats

582 tree@(CaseDef scargs sc _) <- tclift $

595 tree@(CaseDef scargs sc _) <- tclift $

583 simpleCase tcase False reflect CompileTime fc pdef

596 simpleCase tcase False reflect CompileTime fc pdef

584 cov <- coverage

597 cov <- coverage

@@ -600,13 +613,11 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

600 return (filter (noMatch ist clhs) missing')

613 return (filter (noMatch ist clhs) missing')

601 else return []

614 else return []

602 let pcover = null pmissing

615 let pcover = null pmissing

603− logLvl 2 $ "Optimising patterns"

604− logLvl 5 $ show optpdef

605

616

606 -- pdef' is the version that gets compiled for run-time

617 -- pdef' is the version that gets compiled for run-time

607 pdef' <- applyOpts optpdef

618 pdef' <- applyOpts optpdef

608− logLvl 2 $ "Optimised patterns"

619+ logLvl 5 $ "After data structure transofmrations:\n" ++ show pdef'

609− logLvl 5 $ show pdef'

620+

610 ist <- getIState

621 ist <- getIState

611 -- let wf = wellFounded ist n sc

622 -- let wf = wellFounded ist n sc

612 let tot = if pcover || AssertTotal `elem` opts

623 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

642 reflect

653 reflect

643 (AssertTotal `elem` opts)

654 (AssertTotal `elem` opts)

644 pats

655 pats

645− pdef pdef' ty)

656+ pdef pdef_inl pdef' ty)

646 addIBC (IBCDef n)

657 addIBC (IBCDef n)

647 setTotality n tot

658 setTotality n tot

648 when (not reflect) $ totcheck (fc, n)

659 when (not reflect) $ totcheck (fc, n)

@@ -686,9 +697,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

686

697

687 getLHS (_, l, _) = l

698 getLHS (_, l, _) = l

688

699

689− simpl ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)

700+ simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)

690−-- Core.Evaluate.simplify ctxt False [] y)

691− simpl ctxt t = t

701+ simple_lhs ctxt t = t

692

702

693 specNames [] = Nothing

703 specNames [] = Nothing

694 specNames (Specialise ns : _) = Just ns

704 specNames (Specialise ns : _) = Just ns

src/Idris/Prover.hs+1

@@ -75,6 +75,7 @@ prove ctxt lit n ty

75 updateContext (addCasedef n (CaseInfo True False) False False True False

76 [Right (P Ref n ty, ptm)]

77 [([], P Ref n ty, ptm)]

78+ [([], P Ref n ty, ptm)]

78 [([], P Ref n ty, ptm')] ty)

79 [([], P Ref n ty, ptm')] ty)

79 solveDeferred n

80 solveDeferred n

80elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])

81elabStep :: ElabState [PDecl] -> ElabD a -> Idris (a, ElabState [PDecl])