Support tuple patterns (desugared to left-associative nested pairs)

rzk-lang · Apr 19, 2024 · d8302a5 · d8302a5
1 parent f378bca
commit d8302a5
Show file tree

Hide file tree

Showing 8 changed files with 17 additions and 2 deletions.
diff --git 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
@@ -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
diff --git a/rzk/src/Language/Rzk/Syntax/Doc.txt b/rzk/src/Language/Rzk/Syntax/Doc.txt
diff --git a/rzk/src/Language/Rzk/Syntax/Par.y b/rzk/src/Language/Rzk/Syntax/Par.y
diff --git a/rzk/src/Language/Rzk/Syntax/Print.hs b/rzk/src/Language/Rzk/Syntax/Print.hs
diff --git a/rzk/src/Language/Rzk/Syntax/Skel.hs b/rzk/src/Language/Rzk/Syntax/Skel.hs
diff --git 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)