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

git.iko.soy/Idris-dev

on master help sign in

Move forcing to Compiler.hs.

5f93139Matus Tejiscak13 years ago

src/IRTS/Compiler.hs+6−1

compare with master

unifiedsplit

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

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

424 return $ LCase tm' alts'

425

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+

426-- There are two transformations in this case:

431-- There are two transformations in this case:

427--

432--

428-- 1. Newtype-case elimination:

433-- 1. Newtype-case elimination:

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

440--

445--

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

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

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

447-- 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.

444--

449--

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

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

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

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

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

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

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

4 Phase(..), CaseTree,

5 simpleCase, small, namesUsed, findCalls, findUsedArgs,

6− substSC, substAlt) where

6+ substSC, substAlt, mkForce) where

8import Idris.Core.TT

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

585 in case alts' of

586 [] -> ImpossibleCase

587

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

589+ --

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

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

589− | proj

591+ -- | proj

590− , delay == txt "Delay"

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

591− -> mkForce n arg sc

593+ -- -> mkForce n arg sc

592

594

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

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

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

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

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

625 notErased (DefaultCase ImpossibleCase) = False

627 notErased (DefaultCase ImpossibleCase) = False

626 notErased _ = True

628 notErased _ = True

627

629

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−

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

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

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

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

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

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

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

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

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

666 n `projectibleInAlt` DefaultCase sc = n `projectibleInSC` sc

643 n `projectibleInAlt` DefaultCase sc = n `projectibleInSC` sc

667

644

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−

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

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

674

646

675 projRep :: Name -> Name -> Int -> SC -> SC

647 projRep :: Name -> Name -> Int -> SC -> SC

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

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

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

703stripLambdas x = x

675stripLambdas x = x

704

676

705−

706substSC :: Name -> Name -> SC -> SC

677substSC :: Name -> Name -> SC -> SC

707substSC n repl (Case n' alts)

678substSC n repl (Case n' alts)

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

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

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

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

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

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

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

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

691substAlt 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)