Skip to content

feat(lift-go): model unkeyed slice/array composite literals #1562

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

Merged
TSavo merged 1 commit into from
May 27, 2026
+32 −1
Merged

feat(lift-go): model unkeyed slice/array composite literals #1562

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
33 changes: 32 additions & 1 deletion implementations/go/provekit-lift-go/lift.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -742,7 +742,7 @@ func (l *lifter) liftExpr(expr ast.Expr) (exprResult, error) {
sort := irSort(l.info.Types[e].Type)
return exprResult{term: ir.MakeCtor("go:index", []ir.IrTerm{base.term, index.term}, sort), alg: op("go:index", base.alg, index.alg), sort: sort}, nil
case *ast.CompositeLit:
return exprResult{}, errAt(e.Pos(), "composite literals are not modeled")
return l.liftCompositeLit(e)
case *ast.FuncLit:
return exprResult{}, errAt(e.Pos(), "function literals are not modeled")
case *ast.ChanType:
Expand Down Expand Up @@ -796,6 +796,37 @@ func (l *lifter) liftCall(call *ast.CallExpr) (exprResult, error) {
return exprResult{term: ir.MakeCtor("go:call", termArgs, sort), alg: alg, sort: sort}, nil
}

// liftCompositeLit models unkeyed slice/array literals (`[]T{e0, e1, …}`):
// elements lift positionally into a `go:slice-literal` ctor. Struct, map, and
// keyed literals stay unmodeled — their shape isn't represented in the IR, and
// inventing one would be a lossy lift dressed as exact. This is enough to lift
// a serializer that emits bytes in a given (non-canonical) order, which a
// consumer's canonical-order precondition does not discharge.
func (l *lifter) liftCompositeLit(e *ast.CompositeLit) (exprResult, error) {
if _, isArray := e.Type.(*ast.ArrayType); !isArray {
return exprResult{}, errAt(e.Pos(), "only slice/array composite literals are modeled")
}
var elemTerms []ir.IrTerm
var elemAlgs []any
for _, elt := range e.Elts {
if _, keyed := elt.(*ast.KeyValueExpr); keyed {
return exprResult{}, errAt(e.Pos(), "keyed composite literals are not modeled")
}
lifted, err := l.liftExpr(elt)
if err != nil {
return exprResult{}, err
}
elemTerms = append(elemTerms, lifted.term)
elemAlgs = append(elemAlgs, lifted.alg)
}
sort := irSort(l.info.Types[e].Type)
return exprResult{
term: ir.MakeCtor("go:slice-literal", elemTerms, sort),
alg: op("go:slice-literal", elemAlgs...),
Comment on lines +824 to +825
Copy link
Copy Markdown

@chatgpt-codex-connector chatgpt-codex-connector Bot May 27, 2026

Choose a reason for hiding this comment

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

P2 Badge Add compiler support for slice literal terms

When a lifted function body or standalone function-contract contains []T{...}, this new go:slice-literal ctor is now emitted into the post/body term, but goExprFromIRTerm in implementations/go/provekit-lift-go/compile.go has no case for it. That makes newly lifted IR fail CompileBody/bare-body round trips, and compiling a contract-only IR for a non-void function can drop the return expression instead of reconstructing the slice literal. Please add the matching compile case or keep refusing these literals until the source compiler can consume the new ctor.

Useful? React with 👍 / 👎.

sort: sort,
}, nil
}

func (l *lifter) liftTarget(expr ast.Expr) (any, error) {
switch e := expr.(type) {
case *ast.Ident:
Expand Down
Loading