Pattern matching for literals#353
Open
lidiapodoluk wants to merge 3 commits into
Open
Conversation
There was a problem hiding this comment.
Pull request overview
This PR implements literal pattern matching (e.g. | 0 => ..., | "x" => ..., | 'a' => ...) across the DBL pipeline, addressing #137 by enabling matches on exact literal values (including nested literal patterns via the general pattern machinery).
Changes:
- Introduces a dedicated
literaltype and newELit/PLitnodes in surface/unification/effect-core ASTs. - Extends type inference + effect inference to type-check/infer literals and literal patterns.
- Extends pattern-match compilation to handle literal columns by lowering to equality checks, and adds an OK test.
Reviewed changes
Copilot reviewed 22 out of 22 changed files in this pull request and generated 13 comments.
Show a summary per file
| File | Description |
|---|---|
| test/ok/ok0177_literalMatch.fram | Adds an OK test for literal patterns (ints/strings/chars/tuples). |
| src/TypeInference/RecDefs.ml | Updates rec-def preparation/type-guessing logic to account for ELit / PLit. |
| src/TypeInference/Pattern.ml | Adds typing for literal patterns (PLit) and literal-to-type mapping. |
| src/TypeInference/ParamResolve.ml | Updates special implicit parameters to use ELit. |
| src/TypeInference/Expr.ml | Changes expression literal inference to route through ELit. |
| src/ToCore/Main.ml | Updates ConE→Core translation for literals via a shared tr_lit. |
| src/Lang/UnifPriv/Syntax.ml | Introduces literal and switches expression literals to ELit; adds PLit. |
| src/Lang/UnifPriv/Ren.ml | Adds renaming support for PLit. |
| src/Lang/Unif.mli | Updates public Unif interface for literal, ELit, and PLit. |
| src/Lang/Surface.ml | Introduces literal and switches surface literals to ELit; adds PLit. |
| src/Lang/ConEPriv/Syntax.ml | Introduces literal and ELit in ConE private syntax. |
| src/Lang/ConEPriv/SExprPrinter.ml | Updates printing for ELit via a shared literal printer. |
| src/Lang/ConE.mli | Updates ConE public interface for literal and ELit. |
| src/EffectInference/PatternMatch.ml | Adds literal-column compilation by lowering to dbl_eq* extern equality checks. |
| src/EffectInference/Pattern.mli | Adds PLit to effect-inference internal pattern type. |
| src/EffectInference/Pattern.ml | Adds checking/translation for literal patterns into ConE patterns. |
| src/EffectInference/ExprUtils.ml | Updates rec-body update logic to treat ELit as a base expression. |
| src/EffectInference/Expr.ml | Switches effect inference literal handling to ELit. |
| src/DblParser/Import.ml | Updates injected ~__modulePath__ to use ELit (EStr ...). |
| src/DblParser/Desugar.ml | Desugars raw literals into ELit and raw literal patterns into PLit. |
| src/DblParser/Attributes.ml | Preserves PLit while applying visibility attributes to patterns. |
| src/ConETypeErase.ml | Updates ConE type erasure to translate literals via a shared literal translator. |
Comments suppressed due to low confidence (1)
test/ok/ok0177_literalMatch.fram:37
- This test file exercises top-level literal patterns, but the motivating issue (#137) is about literals nested inside constructor patterns (e.g.
NNInt 0). Adding a small nested-literal test here will prevent regressions.
let _ = f 3
let _ = fs "compiler"
let _ = fc 'x'
let _ = fp 1 2
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+41
to
+47
| begin match l with | ||
| | ENum n -> | ||
| { er_expr = make (T.ELit(ENum n)); | ||
| er_type = Infered (T.Type.t_var T.BuiltinType.tv_int); | ||
| er_effect = Pure; | ||
| er_constr = [] | ||
| } |
Comment on lines
+48
to
+53
| | ENum64 n -> | ||
| { er_expr = make (T.ELit(ENum64 n)); | ||
| er_type = Infered (T.Type.t_var T.BuiltinType.tv_int64); | ||
| er_effect = Pure; | ||
| er_constr = [] | ||
| } |
Comment on lines
+54
to
+59
| | EStr s -> | ||
| { er_expr = make (T.ELit(EStr s)); | ||
| er_type = Infered (T.Type.t_var T.BuiltinType.tv_string); | ||
| er_effect = Pure; | ||
| er_constr = [] | ||
| } |
Comment on lines
+60
to
+65
| | EChr c -> | ||
| { er_expr = make (T.ELit(EChr c)); | ||
| er_type = Infered (T.Type.t_var T.BuiltinType.tv_char); | ||
| er_effect = Pure; | ||
| er_constr = [] | ||
| } |
Comment on lines
+318
to
+321
| | ENum n -> | ||
| let tp = T.Type.t_var (T.BuiltinType.tv_int) in | ||
| (T.ELit(ENum n), tp, return_pure eff_req) | ||
|
|
Comment on lines
245
to
250
| let (param_expr, param_tvar) = match iname with | ||
| | "~__line__" -> | ||
| (make (T.ENum pos.pos_start_line), T.BuiltinType.tv_int) | ||
| (make (T.ELit(ENum pos.pos_start_line)), T.BuiltinType.tv_int) | ||
| | "~__file__" -> | ||
| (make (T.EStr pos.pos_fname), T.BuiltinType.tv_string) | ||
| (make (T.ELit(EStr pos.pos_fname)), T.BuiltinType.tv_string) | ||
| | _ -> Error.fatal (Error.cannot_resolve_implicit ~pos iname) in |
Comment on lines
+310
to
+313
| | ENum n -> make (PLit (ENum n)) | ||
| | ENum64 n -> make (PLit (ENum64 n)) | ||
| | EStr s -> make (PLit (EStr s)) | ||
| | EChr c -> make (PLit (EChr c)) |
Comment on lines
+549
to
+552
| | ENum n -> make (ELit(ENum n)) | ||
| | ENum64 n -> make (ELit(ENum64 n)) | ||
| | EStr s -> make (ELit(EStr s)) | ||
| | EChr c -> make (ELit(EChr c)) |
Comment on lines
+119
to
121
| (** Literals *) | ||
| and literal = | ||
| | ENum of int |
Comment on lines
+201
to
+214
| begin match l with | ||
| | ENum n -> | ||
| check_lit_scheme (T.Type.t_var T.BuiltinType.tv_int); | ||
| (PLit (ENum n), PEnv.empty) | ||
| | ENum64 n -> | ||
| check_lit_scheme (T.Type.t_var T.BuiltinType.tv_int64); | ||
| (PLit (ENum64 n), PEnv.empty) | ||
| | EStr s -> | ||
| check_lit_scheme (T.Type.t_var T.BuiltinType.tv_string); | ||
| (PLit (EStr s), PEnv.empty) | ||
| | EChr c -> | ||
| check_lit_scheme (T.Type.t_var T.BuiltinType.tv_char); | ||
| (PLit (EChr c), PEnv.empty) | ||
| end |
Xaro8
reviewed
Jun 23, 2026
| er_effect = Pure; | ||
| er_constr = [] | ||
| } | ||
| | ELit l -> |
Xaro8
reviewed
Jun 23, 2026
| let (param_expr, param_tvar) = match iname with | ||
| | "~__line__" -> | ||
| (make (T.ENum pos.pos_start_line), T.BuiltinType.tv_int) | ||
| (make (T.ELit(ENum pos.pos_start_line)), T.BuiltinType.tv_int) |
There was a problem hiding this comment.
I am not sure, but copilot may be onto something with T.Enum
Xaro8
reviewed
Jun 23, 2026
| (make (T.ELit(ENum pos.pos_start_line)), T.BuiltinType.tv_int) | ||
| | "~__file__" -> | ||
| (make (T.EStr pos.pos_fname), T.BuiltinType.tv_string) | ||
| (make (T.ELit(EStr pos.pos_fname)), T.BuiltinType.tv_string) |
Xaro8
reviewed
Jun 23, 2026
| (** ADT-shape proof for option type *) | ||
|
|
||
| (** Literals *) | ||
| and literal = |
Xaro8
reviewed
Jun 23, 2026
There was a problem hiding this comment.
Maybe a good idea would be to output expectations, for tasting framework
Xaro8
reviewed
Jun 23, 2026
Xaro8
left a comment
Xaro8
left a comment
There was a problem hiding this comment.
Overall looks alright to me, I left some minor comments :)
I do not feel competent enough to be really sure if PatternMatch is correct, but it looks thoughtful.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #137, now with requested changes added