c538c34 · 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/IO.idr+9−8

@@ -161,14 +161,15 @@ run__provider (MkIO f) = f (TheWorld prim__TheWorld)

161prim_fork : PrimIO () -> PrimIO Ptr

162prim_fork x = prim_io_return prim__vm -- compiled specially

163

164+namespace IO

164−fork : IO' l () -> IO' l Ptr

165+ fork : IO' l () -> IO' l Ptr

165−fork (MkIO f) = MkIO (\w => prim_io_bind

166+ fork (MkIO f) = MkIO (\w => prim_io_bind

166− (prim_fork (prim_io_bind (f w)

167+ (prim_fork (prim_io_bind (f w)

167− (\ x => prim_io_return x)))

168+ (\ x => prim_io_return x)))

168− (\x => prim_io_return x))

169+ (\x => prim_io_return x))

169−

170+

170−forceGC : IO ()

171+ forceGC : IO ()

171−forceGC = foreign FFI_C "idris_forceGC" (Ptr -> IO ()) prim__vm

172+ forceGC = foreign FFI_C "idris_forceGC" (Ptr -> IO ()) prim__vm

172

173

173--------- The Javascript/Node FFI

174--------- The Javascript/Node FFI

174

175

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

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

632 let inductiveHypothesis = minusSuccPred left right in

633 ?minusSuccPredStepCase'

634

635−-- boolElim

635+-- ifThenElse

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

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

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

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

638−boolElimSuccSucc True t f = Refl

638+ifThenElseSuccSucc True t f = Refl

639−boolElimSuccSucc False t f = Refl

639+ifThenElseSuccSucc False t f = Refl

640−

640+

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

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

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

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

643−boolElimPlusPlusLeft True left t f = Refl

643+ifThenElsePlusPlusLeft True left t f = Refl

644−boolElimPlusPlusLeft False left t f = Refl

644+ifThenElsePlusPlusLeft False left t f = Refl

645−

645+

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

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

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

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

648−boolElimPlusPlusRight True right t f = Refl

648+ifThenElsePlusPlusRight True right t f = Refl

649−boolElimPlusPlusRight False right t f = Refl

649+ifThenElsePlusPlusRight False right t f = Refl

650−

650+

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

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

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

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

653−boolElimMultMultLeft True left t f = Refl

653+ifThenElseMultMultLeft True left t f = Refl

654−boolElimMultMultLeft False left t f = Refl

654+ifThenElseMultMultLeft False left t f = Refl

655−

655+

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

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

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

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

658−boolElimMultMultRight True right t f = Refl

658+ifThenElseMultMultRight True right t f = Refl

659−boolElimMultMultRight False right t f = Refl

659+ifThenElseMultMultRight False right t f = Refl

660

661-- Orders

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

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

912

913maximumSuccSuccStepCase = proof {

914 intros;

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

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

916 trivial;

917}

918

919minimumSuccSuccStepCase = proof {

920 intros;

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

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

922 trivial;

923}

924

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

@@ -1573,6 +1575,9 @@ addImpl' inpat env infns imp_meths ist ptm

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

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

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

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

1575 -- be lifted anyway!)

1577 -- be lifted anyway!)

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

1579+ (ai qq env ds t)

1580+ (ai qq env ds f)

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

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

1577 = case lookupDef n (tt_ctxt ist) of

1582 = case lookupDef n (tt_ctxt ist) of

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

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

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

1865toEither (LeftErr e) = Left e

1870toEither (LeftErr e) = Left e

1866toEither (RightOK ho) = Right ho

1871toEither (RightOK ho) = Right ho

1867

1872

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

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

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

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

1870−

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

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

1872matchClause = matchClause' False

1876matchClause = matchClause' False

1873

1877

@@ -2008,6 +2012,7 @@ substMatchShadow n shs tm t = sm shs t where

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

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

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

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

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

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

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

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

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

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

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

2013 (fmap (sm xs) tm)

2018 (fmap (sm xs) tm)

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

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

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

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

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

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

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

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

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

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

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

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

2041 sm (PTyped x y) = PTyped (sm x) (sm y)

2047 sm (PTyped x y) = PTyped (sm x) (sm y)

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

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

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

2121 return (x', y')) alts

2127 return (x', y')) alts

2122 return $! PCase fc t' alts'

2128 return $! PCase fc t' alts'

2129+ mkUniq (PIfThenElse fc c t f)

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

2123 mkUniq (PPair fc p l r)

2131 mkUniq (PPair fc p l r)

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

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

2125 return $! PPair fc p l' r'

2133 return $! PPair fc p l' r'

src/Idris/AbsSyntaxTree.hs+21−5

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

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

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

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

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

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

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

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

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

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

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

@@ -863,6 +864,7 @@ mapPT f t = f (mpt t) where

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

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

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

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

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

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

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

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

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

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

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

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

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

@@ -1021,6 +1023,7 @@ highestFC (PApp fc _ _) = Just fc

1021highestFC (PAppBind fc _ _) = Just fc

1023highestFC (PAppBind fc _ _) = Just fc

1022highestFC (PMatchApp fc _) = Just fc

1024highestFC (PMatchApp fc _) = Just fc

1023highestFC (PCase fc _ _) = Just fc

1025highestFC (PCase fc _ _) = Just fc

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

1024highestFC (PTrue fc _) = Just fc

1027highestFC (PTrue fc _) = Just fc

1025highestFC (PRefl fc _) = Just fc

1028highestFC (PRefl fc _) = Just fc

1026highestFC (PResolveTC fc) = Just fc

1029highestFC (PResolveTC fc) = Just fc

@@ -1544,9 +1547,15 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1544 noNS (NS _ _) = False

1547 noNS (NS _ _) = False

1545 noNS _ = True

1548 noNS _ = True

1546

1549

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

1551+ group . align . hang 2 . vsep $

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

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

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

1555+ ]

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

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

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

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

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

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

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

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

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

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

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

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

@@ -1644,10 +1653,6 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1644 opStr (NS n _) = opStr n

1653 opStr (NS n _) = opStr n

1645 opStr (UN n) = T.unpack n

1654 opStr (UN n) = T.unpack n

1646

1655

1647− basename :: Name -> Name

1648− basename (NS n _) = basename n

1649− basename n = n

1650−

1651 slist' _ _ e

1656 slist' _ _ e

1652 | containsHole e = Nothing

1657 | containsHole e = Nothing

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

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

@@ -1705,6 +1710,11 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1705 getFixity :: String -> Maybe Fixity

1710 getFixity :: String -> Maybe Fixity

1706 getFixity = flip M.lookup fixities

1711 getFixity = flip M.lookup fixities

1707

1712

1713+-- | Strip away namespace information

1714+basename :: Name -> Name

1715+basename (NS n _) = basename n

1716+basename n = n

1717+

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

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

1709-- guess by the delaborator

1719-- guess by the delaborator

1710isHoleName :: Name -> Bool

1720isHoleName :: Name -> Bool

@@ -1858,6 +1868,7 @@ instance Sized PTerm where

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

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

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

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

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

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

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

1861 size (PTrue fc _) = 1

1872 size (PTrue fc _) = 1

1862 size (PRefl fc _) = 1

1873 size (PRefl fc _) = 1

1863 size (PResolveTC fc) = 1

1874 size (PResolveTC fc) = 1

@@ -1898,6 +1909,7 @@ allNamesIn tm = nub $ ni [] tm

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

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

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

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

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

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

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

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

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

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

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

1903 ni env (PHidden tm) = ni env tm

1915 ni env (PHidden tm) = ni env tm

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2046 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

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

1620 put x1

1621 PQuoteName x1 -> do putWord8 44

1622 put x1

1623−

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

1624+ put x1

1625+ put x2

1626+ put x3

1627+ put x4

1624

1628

1625 get

1629 get

1626 = do i <- getWord8

1630 = do i <- getWord8

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

1755 return (PUnquote x1)

1759 return (PUnquote x1)

1756 44 -> do x1 <- get

1760 44 -> do x1 <- get

1757 return (PQuoteName x1)

1761 return (PQuoteName x1)

1762+ 45 -> do x1 <- get

1763+ x2 <- get

1764+ x3 <- get

1765+ x4 <- get

1766+ return (PIfThenElse x1 x2 x3 x4)

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

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

1759

1768

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

1769instance (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+2−1

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

229 "where", "with", "syntax", "proof", "postulate",

230 "using", "namespace", "class", "instance", "parameters",

231 "public", "private", "abstract", "implicit",

232− "quoteGoal", "constructor"]

232+ "quoteGoal", "constructor",

233+ "if", "then", "else"]

233

234

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

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

235char = Chr.char

236char = 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}