Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
18 commits
Select commit Hold shift + click to select a range
918f13a
WIP: R3 gate #19: numeric aliases align to refinements
briansrls May 9, 2026
1c309a4
Merge remote-tracking branch 'origin/main' into session/snappy-tern-885
briansrls May 9, 2026
d133ee7
WIP: R3 gate #19: numeric aliases align to refinements
briansrls May 9, 2026
fdf5acf
Merge remote-tracking branch 'origin/main' into session/snappy-tern-885
briansrls May 9, 2026
5082452
fix(v3): derive int literal witnesses from Compose<Int, MachineWidth>
briansrls May 9, 2026
24dc031
chore(v3): refresh parse_corpus_manifest after std integer/float pars…
briansrls May 9, 2026
e44069a
Merge remote-tracking branch 'origin/main' into session/snappy-tern-885
briansrls May 9, 2026
e3671fa
Merge remote-tracking branch 'origin/main' into session/snappy-tern-885
briansrls May 9, 2026
ce78ff4
Merge remote-tracking branch 'origin/main' into session/snappy-tern-885
briansrls May 9, 2026
d16c916
Merge remote-tracking branch 'origin/main' into session/snappy-tern-885
briansrls May 9, 2026
e115773
Merge remote-tracking branch 'origin/main' into session/snappy-tern-885
briansrls May 9, 2026
a4276ef
docs(briefs): annotate dissolved R4 carve line for CI discipline check
briansrls May 9, 2026
ff2ad9a
merge: origin/main; reconcile TC3 brief Cross-Pattern-A line with R4 …
briansrls May 9, 2026
fe8628f
Merge remote-tracking branch 'origin/main' into session/snappy-tern-885
briansrls May 9, 2026
ff6d6fc
Merge remote-tracking branch 'origin/main' into session/snappy-tern-885
briansrls May 9, 2026
22bb815
Merge remote-tracking branch 'origin/main' into session/snappy-tern-885
briansrls May 9, 2026
656e187
Merge remote-tracking branch 'origin/main' into session/snappy-tern-885
briansrls May 9, 2026
91830b0
WIP: R3 gate #19: numeric aliases align to refinements
briansrls May 9, 2026
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
17 changes: 7 additions & 10 deletions dsl/std/float.dag
Original file line number Diff line number Diff line change
@@ -1,21 +1,18 @@
// std/float.dag -- Floating-point types as algebraic compositions.
//
// Fixed-width floats are width refinements of a single approximate-float
// algebra axis (`Ieee754Float`) composed with `MachineWidth<Word*>` (R3 §1.8
// gate #19 `numeric_aliases_align_to_refinements`). IEEE 754 rounding still
// breaks pure field laws — approximate semantics remain Grounding's concern.
// Fixed-width floats are width refinements of `ApproximateField<Word*>` (see
// `src/v3/std/approximate_field.dag`) composed with `MachineWidth<Word*>` (R3 §1.8
// gate #19 `numeric_aliases_align_to_refinements`). Approximate field laws subsume
// IEEE-style rounding / NaN policy axes — grounding remains target-specific.

module std.float

import std.bit { Word32, Word64 }
import std.machine_constraints { Compose, MachineWidth }
import v3.std.approximate_field { ApproximateField }

// Opaque substrate carrier for the IEEE-754 approximate-float algebra axis
// (width-independent at this layer; specialization via Compose).
type Ieee754Float

type Float32 = Compose<Ieee754Float, MachineWidth<Word32>>
type Float64 = Compose<Ieee754Float, MachineWidth<Word64>>
type Float32 = Compose<ApproximateField<Word32>, MachineWidth<Word32>>
type Float64 = Compose<ApproximateField<Word64>, MachineWidth<Word64>>

// Default alias
type Float = Float64
19,242 changes: 9,634 additions & 9,608 deletions src/v3/compiler/src/bootstrap_generated.rs

Large diffs are not rendered by default.

18,270 changes: 9,148 additions & 9,122 deletions src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs

Large diffs are not rendered by default.

15 changes: 13 additions & 2 deletions src/v3/compiler/src/bootstrap_regen_fresh.rs
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@ const MACHINE_CONSTRAINTS_DAG: &str = include_str!("../../../../dsl/std/machine_
const NAT_DAG: &str = include_str!("../../../../dsl/std/nat.dag");
const INTEGER_DAG: &str = include_str!("../../../../dsl/std/integer.dag");
const RATIONAL_DAG: &str = include_str!("../../../../dsl/std/rational.dag");
const APPROXIMATE_FIELD_DAG: &str = include_str!("../../../v3/std/approximate_field.dag");
const FLOAT_DAG: &str = include_str!("../../../../dsl/std/float.dag");
const STRING_TYPE_DAG: &str = include_str!("../../../../dsl/std/string_type.dag");
const TYPES_DAG: &str = include_str!("../../../../dsl/std/types.dag");
Expand Down Expand Up @@ -82,13 +83,22 @@ pub fn compile_std_bootstrap_dag() -> Dag {

pub fn compile_full_bootstrap_dag_from_std_seed(std_seed: Dag) -> Dag {
let mut dag = std_seed;
load_runtime_bootstrap_authorities(&mut dag, &[], &[]);
// `approximate_field.dag` is part of `std_fixtures()` so `dsl/std/float.dag` can
// import `ApproximateField`; skip the staged copy to avoid duplicate declarations.
load_runtime_bootstrap_authorities(&mut dag, &["src/v3/std/approximate_field.dag"], &[]);
dag
}

pub fn compile_full_bootstrap_without_parse_surface_dag_from_std_seed(std_seed: Dag) -> Dag {
let mut dag = std_seed;
load_runtime_bootstrap_authorities(&mut dag, &["src/v3/std/parse_surface.dag"], &[]);
load_runtime_bootstrap_authorities(
&mut dag,
&[
"src/v3/std/parse_surface.dag",
"src/v3/std/approximate_field.dag",
],
&[],
);
dag
}

Expand Down Expand Up @@ -145,6 +155,7 @@ fn std_fixtures() -> &'static [(&'static str, &'static str)] {
("dsl/std/nat.dag", NAT_DAG),
("dsl/std/integer.dag", INTEGER_DAG),
("dsl/std/rational.dag", RATIONAL_DAG),
("src/v3/std/approximate_field.dag", APPROXIMATE_FIELD_DAG),
("dsl/std/float.dag", FLOAT_DAG),
("dsl/std/types.dag", TYPES_DAG),
("dsl/std/string_type.dag", STRING_TYPE_DAG),
Expand Down
Loading