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

git.iko.soy/Idris-dev

Added idiom brackets

commit7932e2816e3cec09cb69f145c2f0a1c014bd98d6 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 3 Jan 2012, 17:56 (15 years ago) parent53c04f3

4 files changed+34−2

compare with master

unifiedsplit

lib/prelude.idr+14 src/Core/Typecheck.hs+2−2 src/Idris/AbsSyntax.hs+1 src/Idris/Parser.hs+17

lib/prelude.idr+14

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

6969 }

7070}

7171

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

73+ show Nothing = "Nothing";

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

75+}

76+

7277---- Monad and instances

7378

7479infixl 5 >>= ;

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

118123 fmap = map;

119124}

120125

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+

121135---- some mathematical operations

122136

123137%include "math.h"

src/Core/Typecheck.hs+2−2

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

2020 (finalise (normalise ctxt env y))

2121 if c then return ()

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

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

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

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

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

2525

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

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

src/Idris/AbsSyntax.hs+1

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

399399 | PConstant Const

400400 | Placeholder

401401 | PDoBlock [PDo]

402+ | PIdiom FC PTerm

402403 | PReturn FC

403404 | PMetavar Name

404405 | PProof [PTactic]

src/Idris/Parser.hs+17

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

520520 <|> try (pPair syn)

521521 <|> try (pList syn)

522522 <|> try (pAlt syn)

523+ <|> try (pIdiom syn)

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

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

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

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

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

684685 return (DoExp fc e))

685686

687+pIdiom syn

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

689+ return (PIdiom fc e)

690+

686691pConstant :: IParser Const

687692pConstant = do reserved "Integer";return BIType

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

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

988993

989994expandDo :: DSL -> PTerm -> PTerm

990995expandDo 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)

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

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

993999 (map (fmap (expandDo dsl)) args)

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

10101016 [pexp tm,

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

10121018 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

10131020expandDo dsl t = t

10141021

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)

10151031

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

10161033