Add idiom brackets

README.md

@@ -84,12 +84,11 @@ Information about external dependencies are presented in [INSTALL.md](INSTALL.md
 Things still missing
 ====================
 
-+ Some high level syntax, notably idiom brackets 
 + 'using' blocks
++ Disambiguation via 'with'
 + Cumulativity (so we currently have Type : Type! Bear that in mind when you
   think you've proved something :))
 + 'rewrite' doesn't yet work on dependent types
-+ Some details of 'with' not yet done (notably recursive with call syntax)
 + Parts of the ide-mode, particularly syntax highlighting
 + Documentation strings and HTML documentation generation
 + ':search' and ':apropos' at the REPL

src/Idris/Desugar.idr

@@ -114,6 +114,13 @@ bindBangs ((n, fc, btm) :: bs) tm
                           (ILam fc RigW Explicit (Just n)
                                 (Implicit fc False) tm)
 
+idiomise : FC -> RawImp -> RawImp
+idiomise fc (IApp afc f a)
+    = IApp fc (IApp fc (IVar fc (UN "<*>"))
+                    (idiomise afc f))
+                    a
+idiomise fc fn = IApp fc (IVar fc (UN "pure")) fn
+
 data Bang : Type where
 
 mutual
@@ -252,6 +259,9 @@ mutual
                               bangNames $= ((bn, fc, itm) ::)
                             } bs)
            pure (IVar fc bn)
+  desugarB side ps (PIdiom fc term)
+      = do itm <- desugarB side ps term
+           pure (idiomise fc itm)
   desugarB side ps (PList fc args)
       = expandList side ps fc args
   desugarB side ps (PPair fc l r)

src/Idris/Parser.idr

@@ -350,6 +350,12 @@ mutual
            e <- simpleExpr fname indents
            end <- location
            pure (PBang (MkFC fname start end) e)
+    <|> do start <- location
+           symbol "[|"
+           e <- expr pdef fname indents
+           symbol "|]"
+           end <- location
+           pure (PIdiom (MkFC fname start end) e)
     <|> do start <- location
            symbol "%"; exactIdent "unifyLog"
            e <- expr pdef fname indents

src/Idris/Syntax.idr

@@ -78,6 +78,7 @@ mutual
 
        PDoBlock : FC -> List PDo -> PTerm
        PBang : FC -> PTerm -> PTerm
+       PIdiom : FC -> PTerm -> PTerm
        PList : FC -> List PTerm -> PTerm
        PPair : FC -> PTerm -> PTerm -> PTerm
        PDPair : FC -> PTerm -> PTerm -> PTerm -> PTerm
@@ -93,8 +94,7 @@ mutual
        -- Debugging
        PUnifyLog : FC -> PTerm -> PTerm
 
-       -- TODO: Idiom brackets (?),
-       -- 'with' disambiguation
+       -- TODO: 'with' disambiguation
 
   public export
   data PFieldUpdate : Type where
@@ -443,6 +443,7 @@ mutual
     showPrec d (PDoBlock _ ds)
         = "do " ++ showSep " ; " (map showDo ds)
     showPrec d (PBang _ tm) = "!" ++ showPrec d tm
+    showPrec d (PIdiom _ tm) = "[|" ++ showPrec d tm ++ "|]"
     showPrec d (PList _ xs)
         = "[" ++ showSep ", " (map (showPrec d) xs) ++ "]"
     showPrec d (PPair _ l r) = "(" ++ showPrec d l ++ ", " ++ showPrec d r ++ ")"

src/Parser/Lexer.idr

@@ -116,6 +116,7 @@ symbols : List String
 symbols
     = [".(", -- for things such as Foo.Bar.(+)
        "@{",
+       "[|", "|]",
        "(", ")", "{", "}", "[", "]", ",", ";", "_",
        "`(", "`"]
 

tests/Main.idr

@@ -29,7 +29,7 @@ idrisTests
        "basic016", "basic017", "basic018", "basic019", "basic020",
        "basic021", "basic022", "basic023", "basic024", "basic025",
        "basic026", "basic027", "basic028", "basic029", "basic030",
-       "basic031",
+       "basic031", "basic032",
        "coverage001", "coverage002", "coverage003", "coverage004",
        "error001", "error002", "error003", "error004", "error005",
        "error006", "error007", "error008", "error009", "error010",

tests/chez/chez011/expected

@@ -2,13 +2,6 @@
 "12"
 True
 False
-     ____    __     _         ___                                           
-    /  _/___/ /____(_)____   |__ \                                          
-    / // __  / ___/ / ___/   __/ /     Version 0.0.0-9cd040fcb
-  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org           
- /___/\__,_/_/  /_/____/   /____/                                           
-
-Welcome to Idris 2.  Enjoy yourself!
 1/1: Building bangs (bangs.idr)
 Main> Just 7
 Main> Just 7

tests/chez/chez011/run

@@ -1,3 +1,3 @@
-$1 bangs.idr < input
+$1 --no-banner bangs.idr < input
 
 rm -rf build

tests/idris2/basic032/Idiom.idr

@@ -0,0 +1,15 @@
+export
+record Core t where
+  constructor MkCore
+  runCore : IO (Either String t)
+
+pure : a -> Core a
+pure x = MkCore (pure (pure x))
+
+export
+(<*>) : Core (a -> b) -> Core a -> Core b
+(<*>) (MkCore f) (MkCore a) = MkCore [| f `Prelude.(<*>)` a |]
+
+addm : Maybe Int -> Maybe Int -> Maybe Int
+addm x y = [| x + y |]
+

tests/idris2/basic032/expected

@@ -0,0 +1,3 @@
+1/1: Building Idiom (Idiom.idr)
+Main> Just 7
+Main> Bye for now!

tests/idris2/basic032/input

@@ -0,0 +1,2 @@
+addm (Just 3) (Just 4)
+:q

tests/idris2/basic032/run

@@ -0,0 +1,3 @@
+$1 --no-banner Idiom.idr < input
+
+rm -rf build