From 9357abb2790a0c93dbee996e2f4617ae6d427d14 Mon Sep 17 00:00:00 2001 From: Lilleman auf Larv Date: Mon, 5 Oct 2026 15:28:35 +0200 Subject: [PATCH] Move DataType into internal/datatype, aliased by the root, and what a proof knows of a value into internal/proven --- builtins.go | 20 ++- builtins_test.go | 1 - calc.go | 5 +- datatype.go | 29 ++-- format.go | 3 +- internal/datatype/datatype.go | 34 +++++ internal/proven/proven.go | 209 +++++++++++++++++++++++++++ struct.go | 7 +- valueproof.go | 260 +++++----------------------------- 9 files changed, 305 insertions(+), 263 deletions(-) create mode 100644 internal/datatype/datatype.go create mode 100644 internal/proven/proven.go diff --git a/builtins.go b/builtins.go index 3b2155a..9b797a1 100644 --- a/builtins.go +++ b/builtins.go @@ -9,6 +9,7 @@ import ( "strings" "github.com/larvit/fejkdata/internal/drawstate" + "github.com/larvit/fejkdata/internal/proven" ) // maxLen caps sample output lengths (hex, nanoid, base64, digits, upper, lower) @@ -20,9 +21,6 @@ const ( maxDecimals = 1024 ) -// shortestDecimals prints the fewest digits that read back as the same float64. -const shortestDecimals = -1 - // builtins is the registry of {name(args)} functions. Derivations read the digits // emitted so far in the current expansion (place them after their payload); // samples read only the rng. A time-based id (uuid v7, ulid) draws its timestamp @@ -35,8 +33,8 @@ var builtins = withTransforms(map[string]builtin{ "ulid": {arity: 0, prep: sample(ulid)}, "nanoid": {arity: 1, checkArgs: posIntArg, prep: chars(nanoidAlphabet)}, "hex": {arity: 1, checkArgs: posIntArg, prep: chars(hexDigits)}, - "digits": {arity: 1, checkArgs: posIntArg, prep: chars("0123456789"), prints: DataTypeString, proveNumber: func(token string, prints DataType, a []string) proven { - return printing(token, prints, bounded(0, math.Pow(10, float64(atoi(a[0])))-1, true)) + "digits": {arity: 1, checkArgs: posIntArg, prep: chars("0123456789"), prints: DataTypeString, proveNumber: func(token string, prints DataType, a []string) proven.Value { + return proven.Printing(token, prints, proven.Bounded(0, math.Pow(10, float64(atoi(a[0])))-1, true)) }}, "upper": {arity: 1, checkArgs: posIntArg, prep: chars("ABCDEFGHIJKLMNOPQRSTUVWXYZ")}, "lower": {arity: 1, checkArgs: posIntArg, prep: chars("abcdefghijklmnopqrstuvwxyz")}, @@ -49,16 +47,16 @@ var builtins = withTransforms(map[string]builtin{ "int": {arity: 2, checkArgs: intRangeArgs, prep: func(a []string) callFn { lo, span := atoi(a[0]), atoi(a[1])-atoi(a[0])+1 return func(s *drawstate.State, _ string, _ []string) string { return strconv.Itoa(lo + s.IntN(span)) } - }, prints: DataTypeInteger, proveNumber: func(token string, prints DataType, a []string) proven { - return printing(token, prints, bounded(float64(atoi(a[0])), float64(atoi(a[1])), true)) + }, prints: DataTypeInteger, proveNumber: func(token string, prints DataType, a []string) proven.Value { + return proven.Printing(token, prints, proven.Bounded(float64(atoi(a[0])), float64(atoi(a[1])), true)) }}, "float": {arity: 3, checkArgs: floatArgs, prep: func(a []string) callFn { lo, hi, dp := atof(a[0]), atof(a[1]), atoi(a[2]) return func(s *drawstate.State, _ string, _ []string) string { return formatFloat(lo+s.Float64()*(hi-lo), dp) } - }, prints: DataTypeNumber, proveNumber: func(token string, _ DataType, a []string) proven { - return printedNumber(token, bounded(atof(a[0]), atof(a[1]), false), atoi(a[2])) + }, prints: DataTypeNumber, proveNumber: func(token string, _ DataType, a []string) proven.Value { + return proven.PrintedNumber(token, proven.Bounded(atof(a[0]), atof(a[1]), false), atoi(a[2])) }}, "iban": {arity: 1, checkArgs: ibanArg, prep: func(a []string) callFn { cc := a[0] @@ -78,8 +76,8 @@ var builtins = withTransforms(map[string]builtin{ return func(s *drawstate.State, _ string, _ []string) string { return strconv.FormatUint(s.Seq(key), 10) } - }, prints: DataTypeInteger, proveNumber: func(token string, prints DataType, _ []string) proven { - return printing(token, prints, bounded(1, math.MaxInt64, true)) + }, prints: DataTypeInteger, proveNumber: func(token string, prints DataType, _ []string) proven.Value { + return proven.Printing(token, prints, proven.Bounded(1, math.MaxInt64, true)) }}, }) diff --git a/builtins_test.go b/builtins_test.go index 4d2408c..52ba4f4 100644 --- a/builtins_test.go +++ b/builtins_test.go @@ -8,7 +8,6 @@ import ( "strings" "testing" "time" - ) func TestBuiltinIDGenerators(t *testing.T) { diff --git a/calc.go b/calc.go index 6261fec..f921524 100644 --- a/calc.go +++ b/calc.go @@ -9,6 +9,7 @@ import ( "github.com/larvit/fejkdata/internal/drawstate" "github.com/larvit/fejkdata/internal/grammar" + "github.com/larvit/fejkdata/internal/proven" ) // evalCalc evaluates an expression over the operand values expand already read, so it @@ -218,12 +219,12 @@ func parsedCalc(expr string) grammar.Calc { return c } -// calcDecimals is a calc's decimals count, or shortestDecimals where it names none. +// calcDecimals is a calc's decimals count, or proven.ShortestDecimals where it names none. func calcDecimals(args []string) int { if len(args) == 2 { return atoi(args[1]) } - return shortestDecimals + return proven.ShortestDecimals } // calcOperands lists the operands a calc's args read, fields or names. checkCalc reports diff --git a/datatype.go b/datatype.go index 4c3bdb1..5c2a123 100644 --- a/datatype.go +++ b/datatype.go @@ -3,32 +3,21 @@ package fejkdata import ( "errors" "fmt" + + "github.com/larvit/fejkdata/internal/datatype" ) // DataType is what a record column holds, which decides how a record writes its value. -type DataType int +type DataType = datatype.DataType // The datatypes a column declares with "datatype"; a column without one is a string. const ( - DataTypeString DataType = iota - DataTypeInteger - DataTypeNumber - DataTypeBoolean + DataTypeString = datatype.String + DataTypeInteger = datatype.Integer + DataTypeNumber = datatype.Number + DataTypeBoolean = datatype.Boolean ) -var ( - dataTypeNames = [...]string{"string", "integer", "number", "boolean"} - dataTypeNouns = [...]string{"text", "an integer", "a number", "a boolean"} -) - -// String is the datatype as data spells it. -func (d DataType) String() string { - if d < 0 || int(d) >= len(dataTypeNames) { - return fmt.Sprintf("DataType(%d)", int(d)) - } - return dataTypeNames[d] -} - // position is where a JSON value sits, which decides whether it may carry a datatype or // be null. type position int @@ -174,7 +163,7 @@ func disagreement(a *template, da DataType, b *template, db DataType) error { fix, other, want = b, a, da } held := fmt.Sprintf("its items hold %s and %s; a column holds one datatype", da, db) - fits := (&valueProof{}).proveColumnItem(fix).not[want] == "" + fits := (&valueProof{}).proveColumnItem(fix).Not[want] == "" switch kindOf(fix) { case kindDeclares: return errors.New(held) @@ -189,7 +178,7 @@ func disagreement(a *template, da DataType, b *template, db DataType) error { panic(internalError("two text items hold one datatype, so they never disagree")) case kindReads: if !fits { - return fmt.Errorf(`item %q is not %s, the datatype item %q takes from the column it reads; to read that column as text, %s`, fix.format, dataTypeNouns[want], other.format, asText(other)) + return fmt.Errorf(`item %q is not %s, the datatype item %q takes from the column it reads; to read that column as text, %s`, fix.format, datatype.Noun(want), other.format, asText(other)) } } if fix.fromString { // an object may carry a weight, which this spelling would drop diff --git a/format.go b/format.go index c51891a..176ba2e 100644 --- a/format.go +++ b/format.go @@ -6,6 +6,7 @@ import ( "github.com/larvit/fejkdata/internal/drawstate" "github.com/larvit/fejkdata/internal/grammar" + "github.com/larvit/fejkdata/internal/proven" ) // builtin is a format-string function invoked as {name(args)}. It receives the @@ -27,7 +28,7 @@ type builtin struct { // proveNumber bounds the number a call's text reads as, token its body, and says which // datatypes that text is not; set it where every render reads as a finite number, which // makes the call a calc operand, and leave it nil otherwise. - proveNumber func(token string, prints DataType, args []string) proven + proveNumber func(token string, prints DataType, args []string) proven.Value // prints is the datatype a call's text is, handed to proveNumber: DataTypeString where it // reads as a number no column should type, as digits' leading zeros; unset where // proveNumber is nil. diff --git a/internal/datatype/datatype.go b/internal/datatype/datatype.go new file mode 100644 index 0000000..c646aa2 --- /dev/null +++ b/internal/datatype/datatype.go @@ -0,0 +1,34 @@ +// Package datatype names what a record column holds. +package datatype + +import "fmt" + +// DataType is what a record column holds, which decides how a record writes its value. +type DataType int + +// The datatypes a column declares with "datatype"; a column without one is a string. +const ( + String DataType = iota + Integer + Number + Boolean +) + +// Count is the number of datatypes, for an array indexed by one. +const Count = len(names) + +var ( + names = [...]string{"string", "integer", "number", "boolean"} + nouns = [...]string{"text", "an integer", "a number", "a boolean"} +) + +// String is the datatype as data spells it. +func (d DataType) String() string { + if d < 0 || int(d) >= len(names) { + return fmt.Sprintf("DataType(%d)", int(d)) + } + return names[d] +} + +// Noun is the datatype as an error names what a value is. +func Noun(d DataType) string { return nouns[d] } diff --git a/internal/proven/proven.go b/internal/proven/proven.go new file mode 100644 index 0000000..9ed15ff --- /dev/null +++ b/internal/proven/proven.go @@ -0,0 +1,209 @@ +// Package proven holds what a proof knows of every render of a value, and the arithmetic +// that bounds a calc from its operands. +package proven + +import ( + "fmt" + "math" + "regexp" + "strconv" + "strings" + + "github.com/larvit/fejkdata/internal/datatype" + "github.com/larvit/fejkdata/internal/grammar" +) + +// Value is what a proof knows of every render of a node: bounds on the number each +// reads as, and per datatype why some render's text is not one ("" when none). +type Value struct { + Lo, Hi float64 + NonZero float64 // every value is at least this far from zero; 0 when one can be zero + Integral bool + NotOperand string // why some render reads as no finite number, the way calc reads it + Not [datatype.Count]string + Nullable bool // some draw of a column is null +} + +// ShortestDecimals prints the fewest digits that read back as the same float64. +const ShortestDecimals = -1 + +// limit is the largest magnitude a proof accepts as finite, far enough below +// math.MaxFloat64 that rounding in the bounds cannot hide an overflow. +const limit = 1e300 + +// Or is what a proof knows of a render that is either v or w. +func (v Value) Or(w Value) Value { + v.Lo, v.Hi, v.NonZero = min(v.Lo, w.Lo), max(v.Hi, w.Hi), min(v.NonZero, w.NonZero) + v.Integral, v.Nullable = v.Integral && w.Integral, v.Nullable || w.Nullable + if v.NotOperand == "" { + v.NotOperand = w.NotOperand + } + for d := range v.Not { + if v.Not[d] == "" { + v.Not[d] = w.Not[d] + } + } + return v +} + +// Calc bounds a calc expression from its operands, or says why it cannot. +func Calc(expr grammar.CalcNode, operand func(name string) Value) (Value, string) { + v, doubt := bound(expr, operand) + if doubt == "" && !(magnitude(v) <= limit) { + doubt = grammar.CalcText(expr) + " is not proven within 1e300" + } + return v, doubt +} + +func bound(n grammar.CalcNode, operand func(name string) Value) (Value, string) { + switch n := n.(type) { + case grammar.CalcNum: + v := float64(n) + return Bounded(v, v, v == math.Trunc(v)), "" + case grammar.CalcVar: + v := operand(n.Name) + if v.NotOperand != "" { + return Value{}, fmt.Sprintf("operand %q: %s", n.Name, v.NotOperand) + } + return Value{Lo: v.Lo, Hi: v.Hi, NonZero: v.NonZero, Integral: v.Integral}, "" + case grammar.CalcNeg: + v, doubt := bound(n.X, operand) + v.Lo, v.Hi = -v.Hi, -v.Lo + return v, doubt + case grammar.CalcBin: + l, doubt := bound(n.L, operand) + if doubt != "" { + return l, doubt + } + r, doubt := bound(n.R, operand) + if doubt != "" { + return r, doubt + } + return combine(n, l, r) + } + panic(fmt.Sprintf("fejkdata: internal error: calc node %T has no bound", n)) +} + +// combine bounds one operation from the bounds of its sides. +func combine(n grammar.CalcBin, l, r Value) (Value, string) { + var v Value + integral := l.Integral && r.Integral + switch n.Operator { + case '+': + v = Bounded(l.Lo+r.Lo, l.Hi+r.Hi, integral) + case '-': + v = Bounded(l.Lo-r.Hi, l.Hi-r.Lo, integral) + case '*': + v = Bounded(min(l.Lo*r.Lo, l.Lo*r.Hi, l.Hi*r.Lo, l.Hi*r.Hi), max(l.Lo*r.Lo, l.Lo*r.Hi, l.Hi*r.Lo, l.Hi*r.Hi), integral) + v.NonZero = max(v.NonZero, l.NonZero*r.NonZero) + default: + if r.NonZero == 0 { + return v, fmt.Sprintf("divides by %s, which is not proven nonzero", grammar.CalcText(n.R)) + } + m := magnitude(l) / r.NonZero + v = Value{Lo: -m, Hi: m, NonZero: l.NonZero / magnitude(r)} + } + if !(magnitude(v) <= limit) { + return v, grammar.CalcText(n) + " is not proven within 1e300" + } + return v, "" +} + +// Bounded is a number in [lo, hi], its distance from zero read off the bounds. +func Bounded(lo, hi float64, integral bool) Value { + v := Value{Lo: lo, Hi: hi, Integral: integral} + switch { + case lo > 0: + v.NonZero = lo + case hi < 0: + v.NonZero = -hi + } + return v +} + +func magnitude(v Value) float64 { return math.Max(math.Abs(v.Lo), math.Abs(v.Hi)) } + +// PrintedNumber is what a token printing v to dp decimals holds. +func PrintedNumber(token string, v Value, dp int) Value { + if dp == ShortestDecimals { + if v.Integral { // a whole value prints with no point + return printedInteger(token, v) + } + return Printing(token, datatype.Number, v) + } + half, _ := strconv.ParseFloat("5e-"+strconv.Itoa(dp+1), 64) + v = Value{Lo: v.Lo - half, Hi: v.Hi + half, NonZero: math.Max(0, v.NonZero-half), Integral: v.Integral || dp == 0} + if dp == 0 { + return printedInteger(token, v) + } + return Printing(token, datatype.Number, v) +} + +func printedInteger(token string, v Value) Value { + v = Printing(token, datatype.Integer, v) + if !(magnitude(v) < math.MaxInt64) { + v.Not[datatype.Integer] = fmt.Sprintf("{%s} is not proven within int64", token) + } + return v +} + +// Printing is v for a token whose every render is text of datatype prints, with a reason +// against each datatype that text is not. +func Printing(token string, prints datatype.DataType, v Value) Value { + for d := datatype.Integer; d <= datatype.Boolean; d++ { + if prints != d && !(prints == datatype.Integer && d == datatype.Number) { + v.Not[d] = fmt.Sprintf("{%s} prints %s, not %s", token, datatype.Noun(prints), datatype.Noun(d)) + } + } + return v +} + +// Unproven is a render no datatype and no calc can take, for why. +func Unproven(why string) Value { + v := Value{NotOperand: why} + for d := datatype.Integer; d <= datatype.Boolean; d++ { + v.Not[d] = why + } + return v +} + +var ( + integerText = regexp.MustCompile(`^-?(0|[1-9][0-9]*)$`) + numberText = regexp.MustCompile(`^-?(0|[1-9][0-9]*)(\.[0-9]+)?([eE][+-]?[0-9]+)?$`) +) + +// Literal proves fixed text: the number calc reads it as, and each datatype it is. +func Literal(text string) Value { + var v Value + if f, err := strconv.ParseFloat(strings.TrimSpace(text), 64); err != nil || math.IsNaN(f) || math.IsInf(f, 0) { + v.NotOperand = fmt.Sprintf("%q is not a number", text) + } else { + v = Bounded(f, f, f == math.Trunc(f)) + } + if _, err := strconv.ParseInt(text, 10, 64); !integerText.MatchString(text) { + v.Not[datatype.Integer] = fmt.Sprintf("%q is not an integer", text) + } else if err != nil { + v.Not[datatype.Integer] = fmt.Sprintf("%q is past the int64 range", text) + } + if v.NotOperand != "" || !numberText.MatchString(text) { + v.Not[datatype.Number] = fmt.Sprintf("%q is not a number", text) + } + if text != "true" && text != "false" { + v.Not[datatype.Boolean] = fmt.Sprintf("%q is not a boolean", text) + } + return signedZero(text, v) +} + +// signedZero refuses a zero written with a sign as a typed value, naming it unsigned. +func signedZero(text string, v Value) Value { + mantissa, _, _ := strings.Cut(strings.ToLower(text), "e") + if !strings.HasPrefix(text, "-") || v.NotOperand != "" || strings.Trim(mantissa, "-0.") != "" { + return v + } + for _, d := range []datatype.DataType{datatype.Integer, datatype.Number} { + if v.Not[d] == "" { + v.Not[d] = fmt.Sprintf("%q is zero written with a sign; write %q", text, text[1:]) + } + } + return v +} diff --git a/struct.go b/struct.go index 2c7e1ef..013bc8f 100644 --- a/struct.go +++ b/struct.go @@ -11,6 +11,7 @@ import ( "github.com/larvit/fejkdata/internal/drawstate" "github.com/larvit/fejkdata/internal/grammar" + "github.com/larvit/fejkdata/internal/proven" ) // FakeStruct fills the struct v points to. Each exported field tagged `fake:"…"` is a @@ -308,14 +309,14 @@ var columnKinds = map[reflect.Kind]columnKind{ // holds reports whether a field of this kind holds every value v proves. An integer prints // whole, so its bounds round inward first. -func (k columnKind) holds(v proven) bool { +func (k columnKind) holds(v proven.Value) bool { switch k.datatype { case DataTypeString, DataTypeBoolean: return true case DataTypeInteger: - return math.Ceil(v.lo) >= k.lo && math.Floor(v.hi) <= k.hi + return math.Ceil(v.Lo) >= k.lo && math.Floor(v.Hi) <= k.hi } - return v.lo >= k.lo && v.hi <= k.hi + return v.Lo >= k.lo && v.Hi <= k.hi } // fill draws the record into v's tagged fields, then each nested struct as a record of its own. diff --git a/valueproof.go b/valueproof.go index 444c636..58f9a20 100644 --- a/valueproof.go +++ b/valueproof.go @@ -2,31 +2,18 @@ package fejkdata import ( "fmt" - "math" "reflect" - "regexp" "slices" - "strconv" "strings" "github.com/larvit/fejkdata/internal/grammar" + "github.com/larvit/fejkdata/internal/proven" ) -// proven is what a proof knows of every render of a node: bounds on the number each -// reads as, and per datatype why some render's text is not one ("" when none). -type proven struct { - lo, hi float64 - nonZero float64 // every value is at least this far from zero; 0 when one can be zero - integral bool - notOperand string // why some render reads as no finite number, the way calc reads it - not [len(dataTypeNames)]string - nullable bool // some draw of a column is null -} - // valueProof proves what typed columns and their calc operands hold, each node once per scope. type valueProof struct { - memo map[node]proven - columnMemo map[node]proven + memo map[node]proven.Value + columnMemo map[node]proven.Value } // checkDatatype rejects a typed column item some render of which is not text of its datatype, @@ -40,7 +27,7 @@ func (p *valueProof) checkDatatype(path string, n node) error { if r := t.link.readsColumn; r != nil && columnDatatype(r.column) == t.datatype { return fmt.Errorf(`%s: %s takes datatype %s from the column it reads; drop "datatype"`, path, t.format, t.datatype) } - if reason := p.proveColumnItem(t).not[t.datatype]; reason != "" { + if reason := p.proveColumnItem(t).Not[t.datatype]; reason != "" { return fmt.Errorf("%s: datatype %s: %s", path, t.datatype, reason) } return nil @@ -58,7 +45,7 @@ func (p *valueProof) checkField(label string, ft reflect.Type, column node) erro elem := ft if ft.Kind() == reflect.Pointer { elem = ft.Elem() - } else if p.proveColumn(column).nullable { + } else if p.proveColumn(column).Nullable { return fmt.Errorf("%s: its tag can draw null, which %s cannot hold; make it *%s", label, ft, ft) } kind := columnKinds[elem.Kind()] @@ -67,7 +54,7 @@ func (p *valueProof) checkField(label string, ft reflect.Type, column node) erro } for _, it := range items { v := p.proveColumnItem(it) - if reason := v.not[kind.datatype]; reason != "" { + if reason := v.Not[kind.datatype]; reason != "" { return fmt.Errorf("%s (%s): %s", label, ft, reason) } if !kind.holds(v) { @@ -78,7 +65,7 @@ func (p *valueProof) checkField(label string, ft reflect.Type, column node) erro } // proveColumnItem proves a column item: what it renders, or, when it is a column it reads, that column. -func (p *valueProof) proveColumnItem(t *template) proven { +func (p *valueProof) proveColumnItem(t *template) proven.Value { if t.link.readsColumn == nil { return p.prove(t) } @@ -87,35 +74,35 @@ func (p *valueProof) proveColumnItem(t *template) proven { // proveColumn proves a column over what its items draw, a null item marking it null rather than // rendering "". -func (p *valueProof) proveColumn(n node) proven { +func (p *valueProof) proveColumn(n node) proven.Value { if v, done := p.columnMemo[n]; done { return v } if p.columnMemo == nil { - p.columnMemo = map[node]proven{} + p.columnMemo = map[node]proven.Value{} } items, nullable := columnItems(n) - var v proven + var v proven.Value for i, it := range items { if w := p.proveColumnItem(it); i == 0 { v = w } else { - v = v.or(w) + v = v.Or(w) } } - v.nullable = v.nullable || nullable + v.Nullable = v.Nullable || nullable p.columnMemo[n] = v return v } -func (p *valueProof) prove(n node) proven { +func (p *valueProof) prove(n node) proven.Value { if v, done := p.memo[n]; done { return v } if p.memo == nil { - p.memo = map[node]proven{} + p.memo = map[node]proven.Value{} } - var v proven + var v proven.Value switch n := n.(type) { case *choice: v = p.proveUnion(n.items) @@ -126,9 +113,9 @@ func (p *valueProof) prove(n node) proven { case *table: v = p.prove(n.rowNode) case *tableRow: - v = unproven(fmt.Sprintf("%q renders a row of %s, which is composed text", n.t.formatTemplate.format, n.t.segment)) + v = proven.Unproven(fmt.Sprintf("%q renders a row of %s, which is composed text", n.t.formatTemplate.format, n.t.segment)) case *nullItem: - v = unproven(`it reads a null, which renders "" outside its own column`) + v = proven.Unproven(`it reads a null, which renders "" outside its own column`) default: panic(internalError("prove has no case for node %T", n)) } @@ -137,59 +124,44 @@ func (p *valueProof) prove(n node) proven { } // proveCells proves a table column over every cell it may render. -func (p *valueProof) proveCells(c *tableColumn) proven { - var v proven +func (p *valueProof) proveCells(c *tableColumn) proven.Value { + var v proven.Value for r := 0; r < c.t.rowCount(); r++ { - var w proven + var w proven.Value if cell := c.t.cellTemplate(r, c.i); cell != nil { w = p.prove(cell) } else { - w = literalValue(c.t.cell(r, c.i)) + w = proven.Literal(c.t.cell(r, c.i)) } if r == 0 { v = w } else { - v = v.or(w) + v = v.Or(w) } } return v } -func (p *valueProof) proveUnion(nodes []node) proven { +func (p *valueProof) proveUnion(nodes []node) proven.Value { v := p.prove(nodes[0]) for _, n := range nodes[1:] { - v = v.or(p.prove(n)) - } - return v -} - -// or is what a proof knows of a render that is either v or w. -func (v proven) or(w proven) proven { - v.lo, v.hi, v.nonZero = min(v.lo, w.lo), max(v.hi, w.hi), min(v.nonZero, w.nonZero) - v.integral, v.nullable = v.integral && w.integral, v.nullable || w.nullable - if v.notOperand == "" { - v.notOperand = w.notOperand - } - for d := range v.not { - if v.not[d] == "" { - v.not[d] = w.not[d] - } + v = v.Or(p.prove(n)) } return v } // proveTemplate proves a template that renders one value: fixed text, or a format that is // one token alone. -func (p *valueProof) proveTemplate(t *template) proven { +func (p *valueProof) proveTemplate(t *template) proven.Value { lit, fixed := t.fixedText() switch { case t.repeat != 1: - return unproven(fmt.Sprintf("%q carries a repeat, which composes text rather than one value", t.format)) + return proven.Unproven(fmt.Sprintf("%q carries a repeat, which composes text rather than one value", t.format)) case fixed: - return literalValue(lit) + return proven.Literal(lit) case len(t.compiled.ops) != 1: - v := unproven(notOneValue(t.format, typedCalls)) - v.notOperand = notOneValue(t.format, operandCalls) + v := proven.Unproven(notOneValue(t.format, typedCalls)) + v.NotOperand = notOneValue(t.format, operandCalls) return v } o := t.compiled.ops[0] @@ -206,131 +178,19 @@ func (p *valueProof) proveTemplate(t *template) proven { case builtins[name].proveNumber != nil: return builtins[name].proveNumber(body, builtins[name].prints, args) case isTransform: - return unproven(fmt.Sprintf("{%s} rewrites text rather than printing a value; write the values it would print", body)) + return proven.Unproven(fmt.Sprintf("{%s} rewrites text rather than printing a value; write the values it would print", body)) } - return printing(body, DataTypeString, proven{notOperand: fmt.Sprintf("{%s} prints text, not a number", body)}) + return proven.Printing(body, DataTypeString, proven.Value{NotOperand: fmt.Sprintf("{%s} prints text, not a number", body)}) } -func (p *valueProof) proveCalc(o op) proven { +func (p *valueProof) proveCalc(o op) proven.Value { body, args := o.Body, o.Args - expr := parsedCalc(args[0]).Expr nodes := operandNodes(o) - v, doubt := p.proveExpr(expr, func(name string) proven { return p.proveUnion(nodes(name)) }) - if doubt == "" && !(magnitude(v) <= calcLimit) { - doubt = grammar.CalcText(expr) + " is not proven within 1e300" - } + v, doubt := proven.Calc(parsedCalc(args[0]).Expr, func(name string) proven.Value { return p.proveUnion(nodes(name)) }) if doubt != "" { - return unproven(fmt.Sprintf("{%s}: %s", body, doubt)) + return proven.Unproven(fmt.Sprintf("{%s}: %s", body, doubt)) } - return printedNumber(body, v, calcDecimals(args)) -} - -// calcLimit is the largest magnitude a proof accepts as finite, far enough below -// math.MaxFloat64 that rounding in the bounds cannot hide an overflow. -const calcLimit = 1e300 - -// proveExpr bounds a calc expression from its operands, or says why it cannot. -func (p *valueProof) proveExpr(n grammar.CalcNode, operand func(name string) proven) (proven, string) { - switch n := n.(type) { - case grammar.CalcNum: - v := float64(n) - return bounded(v, v, v == math.Trunc(v)), "" - case grammar.CalcVar: - v := operand(n.Name) - if v.notOperand != "" { - return proven{}, fmt.Sprintf("operand %q: %s", n.Name, v.notOperand) - } - return proven{lo: v.lo, hi: v.hi, nonZero: v.nonZero, integral: v.integral}, "" - case grammar.CalcNeg: - v, doubt := p.proveExpr(n.X, operand) - v.lo, v.hi = -v.hi, -v.lo - return v, doubt - case grammar.CalcBin: - l, doubt := p.proveExpr(n.L, operand) - if doubt != "" { - return l, doubt - } - r, doubt := p.proveExpr(n.R, operand) - if doubt != "" { - return r, doubt - } - return combine(n, l, r) - } - panic(internalError("calc node %T has no bound", n)) -} - -// combine bounds one operation from the bounds of its sides. -func combine(n grammar.CalcBin, l, r proven) (proven, string) { - var v proven - integral := l.integral && r.integral - switch n.Operator { - case '+': - v = bounded(l.lo+r.lo, l.hi+r.hi, integral) - case '-': - v = bounded(l.lo-r.hi, l.hi-r.lo, integral) - case '*': - v = bounded(min(l.lo*r.lo, l.lo*r.hi, l.hi*r.lo, l.hi*r.hi), max(l.lo*r.lo, l.lo*r.hi, l.hi*r.lo, l.hi*r.hi), integral) - v.nonZero = max(v.nonZero, l.nonZero*r.nonZero) - default: - if r.nonZero == 0 { - return v, fmt.Sprintf("divides by %s, which is not proven nonzero", grammar.CalcText(n.R)) - } - m := magnitude(l) / r.nonZero - v = proven{lo: -m, hi: m, nonZero: l.nonZero / magnitude(r)} - } - if !(magnitude(v) <= calcLimit) { - return v, grammar.CalcText(n) + " is not proven within 1e300" - } - return v, "" -} - -// bounded is a number in [lo, hi], its distance from zero read off the bounds. -func bounded(lo, hi float64, integral bool) proven { - v := proven{lo: lo, hi: hi, integral: integral} - switch { - case lo > 0: - v.nonZero = lo - case hi < 0: - v.nonZero = -hi - } - return v -} - -func magnitude(v proven) float64 { return math.Max(math.Abs(v.lo), math.Abs(v.hi)) } - -// printedNumber is what a token printing v to dp decimals holds. -func printedNumber(token string, v proven, dp int) proven { - if dp == shortestDecimals { - if v.integral { // a whole value prints with no point - return printedInteger(token, v) - } - return printing(token, DataTypeNumber, v) - } - half, _ := strconv.ParseFloat("5e-"+strconv.Itoa(dp+1), 64) - v = proven{lo: v.lo - half, hi: v.hi + half, nonZero: math.Max(0, v.nonZero-half), integral: v.integral || dp == 0} - if dp == 0 { - return printedInteger(token, v) - } - return printing(token, DataTypeNumber, v) -} - -func printedInteger(token string, v proven) proven { - v = printing(token, DataTypeInteger, v) - if !(magnitude(v) < math.MaxInt64) { - v.not[DataTypeInteger] = fmt.Sprintf("{%s} is not proven within int64", token) - } - return v -} - -// printing is v for a token whose every render is text of datatype prints, with a reason -// against each datatype that text is not. -func printing(token string, prints DataType, v proven) proven { - for d := DataTypeInteger; d <= DataTypeBoolean; d++ { - if prints != d && !(prints == DataTypeInteger && d == DataTypeNumber) { - v.not[d] = fmt.Sprintf("{%s} prints %s, not %s", token, dataTypeNouns[prints], dataTypeNouns[d]) - } - } - return v + return proven.PrintedNumber(body, v, calcDecimals(args)) } var typedCalls, operandCalls = numberCalls(false), numberCalls(true) @@ -351,53 +211,3 @@ func numberCalls(text bool) string { func notOneValue(format, calls string) string { return fmt.Sprintf("%q is not one value; write one literal or one %s, or read one", format, calls) } - -// unproven is a render no datatype and no calc can take, for why. -func unproven(why string) proven { - v := proven{notOperand: why} - for d := DataTypeInteger; d <= DataTypeBoolean; d++ { - v.not[d] = why - } - return v -} - -var ( - integerText = regexp.MustCompile(`^-?(0|[1-9][0-9]*)$`) - numberText = regexp.MustCompile(`^-?(0|[1-9][0-9]*)(\.[0-9]+)?([eE][+-]?[0-9]+)?$`) -) - -// literalValue proves fixed text: the number calc reads it as, and each datatype it is. -func literalValue(text string) proven { - var v proven - if f, err := strconv.ParseFloat(strings.TrimSpace(text), 64); err != nil || math.IsNaN(f) || math.IsInf(f, 0) { - v.notOperand = fmt.Sprintf("%q is not a number", text) - } else { - v = bounded(f, f, f == math.Trunc(f)) - } - if _, err := strconv.ParseInt(text, 10, 64); !integerText.MatchString(text) { - v.not[DataTypeInteger] = fmt.Sprintf("%q is not an integer", text) - } else if err != nil { - v.not[DataTypeInteger] = fmt.Sprintf("%q is past the int64 range", text) - } - if v.notOperand != "" || !numberText.MatchString(text) { - v.not[DataTypeNumber] = fmt.Sprintf("%q is not a number", text) - } - if text != "true" && text != "false" { - v.not[DataTypeBoolean] = fmt.Sprintf("%q is not a boolean", text) - } - return signedZero(text, v) -} - -// signedZero refuses a zero written with a sign as a typed value, naming it unsigned. -func signedZero(text string, v proven) proven { - mantissa, _, _ := strings.Cut(strings.ToLower(text), "e") - if !strings.HasPrefix(text, "-") || v.notOperand != "" || strings.Trim(mantissa, "-0.") != "" { - return v - } - for _, d := range []DataType{DataTypeInteger, DataTypeNumber} { - if v.not[d] == "" { - v.not[d] = fmt.Sprintf("%q is zero written with a sign; write %q", text, text[1:]) - } - } - return v -}