From 8adcfada5ba7263f0ef884c6d1ae3bee4949ed09 Mon Sep 17 00:00:00 2001 From: Andre Videla Date: Sat, 20 Jul 2024 00:01:37 +0100 Subject: [PATCH 1/2] Add support for dictionary syntax sugar --- src/Idris/Desugar.idr | 14 ++++++++++++++ src/Idris/Parser.idr | 17 ++++++++++++++++- src/Idris/Pretty.idr | 2 ++ src/Idris/Syntax.idr | 12 ++++++++++++ src/Idris/Syntax/Traversals.idr | 15 +++++++++++++++ tests/Main.idr | 4 +++- tests/idris2/misc/dictionary001/Main.idr | 24 ++++++++++++++++++++++++ tests/idris2/misc/dictionary001/expected | 1 + tests/idris2/misc/dictionary001/run | 3 +++ 9 files changed, 90 insertions(+), 2 deletions(-) create mode 100644 tests/idris2/misc/dictionary001/Main.idr create mode 100644 tests/idris2/misc/dictionary001/expected create mode 100755 tests/idris2/misc/dictionary001/run diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index 02b41723e1..d012d06fd1 100644 --- a/src/Idris/Desugar.idr +++ b/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 "Nil")) + expandDict side ps nilFC ((k, v) :: xs) + = pure $ apply (IVar emptyFC (UN $ Basic "KeyVal")) + [!(desugarB side ps k), !(desugarB side ps v), !(expandDict side ps nilFC xs)] + expandSnocList : {auto s : Ref Syn SyntaxInfo} -> {auto b : Ref Bang BangData} -> diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index fd941c347a..8703c3ae6e 100644 --- a/src/Idris/Parser.idr +++ b/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 <|> 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,19 @@ mutual (x, t, e) <- pure b.val pure (PIfThenElse (boundToFC fname b) x t e) + 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 diff --git a/src/Idris/Pretty.idr b/src/Idris/Pretty.idr index 87313d7a4a..3a4329c3fb 100644 --- a/src/Idris/Pretty.idr +++ b/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)) diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index 3973b1cb4e..d3b70dead6 100644 --- a/src/Idris/Syntax.idr +++ b/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) = diff --git a/src/Idris/Syntax/Traversals.idr b/src/Idris/Syntax/Traversals.idr index c2d45212cd..0f23773a78 100644 --- a/src/Idris/Syntax/Traversals.idr +++ b/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 diff --git a/tests/Main.idr b/tests/Main.idr index 4718724b1f..9758165360 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -149,7 +149,9 @@ idrisTests = MkTestPool "Misc" [] Nothing -- quantifiers "quantifiers001", -- unification - "unification001" + "unification001", + -- dictionary syntax + "dictionary001" ] typeddTests : IO TestPool diff --git a/tests/idris2/misc/dictionary001/Main.idr b/tests/idris2/misc/dictionary001/Main.idr new file mode 100644 index 0000000000..80e5a09195 --- /dev/null +++ b/tests/idris2/misc/dictionary001/Main.idr @@ -0,0 +1,24 @@ + +data Dict : Type -> Type -> Type where + Nil : Dict key val + KeyVal : 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 (KeyVal k v rest) = 1 + testPat rest + diff --git a/tests/idris2/misc/dictionary001/expected b/tests/idris2/misc/dictionary001/expected new file mode 100644 index 0000000000..b2b84aa45a --- /dev/null +++ b/tests/idris2/misc/dictionary001/expected @@ -0,0 +1 @@ +1/1: Building Main (Main.idr) diff --git a/tests/idris2/misc/dictionary001/run b/tests/idris2/misc/dictionary001/run new file mode 100755 index 0000000000..d49bfd87de --- /dev/null +++ b/tests/idris2/misc/dictionary001/run @@ -0,0 +1,3 @@ +. ../../../testutils.sh + +check Main.idr From f33cdc68df8dc2017d40bc9da86501daa788fb55 Mon Sep 17 00:00:00 2001 From: Andre Videla Date: Fri, 26 Jul 2024 01:13:21 +0100 Subject: [PATCH 2/2] add tests for JSON DSL --- src/Idris/Desugar.idr | 4 +- src/Idris/Parser.idr | 7 ++- tests/idris2/misc/dictionary001/JSON.idr | 64 ++++++++++++++++++++++++ tests/idris2/misc/dictionary001/Main.idr | 10 ++-- tests/idris2/misc/dictionary001/expected | 1 + tests/idris2/misc/dictionary001/run | 1 + 6 files changed, 79 insertions(+), 8 deletions(-) create mode 100644 tests/idris2/misc/dictionary001/JSON.idr diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index d012d06fd1..042b75adff 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -609,9 +609,9 @@ mutual {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 "Nil")) + expandDict side ps nilFC [] = pure (IVar nilFC (UN $ Basic "DNil")) expandDict side ps nilFC ((k, v) :: xs) - = pure $ apply (IVar emptyFC (UN $ Basic "KeyVal")) + = pure $ apply (IVar emptyFC (UN $ Basic "DCons")) [!(desugarB side ps k), !(desugarB side ps v), !(expandDict side ps nilFC xs)] expandSnocList diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 8703c3ae6e..8aee3ec359 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -640,7 +640,7 @@ mutual <|> do start <- bounds (symbol "[>") listExpr fname start indents <|> do start <- bounds (symbol "[") - listExpr fname start indents <|> dict fname indents + 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" @@ -894,6 +894,11 @@ 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 diff --git a/tests/idris2/misc/dictionary001/JSON.idr b/tests/idris2/misc/dictionary001/JSON.idr new file mode 100644 index 0000000000..a3623155e7 --- /dev/null +++ b/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 + ] + ] + diff --git a/tests/idris2/misc/dictionary001/Main.idr b/tests/idris2/misc/dictionary001/Main.idr index 80e5a09195..8260c31eaf 100644 --- a/tests/idris2/misc/dictionary001/Main.idr +++ b/tests/idris2/misc/dictionary001/Main.idr @@ -1,10 +1,10 @@ data Dict : Type -> Type -> Type where - Nil : Dict key val - KeyVal : key -> val -> Dict key val -> Dict key val + DNil : Dict key val + DCons : key -> val -> Dict key val -> Dict key val testEmpty : Dict String Nat -testEmpty = [] +testEmpty = [:=] test1 : Dict String Nat test1 = [ "hello" := 1 ] @@ -18,7 +18,7 @@ testLet : Dict String Nat testLet = let x := [ "a" := 3 , "b" := 4 ] in x testPat : Dict String Nat -> Nat -testPat [] = 0 +testPat [:=] = 0 testPat [ k := v ] = 1 -testPat (KeyVal k v rest) = 1 + testPat rest +testPat (DCons k v rest) = 1 + testPat rest diff --git a/tests/idris2/misc/dictionary001/expected b/tests/idris2/misc/dictionary001/expected index b2b84aa45a..91c9fc1b8d 100644 --- a/tests/idris2/misc/dictionary001/expected +++ b/tests/idris2/misc/dictionary001/expected @@ -1 +1,2 @@ 1/1: Building Main (Main.idr) +1/1: Building JSON (JSON.idr) diff --git a/tests/idris2/misc/dictionary001/run b/tests/idris2/misc/dictionary001/run index d49bfd87de..5b0ef072fe 100755 --- a/tests/idris2/misc/dictionary001/run +++ b/tests/idris2/misc/dictionary001/run @@ -1,3 +1,4 @@ . ../../../testutils.sh check Main.idr +check JSON.idr