Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
64 changes: 64 additions & 0 deletions src/v2/compiler/complexity_gate/comprep_pipeline_bridge.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,64 @@
// Scope: shared tokenize→parse→normalize→resolve bridge for COMPREP test-subject producers.
// Single authority for the pipeline chain; per-fn producers pass their GrammarRoot +
// production_name and call comprep_source_resolved_root to obtain the resolved Arrow Node.
// Consumers: wave-1 subject producers (can migrate), D2 rewrite-rule test-subject producers.
// Design: DESIGN.md §2 horizontal — one pipeline path, derived per subject (not forked per fn).
// Hardwired: dag_language_model_wave1 (MVP1 .dag surface). New media → new bridge or param.

module v2.test.complexity_gate.comprep_pipeline_bridge

import v2.compiler.normalize { normalize }
import v2.compiler.parse { ValidatedGrammarRoot, grammar_validate_for_parse, parse_production_tree }
import v2.compiler.resolve { resolve }
import v2.compiler.tokenize { tokenize }
import v2.extdeps.languages.dag { dag_language_model_wave1 }
import v2.std.collection { List }
import v2.std.compilers.lexing { Token }
import v2.std.diagnostic { Accepted, Outcome, Rejected, bind_outcome, port_locus }
import v2.std.grammar { GrammarRoot, ParseTree }
import v2.std.node { Node, Symbol }
import v2.std.text { String }


// Run the four-stage comprep pipeline on a source snippet:
// tokenize → validate+parse (parse_root, production_name) → normalize → resolve
// Returns the resolved Arrow Node, ready for body extraction by the caller.
//
// file: diagnostic locus symbol — callers pass their own (e.g. ^d2_nested_slow_form_file).
// parse_root / production_name: the grammar this snippet is parsed under — callers construct.
// Grammar validation is fail-closed before any tokenize work.
fn comprep_source_resolved_root(
source_text: String,
parse_root: GrammarRoot,
production_name: Symbol,
file: Symbol
) -> Outcome<Node> {
let lm = dag_language_model_wave1()
match grammar_validate_for_parse(
root: parse_root,
at: port_locus(port: ^comprep_pipeline_bridge_grammar_locus)
) {
Rejected { diagnostics: r } => Rejected { diagnostics: r }
Accepted { value: validated, diagnostics: _ } =>
bind_outcome(
o: tokenize(text: source_text, file: file, rules: lm.lex),
f: fn(token_stream) {
bind_outcome(
o: parse_production_tree(
tokens: token_stream.tokens,
validated: validated,
production_name: production_name
),
f: fn(parsed) {
bind_outcome(
o: normalize(parse_tree: parsed),
f: fn(normalized) {
resolve(tree: normalized, lm: lm)
}
)
}
)
}
)
}
}
43 changes: 43 additions & 0 deletions src/v2/compiler/complexity_gate/comprep_pipeline_bridge_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
// Status: EXECUTED Bool witness — comprep bridge resolves MVP1 loop source without error.
//
// Discriminating: goes RED if any stage of the tokenize→parse→normalize→resolve chain
// in comprep_source_resolved_root breaks (bad grammar root, tokenize error, parse failure,
// normalize or resolve fault). A trivially-passing bridge would let stage regressions hide.
//
// Single test function: Accepted on valid source confirms the full four-stage pipeline is live.
// Grammar-gap note: nested-Cardinality source text is deferred to the Rule-1 follow-up PR
// where hand-constructed Nodes drive the rewrite-rule witnesses.

module v2.test.complexity_gate.comprep_pipeline_bridge_test

import v2.test.complexity_gate.comprep_pipeline_bridge { comprep_source_resolved_root }
import v2.extdeps.languages.dag {
dag_grammar_production_mvp1_fn_loop,
dag_mvp1_loop_source_text
}
import v2.std.collection { Set }
import v2.std.diagnostic { Accepted, Rejected }
import v2.std.grammar { GrammarProduction, GrammarRoot }
import v2.std.logic { Bool }

fn comprep_bridge_test_loop_grammar_root() -> GrammarRoot {
GrammarRoot {
start: ^dag_production_mvp1_fn_loop,
productions: [dag_grammar_production_mvp1_fn_loop()],
sync_tokens: Set { member: fn(_) { false } }
}
}

// Full pipeline resolves the MVP1 loop source without fault.
// Goes RED if tokenize, parse, normalize, or resolve fails for any reason.
test fn comprep_pipeline_bridge_resolves_loop_source() -> Bool {
match comprep_source_resolved_root(
source_text: dag_mvp1_loop_source_text,
parse_root: comprep_bridge_test_loop_grammar_root(),
production_name: ^dag_production_mvp1_fn_loop,
file: ^comprep_pipeline_bridge_test_file
) {
Accepted { value: _, diagnostics: _ } => true
Rejected { diagnostics: _ } => false
}
}
6 changes: 5 additions & 1 deletion src/v2/lens/cost.dag
Original file line number Diff line number Diff line change
Expand Up @@ -391,7 +391,11 @@ fn compose_child_cost(
) -> SymbolicCost {
match mode {
SequentialCost => symbolic_sequential(a: acc, b: child)
AlternativeCost => symbolic_max(a: acc, b: child)
// Per-alternative factor = max(acc, max(branch, one decision step)). symbolic_max
// floors ONLY zero: max(acc, max(0,1))=max(acc,1) — a zero-cost branch still costs
// one decision; max(acc, max(1,1))=max(acc,1) and max(acc, max(linear,1))=max(acc,linear)
// leave unit/linear branches unchanged. symbolic_max itself absorbing zero untouched.
AlternativeCost => symbolic_max(a: acc, b: symbolic_max(a: child, b: unit_cost()))
// Per-iteration factor = max(body, one control step). symbolic_max floors ONLY
// zero: max(0,1)=1 (empty body -> O(n)); max(1,1)=1 and max(linear,1)=linear leave
// unit/linear bodies unchanged vs plain symbolic_product. Absorbing zero untouched.
Expand Down
71 changes: 71 additions & 0 deletions src/v2/lens/cost/disj_alternative_floor_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,71 @@
// Status: EXECUTED Bool witness — all-zero Disj arms still cost at least O(1).
//
// Pins the cost-lens AlternativeCost floor (cost.dag `compose_child_cost` AlternativeCost arm).
// Two checks together pin the CORRECT fix uniquely:
// (1) bug-fix: cost_lens(Disj([Atom, Atom])) projects unit_cost(), NOT zero_cost() —
// selecting between alternatives has a non-trivial cost even when every branch body is free.
// (2) control: symbolic_max's zero-absorption is PRESERVED — symbolic_max(0, 0) == 0.
// (2) is what distinguishes the right fix (symbolic_max(child, unit) floor at the
// AlternativeCost layer) from the wrong one (removing zero-absorption inside symbolic_max):
// BOTH make (1) green, but the wrong fix makes (2) RED.

module v2.test.lens_cost.disj_alternative_floor

import v2.lens.cost {
cost_lens,
symbolic_max,
unit_cost,
zero_cost
}
import v2.std.logic { Bool }
import v2.std.node {
Atom,
Disj,
Edge,
Node,
Positional,
SyntheticOccurrence,
TypeNode
}
import v2.std.witness { Holds }

// Two zero-cost Disj arms (Atom base cost = zero_cost).
data disj_floor_arm_a: Node = Node {
kind: TypeNode { connective: Atom { identity: ^disj_floor_arm_a_atom } },
children: [],
occurrence_id: SyntheticOccurrence
}

data disj_floor_arm_b: Node = Node {
kind: TypeNode { connective: Atom { identity: ^disj_floor_arm_b_atom } },
children: [],
occurrence_id: SyntheticOccurrence
}

// Disj with two zero-cost arms — the structure cost_lens folds.
data disj_floor_input: Node = Node {
kind: TypeNode { connective: Disj },
children: [
Edge { label: Positional, target: disj_floor_arm_a },
Edge { label: Positional, target: disj_floor_arm_b }
],
occurrence_id: SyntheticOccurrence
}

// (1) Bug-fix: a Disj over zero-cost branches projects unit_cost(), not zero_cost().
fn disj_floor_projects_unit() -> Bool {
match cost_lens(n: disj_floor_input) {
Holds { value: actual } => actual == unit_cost()
_ => false
}
}

// (2) Control: symbolic_max keeps absorbing zero — max(0, 0) == 0. The wrong fix
// (removing zero-absorption inside symbolic_max) makes this return unit_cost(), going RED here.
fn symbolic_max_absorbs_zero() -> Bool {
symbolic_max(a: zero_cost(), b: zero_cost()) == zero_cost()
}

test fn disj_alternative_floor_holds() -> Bool {
disj_floor_projects_unit() && symbolic_max_absorbs_zero()
}