Dictionary syntax

src/Idris/Desugar.idr

@@ -354,6 +354,8 @@ mutual
       = let ps' = definedIn xs ++ ps in
             pure $ ILocal fc (concat !(traverse (desugarDecl ps') xs))
                              !(desugar side ps' scope)
+  desugarB side ps (PDict fc fs)
+      = expandDict side ps emptyFC fs
   desugarB side ps (PApp pfc (PUpdate fc fs) rec)
       = pure $ IUpdate pfc !(traverse (desugarUpdate side ps) fs)
                            !(desugarB side ps rec)
@@ -600,6 +602,18 @@ mutual
       = pure $ apply (IVar consFC (UN $ Basic "::"))
                 [!(desugarB side ps x), !(expandList side ps nilFC xs)]
 
+  expandDict : {auto s : Ref Syn SyntaxInfo} ->
+               {auto b : Ref Bang BangData} ->
+               {auto c : Ref Ctxt Defs} ->
+               {auto u : Ref UST UState} ->
+               {auto m : Ref MD Metadata} ->
+               {auto o : Ref ROpts REPLOpts} ->
+               Side -> List Name -> (nilFC : FC) -> PDictionary -> Core RawImp
+  expandDict side ps nilFC [] = pure (IVar nilFC (UN $ Basic "DNil"))
+  expandDict side ps nilFC ((k, v) :: xs)
+      = pure $ apply (IVar emptyFC (UN $ Basic "DCons"))
+          [!(desugarB side ps k), !(desugarB side ps v), !(expandDict side ps nilFC xs)]
+
   expandSnocList
              : {auto s : Ref Syn SyntaxInfo} ->
                {auto b : Ref Bang BangData} ->

src/Idris/Parser.idr

@@ -637,8 +637,10 @@ mutual
            bracketedExpr fname start indents
     <|> do start <- bounds (symbol "[<")
            snocListExpr fname start indents
-    <|> do start <- bounds (symbol "[>" <|> symbol "[")
+    <|> do start <- bounds (symbol "[>")
            listExpr fname start indents
+    <|> do start <- bounds (symbol "[")
+           listExpr fname start indents <|> emptyDict fname indents <|> dict fname indents
     <|> do b <- bounds (decoratedSymbol fname "!" *> simpleExpr fname indents)
            pure (PBang (virtualiseFC $ boundToFC fname b) b.val)
     <|> do b <- bounds $ do decoratedPragma fname "logging"
@@ -892,6 +894,24 @@ mutual
            (x, t, e) <- pure b.val
            pure (PIfThenElse (boundToFC fname b) x t e)
 
+  emptyDict : OriginDesc -> IndentInfo -> Rule PTerm
+  emptyDict fname idents = do
+    b <- bounds $ symbol ":=" >> symbol "]"
+    pure $ PDict (boundToFC fname b) []
+
+  dict : OriginDesc -> IndentInfo -> Rule PTerm
+  dict fname indents = do
+    b <- bounds $ do
+      commit
+      fs <- sepBy1 (decoratedSymbol fname ",") $ do
+        l <- expr pdef fname indents
+        ignore (decoratedSymbol fname ":=")
+        r <- expr pdef fname indents
+        pure (l, r)
+      decoratedSymbol fname "]"
+      pure fs
+    pure $ PDict (boundToFC fname b) (List1.forget b.val)
+
   record_ : OriginDesc -> IndentInfo -> Rule PTerm
   record_ fname indents
       = do

src/Idris/Pretty.idr

@@ -294,6 +294,8 @@ mutual
     prettyPrec d (PLocal _ ds sc) =
       parenthesise (d > startPrec) $ group $ align $
         let_ <++> braces (angles (angles "definitions")) <+> line <+> in_ <++> pretty sc
+    prettyPrec d (PDict _ fs) =
+      ?render222
     prettyPrec d (PUpdate _ fs) =
       parenthesise (d > startPrec) $ group $
         record_ <++> braces (vsep $ punctuate comma (prettyPFieldUpdate <$> fs))

src/Idris/Syntax.idr

@@ -104,6 +104,7 @@ mutual
        PCase : FC -> List (PFnOpt' nm) -> PTerm' nm -> List (PClause' nm) -> PTerm' nm
        PLocal : FC -> List (PDecl' nm) -> (scope : PTerm' nm) -> PTerm' nm
        PUpdate : FC -> List (PFieldUpdate' nm) -> PTerm' nm
+       PDict : FC -> PDictionary' nm -> PTerm' nm
        PApp : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm
        PWithApp : FC -> PTerm' nm -> PTerm' nm -> PTerm' nm
        PNamedApp : FC -> PTerm' nm -> Name -> PTerm' nm -> PTerm' nm
@@ -176,6 +177,7 @@ mutual
   getPTermLoc (PLet fc _ _ _ _ _ _) = fc
   getPTermLoc (PCase fc _ _ _) = fc
   getPTermLoc (PLocal fc _ _) = fc
+  getPTermLoc (PDict fc _) = fc
   getPTermLoc (PUpdate fc _) = fc
   getPTermLoc (PApp fc _ _) = fc
   getPTermLoc (PWithApp fc _ _) = fc
@@ -232,6 +234,14 @@ mutual
        PSetField : (path : List String) -> PTerm' nm -> PFieldUpdate' nm
        PSetFieldApp : (path : List String) -> PTerm' nm -> PFieldUpdate' nm
 
+  public export
+  PDictionary' : Type -> Type
+  PDictionary' nm = List (PTerm' nm, PTerm' nm)
+
+  public export
+  PDictionary : Type
+  PDictionary = List (PTerm, PTerm)
+
   public export
   PDo : Type
   PDo = PDo' Name
@@ -771,6 +781,8 @@ parameters {0 nm : Type} (toName : nm -> Name)
         showCase (MkImpossible _ lhs) = showPTerm lhs ++ " impossible"
   showPTermPrec d (PLocal _ ds sc) -- We'll never see this when displaying a normal form...
         = "let { << definitions >>  } in " ++ showPTermPrec d sc
+  showPTermPrec d (PDict _ fs)
+        = ?hello
   showPTermPrec d (PUpdate _ fs)
         = "record { " ++ showSep ", " (map showUpdate fs) ++ " }"
   showPTermPrec d (PApp _ f a) =

src/Idris/Syntax/Traversals.idr

@@ -45,6 +45,9 @@ mapPTermM f = goPTerm where
       PLocal fc <$> goPDecls xs
                 <*> goPTerm scope
       >>= f
+    goPTerm (PDict fc xs) =
+      PDict fc <$> goPDict xs
+      >>= f
     goPTerm (PUpdate fc xs) =
       PUpdate fc <$> goPFieldUpdates xs
       >>= f
@@ -329,6 +332,10 @@ mapPTermM f = goPTerm where
     goPTerms []        = pure []
     goPTerms (t :: ts) = (::) <$> goPTerm t <*> goPTerms ts
 
+    goPDict : List (PTerm' nm, PTerm' nm) -> Core (List (PTerm' nm, PTerm' nm))
+    goPDict []             = pure []
+    goPDict ((t, s) :: ts) = (::) <$> (MkPair <$> goPTerm t <*> goPTerm s) <*> goPDict ts
+
     goPairedPTerms : List (x, PTerm' nm) -> Core (List (x, PTerm' nm))
     goPairedPTerms []             = pure []
     goPairedPTerms ((a, t) :: ts) =
@@ -420,6 +427,8 @@ mapPTerm f = goPTerm where
       = f $ PCase fc (goPFnOpt <$>  opts) (goPTerm x) (goPClause <$> xs)
     goPTerm (PLocal fc xs scope)
       = f $ PLocal fc (goPDecl <$> xs) (goPTerm scope)
+    goPTerm (PDict fc xs)
+      = f $ PDict fc (goPDict xs)
     goPTerm (PUpdate fc xs)
       = f $ PUpdate fc (goPFieldUpdate <$> xs)
     goPTerm (PApp fc x y)
@@ -504,6 +513,11 @@ mapPTerm f = goPTerm where
     goPTerm (PWithUnambigNames fc ns rhs)
       = f $ PWithUnambigNames fc ns (goPTerm rhs)
 
+    goPDict : List (PTerm' nm, PTerm' nm) -> List (PTerm' nm, PTerm' nm)
+    goPDict [] = []
+    goPDict ((t, s) :: ts)
+        = (goPTerm t, goPTerm s) :: goPDict ts
+
     goPFieldUpdate : PFieldUpdate' nm -> PFieldUpdate' nm
     goPFieldUpdate (PSetField p t)    = PSetField p $ goPTerm t
     goPFieldUpdate (PSetFieldApp p t) = PSetFieldApp p $ goPTerm t
@@ -618,6 +632,7 @@ substFC fc = mapPTerm $ \case
   PLet _ x pat nTy nVal scope alts => PLet fc x pat nTy nVal scope alts
   PCase _ opts x xs => PCase fc opts x xs
   PLocal _ xs scope => PLocal fc xs scope
+  PDict _ xs => PDict fc xs
   PUpdate _ xs => PUpdate fc xs
   PApp _ x y => PApp fc x y
   PWithApp _ x y => PWithApp fc x y

tests/Main.idr

@@ -149,7 +149,9 @@ idrisTests = MkTestPool "Misc" [] Nothing
        -- quantifiers
        "quantifiers001",
        -- unification
-       "unification001"
+       "unification001",
+       -- dictionary syntax
+       "dictionary001"
        ]
 
 typeddTests : IO TestPool

tests/idris2/misc/dictionary001/JSON.idr

@@ -0,0 +1,64 @@
+
+-- JSON DLS
+namespace Map
+  public export
+  data StrMap : Type -> Type where
+    DNil : StrMap a
+    DCons : String -> a -> StrMap a -> StrMap a
+
+data JSON = Object (StrMap JSON) | Array (List JSON) | Number Double | Str String
+
+DCons : String -> JSON -> StrMap JSON -> JSON
+DCons key val m = Object (DCons key val m)
+
+(::) : JSON -> List JSON -> JSON
+(::) x xs = Array (x :: xs)
+
+Nil : JSON
+Nil = Array []
+
+DNil : JSON
+DNil = Object DNil
+
+fromString : String -> JSON
+fromString = Str
+
+fromInteger : Integer -> JSON
+fromInteger = Number . cast
+
+fromDouble : Double -> JSON
+fromDouble = Number
+
+-- Building JSON Values
+
+testEmptyArray : JSON
+testEmptyArray = []
+
+testEmptyObj : JSON
+testEmptyObj = [:=]
+
+testObject : JSON
+testObject = [ "hello" := "world"
+             , "key2" := "value2"
+             ]
+
+testNested : JSON
+testNested =
+  [ "key1" := 3
+  , "key2" := "hello"
+  , "key3" := [1, 2, "hello"]
+  , "key4" := [ "nestedKey1" := "nestedVal1"
+              , "nestedKey2" := [ "nestedArray1", "nestedArray2" ]
+              ]
+  , "key4" :=
+    [ "Nestedkey3" :=
+      [ "NestedKey4" := [:=]
+      , "NestedKey5" :=
+        [ "NestedKey6" := "vlue"
+        , "NestedKey7" := []
+        ]
+      ]
+    , "NestedKey8" := 5
+    ]
+  ]
+

tests/idris2/misc/dictionary001/Main.idr

@@ -0,0 +1,24 @@
+
+data Dict : Type -> Type -> Type where
+  DNil : Dict key val
+  DCons : key -> val -> Dict key val -> Dict key val
+
+testEmpty : Dict String Nat
+testEmpty = [:=]
+
+test1 : Dict String Nat
+test1 = [ "hello" := 1 ]
+
+test2 : Dict String Nat
+test2 = [ "hello" := 1
+        , "world" := 2
+        ]
+
+testLet : Dict String Nat
+testLet = let x := [ "a" := 3 , "b" := 4 ] in x
+
+testPat : Dict String Nat -> Nat
+testPat [:=] = 0
+testPat [ k := v ] = 1
+testPat (DCons k v rest) = 1 + testPat rest
+

tests/idris2/misc/dictionary001/expected

@@ -0,0 +1,2 @@
+1/1: Building Main (Main.idr)
+1/1: Building JSON (JSON.idr)

tests/idris2/misc/dictionary001/run

@@ -0,0 +1,4 @@
+. ../../../testutils.sh
+
+check Main.idr
+check JSON.idr