90127b3 · Idris-dev · git.iko.soy

CHANGELOG+6

compare with master

unifiedsplit

@@ -36,6 +36,12 @@ New in 0.9.18:

36 "n". If "n" is lexically bound, then the resulting quotation will be for it,

37 whereas if it is not, then it will succeed with a quotation of the unique

38 global name that matches.

39+* if ... then ... else ... is now built-in syntax instead of being defined in

40+ a library. It is shown in REPL output and error messages, rather than its

41+ desugaring.

42+* The desugaring of if ... then ... else ... has been renamed to ifThenElse from

43+ boolElim. This is for consistency with GHC Haskell and scala-virtualized, and

44+ to reflect that if-notation makes sense with non-Bool datatypes.

39

45

40New in 0.9.17:

46New in 0.9.17:

41--------------

47--------------

docs/faq/faq.rst+7−7

@@ -59,16 +59,16 @@ concrete ``Int``, whereas ``thing_comp`` is a computation which will produce an

59How can I make lazy control structures?

60=======================================

61

62−You can make control structures using the special Lazy type. For example,

62+You can make control structures using the special Lazy type. For

63+example, ``if...then...else...`` in Idris expands to an application of

64+a function named ``ifThenElse``. The default implementation for

63−``if...then...else`` is defined as follows in the library:

65+Booleans is defined as follows in the library:

64

66

65.. code-block:: idris

67.. code-block:: idris

66

68

67− boolElim : Bool -> (t : Lazy a) -> (e : Lazy a) -> a

69+ ifThenElse : Bool -> (t : Lazy a) -> (e : Lazy a) -> a

68− boolElim True t e = t

70+ ifThenElse True t e = t

69− boolElim False t e = e

71+ ifThenElse False t e = e

70−

71− syntax if [test] then [t] else [e] = boolElim test t e

72

73The type ``Lazy a`` for ``t`` and ``f`` indicates that those arguments will

74only be evaluated if they are used, that is, they are evaluated lazily.

libs/prelude/Prelude/Bool.idr+3−6

@@ -11,12 +11,9 @@ import Prelude.Uninhabited

11||| @ b the condition on the if

12||| @ t the value if b is true

13||| @ e the falue if b is false

14−boolElim : (b : Bool) -> (t : Lazy a) -> (e : Lazy a) -> a

14+ifThenElse : (b : Bool) -> (t : Lazy a) -> (e : Lazy a) -> a

15−boolElim True t e = t

15+ifThenElse True t e = t

16−boolElim False t e = e

16+ifThenElse False t e = e

17−

18−-- Syntactic sugar for boolean elimination.

19−syntax if [test] then [t] else [e] = boolElim test (Delay t) (Delay e)

20

17

21-- Boolean Operator Precedence

18-- Boolean Operator Precedence

22infixl 4 &&, ||

19infixl 4 &&, ||

libs/prelude/Prelude/Classes.idr+1−1

@@ -86,7 +86,7 @@ class Eq a => Ord a where

86 (>=) x y = x > y || x == y

87

88 max : a -> a -> a

89− max x y = if (x > y) then x else y

89+ max x y = if x > y then x else y

90

91 min : a -> a -> a

92 min x y = if (x < y) then x else y

libs/prelude/Prelude/Nat.idr+27−27

@@ -630,31 +630,31 @@ minusSuccPred (S left) (S right) =

630 let inductiveHypothesis = minusSuccPred left right in

631 ?minusSuccPredStepCase'

632

633−-- boolElim

633+-- ifThenElse

634−total boolElimSuccSucc : (cond : Bool) -> (t : Nat) -> (f : Nat) ->

634+total ifThenElseSuccSucc : (cond : Bool) -> (t : Nat) -> (f : Nat) ->

635− S (boolElim cond t f) = boolElim cond (S t) (S f)

635+ S (ifThenElse cond t f) = ifThenElse cond (S t) (S f)

636−boolElimSuccSucc True t f = Refl

636+ifThenElseSuccSucc True t f = Refl

637−boolElimSuccSucc False t f = Refl

637+ifThenElseSuccSucc False t f = Refl

638−

638+

639−total boolElimPlusPlusLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) ->

639+total ifThenElsePlusPlusLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) ->

640− left + (boolElim cond t f) = boolElim cond (left + t) (left + f)

640+ left + (ifThenElse cond t f) = ifThenElse cond (left + t) (left + f)

641−boolElimPlusPlusLeft True left t f = Refl

641+ifThenElsePlusPlusLeft True left t f = Refl

642−boolElimPlusPlusLeft False left t f = Refl

642+ifThenElsePlusPlusLeft False left t f = Refl

643−

643+

644−total boolElimPlusPlusRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) ->

644+total ifThenElsePlusPlusRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) ->

645− (boolElim cond t f) + right = boolElim cond (t + right) (f + right)

645+ (ifThenElse cond t f) + right = ifThenElse cond (t + right) (f + right)

646−boolElimPlusPlusRight True right t f = Refl

646+ifThenElsePlusPlusRight True right t f = Refl

647−boolElimPlusPlusRight False right t f = Refl

647+ifThenElsePlusPlusRight False right t f = Refl

648−

648+

649−total boolElimMultMultLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) ->

649+total ifThenElseMultMultLeft : (cond : Bool) -> (left : Nat) -> (t : Nat) -> (f : Nat) ->

650− left * (boolElim cond t f) = boolElim cond (left * t) (left * f)

650+ left * (ifThenElse cond t f) = ifThenElse cond (left * t) (left * f)

651−boolElimMultMultLeft True left t f = Refl

651+ifThenElseMultMultLeft True left t f = Refl

652−boolElimMultMultLeft False left t f = Refl

652+ifThenElseMultMultLeft False left t f = Refl

653−

653+

654−total boolElimMultMultRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) ->

654+total ifThenElseMultMultRight : (cond : Bool) -> (right : Nat) -> (t : Nat) -> (f : Nat) ->

655− (boolElim cond t f) * right = boolElim cond (t * right) (f * right)

655+ (ifThenElse cond t f) * right = ifThenElse cond (t * right) (f * right)

656−boolElimMultMultRight True right t f = Refl

656+ifThenElseMultMultRight True right t f = Refl

657−boolElimMultMultRight False right t f = Refl

657+ifThenElseMultMultRight False right t f = Refl

658

659-- Orders

660total lteNTrue : (n : Nat) -> lte n n = True

@@ -910,13 +910,13 @@ plusZeroRightNeutralStepCase = proof {

910

911maximumSuccSuccStepCase = proof {

912 intros;

913− rewrite sym (boolElimSuccSucc (lte left right) (S right) (S left));

913+ rewrite sym (ifThenElseSuccSucc (lte left right) (S right) (S left));

914 trivial;

915}

916

917minimumSuccSuccStepCase = proof {

918 intros;

919− rewrite (boolElimSuccSucc (lte left right) (S left) (S right));

919+ rewrite (ifThenElseSuccSucc (lte left right) (S left) (S right));

920 trivial;

921}

922

src/IRTS/Compiler.hs+3−1

@@ -299,9 +299,11 @@ irTerm vs env tm@(App _ f a) = do

299 -- a really common case, and the laziness hurts...

300 (P _ (NS (UN be) [b,p]) _, [_,x,(App _ (App _ (App _ (P _ (UN d) _) _) _) t),

301 (App _ (App _ (App _ (P _ (UN d') _) _) _) e)])

302− | be == txt "boolElim"

302+ | be == txt "ifThenElse"

303 , d == txt "Delay"

304 , d' == txt "Delay"

305+ , b == txt "Bool"

306+ , p == txt "Prelude"

305 -> do

307 -> do

306 x' <- irTerm vs env x

308 x' <- irTerm vs env x

307 t' <- irTerm vs env t

309 t' <- irTerm vs env t

src/Idris/AbsSyntax.hs+10−2

@@ -18,6 +18,7 @@ import System.Console.Haskeline

18import System.IO

19

20import Control.Applicative

21+import Control.Monad (liftM3)

21import Control.Monad.State

22import Control.Monad.State

22

23

23import Data.List hiding (insert,union)

24import Data.List hiding (insert,union)

@@ -1011,6 +1012,7 @@ expandParams dec ps ns infs tm = en tm

1011 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)

1012 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)

1012 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)

1013 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)

1013 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)

1014 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)

1015+ en (PIfThenElse fc c t f) = PIfThenElse fc (en c) (en t) (en f)

1014 en (PRunElab fc tm) = PRunElab fc (en tm)

1016 en (PRunElab fc tm) = PRunElab fc (en tm)

1015 en t = t

1017 en t = t

1016

1018

@@ -1578,6 +1580,9 @@ addImpl' inpat env infns imp_meths ist ptm

1578 -- If the name in a lambda is a constructor name, do this as a 'case'

1580 -- If the name in a lambda is a constructor name, do this as a 'case'

1579 -- instead (it is harmless to do so, especially since the lambda will

1581 -- instead (it is harmless to do so, especially since the lambda will

1580 -- be lifted anyway!)

1582 -- be lifted anyway!)

1583+ ai qq env ds (PIfThenElse fc c t f) = PIfThenElse fc (ai qq env ds c)

1584+ (ai qq env ds t)

1585+ (ai qq env ds f)

1581 ai qq env ds (PLam fc n ty sc)

1586 ai qq env ds (PLam fc n ty sc)

1582 = case lookupDef n (tt_ctxt ist) of

1587 = case lookupDef n (tt_ctxt ist) of

1583 [] -> let ty' = ai qq env ds ty

1588 [] -> let ty' = ai qq env ds ty

@@ -1870,9 +1875,8 @@ instance Monad (EitherErr a) where

1870toEither (LeftErr e) = Left e

1875toEither (LeftErr e) = Left e

1871toEither (RightOK ho) = Right ho

1876toEither (RightOK ho) = Right ho

1872

1877

1873−-- syntactic match of a against b, returning pair of variables in a

1878+-- | Syntactic match of a against b, returning pair of variables in a

1874-- and what they match. Returns the pair that failed if not a match.

1879-- and what they match. Returns the pair that failed if not a match.

1875−

1876matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]

1880matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]

1877matchClause = matchClause' False

1881matchClause = matchClause' False

1878

1882

@@ -2013,6 +2017,7 @@ substMatchShadow n shs tm t = sm shs t where

2013 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)

2017 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)

2014 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)

2018 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)

2015 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)

2019 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)

2020+ sm xs (PIfThenElse fc c t f) = PIfThenElse fc (sm xs c) (sm xs t) (sm xs f)

2016 sm xs (PEq f xt yt x y) = PEq f (sm xs xt) (sm xs yt) (sm xs x) (sm xs y)

2021 sm xs (PEq f xt yt x y) = PEq f (sm xs xt) (sm xs yt) (sm xs x) (sm xs y)

2017 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)

2022 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)

2018 (fmap (sm xs) tm)

2023 (fmap (sm xs) tm)

@@ -2041,6 +2046,7 @@ shadow n n' t = sm t where

2041 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

2046 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

2042 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)

2047 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)

2043 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)

2048 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)

2049+ sm (PIfThenElse fc c t f) = PIfThenElse fc (sm c) (sm t) (sm f)

2044 sm (PEq f xt yt x y) = PEq f (sm xt) (sm yt) (sm x) (sm y)

2050 sm (PEq f xt yt x y) = PEq f (sm xt) (sm yt) (sm x) (sm y)

2045 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)

2051 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)

2046 sm (PTyped x y) = PTyped (sm x) (sm y)

2052 sm (PTyped x y) = PTyped (sm x) (sm y)

@@ -2125,6 +2131,8 @@ mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where

2125 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y

2131 alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y

2126 return (x', y')) alts

2132 return (x', y')) alts

2127 return $! PCase fc t' alts'

2133 return $! PCase fc t' alts'

2134+ mkUniq (PIfThenElse fc c t f)

2135+ = liftM3 (PIfThenElse fc) (mkUniq c) (mkUniq t) (mkUniq f)

2128 mkUniq (PPair fc p l r)

2136 mkUniq (PPair fc p l r)

2129 = do l' <- mkUniq l; r' <- mkUniq r

2137 = do l' <- mkUniq l; r' <- mkUniq r

2130 return $! PPair fc p l' r'

2138 return $! PPair fc p l' r'

src/Idris/AbsSyntaxTree.hs+21−5

@@ -805,6 +805,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

805 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)

806 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application

807 | PMatchApp FC Name -- ^ Make an application by type matching

808+ | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse

808 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs

809 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs

809 | PTrue FC PunInfo -- ^ Unit type..?

810 | PTrue FC PunInfo -- ^ Unit type..?

810 | PRefl FC PTerm -- ^ The canonical proof of the equality type

811 | PRefl FC PTerm -- ^ The canonical proof of the equality type

@@ -855,6 +856,7 @@ mapPT f t = f (mpt t) where

855 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)

856 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)

856 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)

857 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)

857 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)

858 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)

859+ mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)

858 mpt (PEq fc lt rt l r) = PEq fc (mapPT f lt) (mapPT f rt) (mapPT f l) (mapPT f r)

860 mpt (PEq fc lt rt l r) = PEq fc (mapPT f lt) (mapPT f rt) (mapPT f l) (mapPT f r)

859 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)

861 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)

860 mpt (PPair fc p l r) = PPair fc p (mapPT f l) (mapPT f r)

862 mpt (PPair fc p l r) = PPair fc p (mapPT f l) (mapPT f r)

@@ -1013,6 +1015,7 @@ highestFC (PApp fc _ _) = Just fc

1013highestFC (PAppBind fc _ _) = Just fc

1015highestFC (PAppBind fc _ _) = Just fc

1014highestFC (PMatchApp fc _) = Just fc

1016highestFC (PMatchApp fc _) = Just fc

1015highestFC (PCase fc _ _) = Just fc

1017highestFC (PCase fc _ _) = Just fc

1018+highestFC (PIfThenElse fc _ _ _) = Just fc

1016highestFC (PTrue fc _) = Just fc

1019highestFC (PTrue fc _) = Just fc

1017highestFC (PRefl fc _) = Just fc

1020highestFC (PRefl fc _) = Just fc

1018highestFC (PResolveTC fc) = Just fc

1021highestFC (PResolveTC fc) = Just fc

@@ -1536,9 +1539,15 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1536 noNS (NS _ _) = False

1539 noNS (NS _ _) = False

1537 noNS _ = True

1540 noNS _ = True

1538

1541

1542+ prettySe p bnd (PIfThenElse _ c t f) =

1543+ group . align . hang 2 . vsep $

1544+ [ kwd "if" <+> prettySe startPrec bnd c

1545+ , kwd "then" <+> prettySe startPrec bnd t

1546+ , kwd "else" <+> prettySe startPrec bnd f

1547+ ]

1539 prettySe p bnd (PHidden tm) = text "." <> prettySe funcAppPrec bnd tm

1548 prettySe p bnd (PHidden tm) = text "." <> prettySe funcAppPrec bnd tm

1540 prettySe p bnd (PRefl _ _) = annName eqCon $ text "Refl"

1549 prettySe p bnd (PRefl _ _) = annName eqCon $ text "Refl"

1541− prettySe p bnd (PResolveTC _) = text "resolvetc"

1550+ prettySe p bnd (PResolveTC _) = kwd "%instance"

1542 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"

1551 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"

1543 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"

1552 prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"

1544 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"

1553 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"

@@ -1636,10 +1645,6 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1636 opStr (NS n _) = opStr n

1645 opStr (NS n _) = opStr n

1637 opStr (UN n) = T.unpack n

1646 opStr (UN n) = T.unpack n

1638

1647

1639− basename :: Name -> Name

1640− basename (NS n _) = basename n

1641− basename n = n

1642−

1643 slist' _ _ e

1648 slist' _ _ e

1644 | containsHole e = Nothing

1649 | containsHole e = Nothing

1645 slist' p bnd (PApp _ (PRef _ nil) _)

1650 slist' p bnd (PApp _ (PRef _ nil) _)

@@ -1697,6 +1702,11 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1697 getFixity :: String -> Maybe Fixity

1702 getFixity :: String -> Maybe Fixity

1698 getFixity = flip M.lookup fixities

1703 getFixity = flip M.lookup fixities

1699

1704

1705+-- | Strip away namespace information

1706+basename :: Name -> Name

1707+basename (NS n _) = basename n

1708+basename n = n

1709+

1700-- | Determine whether a name was the one inserted for a hole or

1710-- | Determine whether a name was the one inserted for a hole or

1701-- guess by the delaborator

1711-- guess by the delaborator

1702isHoleName :: Name -> Bool

1712isHoleName :: Name -> Bool

@@ -1850,6 +1860,7 @@ instance Sized PTerm where

1850 size (PApp fc name args) = 1 + size args

1860 size (PApp fc name args) = 1 + size args

1851 size (PAppBind fc name args) = 1 + size args

1861 size (PAppBind fc name args) = 1 + size args

1852 size (PCase fc trm bdy) = 1 + size trm + size bdy

1862 size (PCase fc trm bdy) = 1 + size trm + size bdy

1863+ size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])

1853 size (PTrue fc _) = 1

1864 size (PTrue fc _) = 1

1854 size (PRefl fc _) = 1

1865 size (PRefl fc _) = 1

1855 size (PResolveTC fc) = 1

1866 size (PResolveTC fc) = 1

@@ -1890,6 +1901,7 @@ allNamesIn tm = nub $ ni [] tm

1890 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1901 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1891 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1902 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

1892 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

1903 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

1904+ ni env (PIfThenElse _ c t f) = ni env c ++ ni env t ++ ni env f

1893 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc

1905 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc

1894 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1906 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1895 ni env (PHidden tm) = ni env tm

1907 ni env (PHidden tm) = ni env tm

@@ -1916,6 +1928,7 @@ boundNamesIn tm = S.toList (ni S.empty tm)

1916 ni set (PApp _ f as) = niTms (ni set f) (map getTm as)

1928 ni set (PApp _ f as) = niTms (ni set f) (map getTm as)

1917 ni set (PAppBind _ f as) = niTms (ni set f) (map getTm as)

1929 ni set (PAppBind _ f as) = niTms (ni set f) (map getTm as)

1918 ni set (PCase _ c os) = niTms (ni set c) (map snd os)

1930 ni set (PCase _ c os) = niTms (ni set c) (map snd os)

1931+ ni set (PIfThenElse _ c t f) = niTms set [c, t, f]

1919 ni set (PLam fc n ty sc) = S.insert n $ ni (ni set ty) sc

1932 ni set (PLam fc n ty sc) = S.insert n $ ni (ni set ty) sc

1920 ni set (PLet fc n ty val sc) = S.insert n $ ni (ni (ni set ty) val) sc

1933 ni set (PLet fc n ty val sc) = S.insert n $ ni (ni (ni set ty) val) sc

1921 ni set (PPi p n ty sc) = niTacImp (S.insert n $ ni (ni set ty) sc) p

1934 ni set (PPi p n ty sc) = niTacImp (S.insert n $ ni (ni set ty) sc) p

@@ -1956,6 +1969,7 @@ implicitNamesIn uvars ist tm = nub $ ni [] tm

1956 -- names in 'os', not counting the names bound in the cases

1969 -- names in 'os', not counting the names bound in the cases

1957 (nub (concatMap (ni env) (map snd os))

1970 (nub (concatMap (ni env) (map snd os))

1958 \\ nub (concatMap (ni env) (map fst os)))

1971 \\ nub (concatMap (ni env) (map fst os)))

1972+ ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]

1959 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc

1973 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc

1960 ni env (PPi p n ty sc) = ni env ty ++ ni (n:env) sc

1974 ni env (PPi p n ty sc) = ni env ty ++ ni (n:env) sc

1961 ni env (PEq _ _ _ l r) = ni env l ++ ni env r

1975 ni env (PEq _ _ _ l r) = ni env l ++ ni env r

@@ -1986,6 +2000,7 @@ namesIn uvars ist tm = nub $ ni [] tm

1986 -- names in 'os', not counting the names bound in the cases

2000 -- names in 'os', not counting the names bound in the cases

1987 (nub (concatMap (ni env) (map snd os))

2001 (nub (concatMap (ni env) (map snd os))

1988 \\ nub (concatMap (ni env) (map fst os)))

2002 \\ nub (concatMap (ni env) (map fst os)))

2003+ ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]

1989 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc

2004 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc

1990 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

2005 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

1991 ni env (PEq _ _ _ l r) = ni env l ++ ni env r

2006 ni env (PEq _ _ _ l r) = ni env l ++ ni env r

@@ -2017,6 +2032,7 @@ usedNamesIn vars ist tm = nub $ ni [] tm

2017 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

2032 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

2018 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

2033 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

2019 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

2034 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

2035+ ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]

2020 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc

2036 ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc

2021 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

2037 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

2022 ni env (PEq _ _ _ l r) = ni env l ++ ni env r

2038 ni env (PEq _ _ _ l r) = ni env l ++ ni env r

src/Idris/DSL.hs+43−37

@@ -24,7 +24,7 @@ dslify syn i = transform dslifyApp

24 dslifyApp t = t

25

26desugar :: SyntaxInfo -> IState -> PTerm -> PTerm

27−desugar syn i t = let t' = expandDo (dsl_info syn) t

27+desugar syn i t = let t' = expandSugar (dsl_info syn) t

28 in dslify syn i t'

29

30mkTTName :: FC -> Name -> PTerm

@@ -44,50 +44,56 @@ mkTTName fc n =

44 , pexp (stringC nm)]

45 otherwise -> PRef fc $ reflm "NErased"

46

47−expandDo :: DSL -> PTerm -> PTerm

47+expandSugar :: DSL -> PTerm -> PTerm

48−expandDo dsl (PLam fc n ty tm)

48+expandSugar dsl (PLam fc n ty tm)

49 | Just lam <- dsl_lambda dsl

50 = let sc = PApp fc lam [ pexp (mkTTName fc n)

51 , pexp (var dsl n tm 0)]

52− in expandDo dsl sc

52+ in expandSugar dsl sc

53−expandDo dsl (PLam fc n ty tm) = PLam fc n (expandDo dsl ty) (expandDo dsl tm)

53+expandSugar dsl (PLam fc n ty tm) = PLam fc n (expandSugar dsl ty) (expandSugar dsl tm)

54−expandDo dsl (PLet fc n ty v tm)

54+expandSugar dsl (PLet fc n ty v tm)

55 | Just letb <- dsl_let dsl

56 = let sc = PApp (fileFC "(dsl)") letb [ pexp (mkTTName fc n)

57 , pexp v

58 , pexp (var dsl n tm 0)]

59− in expandDo dsl sc

59+ in expandSugar dsl sc

60−expandDo dsl (PLet fc n ty v tm) = PLet fc n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)

60+expandSugar dsl (PLet fc n ty v tm) = PLet fc n (expandSugar dsl ty) (expandSugar dsl v) (expandSugar dsl tm)

61−expandDo dsl (PPi p n ty tm)

61+expandSugar dsl (PPi p n ty tm)

62 | Just pi <- dsl_pi dsl

63 = let sc = PApp (fileFC "(dsl)") pi [ pexp (mkTTName (fileFC "(dsl)") n)

64 , pexp ty

65 , pexp (var dsl n tm 0)]

66− in expandDo dsl sc

66+ in expandSugar dsl sc

67−expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)

67+expandSugar dsl (PPi p n ty tm) = PPi p n (expandSugar dsl ty) (expandSugar dsl tm)

68−expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)

68+expandSugar dsl (PApp fc t args) = PApp fc (expandSugar dsl t)

69− (map (fmap (expandDo dsl)) args)

69+ (map (fmap (expandSugar dsl)) args)

70−expandDo dsl (PAppBind fc t args) = PAppBind fc (expandDo dsl t)

70+expandSugar dsl (PAppBind fc t args) = PAppBind fc (expandSugar dsl t)

71− (map (fmap (expandDo dsl)) args)

71+ (map (fmap (expandSugar dsl)) args)

72−expandDo dsl (PCase fc s opts) = PCase fc (expandDo dsl s)

72+expandSugar dsl (PCase fc s opts) = PCase fc (expandSugar dsl s)

73− (map (pmap (expandDo dsl)) opts)

73+ (map (pmap (expandSugar dsl)) opts)

74+expandSugar dsl (PIfThenElse fc c t f) =

75+ PApp fc (PRef (FC (fc_fname fc) (fc_start fc) (fc_start fc)) (sUN "ifThenElse"))

76+ [ PExp 0 [] (sMN 0 "condition") $ expandSugar dsl c

77+ , PExp 0 [] (sMN 0 "whenTrue") $ expandSugar dsl t

78+ , PExp 0 [] (sMN 0 "whenFalse") $ expandSugar dsl f

79+ ]

74−expandDo dsl (PEq fc lt rt l r) = PEq fc (expandDo dsl lt) (expandDo dsl rt)

80+expandSugar dsl (PEq fc lt rt l r) = PEq fc (expandSugar dsl lt) (expandSugar dsl rt)

75− (expandDo dsl l) (expandDo dsl r)

81+ (expandSugar dsl l) (expandSugar dsl r)

76−expandDo dsl (PPair fc p l r) = PPair fc p (expandDo dsl l) (expandDo dsl r)

82+expandSugar dsl (PPair fc p l r) = PPair fc p (expandSugar dsl l) (expandSugar dsl r)

77−expandDo dsl (PDPair fc p l t r) = PDPair fc p (expandDo dsl l) (expandDo dsl t)

83+expandSugar dsl (PDPair fc p l t r) = PDPair fc p (expandSugar dsl l) (expandSugar dsl t)

78− (expandDo dsl r)

84+ (expandSugar dsl r)

79−expandDo dsl (PAlternative a as) = PAlternative a (map (expandDo dsl) as)

85+expandSugar dsl (PAlternative a as) = PAlternative a (map (expandSugar dsl) as)

80−expandDo dsl (PHidden t) = PHidden (expandDo dsl t)

86+expandSugar dsl (PHidden t) = PHidden (expandSugar dsl t)

81−expandDo dsl (PNoImplicits t) = PNoImplicits (expandDo dsl t)

87+expandSugar dsl (PNoImplicits t) = PNoImplicits (expandSugar dsl t)

82−expandDo dsl (PUnifyLog t) = PUnifyLog (expandDo dsl t)

88+expandSugar dsl (PUnifyLog t) = PUnifyLog (expandSugar dsl t)

83−expandDo dsl (PDisamb ns t) = PDisamb ns (expandDo dsl t)

89+expandSugar dsl (PDisamb ns t) = PDisamb ns (expandSugar dsl t)

84−expandDo dsl (PReturn fc) = dsl_return dsl

90+expandSugar dsl (PReturn fc) = dsl_return dsl

85−expandDo dsl (PRewrite fc r t ty)

91+expandSugar dsl (PRewrite fc r t ty)

86− = PRewrite fc r (expandDo dsl t) ty

92+ = PRewrite fc r (expandSugar dsl t) ty

87−expandDo dsl (PGoal fc r n sc)

93+expandSugar dsl (PGoal fc r n sc)

88− = PGoal fc (expandDo dsl r) n (expandDo dsl sc)

94+ = PGoal fc (expandSugar dsl r) n (expandSugar dsl sc)

89−expandDo dsl (PDoBlock ds)

95+expandSugar dsl (PDoBlock ds)

90− = expandDo dsl $ debind (dsl_bind dsl) (block (dsl_bind dsl) ds)

96+ = expandSugar dsl $ debind (dsl_bind dsl) (block (dsl_bind dsl) ds)

91 where

97 where

92 block b [DoExp fc tm] = tm

98 block b [DoExp fc tm] = tm

93 block b [a] = PElabError (Msg "Last statement in do block must be an expression")

99 block b [a] = PElabError (Msg "Last statement in do block must be an expression")

@@ -107,9 +113,9 @@ expandDo dsl (PDoBlock ds)

107 pexp (PLam fc (sMN 0 "bindx") Placeholder (block b rest))]

113 pexp (PLam fc (sMN 0 "bindx") Placeholder (block b rest))]

108 block b _ = PElabError (Msg "Invalid statement in do block")

114 block b _ = PElabError (Msg "Invalid statement in do block")

109

115

110−expandDo dsl (PIdiom fc e) = expandDo dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e

116+expandSugar dsl (PIdiom fc e) = expandSugar dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e

111−expandDo dsl (PRunElab fc tm) = PRunElab fc $ expandDo dsl tm

117+expandSugar dsl (PRunElab fc tm) = PRunElab fc $ expandSugar dsl tm

112−expandDo dsl t = t

118+expandSugar dsl t = t

113

119

114-- | Replace DSL-bound variable in a term

120-- | Replace DSL-bound variable in a term

115var :: DSL -> Name -> PTerm -> Int -> PTerm

121var :: DSL -> Name -> PTerm -> Int -> PTerm

src/Idris/DeepSeq.hs+1

@@ -211,6 +211,7 @@ instance NFData PTerm where

211 rnf (PAppBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

212 rnf (PMatchApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

213 rnf (PCase x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

214+ rnf (PIfThenElse x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

214 rnf (PTrue x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

215 rnf (PTrue x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

215 rnf (PRefl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

216 rnf (PRefl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

216 rnf (PResolveTC x1) = rnf x1 `seq` ()

217 rnf (PResolveTC x1) = rnf x1 `seq` ()

src/Idris/Delaborate.hs+13−1

@@ -15,6 +15,7 @@ import Idris.ErrReverse

15

16import Prelude hiding ((<$>))

17

18+import Data.Maybe (mapMaybe)

18import Data.List (intersperse, nub)

19import Data.List (intersperse, nub)

19import qualified Data.Text as T

20import qualified Data.Text as T

20import Control.Monad.State

21import Control.Monad.State

@@ -49,7 +50,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

49 where

50 where

50 un = fileFC "(val)"

51 un = fileFC "(val)"

51

52

52− de env _ (App _ f a) = deFn env f [a]

53+ de env _ (App _ f a) = resugarApp env $ deFn env f [a]

53 de env _ (V i) | i < length env = PRef un (snd (env!!i))

54 de env _ (V i) | i < length env = PRef un (snd (env!!i))

54 | otherwise = PRef un (sUN ("v" ++ show i ++ ""))

55 | otherwise = PRef un (sUN ("v" ++ show i ++ ""))

55 de env _ (P _ n _) | n == unitTy = PTrue un IsType

56 de env _ (P _ n _) | n == unitTy = PTrue un IsType

@@ -149,6 +150,17 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

149 isCN (SN (CaseN _)) = True

150 isCN (SN (CaseN _)) = True

150 isCN _ = False

151 isCN _ = False

151

152

153+ resugarApp env (PApp _ (PRef _ n) args)

154+ | [c, t, f] <- mapMaybe explicitTerm args

155+ , basename n == sUN "ifThenElse"

156+ = PIfThenElse un c (dedelay t) (dedelay f)

157+ where dedelay (PApp _ (PRef _ delay) [_, _, obj])

158+ | delay == sUN "Delay" = getTm obj

159+ dedelay x = x

160+ explicitTerm (PExp {getTm = tm}) = Just tm

161+ explicitTerm _ = Nothing

162+ resugarApp env tm = tm

163+

152 delabCase :: [(Name, Name)] -> [PArg] -> Name -> Term -> Name -> [Term] -> Maybe PTerm

164 delabCase :: [(Name, Name)] -> [PArg] -> Name -> Term -> Name -> [Term] -> Maybe PTerm

153 delabCase env imps scvar scrutinee caseName caseArgs =

165 delabCase env imps scvar scrutinee caseName caseArgs =

154 do cases <- case lookupCtxt caseName (idris_patdefs ist) of

166 do cases <- case lookupCtxt caseName (idris_patdefs ist) of

src/Idris/ElabQuasiquote.hs+6−1

@@ -37,7 +37,7 @@ extractTUnquotes n (GoalType s tac)

37extractTUnquotes n (TCheck t) = extract1 n TCheck t

38extractTUnquotes n (TEval t) = extract1 n TEval t

39extractTUnquotes n (Claim name t) = extract1 n (Claim name) t

40−extractTUnquotes n tac = return (tac, []) -- the rest don't contain PTerms

40+extractTUnquotes n tac = return (tac, []) -- the rest don't contain PTerms, or have been desugared away

41

42extractPArgUnquotes :: Int -> PArg -> Elab' aux (PArg, [(Name, PTerm)])

43extractPArgUnquotes d (PImp p m opts n t) =

@@ -104,6 +104,11 @@ extractUnquotes n (PCase fc expr cases)

104 (pats', exs1) <- fmap unzip $ mapM (extractUnquotes n) pats

105 (rhss', exs2) <- fmap unzip $ mapM (extractUnquotes n) rhss

106 return (PCase fc expr' (zip pats' rhss'), ex1 ++ concat exs1 ++ concat exs2)

107+extractUnquotes n (PIfThenElse fc c t f)

108+ = do (c', ex1) <- extractUnquotes n c

109+ (t', ex2) <- extractUnquotes n t

110+ (f', ex3) <- extractUnquotes n f

111+ return (PIfThenElse fc c' t' f', ex1 ++ ex2 ++ ex3)

107extractUnquotes n (PRefl fc x)

112extractUnquotes n (PRefl fc x)

108 = do (x', ex) <- extractUnquotes n x

113 = do (x', ex) <- extractUnquotes n x

109 return (PRefl fc x', ex)

114 return (PRefl fc x', ex)

src/Idris/Error.hs+1

@@ -102,6 +102,7 @@ warnDisamb ist (PAppBind _ f args) = warnDisamb ist f >>

102warnDisamb ist (PMatchApp _ _) = return ()

103warnDisamb ist (PCase _ tm cases) = warnDisamb ist tm >>

104 mapM_ (\(x,y)-> warnDisamb ist x >> warnDisamb ist y) cases

105+warnDisamb ist (PIfThenElse _ c t f) = mapM_ (warnDisamb ist) [c, t, f]

105warnDisamb ist (PTrue _ _) = return ()

106warnDisamb ist (PTrue _ _) = return ()

106warnDisamb ist (PRefl _ tm) = warnDisamb ist tm

107warnDisamb ist (PRefl _ tm) = warnDisamb ist tm

107warnDisamb ist (PResolveTC _) = return ()

108warnDisamb ist (PResolveTC _) = return ()

src/Idris/IBC.hs+10−1

@@ -1616,7 +1616,11 @@ instance Binary PTerm where

1616 put x1

1617 PQuoteName x1 -> do putWord8 44

1618 put x1

1619−

1619+ PIfThenElse x1 x2 x3 x4 -> do putWord8 45

1620+ put x1

1621+ put x2

1622+ put x3

1623+ put x4

1620

1624

1621 get

1625 get

1622 = do i <- getWord8

1626 = do i <- getWord8

@@ -1751,6 +1755,11 @@ instance Binary PTerm where

1751 return (PUnquote x1)

1755 return (PUnquote x1)

1752 44 -> do x1 <- get

1756 44 -> do x1 <- get

1753 return (PQuoteName x1)

1757 return (PQuoteName x1)

1758+ 45 -> do x1 <- get

1759+ x2 <- get

1760+ x3 <- get

1761+ x4 <- get

1762+ return (PIfThenElse x1 x2 x3 x4)

1754 _ -> error "Corrupted binary data for PTerm"

1763 _ -> error "Corrupted binary data for PTerm"

1755

1764

1756instance (Binary t) => Binary (PTactic' t) where

1765instance (Binary t) => Binary (PTactic' t) where

src/Idris/IdrisDoc.hs+1

@@ -302,6 +302,7 @@ extractPTermNames (PAppBind _ p pas) = let names = concatMap extractPArg pas

302extractPTermNames (PMatchApp _ n) = [n]

303extractPTermNames (PCase _ p ps) = let (ps1, ps2) = unzip ps

304 in concatMap extract (p:(ps1 ++ ps2))

305+extractPTermNames (PIfThenElse _ c t f) = concatMap extract [c, t, f]

305extractPTermNames (PRefl _ p) = extract p

306extractPTermNames (PRefl _ p) = extract p

306extractPTermNames (PEq _ _ _ p1 p2) = concatMap extract [p1, p2]

307extractPTermNames (PEq _ _ _ p1 p2) = concatMap extract [p1, p2]

307extractPTermNames (PRewrite _ a b m) | Just c <- m =

308extractPTermNames (PRewrite _ a b m) | Just c <- m =

src/Idris/ParseExpr.hs+23−2

@@ -178,6 +178,8 @@ extension syn ns rules =

178 = PAppBind fc (update ns t) (map (fmap (update ns)) args)

179 update ns (PCase fc c opts)

180 = PCase fc (update ns c) (map (pmap (update ns)) opts)

181+ update ns (PIfThenElse fc c t f)

182+ = PIfThenElse fc (update ns c) (update ns t) (update ns f)

181 update ns (PPair fc p l r) = PPair fc p (update ns l) (update ns r)

183 update ns (PPair fc p l r) = PPair fc p (update ns l) (update ns r)

182 update ns (PDPair fc p l t r)

184 update ns (PDPair fc p l t r)

183 = PDPair fc p (update ns l) (update ns t) (update ns r)

185 = PDPair fc p (update ns l) (update ns t) (update ns r)

@@ -210,6 +212,7 @@ InternalExpr ::=

210 | Lambda

212 | Lambda

211 | QuoteGoal

213 | QuoteGoal

212 | Let

214 | Let

215+ | If

213 | RewriteTerm

216 | RewriteTerm

214 | CaseExpr

217 | CaseExpr

215 | DoBlock

218 | DoBlock

@@ -224,6 +227,7 @@ internalExpr syn =

224 <|> disamb syn

227 <|> disamb syn

225 <|> noImplicits syn

228 <|> noImplicits syn

226 <|> recordType syn

229 <|> recordType syn

230+ <|> if_ syn

227 <|> lambda syn

231 <|> lambda syn

228 <|> quoteGoal syn

232 <|> quoteGoal syn

229 <|> let_ syn

233 <|> let_ syn

@@ -673,7 +677,7 @@ FieldType ::=

673@

677@

674-}

678-}

675recordType :: SyntaxInfo -> IdrisParser PTerm

679recordType :: SyntaxInfo -> IdrisParser PTerm

676−recordType syn =

680+recordType syn =

677 do reserved "record"

681 do reserved "record"

678 lchar '{'

682 lchar '{'

679 fgs <- fieldGetOrSet

683 fgs <- fieldGetOrSet

@@ -842,7 +846,24 @@ let_binding syn = do fc <- getFC;

842 ts <- option [] (do lchar '|'

846 ts <- option [] (do lchar '|'

843 sepBy1 (do_alt syn) (lchar '|'))

847 sepBy1 (do_alt syn) (lchar '|'))

844 return (fc,pat,ty,v,ts)

848 return (fc,pat,ty,v,ts)

845−

849+

850+{- | Parses a conditional expression

851+@

852+If ::= 'if' Expr 'then' Expr 'else' Expr

853+@

854+

855+-}

856+if_ :: SyntaxInfo -> IdrisParser PTerm

857+if_ syn = (do reserved "if"

858+ fc <- getFC

859+ c <- expr syn

860+ reserved "then"

861+ t <- expr syn

862+ reserved "else"

863+ f <- expr syn

864+ return (PIfThenElse fc c t f))

865+ <?> "conditional expression"

866+

846

867

847{- | Parses a quote goal

868{- | Parses a quote goal

848

869

src/Idris/ParseHelpers.hs+1−1

@@ -231,7 +231,7 @@ idrisStyle = IdentifierStyle _styleName _styleStart _styleLetter _styleReserved

231 "where", "with", "syntax", "proof", "postulate",

232 "using", "namespace", "class", "instance", "parameters",

233 "public", "private", "abstract", "implicit",

234− "quoteGoal"]

234+ "quoteGoal", "if", "then", "else"]

235

236char :: MonadicParsing m => Char -> m Char

237char = Chr.char

test/dsl002/test014.idr+2−2

@@ -11,7 +11,7 @@ pstring Writing = "w"

11data FILE : Purpose -> Type where

12 OpenH : File -> FILE p

13

14−syntax ifM [test] then [t] else [e]

14+syntax "ifM" [test] "then" [t] "else" [e]

15 = test >>= (\b => if b then t else e)

16

17open : String -> (p:Purpose) -> Creator (Either () (FILE p))

@@ -35,7 +35,7 @@ syntax reof [h] = Use eof h

35

36syntax rputStrLn [s] = Lift (putStrLn s)

37

38−syntax if opened [f] then [e] else [t] = Check f t e

38+syntax "if" "opened" [f] "then" [e] "else" [t] = Check f t e

39

40

41

test/effects003/foo+8−8

@@ -1,10 +1,10 @@

1(constructor of Default.Default,[Main.Hangman Main.NotRunning,Default.Hangman NotRunning instance of Default.Default, method default],[],[[PImp {priority = 1, machine_inf = True, argopts = [], pname = a, getTm = Type},PExp {priority = 1, argopts = [], pname = default, getTm = a}]])

2(constructor of Default.Default,[Main.Hangman Main.NotRunning],[],[[PImp {priority = 1, machine_inf = True, argopts = [], pname = a, getTm = Type},PExp {priority = 1, argopts = [], pname = default, getTm = a}]])

3(Main.Hangman,[Main.NotRunning],[],[[PExp {priority = 1, argopts = [], pname = __pi_arg, getTm = HState}]])

4−(Prelude.Bool.boolElim,[Char,Prelude.Bool.|| (Prelude.Bool.not (Prelude.Char.isAlpha c)) (Delay LazyEval Prelude.Bool.Bool (PE_elem_f54 c got)),Delay LazyEval Char c,Delay LazyEval Char '-'],[[False,False,False,False]],[[PImp {priority = 1, machine_inf = True, argopts = [], pname = a, getTm = _},PExp {priority = 1, argopts = [], pname = b, getTm = Bool},PExp {priority = 1, argopts = [], pname = t, getTm = Lazy a},PExp {priority = 1, argopts = [], pname = e, getTm = Lazy a}]])

4+(Prelude.Bool.ifThenElse,[Char,Prelude.Bool.|| (Prelude.Bool.not (Prelude.Char.isAlpha c)) (Delay LazyEval Prelude.Bool.Bool (PE_elem_f54 c got)),Delay LazyEval Char c,Delay LazyEval Char '-'],[[False,False,False,False]],[[PImp {priority = 1, machine_inf = True, argopts = [], pname = a, getTm = _},PExp {priority = 1, argopts = [], pname = b, getTm = Bool},PExp {priority = 1, argopts = [], pname = t, getTm = Lazy a},PExp {priority = 1, argopts = [], pname = e, getTm = Lazy a}]])

5−(Prelude.Bool.boolElim,[Char,Prelude.Bool.|| (Prelude.Bool.not (Prelude.Char.isAlpha c)) (Delay LazyEval Prelude.Bool.Bool (PE_elem_f54 c got)),Delay LazyEval Char c],[[False,False,False,False]],[[PImp {priority = 1, machine_inf = True, argopts = [], pname = a, getTm = _},PExp {priority = 1, argopts = [], pname = b, getTm = Bool},PExp {priority = 1, argopts = [], pname = t, getTm = Lazy a},PExp {priority = 1, argopts = [], pname = e, getTm = Lazy a}]])

5+(Prelude.Bool.ifThenElse,[Char,Prelude.Bool.|| (Prelude.Bool.not (Prelude.Char.isAlpha c)) (Delay LazyEval Prelude.Bool.Bool (PE_elem_f54 c got)),Delay LazyEval Char c],[[False,False,False,False]],[[PImp {priority = 1, machine_inf = True, argopts = [], pname = a, getTm = _},PExp {priority = 1, argopts = [], pname = b, getTm = Bool},PExp {priority = 1, argopts = [], pname = t, getTm = Lazy a},PExp {priority = 1, argopts = [], pname = e, getTm = Lazy a}]])

6−(Prelude.Bool.boolElim,[Char,Prelude.Bool.|| (Prelude.Bool.not (Prelude.Char.isAlpha c)) (Delay LazyEval Prelude.Bool.Bool (PE_elem_f54 c got))],[[False,False,False,False]],[[PImp {priority = 1, machine_inf = True, argopts = [], pname = a, getTm = _},PExp {priority = 1, argopts = [], pname = b, getTm = Bool},PExp {priority = 1, argopts = [], pname = t, getTm = Lazy a},PExp {priority = 1, argopts = [], pname = e, getTm = Lazy a}]])

6+(Prelude.Bool.ifThenElse,[Char,Prelude.Bool.|| (Prelude.Bool.not (Prelude.Char.isAlpha c)) (Delay LazyEval Prelude.Bool.Bool (PE_elem_f54 c got))],[[False,False,False,False]],[[PImp {priority = 1, machine_inf = True, argopts = [], pname = a, getTm = _},PExp {priority = 1, argopts = [], pname = b, getTm = Bool},PExp {priority = 1, argopts = [], pname = t, getTm = Lazy a},PExp {priority = 1, argopts = [], pname = e, getTm = Lazy a}]])

7−(Prelude.Bool.boolElim,[Char],[[False,False,False,False]],[[PImp {priority = 1, machine_inf = True, argopts = [], pname = a, getTm = _},PExp {priority = 1, argopts = [], pname = b, getTm = Bool},PExp {priority = 1, argopts = [], pname = t, getTm = Lazy a},PExp {priority = 1, argopts = [], pname = e, getTm = Lazy a}]])

7+(Prelude.Bool.ifThenElse,[Char],[[False,False,False,False]],[[PImp {priority = 1, machine_inf = True, argopts = [], pname = a, getTm = _},PExp {priority = 1, argopts = [], pname = b, getTm = Bool},PExp {priority = 1, argopts = [], pname = t, getTm = Lazy a},PExp {priority = 1, argopts = [], pname = e, getTm = Lazy a}]])

8(Prelude.Bool.||,[Prelude.Bool.not (Prelude.Char.isAlpha c),Delay LazyEval Prelude.Bool.Bool (PE_elem_f54 c got)],[[False,False]],[[PExp {priority = 1, argopts = [], pname = __pi_arg, getTm = Bool},PExp {priority = 1, argopts = [], pname = __pi_arg1, getTm = Lazy Bool}]])

9(Prelude.Bool.||,[Prelude.Bool.not (Prelude.Char.isAlpha c)],[[False,False]],[[PExp {priority = 1, argopts = [], pname = __pi_arg, getTm = Bool},PExp {priority = 1, argopts = [], pname = __pi_arg1, getTm = Lazy Bool}]])

10(Prelude.Bool.not,[Prelude.Char.isAlpha c],[[False]],[[PExp {priority = 1, argopts = [], pname = __pi_arg, getTm = Bool}]])

@@ -56,10 +56,10 @@

56(assert_total,[Prelude.List.List Char,Main.letters xs],[[False,False]],[[PImp {priority = 1, machine_inf = True, argopts = [], pname = a, getTm = _},PExp {priority = 1, argopts = [], pname = __pi_arg, getTm = a}]])

57(assert_total,[Prelude.List.List Char],[[False,False]],[[PImp {priority = 1, machine_inf = True, argopts = [], pname = a, getTm = _},PExp {priority = 1, argopts = [], pname = __pi_arg, getTm = a}]])

58(Prelude.List.List,[Char],[],[[PExp {priority = 1, argopts = [], pname = {_t0}, getTm = Type}]])

59−(Prelude.Bool.boolElim,[Prelude.List.List Char,Prelude.Bool.|| (Prelude.Bool.not (Prelude.Char.isAlpha y)) (Delay LazyEval Prelude.Bool.Bool (PE_elem_f54 y xs')),Delay LazyEval (Prelude.List.List Char) xs',Delay LazyEval (Prelude.List.List Char) (Prelude.List.:: Char y xs')],[[False,False,False,False]],[[PImp {priority = 1, machine_inf = True, argopts = [], pname = a, getTm = _},PExp {priority = 1, argopts = [], pname = b, getTm = Bool},PExp {priority = 1, argopts = [], pname = t, getTm = Lazy a},PExp {priority = 1, argopts = [], pname = e, getTm = Lazy a}]])

59+(Prelude.Bool.ifThenElse,[Prelude.List.List Char,Prelude.Bool.|| (Prelude.Bool.not (Prelude.Char.isAlpha y)) (Delay LazyEval Prelude.Bool.Bool (PE_elem_f54 y xs')),Delay LazyEval (Prelude.List.List Char) xs',Delay LazyEval (Prelude.List.List Char) (Prelude.List.:: Char y xs')],[[False,False,False,False]],[[PImp {priority = 1, machine_inf = True, argopts = [], pname = a, getTm = _},PExp {priority = 1, argopts = [], pname = b, getTm = Bool},PExp {priority = 1, argopts = [], pname = t, getTm = Lazy a},PExp {priority = 1, argopts = [], pname = e, getTm = Lazy a}]])

60−(Prelude.Bool.boolElim,[Prelude.List.List Char,Prelude.Bool.|| (Prelude.Bool.not (Prelude.Char.isAlpha y)) (Delay LazyEval Prelude.Bool.Bool (PE_elem_f54 y xs')),Delay LazyEval (Prelude.List.List Char) xs'],[[False,False,False,False]],[[PImp {priority = 1, machine_inf = True, argopts = [], pname = a, getTm = _},PExp {priority = 1, argopts = [], pname = b, getTm = Bool},PExp {priority = 1, argopts = [], pname = t, getTm = Lazy a},PExp {priority = 1, argopts = [], pname = e, getTm = Lazy a}]])

60+(Prelude.Bool.ifThenElse,[Prelude.List.List Char,Prelude.Bool.|| (Prelude.Bool.not (Prelude.Char.isAlpha y)) (Delay LazyEval Prelude.Bool.Bool (PE_elem_f54 y xs')),Delay LazyEval (Prelude.List.List Char) xs'],[[False,False,False,False]],[[PImp {priority = 1, machine_inf = True, argopts = [], pname = a, getTm = _},PExp {priority = 1, argopts = [], pname = b, getTm = Bool},PExp {priority = 1, argopts = [], pname = t, getTm = Lazy a},PExp {priority = 1, argopts = [], pname = e, getTm = Lazy a}]])

61−(Prelude.Bool.boolElim,[Prelude.List.List Char,Prelude.Bool.|| (Prelude.Bool.not (Prelude.Char.isAlpha y)) (Delay LazyEval Prelude.Bool.Bool (PE_elem_f54 y xs'))],[[False,False,False,False]],[[PImp {priority = 1, machine_inf = True, argopts = [], pname = a, getTm = _},PExp {priority = 1, argopts = [], pname = b, getTm = Bool},PExp {priority = 1, argopts = [], pname = t, getTm = Lazy a},PExp {priority = 1, argopts = [], pname = e, getTm = Lazy a}]])

61+(Prelude.Bool.ifThenElse,[Prelude.List.List Char,Prelude.Bool.|| (Prelude.Bool.not (Prelude.Char.isAlpha y)) (Delay LazyEval Prelude.Bool.Bool (PE_elem_f54 y xs'))],[[False,False,False,False]],[[PImp {priority = 1, machine_inf = True, argopts = [], pname = a, getTm = _},PExp {priority = 1, argopts = [], pname = b, getTm = Bool},PExp {priority = 1, argopts = [], pname = t, getTm = Lazy a},PExp {priority = 1, argopts = [], pname = e, getTm = Lazy a}]])

62−(Prelude.Bool.boolElim,[Prelude.List.List Char],[[False,False,False,False]],[[PImp {priority = 1, machine_inf = True, argopts = [], pname = a, getTm = _},PExp {priority = 1, argopts = [], pname = b, getTm = Bool},PExp {priority = 1, argopts = [], pname = t, getTm = Lazy a},PExp {priority = 1, argopts = [], pname = e, getTm = Lazy a}]])

62+(Prelude.Bool.ifThenElse,[Prelude.List.List Char],[[False,False,False,False]],[[PImp {priority = 1, machine_inf = True, argopts = [], pname = a, getTm = _},PExp {priority = 1, argopts = [], pname = b, getTm = Bool},PExp {priority = 1, argopts = [], pname = t, getTm = Lazy a},PExp {priority = 1, argopts = [], pname = e, getTm = Lazy a}]])

63(Prelude.List.List,[Char],[],[[PExp {priority = 1, argopts = [], pname = {_t0}, getTm = Type}]])

64(Prelude.Bool.||,[Prelude.Bool.not (Prelude.Char.isAlpha y),Delay LazyEval Prelude.Bool.Bool (PE_elem_f54 y xs')],[[False,False]],[[PExp {priority = 1, argopts = [], pname = __pi_arg, getTm = Bool},PExp {priority = 1, argopts = [], pname = __pi_arg1, getTm = Lazy Bool}]])

65(Prelude.Bool.||,[Prelude.Bool.not (Prelude.Char.isAlpha y)],[[False,False]],[[PExp {priority = 1, argopts = [], pname = __pi_arg, getTm = Bool},PExp {priority = 1, argopts = [], pname = __pi_arg1, getTm = Lazy Bool}]])

test/reg012/reg012.lidr+1−1

@@ -32,5 +32,5 @@

32> modifyFunLemma f (a,b) =

33> rewrite soTrue (reflexive_eqeq a) in Refl

34

35− replace {P = \ z => boolElim (a == a) b (f a) = boolElim z b (f a)}

35+ replace {P = \ z => ifThenElse (a == a) b (f a) = ifThenElse z b (f a)}

36 (soTrue (reflexive_eqeq a)) Refl

test/totality002/test017.idr+2−2

@@ -93,8 +93,8 @@ maxCommutative (S left) (S right) =

93

94maxCommutativeStepCase = proof {

95 intros;

96− rewrite (boolElimSuccSucc (lte left right) right left);

96+ rewrite (ifThenElseSuccSucc (lte left right) right left);

97− rewrite (boolElimSuccSucc (lte right left) left right);

97+ rewrite (ifThenElseSuccSucc (lte right left) left right);

98 rewrite inductiveHypothesis;

99 trivial;

100}