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

git.iko.soy/Idris-dev

High-level if ... then ... else ... expression

Now, conditionals are implemented by the compiler rather than a library. This gives better error messages and more readable output, at the cost of more Haskell and less Idris. Also, boolElim is renamed to ifThenElse for consistency with other languages that support overloading of conditional expressions (GHC Haskell and scala-virtualized) and to reflect that things other than Booleans will be eliminated by overloadings.

commit90127b39c4d96ccd84908dbf4bbfe5f870c9c63a authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateWed 6 May 2015, 15:44 (11 years ago) parenta129823

21 files changed+190−105

compare with master

unifiedsplit

CHANGELOG+6

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

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

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

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

3945

4046New in 0.9.17:

4147--------------

docs/faq/faq.rst+7−7

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

5959How can I make lazy control structures?

6060=======================================

6161

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

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

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

65+Booleans is defined as follows in the library:

6466

6567.. code-block:: idris

6668

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

68− boolElim True t e = t

69− boolElim False t e = e

70−

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

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

70+ ifThenElse True t e = t

71+ ifThenElse False t e = e

7272

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

7474only 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

1111||| @ b the condition on the if

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

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

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

15−boolElim True t e = t

16−boolElim 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)

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

15+ifThenElse True t e = t

16+ifThenElse False t e = e

2017

2118-- Boolean Operator Precedence

2219infixl 4 &&, ||

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

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

8686 (>=) x y = x > y || x == y

8787

8888 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

9090

9191 min : a -> a -> a

9292 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) =

630630 let inductiveHypothesis = minusSuccPred left right in

631631 ?minusSuccPredStepCase'

632632

633−-- boolElim

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

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

636−boolElimSuccSucc True t f = Refl

637−boolElimSuccSucc False t f = Refl

638−

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

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

641−boolElimPlusPlusLeft True left t f = Refl

642−boolElimPlusPlusLeft False left t f = Refl

643−

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

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

646−boolElimPlusPlusRight True right t f = Refl

647−boolElimPlusPlusRight False right t f = Refl

648−

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

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

651−boolElimMultMultLeft True left t f = Refl

652−boolElimMultMultLeft False left t f = Refl

653−

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

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

656−boolElimMultMultRight True right t f = Refl

657−boolElimMultMultRight False right t f = Refl

633+-- ifThenElse

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

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

636+ifThenElseSuccSucc True t f = Refl

637+ifThenElseSuccSucc False t f = Refl

638+

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

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

641+ifThenElsePlusPlusLeft True left t f = Refl

642+ifThenElsePlusPlusLeft False left t f = Refl

643+

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

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

646+ifThenElsePlusPlusRight True right t f = Refl

647+ifThenElsePlusPlusRight False right t f = Refl

648+

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

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

651+ifThenElseMultMultLeft True left t f = Refl

652+ifThenElseMultMultLeft False left t f = Refl

653+

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

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

656+ifThenElseMultMultRight True right t f = Refl

657+ifThenElseMultMultRight False right t f = Refl

658658

659659-- Orders

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

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

910910

911911maximumSuccSuccStepCase = proof {

912912 intros;

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

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

914914 trivial;

915915}

916916

917917minimumSuccSuccStepCase = proof {

918918 intros;

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

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

920920 trivial;

921921}

922922

src/IRTS/Compiler.hs+3−1

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

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

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

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

302− | be == txt "boolElim"

302+ | be == txt "ifThenElse"

303303 , d == txt "Delay"

304304 , d' == txt "Delay"

305+ , b == txt "Bool"

306+ , p == txt "Prelude"

305307 -> do

306308 x' <- irTerm vs env x

307309 t' <- irTerm vs env t

src/Idris/AbsSyntax.hs+10−2

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

1818import System.IO

1919

2020import Control.Applicative

21+import Control.Monad (liftM3)

2122import Control.Monad.State

2223

2324import Data.List hiding (insert,union)

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

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

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

10131014 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)

10141016 en (PRunElab fc tm) = PRunElab fc (en tm)

10151017 en t = t

10161018

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

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

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

15801582 -- 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)

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

15821587 = case lookupDef n (tt_ctxt ist) of

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

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

18701875toEither (LeftErr e) = Left e

18711876toEither (RightOK ho) = Right ho

18721877

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

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

1875−

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

18771881matchClause = matchClause' False

18781882

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

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

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

20152019 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)

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

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

20182023 (fmap (sm xs) tm)

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

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

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

20432048 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)

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

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

20462052 sm (PTyped x y) = PTyped (sm x) (sm y)

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

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

21262132 return (x', y')) alts

21272133 return $! PCase fc t' alts'

2134+ mkUniq (PIfThenElse fc c t f)

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

21282136 mkUniq (PPair fc p l r)

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

21302138 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

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

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

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

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

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

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

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

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

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

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

857858 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)

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

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

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

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

10131015highestFC (PAppBind fc _ _) = Just fc

10141016highestFC (PMatchApp fc _) = Just fc

10151017highestFC (PCase fc _ _) = Just fc

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

10161019highestFC (PTrue fc _) = Just fc

10171020highestFC (PRefl fc _) = Just fc

10181021highestFC (PResolveTC fc) = Just fc

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

15361539 noNS (NS _ _) = False

15371540 noNS _ = True

15381541

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+ ]

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

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

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

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

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

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

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

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

16361645 opStr (NS n _) = opStr n

16371646 opStr (UN n) = T.unpack n

16381647

1639− basename :: Name -> Name

1640− basename (NS n _) = basename n

1641− basename n = n

1642−

16431648 slist' _ _ e

16441649 | containsHole e = Nothing

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

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

16971702 getFixity :: String -> Maybe Fixity

16981703 getFixity = flip M.lookup fixities

16991704

1705+-- | Strip away namespace information

1706+basename :: Name -> Name

1707+basename (NS n _) = basename n

1708+basename n = n

1709+

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

17011711-- guess by the delaborator

17021712isHoleName :: Name -> Bool

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

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

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

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

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

18531864 size (PTrue fc _) = 1

18541865 size (PRefl fc _) = 1

18551866 size (PResolveTC fc) = 1

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

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

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

18921903 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

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

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

18951907 ni env (PHidden tm) = ni env tm

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

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

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

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

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

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

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

19211934 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

20192034 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]

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

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

20222038 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

2424 dslifyApp t = t

2525

2626desugar :: 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

2828 in dslify syn i t'

2929

3030mkTTName :: FC -> Name -> PTerm

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

4444 , pexp (stringC nm)]

4545 otherwise -> PRef fc $ reflm "NErased"

4646

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

48−expandDo dsl (PLam fc n ty tm)

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

48+expandSugar dsl (PLam fc n ty tm)

4949 | Just lam <- dsl_lambda dsl

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

5151 , pexp (var dsl n tm 0)]

52− in expandDo dsl sc

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

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

52+ in expandSugar dsl sc

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

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

5555 | Just letb <- dsl_let dsl

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

5757 , pexp v

5858 , pexp (var dsl n tm 0)]

59− in expandDo dsl sc

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

61−expandDo dsl (PPi p n ty tm)

59+ in expandSugar dsl sc

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

61+expandSugar dsl (PPi p n ty tm)

6262 | Just pi <- dsl_pi dsl

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

6464 , pexp ty

6565 , pexp (var dsl n tm 0)]

66− in expandDo dsl sc

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

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

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

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

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

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

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

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

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

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

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

78− (expandDo dsl r)

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

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

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

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

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

84−expandDo dsl (PReturn fc) = dsl_return dsl

85−expandDo dsl (PRewrite fc r t ty)

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

87−expandDo dsl (PGoal fc r n sc)

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

89−expandDo dsl (PDoBlock ds)

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

66+ in expandSugar dsl sc

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

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

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

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

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

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

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+ ]

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

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

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

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

84+ (expandSugar dsl r)

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

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

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

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

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

90+expandSugar dsl (PReturn fc) = dsl_return dsl

91+expandSugar dsl (PRewrite fc r t ty)

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

93+expandSugar dsl (PGoal fc r n sc)

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

95+expandSugar dsl (PDoBlock ds)

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

9197 where

9298 block b [DoExp fc tm] = tm

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

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

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

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

109115

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

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

112−expandDo dsl t = t

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

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

118+expandSugar dsl t = t

113119

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

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

src/Idris/DeepSeq.hs+1

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

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

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

213213 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` ()

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

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

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

src/Idris/Delaborate.hs+13−1

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

1515

1616import Prelude hiding ((<$>))

1717

18+import Data.Maybe (mapMaybe)

1819import Data.List (intersperse, nub)

1920import qualified Data.Text as T

2021import Control.Monad.State

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

4950 where

5051 un = fileFC "(val)"

5152

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

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

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

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

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

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

149150 isCN (SN (CaseN _)) = True

150151 isCN _ = False

151152

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+

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

153165 delabCase env imps scvar scrutinee caseName caseArgs =

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

src/Idris/ElabQuasiquote.hs+6−1

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

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

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

3939extractTUnquotes 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

4141

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

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

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

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

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

106106 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)

107112extractUnquotes n (PRefl fc x)

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

109114 return (PRefl fc x', ex)

src/Idris/Error.hs+1

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

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

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

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

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

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

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

107108warnDisamb ist (PResolveTC _) = return ()

src/Idris/IBC.hs+10−1

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

16161616 put x1

16171617 PQuoteName x1 -> do putWord8 44

16181618 put x1

1619−

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

1620+ put x1

1621+ put x2

1622+ put x3

1623+ put x4

16201624

16211625 get

16221626 = do i <- getWord8

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

17511755 return (PUnquote x1)

17521756 44 -> do x1 <- get

17531757 return (PQuoteName x1)

1758+ 45 -> do x1 <- get

1759+ x2 <- get

1760+ x3 <- get

1761+ x4 <- get

1762+ return (PIfThenElse x1 x2 x3 x4)

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

17551764

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

src/Idris/IdrisDoc.hs+1

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

302302extractPTermNames (PMatchApp _ n) = [n]

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

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

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

305306extractPTermNames (PRefl _ p) = extract p

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

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

src/Idris/ParseExpr.hs+23−2

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

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

179179 update ns (PCase fc c opts)

180180 = 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)

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

182184 update ns (PDPair fc p l t r)

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

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

210212 | Lambda

211213 | QuoteGoal

212214 | Let

215+ | If

213216 | RewriteTerm

214217 | CaseExpr

215218 | DoBlock

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

224227 <|> disamb syn

225228 <|> noImplicits syn

226229 <|> recordType syn

230+ <|> if_ syn

227231 <|> lambda syn

228232 <|> quoteGoal syn

229233 <|> let_ syn

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

673677@

674678-}

675679recordType :: SyntaxInfo -> IdrisParser PTerm

676−recordType syn =

680+recordType syn =

677681 do reserved "record"

678682 lchar '{'

679683 fgs <- fieldGetOrSet

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

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

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

844848 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+

846867

847868{- | Parses a quote goal

848869

src/Idris/ParseHelpers.hs+1−1

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

231231 "where", "with", "syntax", "proof", "postulate",

232232 "using", "namespace", "class", "instance", "parameters",

233233 "public", "private", "abstract", "implicit",

234− "quoteGoal"]

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

235235

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

237237char = Chr.char

test/dsl002/test014.idr+2−2

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

1111data FILE : Purpose -> Type where

1212 OpenH : File -> FILE p

1313

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

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

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

1616

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

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

3535

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

3737

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

3939

4040

4141

test/effects003/foo+8−8

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

11(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}]])

22(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}]])

33(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}]])

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}]])

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}]])

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}]])

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.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.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.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}]])

88(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}]])

99(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}]])

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

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

5656(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}]])

5757(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}]])

5858(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}]])

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}]])

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}]])

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}]])

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.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.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.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}]])

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

6464(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}]])

6565(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 @@

3232> modifyFunLemma f (a,b) =

3333> rewrite soTrue (reflexive_eqeq a) in Refl

3434

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)}

3636 (soTrue (reflexive_eqeq a)) Refl

test/totality002/test017.idr+2−2

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

9393

9494maxCommutativeStepCase = proof {

9595 intros;

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

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

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

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

9898 rewrite inductiveHypothesis;

9999 trivial;

100100}