Documentation
¶
Overview ¶
Package gen lowers a checked bork package to Go source.
The output is a lowering, not a one-to-one translation: bork is expression-oriented, so `if` and blocks that produce values become Go statements writing to temporaries. Go code is built with go/ast and printed with go/printer, so it is always syntactically valid.
Index ¶
- func ArtifactDefinition(fn *check.Func) ([]byte, error)
- func ArtifactSignature(fn *check.Func) string
- func ClosedProofProgram(files []*syntax.File, info *check.Info, queries []check.Query) ([]byte, error)
- func ComptimeBatchProgram(files []*syntax.File, info *check.Info, nodes []*check.Comptime, ...) ([]byte, error)
- func ComptimeFunctions(files []*syntax.File, info *check.Info, node *check.Comptime, ...) []*check.Func
- func ComptimeProgram(files []*syntax.File, info *check.Info, node *check.Comptime) ([]byte, error)
- func DebugPackage(files []*syntax.File, info *check.Info, generatedPath string) ([]byte, error)
- func EvalComptimeProgram(files []*syntax.File, info *check.Info, queries []check.Query) ([]byte, error)
- func EvalProgram(files []*syntax.File, info *check.Info, queries []check.Query) ([]byte, error)
- func Package(files []*syntax.File, info *check.Info) ([]byte, error)
- func StdValidatorArtifact(files []*syntax.File, info *check.Info, runtimeSource []byte) ([]byte, error)
- func Tests(files []*syntax.File, info *check.Info, autoProperties bool) ([]byte, error)
- func TestsWith(files []*syntax.File, info *check.Info, opts TestOptions) ([]byte, error)
- type TestOptions
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
func ArtifactDefinition ¶
ArtifactDefinition omits the syntax back-reference to the owning instance.
func ArtifactSignature ¶
func ClosedProofProgram ¶
func ClosedProofProgram(files []*syntax.File, info *check.Info, queries []check.Query) ([]byte, error)
ClosedProofProgram emits only statically audited predicate selections. It excludes unrelated instances, package initializers and foreign types; callers must also certify the emitted runtime support before reusing any result.
func ComptimeBatchProgram ¶
func ComptimeBatchProgram(files []*syntax.File, info *check.Info, nodes []*check.Comptime, packages map[*check.PackageBinding]*check.Comptime) ([]byte, error)
ComptimeBatchProgram exposes checked recipes through a request protocol. A getter can only read a result the driver has already evaluated and validated.
func ComptimeFunctions ¶
func ComptimeFunctions(files []*syntax.File, info *check.Info, node *check.Comptime, dictionaries ...*check.Dict) []*check.Func
ComptimeFunctions includes helpers referenced by trusted Go bodies as well as ordinary typed calls. Generation uses the same reachability inventory.
func ComptimeProgram ¶
ComptimeProgram executes one checked recipe and writes a versioned value to a compiler-owned file. stdout is never part of the result protocol.
func DebugPackage ¶ added in v0.0.14
DebugPackage preserves runtime statement locations through Go's DWARF line directives. Runtime helpers point back to the retained generated source.
func EvalComptimeProgram ¶
func EvalComptimeProgram(files []*syntax.File, info *check.Info, queries []check.Query) ([]byte, error)
EvalComptimeProgram uses explicit-computation restrictions for proof execution.
func EvalProgram ¶
EvalProgram generates a program that runs the given predicate calls on constants and prints each result (true or false) on its own line. The compiler uses it to evaluate predicates at compile time.
func StdValidatorArtifact ¶
func StdValidatorArtifact(files []*syntax.File, info *check.Info, runtimeSource []byte) ([]byte, error)
StdValidatorArtifact derives native implementation code from the same typed library functions as comptime. Runtime source is type-checked alongside the artifact so call guards preserve single/multiple-result signatures.
func Tests ¶
Tests generates a Go program that runs the package's tests and reports the results. It is built in test mode: facts the compiler takes on trust (`trust`, and what `unsafe go` functions promise) are checked at runtime, so a wrong one fails the test that reaches it. Inference rules, also taken on trust, get property tests that look for counterexamples (see ruleTest).
A test with parameters is a property test (see propertyTest), and with autoProperties, so is every function whose promises are trusted (see autoPropertyCandidate).
Types ¶
type TestOptions ¶
type TestOptions struct {
// AutoProperties property-tests the functions whose promises are
// trusted (see autoPropertyCandidate).
AutoProperties bool
// Hermetic fails, without running it, every test that can reach a
// function doing net in Go code with no mock of it in force (see
// check.Info.Unmocked).
Hermetic bool
}
TestOptions are how Tests builds the test program.
Source Files
¶
- ambient.go
- bindcontext.go
- caller.go
- classes.go
- comptime.go
- data.go
- debug.go
- derive.go
- embed.go
- fanin.go
- gen.go
- goaliases.go
- gobind.go
- gomirror.go
- goopaque.go
- gostruct.go
- hash.go
- helpers.go
- invariantdiagnostics.go
- labels.go
- lazy.go
- lazyfields.go
- mocks.go
- parallel.go
- properties.go
- prune.go
- rules.go
- schema.go
- seq.go
- show.go
- signals.go
- stdvalidators.go
- tests.go
- types.go
- valueops.go
Directories
¶
| Path | Synopsis |
|---|---|
|
cmd
|
|
|
genstdvalidators
command
genstdvalidators derives compiler-owned artifacts from embedded standard code.
|
genstdvalidators derives compiler-owned artifacts from embedded standard code. |