From d8302a5dc12654bd617093187177deb4794fc87c Mon Sep 17 00:00:00 2001 From: Nikolai Kudasov Date: Fri, 19 Apr 2024 17:57:47 +0300 Subject: [PATCH] Support tuple patterns (desugared to left-associative nested pairs) --- rzk/grammar/Syntax.cf | 3 ++- rzk/src/Language/Rzk/Free/Syntax.hs | 9 ++++++++- rzk/src/Language/Rzk/Syntax/Abs.hs | 2 ++ rzk/src/Language/Rzk/Syntax/Doc.txt | 1 + rzk/src/Language/Rzk/Syntax/Par.y | 1 + rzk/src/Language/Rzk/Syntax/Print.hs | 1 + rzk/src/Language/Rzk/Syntax/Skel.hs | 1 + rzk/src/Language/Rzk/VSCode/Tokenize.hs | 1 + 8 files changed, 17 insertions(+), 2 deletions(-) diff --git a/rzk/grammar/Syntax.cf b/rzk/grammar/Syntax.cf index cfabd6fed..c0f0207ee 100644 --- a/rzk/grammar/Syntax.cf +++ b/rzk/grammar/Syntax.cf @@ -60,6 +60,7 @@ SomeSectionName. SectionName ::= VarIdent ; PatternUnit. Pattern ::= "unit" ; PatternVar. Pattern ::= VarIdent ; PatternPair. Pattern ::= "(" Pattern "," Pattern ")" ; +PatternTuple. Pattern ::= "(" Pattern "," Pattern "," [Pattern] ")" ; separator nonempty Pattern "" ; -- Parameter introduction (for lambda abstractions) @@ -78,7 +79,7 @@ ParamVarShapeDeprecated. ParamDecl ::= "{" "(" Pattern ":" Term ")" "|" Term "}" paramVarShapeDeprecated. ParamDecl ::= "{" Pattern ":" Term "|" Term "}" ; define paramVarShapeDeprecated pat cube tope = ParamVarShapeDeprecated pat cube tope ; --- Parameter declaration for Sigma types +-- Parameter declaration for Sigma types SigmaParam. SigmaParam ::= Pattern ":" Term ; separator nonempty SigmaParam "," ; diff --git a/rzk/src/Language/Rzk/Free/Syntax.hs b/rzk/src/Language/Rzk/Free/Syntax.hs index 2a13f360a..2812341c6 100644 --- a/rzk/src/Language/Rzk/Free/Syntax.hs +++ b/rzk/src/Language/Rzk/Free/Syntax.hs @@ -173,6 +173,12 @@ toScopePattern pat bvars = toTerm $ \z -> bindings (Rzk.PatternVar _loc (Rzk.VarIdent _ "_")) _ = [] bindings (Rzk.PatternVar _loc x) t = [(varIdent x, t)] bindings (Rzk.PatternPair _loc l r) t = bindings l (First t) <> bindings r (Second t) + bindings (Rzk.PatternTuple loc p1 p2 ps) t = bindings (desugarTuple loc (reverse ps) p2 p1) t + +desugarTuple loc ps p2 p1 = + case ps of + [] -> Rzk.PatternPair loc p1 p2 + pLast : ps' -> Rzk.PatternPair loc (desugarTuple loc ps' p2 p1) pLast toTerm :: (VarIdent -> Term a) -> Rzk.Term -> Term a toTerm bvars = go @@ -280,7 +286,7 @@ toTerm bvars = go Rzk.TypeSigma _loc pat tA tB -> TypeSigma (patternVar pat) (go tA) (toScopePattern pat bvars tB) - Rzk.TypeSigmaNested _loc ((Rzk.SigmaParam _ patA tA) : (Rzk.SigmaParam _ patB tB) : ps) tN -> + Rzk.TypeSigmaNested _loc ((Rzk.SigmaParam _ patA tA) : (Rzk.SigmaParam _ patB tB) : ps) tN -> go (Rzk.TypeSigmaNested _loc ((Rzk.SigmaParam _loc patX tX) : ps) tN) where patX = Rzk.PatternPair _loc patA patB @@ -325,6 +331,7 @@ patternToTerm = ptt Rzk.PatternVar loc x -> Rzk.Var loc x Rzk.PatternPair loc l r -> Rzk.Pair loc (ptt l) (ptt r) Rzk.PatternUnit loc -> Rzk.Unit loc + Rzk.PatternTuple loc p1 p2 ps -> patternToTerm (desugarTuple loc (reverse ps) p2 p1) unsafeTermToPattern :: Rzk.Term -> Rzk.Pattern unsafeTermToPattern = ttp diff --git a/rzk/src/Language/Rzk/Syntax/Abs.hs b/rzk/src/Language/Rzk/Syntax/Abs.hs index a88cb75ee..9fc1e8034 100644 --- a/rzk/src/Language/Rzk/Syntax/Abs.hs +++ b/rzk/src/Language/Rzk/Syntax/Abs.hs @@ -72,6 +72,7 @@ data Pattern' a = PatternUnit a | PatternVar a (VarIdent' a) | PatternPair a (Pattern' a) (Pattern' a) + | PatternTuple a (Pattern' a) (Pattern' a) [Pattern' a] deriving (C.Eq, C.Ord, C.Show, C.Read, C.Functor, C.Foldable, C.Traversable, C.Data, C.Typeable, C.Generic) type Param = Param' BNFC'Position @@ -258,6 +259,7 @@ instance HasPosition Pattern where PatternUnit p -> p PatternVar p _ -> p PatternPair p _ _ -> p + PatternTuple p _ _ _ -> p instance HasPosition Param where hasPosition = \case diff --git a/rzk/src/Language/Rzk/Syntax/Doc.txt b/rzk/src/Language/Rzk/Syntax/Doc.txt index 965865777..ddc0465ba 100644 --- a/rzk/src/Language/Rzk/Syntax/Doc.txt +++ b/rzk/src/Language/Rzk/Syntax/Doc.txt @@ -97,6 +97,7 @@ All other symbols are terminals. | //Pattern// | -> | ``unit`` | | **|** | //VarIdent// | | **|** | ``(`` //Pattern// ``,`` //Pattern// ``)`` + | | **|** | ``(`` //Pattern// ``,`` //Pattern// ``,`` //[Pattern]// ``)`` | //[Pattern]// | -> | //Pattern// | | **|** | //Pattern// //[Pattern]// | //Param// | -> | //Pattern// diff --git a/rzk/src/Language/Rzk/Syntax/Par.y b/rzk/src/Language/Rzk/Syntax/Par.y index 51bc42bbb..78ec45ac6 100644 --- a/rzk/src/Language/Rzk/Syntax/Par.y +++ b/rzk/src/Language/Rzk/Syntax/Par.y @@ -234,6 +234,7 @@ Pattern : 'unit' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.PatternUnit (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1))) } | VarIdent { (fst $1, Language.Rzk.Syntax.Abs.PatternVar (fst $1) (snd $1)) } | '(' Pattern ',' Pattern ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.PatternPair (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4)) } + | '(' Pattern ',' Pattern ',' ListPattern ')' { (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1), Language.Rzk.Syntax.Abs.PatternTuple (uncurry Language.Rzk.Syntax.Abs.BNFC'Position (tokenLineCol $1)) (snd $2) (snd $4) (snd $6)) } ListPattern :: { (Language.Rzk.Syntax.Abs.BNFC'Position, [Language.Rzk.Syntax.Abs.Pattern]) } ListPattern diff --git a/rzk/src/Language/Rzk/Syntax/Print.hs b/rzk/src/Language/Rzk/Syntax/Print.hs index b51d6a178..b99a4e8e1 100644 --- a/rzk/src/Language/Rzk/Syntax/Print.hs +++ b/rzk/src/Language/Rzk/Syntax/Print.hs @@ -198,6 +198,7 @@ instance Print (Language.Rzk.Syntax.Abs.Pattern' a) where Language.Rzk.Syntax.Abs.PatternUnit _ -> prPrec i 0 (concatD [doc (showString "unit")]) Language.Rzk.Syntax.Abs.PatternVar _ varident -> prPrec i 0 (concatD [prt 0 varident]) Language.Rzk.Syntax.Abs.PatternPair _ pattern_1 pattern_2 -> prPrec i 0 (concatD [doc (showString "("), prt 0 pattern_1, doc (showString ","), prt 0 pattern_2, doc (showString ")")]) + Language.Rzk.Syntax.Abs.PatternTuple _ pattern_1 pattern_2 patterns -> prPrec i 0 (concatD [doc (showString "("), prt 0 pattern_1, doc (showString ","), prt 0 pattern_2, doc (showString ","), prt 0 patterns, doc (showString ")")]) instance Print [Language.Rzk.Syntax.Abs.Pattern' a] where prt _ [] = concatD [] diff --git a/rzk/src/Language/Rzk/Syntax/Skel.hs b/rzk/src/Language/Rzk/Syntax/Skel.hs index 71ccee72a..a48dd7381 100644 --- a/rzk/src/Language/Rzk/Syntax/Skel.hs +++ b/rzk/src/Language/Rzk/Syntax/Skel.hs @@ -71,6 +71,7 @@ transPattern x = case x of Language.Rzk.Syntax.Abs.PatternUnit _ -> failure x Language.Rzk.Syntax.Abs.PatternVar _ varident -> failure x Language.Rzk.Syntax.Abs.PatternPair _ pattern_1 pattern_2 -> failure x + Language.Rzk.Syntax.Abs.PatternTuple _ pattern_1 pattern_2 patterns -> failure x transParam :: Show a => Language.Rzk.Syntax.Abs.Param' a -> Result transParam x = case x of diff --git a/rzk/src/Language/Rzk/VSCode/Tokenize.hs b/rzk/src/Language/Rzk/VSCode/Tokenize.hs index 0a60bdee1..eeb739767 100644 --- a/rzk/src/Language/Rzk/VSCode/Tokenize.hs +++ b/rzk/src/Language/Rzk/VSCode/Tokenize.hs @@ -63,6 +63,7 @@ tokenizePattern = \case PatternVar _loc var -> mkToken var SemanticTokenTypes_Parameter [SemanticTokenModifiers_Declaration] PatternPair _loc l r -> foldMap tokenizePattern [l, r] pat@(PatternUnit _loc) -> mkToken pat SemanticTokenTypes_EnumMember [SemanticTokenModifiers_Declaration] + PatternTuple _loc p1 p2 ps -> foldMap tokenizePattern (p1 : p2 : ps) tokenizeTope :: Term -> [SemanticTokenAbsolute] tokenizeTope = tokenizeTerm' (Just SemanticTokenTypes_String)