19624c7 · Idris-dev · git.iko.soy

CHANGELOG.md+2

compare with master

unifiedsplit

@@ -8,6 +8,8 @@

8+ The `LinearTypes` language extension has been revised. It implements the

9 rules from Bob Atkey's draft "The Syntax and Semantics of Quantitative

10 Type Theory" and now works with holes and case expressions.

11++ Backticked operators can appear in sections, e.g. `(\`LTE\` 42)` or

12+ `(1 \`plus\`)`.

11

13

12## Library Updates

14## Library Updates

13

15

CONTRIBUTORS+1

@@ -107,6 +107,7 @@ Jan de Muijnck-Hughes

107Jan Doms

108Jan Stolarek

109Jason Dagit

110+Jason Felice

110Jason Gross

111Jason Gross

111Jean-Remi Desjardins

112Jean-Remi Desjardins

112Jeff Hemphill

113Jeff Hemphill

src/Idris/Parser/Expr.hs+20−18

@@ -468,27 +468,29 @@ bracketed' open syn =

468 lchar ')'

469 return $ PTrue (spanFC open (FC f start (l, c+1))) TypeOrTerm

470 <|> try (dependentPair TypeOrTerm [] open syn)

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

471+ <|> try (do fc <- getFC

472+ opName <- operatorName

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

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

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

474+ guard $ opName /= sUN "-" && opName /= sUN "!"

474− then fail "minus not allowed in section"

475+ e <- expr syn

476+ lchar ')'

475− else return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder

477+ return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder

476− (PApp fc (PRef fc [] (sUN o)) [pexp (PRef fc [] (sMN 1000 "ARG")),

478+ (PApp fc (PRef fc [] opName) [pexp (PRef fc [] (sMN 1000 "ARG")),

477− pexp e]))

479+ pexp e]))

478− <|> try (do l <- simpleExpr syn

480+ <|> try (simpleExpr syn >>= \l ->

479− op <- option Nothing (do o <- operator

481+ try (do opName <- operatorName

480− lchar ')'

482+ lchar ')'

481− return (Just o))

482− fc0 <- getFC

483+ fc <- getFC

483− case op of

484+ return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder

485+ (PApp fc (PRef fc [] opName) [pexp l,

486+ pexp (PRef fc [] (sMN 1000 "ARG"))]))

484− Nothing -> bracketedExpr syn open l

487+ <|> bracketedExpr syn open l)

485− Just o -> return $ PLam fc0 (sMN 1000 "ARG") NoFC Placeholder

486− (PApp fc0 (PRef fc0 [] (sUN o)) [pexp l,

487− pexp (PRef fc0 [] (sMN 1000 "ARG"))]))

488 <|> do l <- expr (allowConstr syn)

489 bracketedExpr (allowConstr syn) open l

490−

490+ where

491−

491+ operatorName :: IdrisParser Name

492+ operatorName = sUN <$> operator

493+ <|> fst <$> between (lchar '`') (lchar '`') fnName

492

494

493{-| Parses the rest of a dependent pair after '(' or '(Expr **' -}

495{-| Parses the rest of a dependent pair after '(' or '(Expr **' -}

494dependentPair :: PunInfo -> [(PTerm, Maybe (FC, PTerm), FC)] -> FC -> SyntaxInfo -> IdrisParser PTerm

496dependentPair :: PunInfo -> [(PTerm, Maybe (FC, PTerm), FC)] -> FC -> SyntaxInfo -> IdrisParser PTerm

test/TestData.hs+23−22

@@ -52,28 +52,29 @@ testFamiliesData = [

52 ("base", "Base",

53 [ ( 1, C_CG )]),

54 ("basic", "Basic",

55− [ ( 1, ANY ),

55+ [ ( 1, ANY ),

56− ( 2, ANY ),

56+ ( 2, ANY ),

57− ( 3, ANY ),

57+ ( 3, ANY ),

58− ( 4, ANY ),

58+ ( 4, ANY ),

59− ( 5, ANY ),

59+ ( 5, ANY ),

60− ( 6, ANY ),

60+ ( 6, ANY ),

61− ( 7, C_CG ),

61+ ( 7, C_CG ),

62− ( 8, ANY ),

62+ ( 8, ANY ),

63− ( 9, ANY ),

63+ ( 9, ANY ),

64− ( 10, ANY ),

64+ ( 10, ANY ),

65− ( 11, C_CG ),

65+ ( 11, C_CG ),

66− ( 12, ANY ),

66+ ( 12, ANY ),

67− ( 13, ANY ),

67+ ( 13, ANY ),

68− ( 14, ANY ),

68+ ( 14, ANY ),

69− ( 15, ANY ),

69+ ( 15, ANY ),

70− ( 16, ANY ),

70+ ( 16, ANY ),

71− ( 17, ANY ),

71+ ( 17, ANY ),

72− ( 18, ANY ),

72+ ( 18, ANY ),

73− ( 19, ANY ),

73+ ( 19, ANY ),

74− ( 20, ANY ),

74+ ( 20, ANY ),

75− ( 21, C_CG ),

75+ ( 21, C_CG ),

76− ( 22, NODE_CG )]),

76+ ( 22, NODE_CG ),

77+ ( 23, ANY )]),

77 ("bignum", "Bignum",

78 ("bignum", "Bignum",

78 [ ( 1, ANY ),

79 [ ( 1, ANY ),

79 ( 2, ANY )]),

80 ( 2, ANY )]),

test/basic023/expectednew file+6

@@ -0,0 +1,6 @@

1+True

2+True

3+True

4+True

5+True

6+True

test/basic023/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ sections.idr -o sections

3+./sections

4+rm -f sections *.ibc

test/basic023/sections.idrnew file+19

@@ -0,0 +1,19 @@

1+preInc : Nat -> Nat

2+preInc = (1 `plus`)

3+

4+postInc : Nat -> Nat

5+postInc = (`plus` 1)

6+

7+cons : Int -> List Int -> List Int

8+cons = (::)

9+

10+main : IO ()

11+main = do

12+ printLn $ (1 `cons`) [2] == [1,2]

13+ printLn $ (1 ::) [2] == [1,2]

14+ printLn $ (`cons` [2]) 1 == [1,2]

15+ printLn $ (:: [2]) 1 == [1,2]

16+ let x : Integer = 4

17+ printLn $ (- x) == -4 -- prefix, not section

18+ let io : IO Integer = pure 9

19+ printLn $ (! io) == 9 -- prefix, not section