375c986 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #2236 from david-christiansen/if-overloading

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

commit375c9863bfb05b8f8aff03da1f58d5bab5877842 authorDavid Christiansen <david@davidchristiansen.dk> dateWed 6 May 2015, 18:21 (11 years ago) parenta129823 90127b3

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}