Add exact units, signed time, and interval type-system core

.github/workflows/ci-edric-types.yml

@@ -0,0 +1,24 @@
+name: Edric type-system smoke
+
+on:
+  pull_request:
+    paths:
+      - '_/examples/units-time-intervals/**'
+      - '_/tests/idris2/basic/edric007/**'
+      - '_/edric'
+      - '.github/workflows/ci-edric-types.yml'
+  push:
+    paths:
+      - '_/examples/units-time-intervals/**'
+      - '_/tests/idris2/basic/edric007/**'
+      - '_/edric'
+      - '.github/workflows/ci-edric-types.yml'
+
+jobs:
+  units-time-intervals:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Bootstrap Edric and run focused smoke suite
+        run: ./_/edric all

.github/workflows/ci-source-layout.yml

@@ -18,3 +18,10 @@ jobs:
           test -d TTImp
           test -L _/src
           test "$(readlink _/src)" = ".."
+      - name: Verify top-level edric compatibility entrypoint
+        shell: sh
+        run: |
+          test -x edric
+          dash -n edric
+          sh -n edric
+          ./edric --help | grep -F 'usage: ./_/edric'

.github/workflows/ci_idric_style.yml

@@ -0,0 +1,20 @@
+name: Idriç source-style drift check
+
+on:
+  push:
+  pull_request:
+
+permissions:
+  contents: read
+
+jobs:
+  style:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683
+        with:
+          fetch-depth: 0
+      - name: Check newly added Idriç source
+        uses: isomorphisms/ai-ci/idric-style@d76e865c3742c51308ddf211ee6f5b724f4104de
+        with:
+          base: ${{ github.event_name == 'pull_request' && 'HEAD^1' || github.event.before }}

AGENTS.md

@@ -0,0 +1,37 @@
+# Idriç agent instructions
+
+Before writing or reviewing Idriç-facing source, read:
+
+1. [`STYLE.md`](STYLE.md)
+2. [`examples/intent/railway/`](examples/intent/railway/README.md)
+3. [`examples/intent/http_server/`](examples/intent/http_server/README.md)
+4. [`_/AGENTS.md`](_/AGENTS.md) for repository and branch rules
+
+Apply the shared evidence and acceptance guardrails in
+`isomorphisms/ai-ci/AGENTS.md`.
+
+`STYLE.md` is the canonical source-style guide. The two intent examples are the
+canonical structural references. This file is operational guidance; do not copy
+the full style guide into `AGENTS.md`.
+
+The repository contains a large inherited Idris codebase. Its existence is not
+permission to reproduce Idris/Haskell style in new Idriç work.
+
+Inspect the relevant surrounding Idriç work before inventing a new pattern, but
+do not promote arbitrary existing files into style authorities. Human
+corrections and the canonical guide/examples take precedence.
+
+Do not restore a rejected language ontology under its old name or a near-synonym
+because it survives in inherited code, generated output, an old branch, or an
+upstream convention. Preserve the current semantic distinction first.
+
+For compiler/backend claims, bind evidence to the exact source head and material
+compiler/backend pins. Source presence, generated output, compilation, and an
+oracle or fallback do not prove execution through the named backend.
+
+Keep language and mathematical semantics above compiler, ABI, storage, and
+machine representations. A convenient representation may implement an object;
+it does not define the object unless the language semantics explicitly say so.
+
+Work on a branch, keep changes narrow, and run the checks relevant to the code
+you changed before proposing it for merge.

ANF_READABLE_NAMES.md

@@ -0,0 +1,54 @@
+# Readable administrative-normal-form names
+
+The `A` at the beginning of these compiler constructors marked the administrative-normal-form layer. This branch spells out that layer instead of requiring the reader to remember the initial.
+
+The module path remains `Compiler.ANF`, which is the conventional short name for the compiler pass. The datatype and the terms being read inside the module use complete names.
+
+## Main expression vocabulary
+
+| Old name | Readable name |
+|---|---|
+| `ANF` | `Administrative_Normal_Form` |
+| `AVar` | `Administrative_Normal_Form_Variable` |
+| `ALocal` | `Administrative_Normal_Form_Local_Variable` |
+| `ANull` | `Administrative_Normal_Form_Erased_Variable` |
+| `AV` | `Administrative_Normal_Form_Variable_Expression` |
+| `AAppName` | `Administrative_Normal_Form_Named_Function_Application` |
+| `AUnderApp` | `Administrative_Normal_Form_Partial_Application` |
+| `AApp` | `Administrative_Normal_Form_Closure_Application` |
+| `ALet` | `Administrative_Normal_Form_Binding` |
+| `ACon` | `Administrative_Normal_Form_Constructor_Value` |
+| `AOp` | `Administrative_Normal_Form_Primitive_Operation` |
+| `AExtPrim` | `Administrative_Normal_Form_External_Primitive` |
+| `AConCase` | `Administrative_Normal_Form_Constructor_Case` |
+| `AConstCase` | `Administrative_Normal_Form_Constant_Case` |
+| `APrimVal` | `Administrative_Normal_Form_Primitive_Value` |
+| `AErased` | `Administrative_Normal_Form_Erased_Value` |
+| `ACrash` | `Administrative_Normal_Form_Crash` |
+
+## Case alternatives and definitions
+
+| Old name | Readable name |
+|---|---|
+| `AConAlt` | `Administrative_Normal_Form_Constructor_Alternative` |
+| `MkAConAlt` | `Make_Administrative_Normal_Form_Constructor_Alternative` |
+| `AConstAlt` | `Administrative_Normal_Form_Constant_Alternative` |
+| `MkAConstAlt` | `Make_Administrative_Normal_Form_Constant_Alternative` |
+| `ANFDef` | `Administrative_Normal_Form_Definition` |
+| `MkAFun` | `Make_Administrative_Normal_Form_Function` |
+| `MkACon` | `Make_Administrative_Normal_Form_Constructor` |
+| `MkAForeign` | `Make_Administrative_Normal_Form_Foreign_Function` |
+| `MkAError` | `Make_Administrative_Normal_Form_Error` |
+
+## Nearby helper names
+
+| Old name | Readable name |
+|---|---|
+| `AVars` | `Administrative_Normal_Form_Variable_Environment` |
+| `toANF` | `to_administrative_normal_form` |
+| `anf` | `convert_expression_to_administrative_normal_form` |
+| `anfArgs` | `convert_arguments_to_administrative_normal_form` |
+| `anfConAlt` | `convert_constructor_alternative_to_administrative_normal_form` |
+| `anfConstAlt` | `convert_constant_alternative_to_administrative_normal_form` |
+
+The earlier TTImp names also use `Elaborable_` now, replacing the awkward `Elaboratable_` spelling.

COMPLEX-PROJECTIVE.md

@@ -0,0 +1,61 @@
+# Complex and projective semantic boundary
+
+This slice establishes the type-level distinction needed by complex and projective arithmetic without choosing a machine representation or silently settling the separate floating-precision work.
+
+## What the checker now distinguishes
+
+`ComplexCoordinates complex n` is the structural type of an element of a complex coordinate space with exactly `n` coordinates. `ComplexProjectivePoint complex n` is a projective point with a nonzero homogeneous representative containing exactly `n + 1` complex coordinates.
+
+The `complex` parameter is deliberate. The current canonical tree does not yet have a settled general real-scalar hierarchy whose precision semantics can honestly define the numerical carrier for the mathematical field C. This module therefore does **not** define C as two `Double`s, two `Float32`s, a GLSL `vec2`, or an x86 register pair merely to obtain executable code.
+
+The concrete executable Float32 implementation currently belongs to the x86-64 leading backend and is checked against the shared corpus at `_/fixtures/complex-projective/float32.json`. The exact `ExactComplex` type in `QuadraticForms.idric` remains a Gaussian-integral test scalar used only to make structural identities reduce exactly in compiler acceptance.
+
+## Projective semantics
+
+For projective dimension `n`, a representative has `n + 1` homogeneous coordinates. The all-zero tuple is excluded by `NonzeroHomogeneousCoordinates`.
+
+The runtime representation may carry a homogeneous tuple directly. The semantic point is the equivalence class under common nonzero complex rescaling:
+
+```text
+[z0:...:zn] = [lambda z0:...:lambda zn],  lambda != 0.
+```
+
+`projective_rescaling_witness` expresses one explicit witness for that quotient relation. Raw component equality is not projective equality. There is intentionally no ordinary `Eq` instance, vector addition, or multiplication for `ComplexProjectivePoint`.
+
+Normalization is not part of construction. A backend may choose a gauge for numerical stability, chart extraction, comparison, serialization, or rendering, but common scale is otherwise retained as redundant homogeneous information.
+
+## Affine chart
+
+`affine_to_projective` implements
+
+```text
+(z1,...,zn) -> [1:z1:...:zn].
+```
+
+`projective_first_chart` divides by the first homogeneous coordinate only when that coordinate is nonzero. For CP^1, `[0:1]` therefore remains the point at infinity and is outside this chart.
+
+## Holomorphic boundary
+
+Projective structure does not make observational operations holomorphic. Conjugation, magnitude, phase, gauge choice, and coloring may be used for observation or rendering. They must not be inserted into an evolving value that is meant to remain holomorphic.
+
+The shared render fixture uses the current whole-plane explorer model
+
+```text
+f(z) = R(z) exp(q(z))
+```
+
+where `R` carries an explicit zero/pole divisor and `q` is an entire polynomial. The fixture contains no lasso, overlapping-disc, path, Riemann-surface, or lacunary machinery.
+
+## Precision and tolerances
+
+The shared numerical corpus declares Float32 explicitly. Its machine implementations must preserve that declared width. A wider host calculation may be used only as an external oracle.
+
+Exact-binary32 cases use exact comparison. Ordinary floating cases use an error bound derived from binary32 epsilon and the conditioning/operation count of the case. The current bounded complex-exponential implementation is a degree-7 Taylor polynomial and is accepted only for input magnitude at most `0.5`; its analytic truncation bound is
+
+```text
+exp(|q|) |q|^8 / 8!
+```
+
+plus a separately recorded binary32 rounding allowance. Inputs outside the declared approximation domain must be rejected rather than silently accepted with a larger arbitrary tolerance.
+
+Projective comparison uses rescaling witnesses or invariant cross-products such as `zi*wj - zj*wi`, never raw homogeneous component equality.