9760a72 · Idris-dev · git.iko.soy

207internalExpr :: SyntaxInfo -> IdrisParser PTerm

208internalExpr syn =

209 unifyLog syn

210− <|> try (disamb syn)

210+ <|> disamb syn

211 <|> noImplicits syn

212 <|> recordType syn

213 <|> lambda syn

275{- | Parses a simple expression

276@

277SimpleExpr ::=

278− '![' Term ']'

278+ {- External (User-defined) Simple Expression -}

279 | '?' Name

280 | % 'instance'

281 | 'refl' ('{' Expr '}')?

282 | ProofExpr

283 | TacticsExpr

284 | FnName

285+ | Idiom

285 | List

286 | List

286− | Comprehension

287 | Alt

288− | Idiom

289 | Bracketed

288 | Bracketed

290 | Constant

289 | Constant

291 | Type

290 | Type

292 | '_|_'

291 | '_|_'

293 | '_'

292 | '_'

294− | {- External (User-defined) Simple Expression -}

295 ;

293 ;

296@

294@

297-}

295-}

298simpleExpr :: SyntaxInfo -> IdrisParser PTerm

296simpleExpr :: SyntaxInfo -> IdrisParser PTerm

299simpleExpr syn =

297simpleExpr syn =

300− {-try (do symbol "!["; t <- term; lchar ']'; return $ PQuote t)

298+ try (simpleExternalExpr syn)

301− <|>-} do x <- try (lchar '?' *> name); return (PMetavar x)

299+ <|> do x <- try (lchar '?' *> name); return (PMetavar x)

302 <|> do lchar '%'; fc <- getFC; reserved "instance"; return (PResolveTC fc)

300 <|> do lchar '%'; fc <- getFC; reserved "instance"; return (PResolveTC fc)

303 <|> do reserved "refl"; fc <- getFC;

301 <|> do reserved "refl"; fc <- getFC;

304 tm <- option Placeholder (do lchar '{'; t <- expr syn; lchar '}';

302 tm <- option Placeholder (do lchar '{'; t <- expr syn; lchar '}';

308 <|> proofExpr syn

306 <|> proofExpr syn

309 <|> tacticsExpr syn

307 <|> tacticsExpr syn

310 <|> do reserved "Type"; return PType

308 <|> do reserved "Type"; return PType

311− <|> try (do c <- constant

309+ <|> do c <- constant

312− fc <- getFC

310+ fc <- getFC

313− return (modifyConst syn fc (PConstant c)))

311+ return (modifyConst syn fc (PConstant c))

314− <|> try (do symbol "'"; fc <- getFC; str <- name

312+ <|> do symbol "'"; fc <- getFC; str <- name

315− return (PApp fc (PRef fc (sUN "Symbol_"))

313+ return (PApp fc (PRef fc (sUN "Symbol_"))

316− [pexp (PConstant (Str (show str)))]))

314+ [pexp (PConstant (Str (show str)))])

317 <|> do fc <- getFC

315 <|> do fc <- getFC

318 x <- fnName

316 x <- fnName

319 return (PRef fc x)

317 return (PRef fc x)

320− <|> try (listExpr syn)

321− <|> try (comprehension syn)

322− <|> alt syn

323 <|> idiom syn

318 <|> idiom syn

319+ <|> listExpr syn

320+ <|> alt syn

324 <|> do lchar '!'

321 <|> do lchar '!'

325 s <- simpleExpr syn

322 s <- simpleExpr syn

326 fc <- getFC

323 fc <- getFC

330 fc <- getFC

327 fc <- getFC

331 return (PFalse fc)

328 return (PFalse fc)

332 <|> do lchar '_'; return Placeholder

329 <|> do lchar '_'; return Placeholder

333− <|> simpleExternalExpr syn

334 <?> "expression"

330 <?> "expression"

335

331

336{- |Parses an expression in braces

332{- |Parses an expression in braces

427 ]

423 ]

428modifyConst syn fc x = x

424modifyConst syn fc x = x

429

425

430−{- | Parses a list literal expression e.g. [1,2,3]

431−@

432−ListExpr ::=

433− '[' ExprList? ']'

434−;

435−@

436−@

437−ExprList ::=

438− Expr

439− | Expr ',' ExprList

440− ;

441−@

442− -}

443−listExpr :: SyntaxInfo -> IdrisParser PTerm

444−listExpr syn = do lchar '['; fc <- getFC; xs <- sepBy (expr syn) (lchar ','); lchar ']'

445− return (mkList fc xs)

446− <?> "list expression"

447− where

448− mkList :: FC -> [PTerm] -> PTerm

449− mkList fc [] = PRef fc (sUN "Nil")

450− mkList fc (x : xs) = PApp fc (PRef fc (sUN "::")) [pexp x, pexp (mkList fc xs)]

451−

452−

453{- | Parses an alternative expression

426{- | Parses an alternative expression

454@

427@

455 Alt ::= '(|' Expr_List '|)';

428 Alt ::= '(|' Expr_List '|)';

901 return (sMN 0 "underscore")

874 return (sMN 0 "underscore")

902 <?> "name or placeholder"

875 <?> "name or placeholder"

903

876

904−{- | Parses a list comprehension

877+{- | Parses a list literal expression e.g. [1,2,3] or a comprehension [ (x, y) | x <- xs , y <- ys ]

905@

878@

879+ListExpr ::=

880+ '[' ']'

906−Comprehension ::= '[' Expr '|' DoList ']';

881+ | '[' Expr '|' DoList ']'

882+ | '[' ExprList ']'

883+;

907@

884@

908−

909@

885@

910DoList ::=

886DoList ::=

911 Do

887 Do

912 | Do ',' DoList

888 | Do ',' DoList

913 ;

889 ;

914@

890@

891+@

892+ExprList ::=

893+ Expr

894+ | Expr ',' ExprList

895+ ;

896+@

915−-}

897+ -}

916−comprehension :: SyntaxInfo -> IdrisParser PTerm

898+listExpr :: SyntaxInfo -> IdrisParser PTerm

917−comprehension syn

918− = do lchar '['

899+listExpr syn = do lchar '['; fc <- getFC;

919− fc <- getFC

900+ try (lchar ']' *> return (mkList fc [])) <|> (do

920− pat <- expr syn

901+ x <- expr syn

921− lchar '|'

902+ (do try (lchar '|')

922− qs <- sepBy1 (do_ syn) (lchar ',')

903+ qs <- sepBy1 (do_ syn) (lchar ',')

923− lchar ']'

904+ lchar ']'

924− return (PDoBlock (map addGuard qs ++

905+ return (PDoBlock (map addGuard qs ++

925− [DoExp fc (PApp fc (PRef fc (sUN "return"))

906+ [DoExp fc (PApp fc (PRef fc (sUN "return"))

926− [pexp pat])]))

907+ [pexp x])]))) <|> (do

927− <?> "list comprehension"

908+ xs <- many (lchar ',' *> expr syn)

909+ lchar ']'

910+ return (mkList fc (x:xs))))

911+ <?> "list expression"

912+ where

913+ mkList :: FC -> [PTerm] -> PTerm

914+ mkList fc [] = PRef fc (sUN "Nil")

915+ mkList fc (x : xs) = PApp fc (PRef fc (sUN "::")) [pexp x, pexp (mkList fc xs)]

928− where addGuard :: PDo -> PDo

916+ addGuard :: PDo -> PDo

929− addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (sUN "guard"))

917+ addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (sUN "guard"))

930− [pexp e])

918+ [pexp e])

931− addGuard x = x

919+ addGuard x = x

932

920

933{- | Parses a do-block

921{- | Parses a do-block

934@

922@

1060 <|> do reserved "Bits16x8"; return (AType (ATInt (ITVec IT16 8)))

1048 <|> do reserved "Bits16x8"; return (AType (ATInt (ITVec IT16 8)))

1061 <|> do reserved "Bits32x4"; return (AType (ATInt (ITVec IT32 4)))

1049 <|> do reserved "Bits32x4"; return (AType (ATInt (ITVec IT32 4)))

1062 <|> do reserved "Bits64x2"; return (AType (ATInt (ITVec IT64 2)))

1050 <|> do reserved "Bits64x2"; return (AType (ATInt (ITVec IT64 2)))

1063− <|> try (do f <- float; return $ Fl f)

1051+ <|> do f <- try float; return $ Fl f

1064− <|> try (do i <- natural; return $ BI i)

1052+ <|> do i <- natural; return $ BI i

1065− <|> try (do s <- verbatimStringLiteral; return $ Str s)

1053+ <|> do s <- verbatimStringLiteral; return $ Str s

1066− <|> try (do s <- stringLiteral; return $ Str s)

1054+ <|> do s <- stringLiteral; return $ Str s

1067− <|> try (do c <- charLiteral; return $ Ch c)

1055+ <|> do c <- try charLiteral; return $ Ch c --Currently ambigous with symbols

1068 <?> "constant or literal"

1056 <?> "constant or literal"

1069

1057

1070{- | Parses a verbatim multi-line string literal (triple-quoted)

1058{- | Parses a verbatim multi-line string literal (triple-quoted)

1076@

1064@

1077 -}

1065 -}

1078verbatimStringLiteral :: MonadicParsing m => m String

1066verbatimStringLiteral :: MonadicParsing m => m String

1079−verbatimStringLiteral = token $ do string "\"\"\""

1067+verbatimStringLiteral = token $ do try $ string "\"\"\""

1080 manyTill anyChar $ try (string "\"\"\"")

1068 manyTill anyChar $ try (string "\"\"\"")

1081

1069

1082{- | Parses a static modifier

1070{- | Parses a static modifier