Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add syntax sugar for nested sigma-types #183

Merged
merged 8 commits into from
May 2, 2024
Merged

Add syntax sugar for nested sigma-types #183

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
f378bca
Implemented syntactic sugar for nested sigma types
geffk2 Apr 19, 2024
1fe743d
Corrected overlapping rule
geffk2 Apr 19, 2024
fbaf19c
Added ASCII and Unicode rules
geffk2 Apr 19, 2024
b96c92c
Added lsp tokenization
geffk2 Apr 19, 2024
df9ed14
Support tuple patterns (desugared to left-associative nested pairs)
fizruk Apr 19, 2024
418c65b
Added tuple patterns
geffk2 Apr 26, 2024
1197dc1
Made naming consistent for Sigma Tuples
geffk2 May 1, 2024
48b1b3a
Merge branch 'develop' into syntax-sugar-sigma-types
fizruk May 2, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 10 additions & 0 deletions rzk/grammar/Syntax.cf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -78,6 +79,10 @@ ParamVarShapeDeprecated. ParamDecl ::= "{" "(" Pattern ":" Term ")" "|" Term "}"
paramVarShapeDeprecated. ParamDecl ::= "{" Pattern ":" Term "|" Term "}" ;
define paramVarShapeDeprecated pat cube tope = ParamVarShapeDeprecated pat cube tope ;

-- Parameter declaration for Sigma types
SigmaParam. SigmaParam ::= Pattern ":" Term ;
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ideally, I would like to reuse Param, but I think this should be a separate change, since Param allows shapes and we do not support shape types yet (see #50).

separator nonempty SigmaParam "," ;

Restriction. Restriction ::= Term "↦" Term ;
separator nonempty Restriction "," ;

Expand Down Expand Up @@ -106,6 +111,7 @@ RecOrDeprecated. Term7 ::= "recOR" "(" Term "," Term "," Term "," Term ")" ;
-- Types
TypeFun. Term1 ::= ParamDecl "→" Term1 ;
TypeSigma. Term1 ::= "Σ" "(" Pattern ":" Term ")" "," Term1 ;
TypeSigmaTuple. Term1 ::= "Σ" "(" SigmaParam "," [SigmaParam] ")" "," Term1 ;
TypeUnit. Term7 ::= "Unit" ;
TypeId. Term1 ::= Term2 "=_{" Term "}" Term2 ;
TypeIdSimple. Term1 ::= Term2 "=" Term2 ;
Expand All @@ -115,6 +121,7 @@ TypeExtensionDeprecated. Term7 ::= "<" ParamDecl "→" Term ">" ;
App. Term6 ::= Term6 Term7 ;
Lambda. Term1 ::= "\\" [Param] "→" Term1 ;
Pair. Term7 ::= "(" Term "," Term ")" ;
Tuple. Term7 ::= "(" Term "," Term "," [Term] ")" ;
First. Term6 ::= "π₁" Term7 ;
Second. Term6 ::= "π₂" Term7 ;
Unit. Term7 ::= "unit" ;
Expand Down Expand Up @@ -149,6 +156,7 @@ ASCII_TopeOr. Term2 ::= Term3 "\\/" Term2 ;

ASCII_TypeFun. Term1 ::= ParamDecl "->" Term1 ;
ASCII_TypeSigma. Term1 ::= "Sigma" "(" Pattern ":" Term ")" "," Term1 ;
ASCII_TypeSigmaTuple. Term1 ::= "Sigma" "(" SigmaParam "," [SigmaParam] ")" "," Term1 ;

ASCII_Lambda. Term1 ::= "\\" [Param] "->" Term1 ;
ASCII_Restriction. Restriction ::= Term "|->" Term ;
Expand All @@ -161,4 +169,6 @@ ASCII_Second. Term6 ::= "second" Term7 ;
-- Alternative Unicode syntax rules

unicode_TypeSigmaAlt. Term1 ::= "∑" "(" Pattern ":" Term ")" "," Term1 ; -- \sum
unicode_TypeSigmaTupleAlt. Term1 ::= "∑" "(" SigmaParam "," [SigmaParam] ")" "," Term1 ;
define unicode_TypeSigmaAlt pat fst snd = TypeSigma pat fst snd ;
define unicode_TypeSigmaTupleAlt par pars t = TypeSigmaTuple par pars t ;
20 changes: 18 additions & 2 deletions rzk/src/Language/Rzk/Free/Syntax.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -209,7 +215,6 @@ toTerm bvars = go
(Rzk.TypeFun loc (Rzk.ParamTermShape loc' (patternToTerm pat) cube tope) ret)
t@(Rzk.Lambda loc ((Rzk.ParamPatternShapeDeprecated loc' pat cube tope):params) body) -> deprecated t
(Rzk.Lambda loc ((Rzk.ParamPatternShape loc' [pat] cube tope):params) body)

-- ASCII versions
Rzk.ASCII_CubeUnitStar loc -> go (Rzk.CubeUnitStar loc)
Rzk.ASCII_Cube2_0 loc -> go (Rzk.Cube2_0 loc)
Expand All @@ -223,6 +228,7 @@ toTerm bvars = go

Rzk.ASCII_TypeFun loc param ret -> go (Rzk.TypeFun loc param ret)
Rzk.ASCII_TypeSigma loc pat ty ret -> go (Rzk.TypeSigma loc pat ty ret)
Rzk.ASCII_TypeSigmaTuple loc p ps tN -> go (Rzk.TypeSigmaTuple loc p ps tN)
Rzk.ASCII_Lambda loc pat ret -> go (Rzk.Lambda loc pat ret)
Rzk.ASCII_TypeExtensionDeprecated loc shape type_ -> go (Rzk.TypeExtensionDeprecated loc shape type_)
Rzk.ASCII_First loc term -> go (Rzk.First loc term)
Expand Down Expand Up @@ -256,6 +262,8 @@ toTerm bvars = go
Rzk.Unit _loc -> Unit
Rzk.App _loc f x -> App (go f) (go x)
Rzk.Pair _loc l r -> Pair (go l) (go r)
Rzk.Tuple _loc p1 p2 (p:ps) -> go (Rzk.Tuple _loc (Rzk.Pair _loc p1 p2) p ps)
Rzk.Tuple _loc p1 p2 [] -> go (Rzk.Pair _loc p1 p2)
Rzk.First _loc term -> First (go term)
Rzk.Second _loc term -> Second (go term)
Rzk.Refl _loc -> Refl Nothing
Expand All @@ -280,11 +288,18 @@ toTerm bvars = go
Rzk.TypeSigma _loc pat tA tB ->
TypeSigma (patternVar pat) (go tA) (toScopePattern pat bvars tB)

Rzk.TypeSigmaTuple _loc (Rzk.SigmaParam _ patA tA) ((Rzk.SigmaParam _ patB tB) : ps) tN ->
go (Rzk.TypeSigmaTuple _loc (Rzk.SigmaParam _loc patX tX) ps tN)
where
patX = Rzk.PatternPair _loc patA patB
tX = Rzk.TypeSigma _loc patA tA tB
Rzk.TypeSigmaTuple _loc (Rzk.SigmaParam _ pat tA) [] tB -> go (Rzk.TypeSigma _loc pat tA tB)

Rzk.Lambda _loc [] body -> go body
Rzk.Lambda _loc (Rzk.ParamPattern _ pat : params) body ->
Lambda (patternVar pat) Nothing (toScopePattern pat bvars (Rzk.Lambda _loc params body))
Rzk.Lambda _loc (Rzk.ParamPatternType _ [] _ty : params) body ->
go (Rzk.Lambda _loc params body)
go (Rzk.Lambda _loc params body)
Rzk.Lambda _loc (Rzk.ParamPatternType _ (pat:pats) ty : params) body ->
Lambda (patternVar pat) (Just (go ty, Nothing))
(toScopePattern pat bvars (Rzk.Lambda _loc (Rzk.ParamPatternType _loc pats ty : params) body))
Expand Down Expand Up @@ -317,6 +332,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
Expand Down
19 changes: 19 additions & 0 deletions rzk/src/Language/Rzk/Syntax/Abs.hs
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

8 changes: 8 additions & 0 deletions rzk/src/Language/Rzk/Syntax/Doc.txt
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

24 changes: 24 additions & 0 deletions rzk/src/Language/Rzk/Syntax/Par.y
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

Loading
Loading