Skip to content
3 changes: 3 additions & 0 deletions dsl/extdeps/languages/bash/program.dag
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,7 @@ type ShellStmt
| Pipe { left: ShellStmt, right: ShellStmt }

| EnvPrefixed { name: String, value: ShellWord, command: ShellStmt }
| EnvUnsetCmd { name: String, command: ShellStmt }
| WithRedir { stmt: ShellStmt, redir: Redir }

| Heredoc { path: ShellWord, delimiter: String, body: String }
Expand Down Expand Up @@ -136,6 +137,8 @@ fn serialize_stmt(s: ShellStmt) -> String {
concat(serialize_stmt(s: l), concat(" | ", serialize_stmt(s: r)))
EnvPrefixed { name: n, value: v, command: c } =>
concat(n, concat("=", concat(serialize_word(w: v), concat(" ", serialize_stmt(s: c)))))
EnvUnsetCmd { name: n, command: c } =>
concat("env -u ", concat(n, concat(" ", serialize_stmt(s: c))))
WithRedir { stmt: st, redir: rd } =>
concat(serialize_stmt(s: st), concat(" ", serialize_redir(r: rd)))
Exit { code: c } => concat("exit ", to_string(c))
Expand Down
52 changes: 52 additions & 0 deletions src/v2/extdeps/languages/bash.dag
Original file line number Diff line number Diff line change
Expand Up @@ -1822,6 +1822,58 @@ fn bash_stmt_env_prefixed_target_model(name: String, value: String, command: Str
)
}

fn bash_stmt_env_unset_tokens() -> List<ConcreteSyntaxToken> {
[
FixedToken { token_class: ^bash_token_env_unset_prefix },
BoundToken { token_class: ^bash_token_orch_raw, binding: ^bash_stmt_envp_unset_name },
FixedToken { token_class: ^bash_token_env_unset_sp },
BoundToken { token_class: ^bash_token_orch_raw, binding: ^bash_stmt_envp_unset_command }
]
}

data bash_stmt_env_unset_emitted: Node = bash_conj_emitted_from_tokens(
tokens: bash_stmt_env_unset_tokens()
)

fn bash_stmt_env_unset_source_text(name: String, command: String) -> String {
concat("env -u ", concat(name, concat(" ", command)))
}

fn bash_stmt_env_unset_lex() -> LexRules {
phrase_to_lex_rules(p: phrase([
span(text: "env -u ", class: ^bash_token_env_unset_prefix),
span(text: " ", class: ^bash_token_env_unset_sp)
]))
}

fn bash_stmt_env_unset_translation_rules_node() -> Node {
bash_relation_translation_rules_node(
rule_name: ^bash_relation_rule_stmt_env_unset,
lhs: ^bash_production_stmt_env_unset,
tokens: bash_stmt_env_unset_tokens(),
emitted: bash_stmt_env_unset_emitted
)
}

fn bash_stmt_env_unset_binding_spellings(name: String, command: String) -> Map<Symbol, String> {
map_insert(
map_insert(empty_map(), ^bash_stmt_envp_unset_name, name),
^bash_stmt_envp_unset_command, command
)
}

fn bash_stmt_env_unset_target_model(name: String, command: String) -> TargetModel {
bash_make_bound_tokens_target_model(
rules: bash_stmt_env_unset_translation_rules_node(),
source_literal: ^bash_stmt_env_unset_source_literal,
production_name: ^bash_production_stmt_env_unset,
tokens: bash_stmt_env_unset_tokens(),
source_text: bash_stmt_env_unset_source_text(name: name, command: command),
lex: bash_stmt_env_unset_lex(),
binding_spellings: bash_stmt_env_unset_binding_spellings(name: name, command: command)
)
}

fn bash_stmt_if_tokens() -> List<ConcreteSyntaxToken> {
[
FixedToken { token_class: ^bash_token_if_kw },
Expand Down
24 changes: 24 additions & 0 deletions src/v2/workflow/orch_env_lower.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
module v2.workflow.orch_env_lower

import v2.std.orchestration { EnvBinding, EnvSet, EnvUnset }
import v2.std.algebra { FreeMonoid, list_head, list_tail, HeadFound, HeadAbsent, TailFound, TailAbsent }
import extdeps.languages.bash.program { ShellStmt, EnvPrefixed, EnvUnsetCmd, Lit }

fn lower_env_binding(b: EnvBinding, inner: ShellStmt) -> ShellStmt {
match b {
EnvSet { name: n, value: v } => EnvPrefixed { name: n, value: Lit { text: v }, command: inner }
EnvUnset { name: n } => EnvUnsetCmd { name: n, command: inner }
}
}

fn lower_env_bindings(env: FreeMonoid<EnvBinding>, command: ShellStmt) -> ShellStmt {
match list_head(xs: env) {
HeadAbsent => command
HeadFound { value: b } =>
match list_tail(xs: env) {
TailAbsent => lower_env_binding(b: b, inner: command)
TailFound { tail: rest } =>
lower_env_binding(b: b, inner: lower_env_bindings(env: rest, command: command))
}
}
}
3 changes: 2 additions & 1 deletion src/v2/workflow/orchestration_emit.dag
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ import v2.compiler.emit { emit }
import v2.compiler.infer { InferredFacts, InferredTree }
import v2.workflow.shell_emit { emit_shell_stmt }
import extdeps.languages.bash.program { RawLine }
import v2.workflow.orch_env_lower { lower_env_bindings }
import extdeps.communication.medium { Medium }
import v2.extdeps.languages.bash {
orch_run_emitted_command,
Expand Down Expand Up @@ -50,7 +51,7 @@ fn orch_emit_facts_lookup(key: Node) -> Witness<InferredFacts> {
}
}

data orch_run_env_reduction_dissolution_trigger: String = "orchestration_emit Run/Step/Retry path reduces onto emit_shell_stmt: an env-FREE Run lowers to a RawLine carrying the command and is delegated to emit_shell_stmt now (single orch_raw, green path, proven byte-identical by orch_run_empty_env_delegates_to_shell_emit). An env-BEARING Run lowers to an EnvPrefixed over env plus a RawLine command. The emit-kernel String<->List-Int-codepoint straddle that blocked this is now FIXED by grounding String construction into its native realization (free_monoid_to_string in v1_interpreter.rs, sibling to Int<->Nat PR 5428; the held bash multi-orch_raw weld fixtures have been deleted as receipt; program_multi_orch_raw_byte_identical_holds is the green-by-execution proof). The RESIDUAL blocker is a DIFFERENT, modeling-side gap, not the kernel: EnvBinding has EnvUnset (env -u NAME) and FreeMonoid<EnvBinding> is a LIST, but the bash AST EnvPrefixed models only a single name=value prefix with no EnvUnset node, so an env-bearing Run cannot yet be lowered losslessly. It stays on the orch_run_emitted_command single-string render (orch_emit_run_env_welded) until the bash AST grows an env-unset construct and multi-binding nesting. DISSOLVES WHEN the bash EnvPrefixed AST covers EnvUnset + multi-binding env (modeling follow-on landed by gunbc#5846 'Grow bash AST: EnvUnset node + multi-binding env nesting (dissolve orch_emit_run_env_welded)', which depends on this PR's kernel String grounding and dissolves this welded fn outright; no longer kernel-blocked)."
data orch_run_env_reduction_dissolution_trigger: String = "orchestration_emit Run/Step/Retry path reduces onto emit_shell_stmt: an env-FREE Run lowers to a RawLine carrying the command and is delegated to emit_shell_stmt now (single orch_raw, green path, proven byte-identical by orch_run_empty_env_delegates_to_shell_emit). An env-BEARING Run lowers via lower_env_bindings (orch_env_lower.dag) to a nested EnvPrefixed/EnvUnsetCmd tree over the Run.env FreeMonoid with a RawLine command at the leaf, then delegates to emit_shell_stmt. BOTH blockers are now cleared: (1) the emit-kernel String<->List-Int-codepoint straddle is FIXED by #5841 (free_monoid_to_string grounding; program_multi_orch_raw_byte_identical_holds green-by-execution); (2) the bash AST now models EnvUnsetCmd (env -u NAME) and multi-binding via nesting, proven byte-identical by stmt_env_unset_byte_identical_holds and stmt_env_multi_binding_byte_identical_holds (#5846). orch_emit_run_env_welded DISSOLVES WHEN the integration follow-on lands: replace the orch_emit_run_env_welded call with emit_shell_stmt(lower_env_bindings(env: r.env, command: RawLine { text: r.command })) and delete the weld scaffold (deletion-is-receipt). Verify by orch_run_multi_binding_env_emits_correctly (multi EnvSet + EnvUnset oracle) going green-by-execution."

fn orch_emit_run(r: Run) -> Outcome<Medium<String>> {
match list_head(xs: r.env) {
Expand Down
3 changes: 2 additions & 1 deletion src/v2/workflow/orchestration_emit_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -91,6 +91,7 @@ test fn orch_run_empty_env_delegates_to_shell_emit_holds() -> Bool {

test fn orch_run_env_reduction_trigger_recorded_holds() -> Bool {
string_contains(s: orch_run_env_reduction_dissolution_trigger, pattern: "EnvPrefixed")
&& string_contains(s: orch_run_env_reduction_dissolution_trigger, pattern: "straddle")
&& string_contains(s: orch_run_env_reduction_dissolution_trigger, pattern: "EnvUnset")
&& string_contains(s: orch_run_env_reduction_dissolution_trigger, pattern: "lower_env_bindings")
&& string_contains(s: orch_run_env_reduction_dissolution_trigger, pattern: "DISSOLVES WHEN")
}
29 changes: 29 additions & 0 deletions src/v2/workflow/orchestration_stmt_emit_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ import extdeps.languages.bash.program {
AndOr,
Pipe,
EnvPrefixed,
EnvUnsetCmd,
WithRedir,
Heredoc,
AndThen,
Expand Down Expand Up @@ -157,6 +158,34 @@ test fn stmt_env_prefixed_has_teeth_holds() -> Bool {
stmt_differs_from_oracle_of(s: envp_t(), other: EnvPrefixed { name: "TMPDIR", value: Lit { text: "/x" }, command: cmd_true() })
}

fn env_unset_t() -> ShellStmt {
EnvUnsetCmd { name: "TMPDIR", command: cmd_true() }
}

test fn stmt_env_unset_byte_identical_holds() -> Bool {
stmt_emits_oracle(s: env_unset_t())
}

test fn stmt_env_unset_has_teeth_holds() -> Bool {
stmt_differs_from_oracle_of(s: env_unset_t(), other: EnvUnsetCmd { name: "OTHER", command: cmd_true() })
}

fn env_multi_binding_t() -> ShellStmt {
EnvPrefixed {
name: "KEY",
value: Lit { text: "val" },
command: EnvUnsetCmd { name: "TMPDIR", command: cmd_true() }
}
}

test fn stmt_env_multi_binding_byte_identical_holds() -> Bool {
stmt_emits_oracle(s: env_multi_binding_t())
}

test fn stmt_env_multi_binding_has_teeth_holds() -> Bool {
stmt_differs_from_oracle_of(s: env_multi_binding_t(), other: EnvPrefixed { name: "KEY", value: Lit { text: "other" }, command: EnvUnsetCmd { name: "TMPDIR", command: cmd_true() } })
}

fn heredoc_t() -> ShellStmt {
Heredoc { path: Lit { text: "out" }, delimiter: "EOF", body: "hello" }
}
Expand Down
17 changes: 17 additions & 0 deletions src/v2/workflow/shell_emit.dag
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,8 @@ import v2.extdeps.languages.bash {
bash_stmt_with_redir_target_model,
bash_stmt_env_prefixed_emitted,
bash_stmt_env_prefixed_target_model,
bash_stmt_env_unset_emitted,
bash_stmt_env_unset_target_model,
bash_stmt_if_emitted,
bash_stmt_if_target_model,
bash_stmt_heredoc_emitted,
Expand Down Expand Up @@ -50,6 +52,7 @@ import extdeps.languages.bash.program {
AndOr,
Pipe,
EnvPrefixed,
EnvUnsetCmd,
WithRedir,
Heredoc,
Exit,
Expand Down Expand Up @@ -220,6 +223,16 @@ fn emit_stmt_env_prefixed(name: String, value: String, command: String) -> Outco
)
}

fn emit_stmt_env_unset(name: String, command: String) -> Outcome<Medium<String>> {
emit(
tree: InferredTree {
root: bash_stmt_env_unset_emitted,
facts: Map { lookup: shell_emit_facts_lookup }
},
target: bash_stmt_env_unset_target_model(name: name, command: command)
)
}

fn emit_stmt_if(cond: String, body: String) -> Outcome<Medium<String>> {
emit(
tree: InferredTree {
Expand Down Expand Up @@ -390,6 +403,10 @@ fn emit_shell_stmt(s: ShellStmt) -> Outcome<Medium<String>> {
emit_stmt_env_prefixed(name: n, value: mv.carried, command: mc.carried)
})
})
EnvUnsetCmd { name: n, command: c } =>
bind_outcome(o: emit_shell_stmt(s: c), f: fn(mc) {
emit_stmt_env_unset(name: n, command: mc.carried)
})
WithRedir { stmt: st, redir: rd } =>
bind_outcome(o: emit_shell_stmt(s: st), f: fn(mst) {
bind_outcome(o: emit_redir(r: rd), f: fn(mr) {
Expand Down
Loading