7932e28 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added idiom brackets

7932e28Edwin Brady15 years ago

lib/prelude.idr+14

compare with master

unifiedsplit

@@ -69,6 +69,11 @@ instance Show a => Show (Vect a n) where {

69 }

70}

72+instance Show a => Show (Maybe a) where {

73+ show Nothing = "Nothing";

74+ show (Just x) = "Just " ++ show x;

75+}

76+

72---- Monad and instances

77---- Monad and instances

74infixl 5 >>= ;

79infixl 5 >>= ;

@@ -118,6 +123,15 @@ instance Functor List where {

118 fmap = map;

123 fmap = map;

119}

124}

120

125

126+---- Applicative functors/Idioms

127+

128+infixl 2 <$>;

129+

130+class Functor f => Applicative (f : Set -> Set) where {

131+ pure : a -> f a;

132+ (<$>) : f (a -> b) -> f a -> f b;

133+}

134+

121---- some mathematical operations

135---- some mathematical operations

122

136

123%include "math.h"

137%include "math.h"

src/Core/Typecheck.hs+2−2

@@ -20,8 +20,8 @@ convertsC ctxt env x y

20 (finalise (normalise ctxt env y))

21 if c then return ()

22 else fail ("Can't convert between " ++

23− showEnvDbg env (finalise (normalise ctxt env x)) ++ " and " ++

23+ showEnv env (finalise (normalise ctxt env x)) ++ " and " ++

24− showEnvDbg env (finalise (normalise ctxt env y)))

24+ showEnv env (finalise (normalise ctxt env y)))

26converts :: Context -> Env -> Term -> Term -> TC ()

27converts ctxt env x y = if (finalise (normalise ctxt env x) ==

src/Idris/AbsSyntax.hs+1

@@ -399,6 +399,7 @@ data PTerm = PQuote Raw

399 | PConstant Const

400 | Placeholder

401 | PDoBlock [PDo]

402+ | PIdiom FC PTerm

402 | PReturn FC

403 | PReturn FC

403 | PMetavar Name

404 | PMetavar Name

404 | PProof [PTactic]

405 | PProof [PTactic]

src/Idris/Parser.hs+17

@@ -520,6 +520,7 @@ pSimpleExpr syn =

520 <|> try (pPair syn)

521 <|> try (pList syn)

522 <|> try (pAlt syn)

523+ <|> try (pIdiom syn)

523 <|> try (do lchar '('; e <- pExpr syn; lchar ')'; return e)

524 <|> try (do lchar '('; e <- pExpr syn; lchar ')'; return e)

524 <|> try (do lchar '('; fc <- pfc; o <- operator; e <- pExpr syn; lchar ')'

525 <|> try (do lchar '('; fc <- pfc; o <- operator; e <- pExpr syn; lchar ')'

525 return $ PLam (MN 0 "x") Placeholder

526 return $ PLam (MN 0 "x") Placeholder

@@ -683,6 +684,10 @@ pDo syn

683 <|> try (do e <- pExpr syn; fc <- pfc

684 <|> try (do e <- pExpr syn; fc <- pfc

684 return (DoExp fc e))

685 return (DoExp fc e))

685

686

687+pIdiom syn

688+ = do symbol "[|"; fc <- pfc; e <- pExpr syn; symbol "|]"

689+ return (PIdiom fc e)

690+

686pConstant :: IParser Const

691pConstant :: IParser Const

687pConstant = do reserved "Integer";return BIType

692pConstant = do reserved "Integer";return BIType

688 <|> do reserved "Int"; return IType

693 <|> do reserved "Int"; return IType

@@ -988,6 +993,7 @@ desugar syn i t = let t' = expandDo (dsl_info syn) t in

988

993

989expandDo :: DSL -> PTerm -> PTerm

994expandDo :: DSL -> PTerm -> PTerm

990expandDo dsl (PLam n ty tm) = PLam n (expandDo dsl ty) (expandDo dsl tm)

995expandDo dsl (PLam n ty tm) = PLam n (expandDo dsl ty) (expandDo dsl tm)

996+expandDo dsl (PLet n ty v tm) = PLet n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)

991expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)

997expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)

992expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)

998expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)

993 (map (fmap (expandDo dsl)) args)

999 (map (fmap (expandDo dsl)) args)

@@ -1010,7 +1016,18 @@ expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds

1010 [pexp tm,

1016 [pexp tm,

1011 pexp (PLam (MN 0 "bindx") Placeholder (block b rest))]

1017 pexp (PLam (MN 0 "bindx") Placeholder (block b rest))]

1012 block b _ = PElabError "Invalid statement in do block"

1018 block b _ = PElabError "Invalid statement in do block"

1019+expandDo dsl (PIdiom fc e) = expandDo dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e

1013expandDo dsl t = t

1020expandDo dsl t = t

1014

1021

1022+unIdiom :: PTerm -> PTerm -> FC -> PTerm -> PTerm

1023+unIdiom ap pure fc e@(PApp _ _ _) = let f = getFn e in

1024+ mkap (getFn e)

1025+ where

1026+ getFn (PApp fc f args) = (PApp fc pure [pexp f], args)

1027+ getFn f = (f, [])

1028+

1029+ mkap (f, []) = f

1030+ mkap (f, a:as) = mkap (PApp fc ap [pexp f, a], as)

1015

1031

1032+unIdiom ap pure fc e = PApp fc pure [pexp e]

1016

1033