5f93139 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Move forcing to Compiler.hs.

commit5f93139d2adefca9be8c4b1b402c3f92a0416f8a authorMatus Tejiscak <ziman@functor.sk> dateThu 27 Mar 2014, 14:41 (13 years ago) parent0203531

2 files changed+44−37

compare with master

unifiedsplit

src/IRTS/Compiler.hs+6−1 src/Idris/Core/CaseTree.hs+38−36

src/IRTS/Compiler.hs+6−1

@@ -423,6 +423,11 @@ irSC vs (ProjCase tm alts) = do

423423 alts' <- mapM (irAlt vs tm') alts

424424 return $ LCase tm' alts'

425425

426+-- Transform matching on Delay to applications of Force.

427+irSC vs (Case n [ConCase (UN delay) i [_, _, n'] sc])

428+ | delay == txt "Delay"

429+ = irSC vs $ mkForce n n' sc

430+

426431-- There are two transformations in this case:

427432--

428433-- 1. Newtype-case elimination:

@@ -440,7 +445,7 @@ irSC vs (ProjCase tm alts) = do

440445--

441446-- In the example above, {e0} will most probably have been erased

442447-- so this vain projection would make the resulting program segfault

443−-- because the code generator still emits a PROJECT(...) STG instruction.

448+-- because the code generator still emits a PROJECT(...) G-machine instruction.

444449--

445450-- Hence, we check whether the variables are used at all

446451-- and erase the casesplit if they are not.

src/Idris/Core/CaseTree.hs+38−36

@@ -3,7 +3,7 @@

33module Idris.Core.CaseTree(CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..),

44 Phase(..), CaseTree,

55 simpleCase, small, namesUsed, findCalls, findUsedArgs,

6− substSC, substAlt) where

6+ substSC, substAlt, mkForce) where

88import Idris.Core.TT

@@ -585,10 +585,12 @@ prune proj (Case n alts)

585585 in case alts' of

586586 [] -> ImpossibleCase

587587

588− [ConCase (UN delay) i [t, a, arg] sc]

589− | proj

590− , delay == txt "Delay"

591− -> mkForce n arg sc

588+ -- This will be done in irSC in Compiler.hs.

589+ --

590+ --[ConCase (UN delay) i [t, a, arg] sc]

591+ -- | proj

592+ -- , delay == txt "Delay"

593+ -- -> mkForce n arg sc

592594

593595 -- Projection transformations prevent us from seeing some uses of ctor fields

594596 -- because they delete information about which ctor is being used.

@@ -625,31 +627,6 @@ prune proj (Case n alts)

625627 notErased (DefaultCase ImpossibleCase) = False

626628 notErased _ = True

627629

628− -- single-alternative case on a forced value

629− -- can be translated to a ProjCase directly

630− mkForce n arg (Case x alts) | x == arg

631− = ProjCase (forceArg n) $ map (mkForceAlt n arg) alts

632−

633− mkForce n arg (Case x alts)

634− = Case x (map (mkForceAlt n arg) alts)

635−

636− mkForce n arg (ProjCase t alts)

637− = ProjCase (forceTm n arg t) $ map (mkForceAlt n arg) alts

638−

639− mkForce n arg (STerm t) = STerm (forceTm n arg t)

640− mkForce n arg c = c

641−

642− mkForceAlt n arg (ConCase cn t args rhs)

643− = ConCase cn t args (mkForce n arg rhs)

644− mkForceAlt n arg (FnCase cn args rhs)

645− = FnCase cn args (mkForce n arg rhs)

646− mkForceAlt n arg (ConstCase t rhs)

647− = ConstCase t (mkForce n arg rhs)

648− mkForceAlt n arg (SucCase sn rhs)

649− = SucCase sn (mkForce n arg rhs)

650− mkForceAlt n arg (DefaultCase rhs)

651− = DefaultCase (mkForce n arg rhs)

652−

653630 -- Figure out whether the name is projectible in the SC:

654631 -- For example, (Case n _) only admits /names/ as "n"

655632 -- so we cannot replace n with a projection of anything.

@@ -665,11 +642,6 @@ prune proj (Case n alts)

665642 n `projectibleInAlt` SucCase cn sc = n `projectibleInSC` sc

666643 n `projectibleInAlt` DefaultCase sc = n `projectibleInSC` sc

667644

668− forceTm n arg t = subst arg (forceArg n) t

669−

670− forceArg n = App (App (App (P Ref (sUN "Force") Erased) Erased) Erased)

671− (P Bound n Erased)

672−

673645 mkProj n i xs sc = foldr (\x -> projRep x n i) sc xs

674646

675647 projRep :: Name -> Name -> Int -> SC -> SC

@@ -702,7 +674,6 @@ stripLambdas (CaseDef ns (STerm (Bind x (Lam _) sc)) tm)

702674 = stripLambdas (CaseDef (ns ++ [x]) (STerm (instantiate (P Bound x Erased) sc)) tm)

703675stripLambdas x = x

704676

705−

706677substSC :: Name -> Name -> SC -> SC

707678substSC n repl (Case n' alts)

708679 | n == n' = Case repl (map (substAlt n repl) alts)

@@ -718,3 +689,34 @@ substAlt n repl (SucCase n' sc)

718689 | n == n' = SucCase n (substSC n repl sc)

719690 | otherwise = SucCase n' (substSC n repl sc)

720691substAlt n repl (DefaultCase sc) = DefaultCase (substSC n repl sc)

692+

693+mkForce :: Name -> Name -> SC -> SC

694+mkForce = mkForceSC

695+ where

696+ mkForceSC n arg (Case x alts) | x == arg

697+ = ProjCase (forceArg n) $ map (mkForceAlt n arg) alts

698+

699+ mkForceSC n arg (Case x alts)

700+ = Case x (map (mkForceAlt n arg) alts)

701+

702+ mkForceSC n arg (ProjCase t alts)

703+ = ProjCase (forceTm n arg t) $ map (mkForceAlt n arg) alts

704+

705+ mkForceSC n arg (STerm t) = STerm (forceTm n arg t)

706+ mkForceSC n arg c = c

707+

708+ mkForceAlt n arg (ConCase cn t args rhs)

709+ = ConCase cn t args (mkForceSC n arg rhs)

710+ mkForceAlt n arg (FnCase cn args rhs)

711+ = FnCase cn args (mkForceSC n arg rhs)

712+ mkForceAlt n arg (ConstCase t rhs)

713+ = ConstCase t (mkForceSC n arg rhs)

714+ mkForceAlt n arg (SucCase sn rhs)

715+ = SucCase sn (mkForceSC n arg rhs)

716+ mkForceAlt n arg (DefaultCase rhs)

717+ = DefaultCase (mkForceSC n arg rhs)

718+

719+ forceTm n arg t = subst arg (forceArg n) t

720+

721+ forceArg n = App (App (App (P Ref (sUN "Force") Erased) Erased) Erased)

722+ (P Bound n Erased)