1adeea3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1105 from ahmadsalim/improvement/refactorpis

1adeea3Edwin Brady13 years ago

src/Idris/ParseExpr.hs+45−33

compare with master

unifiedsplit

@@ -54,14 +54,22 @@ fullExpr syn = do x <- expr syn

54 return $ debindApp syn (desugar syn i x)

57−{- |Parses an expression

57+{- | Parses an expression

58@

59− Expr ::= Expr';

59+ Expr ::= Pi

60@

61−-}

61+ -}

62expr :: SyntaxInfo -> IdrisParser PTerm

63+expr = pi

64+

65+{- | Parses an expression with possible operator applied

66+@

67+ OpExpr ::= {- Expression Parser with Operators based on Expr' -};

68+@

69+-}

70+opExpr :: SyntaxInfo -> IdrisParser PTerm

63−expr syn = do i <- get

71+opExpr syn = do i <- get

64− buildExpressionParser (table (idris_infixes i)) (expr' syn)

72+ buildExpressionParser (table (idris_infixes i)) (expr' syn)

66{- | Parses either an internally defined expression or

74{- | Parses either an internally defined expression or

67 a user-defined one

75 a user-defined one

@@ -70,16 +78,10 @@ Expr' ::= "External (User-defined) Syntax"

70 | InternalExpr;

78 | InternalExpr;

71@

79@

72 -}

80 -}

73−expr' syn = doexpr' syn

74−-- = do l <- restOfLine

75−-- f <- getFC

76−-- e <- trace (show (f, l)) $ doexpr' syn

77−-- return e

78−

79−doexpr' :: SyntaxInfo -> IdrisParser PTerm

81+expr' :: SyntaxInfo -> IdrisParser PTerm

80−doexpr' syn = try (externalExpr syn)

82+expr' syn = try (externalExpr syn)

81− <|> internalExpr syn

83+ <|> internalExpr syn

82− <?> "expression"

84+ <?> "expression"

84{- | Parses a user-defined expression -}

86{- | Parses a user-defined expression -}

85externalExpr :: SyntaxInfo -> IdrisParser PTerm

87externalExpr :: SyntaxInfo -> IdrisParser PTerm

@@ -197,7 +199,6 @@ InternalExpr ::=

197 | QuoteGoal

199 | QuoteGoal

198 | Let

200 | Let

199 | RewriteTerm

201 | RewriteTerm

200− | Pi

201 | CaseExpr

202 | CaseExpr

202 | DoBlock

203 | DoBlock

203 | App

204 | App

@@ -214,7 +215,6 @@ internalExpr syn =

214 <|> quoteGoal syn

215 <|> quoteGoal syn

215 <|> let_ syn

216 <|> let_ syn

216 <|> rewriteTerm syn

217 <|> rewriteTerm syn

217− <|> try (pi syn)

218 <|> doBlock syn

219 <|> caseExpr syn

220 <|> app syn

@@ -363,7 +363,7 @@ bracketed' syn =

363 return (PDPair fc TypeOrTerm (PRef fc ln) lty r))

364 <|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')'

365 -- No prefix operators! (bit of a hack here...)

366− if (o == "-" || o == "!")

366+ if (o == "-" || o == "!")

367 then fail "minus not allowed in section"

368 else return $ PLam (sMN 1000 "ARG") Placeholder

369 (PApp fc (PRef fc (sUN o)) [pexp (PRef fc (sMN 1000 "ARG")),

@@ -754,11 +754,16 @@ quoteGoal syn = do reserved "quoteGoal"; n <- name;

754{- | Parses a dependent type signature

755

756@

757−Pi ::=

757+Pi ::= PiOpts Static? Pi'

758− '|'? Static? '(' TypeDeclList ')' DocComment '->' Expr

758+@

759− | '|'? Static? '{' TypeDeclList '}' '->' Expr

759+

760+@

761+Pi' ::=

762+ OpExpr ('->' Pi)?

763+ | '(' TypeDeclList ')' '->' Pi

764+ | '{' TypeDeclList '}' '->' Pi

760− | '{' 'auto' TypeDeclList '}' '->' Expr

765+ | '{' 'auto' TypeDeclList '}' '->' Pi

761− | '{' 'default' TypeDeclList '}' '->' Expr

766+ | '{' 'default' SimpleExpr TypeDeclList '}' '->' Pi

762 ;

767 ;

763@

768@

764 -}

769 -}

@@ -767,37 +772,44 @@ pi :: SyntaxInfo -> IdrisParser PTerm

767pi syn =

772pi syn =

768 do opts <- piOpts syn

773 do opts <- piOpts syn

769 st <- static

774 st <- static

770− (do try (lchar '('); xt <- typeDeclList syn; lchar ')'

775+ (do xt <- try (lchar '(' *> typeDeclList syn <* lchar ')')

771 symbol "->"

776 symbol "->"

772 sc <- expr syn

777 sc <- expr syn

773 return (bindList (PPi (Exp opts st False)) xt sc)) <|> (do

778 return (bindList (PPi (Exp opts st False)) xt sc)) <|> (do

774− lchar '{'

775− (do reserved "auto"

779+ (do try (lchar '{' *> reserved "auto")

776 when (st == Static) $ fail "auto type constraints can not be lazy or static"

780 when (st == Static) $ fail "auto type constraints can not be lazy or static"

777 xt <- typeDeclList syn

781 xt <- typeDeclList syn

778 lchar '}'

782 lchar '}'

779 symbol "->"

783 symbol "->"

780 sc <- expr syn

784 sc <- expr syn

781 return (bindList (PPi

785 return (bindList (PPi

782− (TacImp [] Dynamic (PTactics [Trivial]))) xt sc))

786+ (TacImp [] Dynamic (PTactics [Trivial]))) xt sc)) <|> (do

783− <|> (do

784− reserved "default"

787+ try (lchar '{' *> reserved "default")

785 when (st == Static) $ fail "default tactic constraints can not be lazy or static"

788 when (st == Static) $ fail "default tactic constraints can not be lazy or static"

786 script <- simpleExpr syn

789 script <- simpleExpr syn

787 xt <- typeDeclList syn

790 xt <- typeDeclList syn

788 lchar '}'

791 lchar '}'

789 symbol "->"

792 symbol "->"

790 sc <- expr syn

793 sc <- expr syn

791− return (bindList (PPi (TacImp [] Dynamic script)) xt sc))

794+ return (bindList (PPi (TacImp [] Dynamic script)) xt sc))

792 <|> (if implicitAllowed syn then do

795 <|> (if implicitAllowed syn then do

793− xt <- typeDeclList syn

796+ xt <- try (lchar '{' *> typeDeclList syn <* lchar '}')

794− lchar '}'

795 symbol "->"

797 symbol "->"

796 sc <- expr syn

798 sc <- expr syn

797 return (bindList (PPi (Imp opts st False)) xt sc)

799 return (bindList (PPi (Imp opts st False)) xt sc)

798 else do fail "no implicit arguments allowed here"))

800 else do fail "no implicit arguments allowed here"))

801+ <|> (do x <- opExpr syn

802+ (do symbol "->"

803+ sc <- expr syn

804+ return (PPi (Exp opts st False) (sUN "__pi_arg") x sc))

805+ <|> return x)

799 <?> "dependent type signature"

806 <?> "dependent type signature"

800

807

808+{- | Parses Possible Options for Pi Expressions

809+@

810+ PiOpts ::= '.'?

811+@

812+-}

801piOpts :: SyntaxInfo -> IdrisParser [ArgOpt]

813piOpts :: SyntaxInfo -> IdrisParser [ArgOpt]

802piOpts syn | implicitAllowed syn =

814piOpts syn | implicitAllowed syn =

803 lchar '.' *> return [InaccessibleArg]

815 lchar '.' *> return [InaccessibleArg]

@@ -1079,7 +1091,7 @@ Static ::=

1079@

1091@

1080-}

1092-}

1081static :: IdrisParser Static

1093static :: IdrisParser Static

1082−static = do lchar '['; reserved "static"; lchar ']'; return Static

1094+static = do reserved "[static]"; return Static

1083 <|> return Dynamic

1095 <|> return Dynamic

1084 <?> "static modifier"

1096 <?> "static modifier"

1085

1097

src/Idris/ParseOps.hs+1−2

@@ -38,8 +38,7 @@ table fixes

38 ++ toTable (reverse fixes) ++

39 [[backtick],

40 [binary "$" (\fc x y -> flatten $ PApp fc x [pexp y]) AssocRight],

41− [binary "=" PEq AssocLeft],

41+ [binary "=" PEq AssocLeft]]

42− [binary "->" (\fc x y -> PPi expl (sUN "__pi_arg") x y) AssocRight]]

43 where

42 where

44 flatten :: PTerm -> PTerm -- flatten application

43 flatten :: PTerm -> PTerm -- flatten application

45 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))

44 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))