iter operator-routing-eq-ord.1 (DONE 13/13): drop comparator builtins, route through Eq/Ord
Closes Gitea #1. Realises the "P2 follow-up" called out in examples/prelude.ail:9 — removes the surface comparator names `==` / `!=` / `<` / `<=` / `>` / `>=` from the language entirely, routes the LLM-author's `(app eq …)` / `(app compare …)` / `(app ne|lt|le|gt|ge …)` through prelude.Eq / prelude.Ord class- dispatch, ships six named Float-comparison fns (`float_eq`/`float_ne`/`float_lt`/`float_le`/`float_gt`/`float_ge`) so Float keeps comparability without an Eq/Ord instance, and emits primitive instance bodies with `alwaysinline` so the -O0 IR shape stays at one instruction per comparison. Plan-task journal (13 tasks, single atomic iter per Approach A): Task 1 — Bootstrap: 4 new fixtures (eq_user_adt_smoke.ail, eq_float_must_fail.ail, float_compare_smoke.ail, operator_unbound_check.ail) + 5 new E2E/pin tests as RED starting state. All 5 confirmed RED at start: north-star fixed `NoInstance Eq Unit` (preserved by Unit-eq opening line intentionally added in plan-self-review); float_compare unknown `float_eq`; operator-name typechecked (== still polymorphic); must-fail diagnostic lacked `float_eq`; alwaysinline absent from IR. Task 2 — Codegen alwaysinline + intercept arms: introduced `intercept_emit_wants_alwaysinline` allowlist + appended ` alwaysinline` between `)` and `{` of the `define` line in `emit_fn`; added 9 new intercept arms to `try_emit_primitive_instance_body` — `eq__Int`/`eq__Bool`/ `eq__Unit` + the six `float_*` arms. Task 3 — Prelude reshape: `instance Eq Unit` added; Eq Int/Bool bodies become placeholder-`false` (intercept overrides); six `float_*` free fns added; line-9 P2-follow-up comment removed. Lockstep hash re-pins: prelude_module_hash_pin (3abe0d3fa3c11c99 → new), mono_hash_stability six body-hash literals (eq__Int/Bool/Str + compare__Int/Bool/Str all shifted because placeholder body changes the canonical hash). IR-snapshot regen (hello/list/max3/sum/ws_main) rolled forward into this task at orchestrator's pragmatic call — prelude shift forces the snapshots immediately. Task 4 — Fixture migration: 58 .ail fixtures rewritten (`(app == …)` → `(app eq …)`, etc.; Float-typed operand sites to `(app float_eq …)` / `(app float_lt …)`). eq_ord_user_adt.ail:21 inner `==` → `eq` migration with lockstep eq_ord_e2e.rs:134 body-hash re-pin (3c4cf040cb4e8bb2 → new). Two prose snapshots accepted; deps test + 5 hash_pin literals updated as cascading consequences. Task 5 — Test-scaffold migration: all 8 in-source `#[cfg(test)] mod tests` AST-literal sites threaded (desugar.rs:2414, check/lib.rs:5656/6092/6220, codegen/lib.rs sites). 7 obsolete in-source tests deleted (5 eq_typechecks + 2 lower_eq ADT/Fn rejection — coverage moves to E2E eq_user_adt_smoke + eq_float_must_fail). 2 additional letrec tests deleted (single-module check env can't resolve eq/ge without prelude auto-import; covered by workspace E2E). Task 6 — Lit-pattern desugar: build_eq emits `Term::Var { name: "eq" }` instead of `"=="` at desugar.rs:1109; doc-comment rewritten to describe class-dispatch. Task 7 — Dead-machinery deletion sweep (compile-gated): typchecker builtins (install + list comparator entries deleted); codegen builtin_binop_typed (10 comparator arms deleted from synth.rs, table reduced to arithmetic core); lower_eq fn entirely deleted; `==` short-circuit in lower_app deleted; `is_static_callee` `==` clause deleted; `is_arithmetic_or_comparison_op` renamed to `is_arithmetic_op` + caller-update at codegen/lib.rs:2152 + :2529. Dead `poly_a_a_to_bool` helpers also removed. Workspace build green after compile gate — every caller of the deleted surface was migrated by Tasks 4-6. Task 8 — Float-aware NoInstance diagnostic: check/lib.rs:856-880 addendum extended to name `float_eq` / `float_lt` as the explicit alternative for Eq/Ord at Float; eq_float_noinstance.rs:32-44 assertion extended. Task 9 — IR snapshot regen: subsumed by Task 3 (prelude shift forced immediate snapshot regen; deferring to Task 9 would have left the workspace red between tasks). Task 10 — Prose-projection cleanup: 6 comparator arms deleted from binop_info; 3 in-source mod-tests updated/deleted (comparator-infix rendering would be dishonest now that the operators are no longer language identifiers). Task 11 — Contract updates: 5 design files rewritten to the class-dispatch present — float-semantics.md (arithmetic guarantees retained on +/-/*/; comparison guarantees transferred from ==/!=/< to float_eq/float_ne/float_lt/etc.); prelude-classes.md (Eq Unit added to instance list; new paragraph on six float_* fns; Float-no-Eq/Ord clause gains `→ use float_eq` cross-reference); str-abi.md (clause "REMAIN primitive operators" rewritten to describe class-method dispatch); scope-boundaries.md (multiple operator-name and Pattern::Lit-desugar clauses rewritten); authoring-surface.md (==, <= dropped from operator-example list). Task 12 — Initial acceptance gate: workspace 638/0 GREEN; bench/compile_check + cross_lang 0 regressed; bench/check.py flagged 4 regressions on bench_closure_chain (+29% bump_s, +47% rc_s, +29% bump_rss_kb, +48% rc_rss_kb). Orchestrator initially classified as DONE-with-concerns; Boss reclassified as PARTIAL-via-acceptance-#8-fail after independent re-run, extended iter scope to Task 13. Task 13 — Direct icmp intercept arms (Boss-extension): try_emit_primitive_instance_body gains direct-icmp arms for lt__Int / le__Int / gt__Int / ge__Int / ne__Int, bypassing the compare__Int → Ordering → match indirection that allocated one Ordering ctor per call in tight loops. Each new arm inherits `alwaysinline` via the existing allowlist (extended accordingly). New IR pin test `ord_int_intercept_ir_pin.rs` + smoke fixture `ord_int_intercept_smoke.ail` ratify the optimization — opt -O2 -S confirms zero `call @ail_prelude_lt__Int` in optimized IR; the icmp folds directly at every use site. Bool variants (lt__Bool/etc.) deliberately NOT added — no bench/example calls Ord at Bool; spec-extension permits skipping if unreachable at bench level. Family can be extended symmetrically when first Bool-ordered perf workload appears. Bench-gate post-Task-13: bench_closure_chain bump_s -6.05%, rc_s -2.67%, bump_rss_kb -0.77%, rc_rss_kb +0.46% — all four previously-regressed metrics back inside tolerance. Full bench corpus: 36 metrics, 0 regressed, 0 improved beyond tolerance, 36 stable. bench/check.py exit 0 ✓; bench/compile_check.py exit 0 ✓; bench/cross_lang.py exit 0 ✓. Workspace: 640 passed, 0 failed across all binaries (delta vs. milestone start: +5 new E2E/pin tests added in Task 1 + 1 IR pin added in Task 13 − 9 in-source mod tests deleted as obsolete net ≈ −3). The eq_user_adt_smoke fixture's Unit-opening line was the deliberate RED-first device added in planner self-review so the north-star wouldn't accidentally GREEN at start (user-ADT-Eq on Point with hand-written instance was already operable today; the milestone's actual delivery is operator-name death + Eq Unit + Float-named-fns + cleanup of the two-pathy primitive comparator machinery). Net delta: 96 files changed, 1760 insertions, 1101 deletions; 12 net-new files (6 new fixtures, 5 new E2E/pin tests, 1 stats file). main passes-test-count: 640 (was 633 pre-iter, accounting for the deletions). Spec-vs-acceptance addendum: spec §Testing strategy anticipated the bench-gate-regression case with two recovery paths (`alwaysinline` investigation or "spec needs revisiting toward α"). Task 13 is the third path — direct intercept arms for `lt`/etc. that bypass the compare→match path entirely. The spec's contingency clause was thus generous enough to absorb Task 13 without spec revision, but a future iter that hits a class-method primitive where the body shape introduces a similar codegen cost (Ordering allocation, RC tax, deferred-init) should expect a parallel extension. The pattern is "primitive instance whose canonical body indirects through other class methods that allocate" → add a direct-emit intercept arm + alwaysinline + IR-shape pin. Concerns absorbed: - Codegen lower_app / resolve_top_level_fn gained a prelude-fallback lookup so bare monomorphic prelude fns (`float_eq` etc.) resolve from non-prelude modules without explicit `prelude.float_eq` qualifier. Mirrors the typechecker's implicit prelude import — not in plan but necessary infra for the named-fn surface to be callable. - Recon's "≈10 fixtures" estimate was 6× too low — 58 actual. Mechanical migration; no design impact. - Recon caught 4 in-source AST-literal sites the spec missed (lib.rs:5656 `>=` site + three codegen/lib.rs sites); Task 5 covered all. - Recon caught 2 contract files outside the spec's update set that directly contradicted the milestone (str-abi.md + scope-boundaries.md "REMAIN primitive operators" / "Pattern::Lit desugar to ==" clauses); Task 11 covered all 5. Stats file: `bench/orchestrator-stats/2026-05-21-iter-operator-routing-eq-ord.1.json`. closes #1
This commit is contained in:
@@ -43,7 +43,7 @@
|
||||
(ret (con Int))))
|
||||
(params i acc)
|
||||
(body
|
||||
(if (app < i 0)
|
||||
(if (app lt i 0)
|
||||
acc
|
||||
(let-rec helper
|
||||
(params x)
|
||||
|
||||
@@ -31,9 +31,9 @@
|
||||
(ret (con Int))))
|
||||
(params n acc)
|
||||
(body
|
||||
(if (app == n 1)
|
||||
(if (app eq n 1)
|
||||
acc
|
||||
(if (app == (app % n 2) 0)
|
||||
(if (app eq (app % n 2) 0)
|
||||
(tail-app collatz_steps (app / n 2) (app + acc 1))
|
||||
(tail-app collatz_steps (app + (app * n 3) 1) (app + acc 1))))))
|
||||
|
||||
@@ -45,7 +45,7 @@
|
||||
(ret (con Int))))
|
||||
(params i total)
|
||||
(body
|
||||
(if (app == i 0)
|
||||
(if (app eq i 0)
|
||||
total
|
||||
(tail-app sum_steps_loop
|
||||
(app - i 1)
|
||||
|
||||
@@ -28,7 +28,7 @@
|
||||
(ret (con Int))))
|
||||
(params i acc)
|
||||
(body
|
||||
(if (app == i 0)
|
||||
(if (app eq i 0)
|
||||
acc
|
||||
(tail-app intsum_loop
|
||||
(app - i 1)
|
||||
|
||||
@@ -40,7 +40,7 @@
|
||||
(ret (con List (con Int)))))
|
||||
(params n acc)
|
||||
(body
|
||||
(if (app == n 0)
|
||||
(if (app eq n 0)
|
||||
acc
|
||||
(tail-app build_n
|
||||
(app - n 1)
|
||||
|
||||
@@ -49,7 +49,7 @@
|
||||
(ret (own (con Tree)))))
|
||||
(params depth)
|
||||
(body
|
||||
(if (app == depth 0)
|
||||
(if (app eq depth 0)
|
||||
(term-ctor Tree TLeaf)
|
||||
(term-ctor Tree TNode
|
||||
1
|
||||
@@ -78,7 +78,7 @@
|
||||
(ret (own (con IntList)))))
|
||||
(params n acc)
|
||||
(body
|
||||
(if (app == n 0)
|
||||
(if (app eq n 0)
|
||||
acc
|
||||
(tail-app cons_n_acc
|
||||
(app - n 1)
|
||||
@@ -138,9 +138,9 @@
|
||||
(effects IO)))
|
||||
(params remaining print_countdown chunk_len print_k t)
|
||||
(body
|
||||
(if (app == remaining 0)
|
||||
(if (app eq remaining 0)
|
||||
(app print 9999)
|
||||
(if (app == print_countdown 0)
|
||||
(if (app eq print_countdown 0)
|
||||
(seq
|
||||
(app print (app one_op chunk_len t))
|
||||
(tail-app loop
|
||||
|
||||
@@ -73,7 +73,7 @@
|
||||
(ret (con Tree))))
|
||||
(params depth)
|
||||
(body
|
||||
(if (app == depth 0)
|
||||
(if (app eq depth 0)
|
||||
(term-ctor Tree TLeaf)
|
||||
(term-ctor Tree TNode
|
||||
1
|
||||
@@ -103,7 +103,7 @@
|
||||
(ret (con IntList))))
|
||||
(params n acc)
|
||||
(body
|
||||
(if (app == n 0)
|
||||
(if (app eq n 0)
|
||||
acc
|
||||
(tail-app cons_n_acc
|
||||
(app - n 1)
|
||||
@@ -197,9 +197,9 @@
|
||||
(effects IO)))
|
||||
(params remaining print_countdown chunk_len print_k t)
|
||||
(body
|
||||
(if (app == remaining 0)
|
||||
(if (app eq remaining 0)
|
||||
(app print 9999)
|
||||
(if (app == print_countdown 0)
|
||||
(if (app eq print_countdown 0)
|
||||
(seq
|
||||
(app print (app one_op chunk_len t))
|
||||
(tail-app loop
|
||||
|
||||
@@ -44,7 +44,7 @@
|
||||
(ret (con IntList))))
|
||||
(params n acc)
|
||||
(body
|
||||
(if (app == n 0)
|
||||
(if (app eq n 0)
|
||||
acc
|
||||
(tail-app cons_n_acc
|
||||
(app - n 1)
|
||||
|
||||
@@ -4,7 +4,7 @@ data IntList = INil | ICons(Int, IntList)
|
||||
|
||||
/// Tail-recursive list builder. Result = accumulator-prepended list.
|
||||
fn cons_n_acc(n: Int, acc: IntList) -> IntList {
|
||||
if n == 0 {
|
||||
if eq(n, 0) {
|
||||
acc
|
||||
} else {
|
||||
tail cons_n_acc(n - 1, ICons(n - 1, acc))
|
||||
|
||||
@@ -41,7 +41,7 @@
|
||||
(ret (own (con IntList)))))
|
||||
(params n acc)
|
||||
(body
|
||||
(if (app == n 0)
|
||||
(if (app eq n 0)
|
||||
acc
|
||||
(tail-app cons_n_acc
|
||||
(app - n 1)
|
||||
|
||||
@@ -16,7 +16,7 @@
|
||||
(class Looper)
|
||||
(type (con Int))
|
||||
(method loop_call
|
||||
(body (lam (params (typed i a) (typed acc (con Int))) (ret (con Int)) (body (if (app == i 0) acc (tail-app loop_call (app - i 1) (app + acc (app foo (app + acc i))))))))))
|
||||
(body (lam (params (typed i a) (typed acc (con Int))) (ret (con Int)) (body (if (app eq i 0) acc (tail-app loop_call (app - i 1) (app + acc (app foo (app + acc i))))))))))
|
||||
(fn main
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
|
||||
@@ -42,7 +42,7 @@
|
||||
(ret (con Tree))))
|
||||
(params depth)
|
||||
(body
|
||||
(if (app == depth 0)
|
||||
(if (app eq depth 0)
|
||||
(term-ctor Tree Leaf)
|
||||
(term-ctor Tree Node
|
||||
1
|
||||
|
||||
@@ -23,4 +23,4 @@
|
||||
(case (pat-ctor MkBox a)
|
||||
(match y
|
||||
(case (pat-ctor MkBox b)
|
||||
(app == a b)))))))))))
|
||||
(app eq a b)))))))))))
|
||||
|
||||
+28
-25
@@ -1,26 +1,29 @@
|
||||
; Iter 16e — `==` extends from Int-only to Int/Bool/Str/Unit (polymorphic
|
||||
; dispatch). The builtin's declared type became
|
||||
; forall a. (a, a) -> Bool
|
||||
; and codegen monomorphises on the resolved arg type:
|
||||
; Equality dispatch via the prelude.Eq class for Int/Bool/Str/Unit.
|
||||
; Each `(app eq x y)` call resolves to the matching primitive Eq
|
||||
; instance, lowered via try_emit_primitive_instance_body in the
|
||||
; codegen:
|
||||
; Int → icmp eq i64
|
||||
; Bool → icmp eq i1
|
||||
; Str → @strcmp + icmp eq i32 0
|
||||
; Str → @ail_str_eq (strcmp-based)
|
||||
; Unit → constant i1 true (single-inhabitant type)
|
||||
; ADT/Fn → rejected at codegen with a clear error.
|
||||
;
|
||||
; Float has no Eq instance; partial-Float comparison is done via
|
||||
; the explicit float_eq / float_lt / etc. fns (see
|
||||
; design/contracts/float-semantics.md).
|
||||
;
|
||||
; This fixture exercises all four supported types, both directly via
|
||||
; `(app == ...)` and indirectly via 16c's lit-pattern desugar (which
|
||||
; rewrites `(pat-lit "hi")` → `(if (== sv "hi") body fall_k)` and
|
||||
; therefore inherits 16e's polymorphic `==`).
|
||||
; `(app eq ...)` and indirectly via the lit-pattern desugar (which
|
||||
; rewrites `(pat-lit "hi")` → `(if (eq sv "hi") body fall_k)` and
|
||||
; therefore inherits the same class-dispatch path).
|
||||
;
|
||||
; Expected stdout (one per line):
|
||||
; true ; (== 5 5)
|
||||
; false ; (== 5 6)
|
||||
; false ; (== true false)
|
||||
; true ; (== true true)
|
||||
; true ; (== "hi" "hi")
|
||||
; false ; (== "hi" "ho")
|
||||
; true ; (== () ())
|
||||
; true ; (eq 5 5)
|
||||
; false ; (eq 5 6)
|
||||
; false ; (eq true false)
|
||||
; true ; (eq true true)
|
||||
; true ; (eq "hi" "hi")
|
||||
; false ; (eq "hi" "ho")
|
||||
; true ; (eq () ())
|
||||
; 1 ; classify_str "hi" (lit-pattern hits 1 arm)
|
||||
; 2 ; classify_str "ho" (lit-pattern hits 2 arm)
|
||||
; 0 ; classify_str "??" (default arm)
|
||||
@@ -30,7 +33,7 @@
|
||||
(module eq_demo
|
||||
|
||||
(fn classify_str
|
||||
(doc "Lit-pattern over Str; exercises 16c's build_eq for non-Int.")
|
||||
(doc "Lit-pattern over Str; exercises build_eq's class-dispatch lowering for non-Int.")
|
||||
(type (fn-type (params (con Str)) (ret (con Int))))
|
||||
(params s)
|
||||
(body
|
||||
@@ -40,17 +43,17 @@
|
||||
(case _ 0))))
|
||||
|
||||
(fn main
|
||||
(doc "Drive == at Int/Bool/Str/Unit; then drive classify_str.")
|
||||
(doc "Drive eq at Int/Bool/Str/Unit; then drive classify_str.")
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body
|
||||
(seq (app print (app == 5 5))
|
||||
(seq (app print (app == 5 6))
|
||||
(seq (app print (app == true false))
|
||||
(seq (app print (app == true true))
|
||||
(seq (app print (app == "hi" "hi"))
|
||||
(seq (app print (app == "hi" "ho"))
|
||||
(seq (app print (app == (lit-unit) (lit-unit)))
|
||||
(seq (app print (app eq 5 5))
|
||||
(seq (app print (app eq 5 6))
|
||||
(seq (app print (app eq true false))
|
||||
(seq (app print (app eq true true))
|
||||
(seq (app print (app eq "hi" "hi"))
|
||||
(seq (app print (app eq "hi" "ho"))
|
||||
(seq (app print (app eq (lit-unit) (lit-unit)))
|
||||
(seq (app print (app classify_str "hi"))
|
||||
(seq (app print (app classify_str "ho"))
|
||||
(app print (app classify_str "??"))))))))))))))
|
||||
|
||||
@@ -0,0 +1,6 @@
|
||||
(module eq_float_must_fail
|
||||
(fn main
|
||||
(doc "Klausel-3 discriminator. After operator-routing-eq-ord, `(app eq 1.5 1.5)` must fire `NoInstance Eq Float` with a follow-up sentence naming `float_eq` as the explicit IEEE-aware alternative. Today the diagnostic already fires (no Eq Float instance) but does not name `float_eq` — the milestone adds that hint.")
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body (app print (app eq 1.5 1.5)))))
|
||||
@@ -9,7 +9,7 @@
|
||||
(method eq
|
||||
(body (lam (params (typed a (con IntBox)) (typed b (con IntBox))) (ret (con Bool)) (body (match a
|
||||
(case (pat-ctor MkIntBox ai) (match b
|
||||
(case (pat-ctor MkIntBox bi) (app == ai bi))))))))))
|
||||
(case (pat-ctor MkIntBox bi) (app eq ai bi))))))))))
|
||||
(instance
|
||||
(class prelude.Ord)
|
||||
(type (con IntBox))
|
||||
|
||||
@@ -0,0 +1,28 @@
|
||||
(module eq_user_adt_smoke
|
||||
(data Point
|
||||
(doc "Two-Int-field record. The milestone-defining north-star: an LLM author writes `instance Eq Point` and calls `(app eq p1 p2)` end-to-end through class-dispatch.")
|
||||
(ctor Point (con Int) (con Int)))
|
||||
(instance
|
||||
(class prelude.Eq)
|
||||
(type (con Point))
|
||||
(doc "Eq Point by structural comparison of the two Int fields. The nested `(app eq a1 a2)` calls dispatch to prelude.Eq.eq's Int instance.")
|
||||
(method eq
|
||||
(body (lam
|
||||
(params (typed p1 (con Point)) (typed p2 (con Point)))
|
||||
(ret (con Bool))
|
||||
(body
|
||||
(match p1
|
||||
(case (pat-ctor Point a1 b1)
|
||||
(match p2
|
||||
(case (pat-ctor Point a2 b2)
|
||||
(if (app eq a1 a2) (app eq b1 b2) false))))))))))
|
||||
(fn main
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body
|
||||
(let p1 (term-ctor Point Point 1 2)
|
||||
(let p2 (term-ctor Point Point 1 2)
|
||||
(let p3 (term-ctor Point Point 1 3)
|
||||
(seq (app print (app eq (lit-unit) (lit-unit)))
|
||||
(seq (app print (app eq p1 p2))
|
||||
(app print (app eq p1 p3))))))))))
|
||||
@@ -41,7 +41,7 @@
|
||||
(type (fn-type (params (con Int)) (ret (con Int))))
|
||||
(params n)
|
||||
(body
|
||||
(if (app <= n 0)
|
||||
(if (app le n 0)
|
||||
0
|
||||
(let b (term-ctor Box MkBox n)
|
||||
(match b
|
||||
|
||||
@@ -18,7 +18,7 @@
|
||||
(ret (con Float))))
|
||||
(params n x k)
|
||||
(body
|
||||
(if (app == k 0)
|
||||
(if (app eq k 0)
|
||||
x
|
||||
(tail-app newton_iter
|
||||
n
|
||||
|
||||
@@ -37,9 +37,9 @@
|
||||
(body
|
||||
(if (app is_nan x)
|
||||
-1
|
||||
(if (app > x 1.0e308)
|
||||
(if (app float_gt x 1.0e308)
|
||||
0
|
||||
(if (app < x -1.0e308)
|
||||
(if (app float_lt x -1.0e308)
|
||||
0
|
||||
1)))))
|
||||
|
||||
|
||||
@@ -8,7 +8,7 @@
|
||||
(ret (con Int))))
|
||||
(params n acc)
|
||||
(body
|
||||
(if (app == n 0)
|
||||
(if (app eq n 0)
|
||||
acc
|
||||
(tail-app fact_acc (app - n 1) (app * acc n)))))
|
||||
|
||||
|
||||
@@ -17,6 +17,6 @@
|
||||
(type (fn-type (params (con Int)) (ret (con Int))))
|
||||
(params x)
|
||||
(body
|
||||
(if (app < x 0)
|
||||
(if (app lt x 0)
|
||||
(app - 0 x)
|
||||
x))))
|
||||
|
||||
@@ -12,12 +12,12 @@
|
||||
(type (fn-type (params (con Int)) (ret (con Int))))
|
||||
(params n)
|
||||
(body
|
||||
(if (app < n 2)
|
||||
(if (app lt n 2)
|
||||
n
|
||||
(loop (x (con Int) n) (prev (con Int) 0)
|
||||
(if (app == x prev)
|
||||
(if (app eq x prev)
|
||||
x
|
||||
(let next (app / (app + x (app / n x)) 2)
|
||||
(if (app == next x)
|
||||
(if (app eq next x)
|
||||
next
|
||||
(recur next x)))))))))
|
||||
|
||||
@@ -13,7 +13,7 @@
|
||||
(params start)
|
||||
(body
|
||||
(loop (n (con Int) start) (steps (con Int) 0)
|
||||
(if (app == n 1)
|
||||
(if (app eq n 1)
|
||||
steps
|
||||
(match (app % n 2)
|
||||
(case (pat-lit 0) (recur (app / n 2) (app + steps 1)))
|
||||
|
||||
@@ -7,7 +7,7 @@
|
||||
(type (fn-type (params (con Int)) (ret (con Int))))
|
||||
(params n)
|
||||
(body
|
||||
(if (app == n 0)
|
||||
(if (app eq n 0)
|
||||
0
|
||||
(recur (app - n 1)))))
|
||||
(fn main
|
||||
|
||||
@@ -8,7 +8,7 @@
|
||||
(params n)
|
||||
(body
|
||||
(loop (acc (con Int) 0) (i (con Int) 1)
|
||||
(if (app > i n)
|
||||
(if (app gt i n)
|
||||
acc
|
||||
(recur (app + acc i))))))
|
||||
(fn main
|
||||
|
||||
@@ -8,9 +8,9 @@
|
||||
(params start)
|
||||
(body
|
||||
(loop (i (con Int) start)
|
||||
(if (app == i 0)
|
||||
(if (app eq i 0)
|
||||
i
|
||||
(recur (app > i 0))))))
|
||||
(recur (app gt i 0))))))
|
||||
(fn main
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
|
||||
@@ -9,7 +9,7 @@
|
||||
(params n)
|
||||
(body
|
||||
(loop (i (con Int) n)
|
||||
(if (app == i 1)
|
||||
(if (app eq i 1)
|
||||
1
|
||||
(app * i (recur (app - i 1)))))))
|
||||
(fn main
|
||||
|
||||
@@ -13,7 +13,7 @@
|
||||
(params n)
|
||||
(body
|
||||
(loop (acc (con Int) 0) (i (con Int) 1)
|
||||
(if (app > i n)
|
||||
(if (app gt i n)
|
||||
acc
|
||||
(recur (app apply_int (lam (params (typed d (con Int))) (ret (con Int)) (body (app + acc d))) i)
|
||||
(app + i 1))))))
|
||||
|
||||
@@ -14,7 +14,7 @@
|
||||
(params x y)
|
||||
(body
|
||||
(loop (a (con Int) x) (b (con Int) y)
|
||||
(if (app == b 0)
|
||||
(if (app eq b 0)
|
||||
a
|
||||
(recur b (app % a b))))))
|
||||
(fn main
|
||||
|
||||
@@ -10,7 +10,7 @@
|
||||
(params)
|
||||
(body
|
||||
(loop (tick (con Int) 0) (parity (con Int) 0)
|
||||
(if (app == (app % tick 2) 0)
|
||||
(if (app eq (app % tick 2) 0)
|
||||
(recur (app + tick 1) 1)
|
||||
(recur (app + tick 1) 0)))))
|
||||
(fn main
|
||||
|
||||
@@ -12,7 +12,7 @@
|
||||
(params start)
|
||||
(body
|
||||
(loop (tick (con Int) start) (parity (con Int) 0)
|
||||
(if (app == (app % tick 2) 0)
|
||||
(if (app eq (app % tick 2) 0)
|
||||
(recur (app + tick 1) 1)
|
||||
(recur (app + tick 1) 0)))))
|
||||
(fn main
|
||||
|
||||
@@ -7,7 +7,7 @@
|
||||
(doc "Return category code 0..3 for temperature t in degrees C.")
|
||||
(type (fn-type (params (con Int)) (ret (con Int))))
|
||||
(params t)
|
||||
(body (let code 0 (let code (if (app < t 0) 0 (if (app < t 15) 1 (if (app < t 28) 2 3))) code))))
|
||||
(body (let code 0 (let code (if (app lt t 0) 0 (if (app lt t 15) 1 (if (app lt t 28) 2 3))) code))))
|
||||
|
||||
(fn main
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
|
||||
@@ -7,7 +7,7 @@
|
||||
(fn has_small_factor
|
||||
(type (fn-type (params (con Int)) (ret (con Bool))))
|
||||
(params n)
|
||||
(body (let found false (let found (if (app == (app % n 2) 0) true found) (let found (if (app == (app % n 3) 0) true found) (let found (if (app == (app % n 5) 0) true found) (let found (if (app == (app % n 7) 0) true found) found)))))))
|
||||
(body (let found false (let found (if (app eq (app % n 2) 0) true found) (let found (if (app eq (app % n 3) 0) true found) (let found (if (app eq (app % n 5) 0) true found) (let found (if (app eq (app % n 7) 0) true found) found)))))))
|
||||
|
||||
(fn main
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
|
||||
@@ -18,7 +18,7 @@
|
||||
(params n)
|
||||
(body
|
||||
(loop (i (con Int) 1) (acc (con Int) 0)
|
||||
(if (app > i n)
|
||||
(if (app gt i n)
|
||||
acc
|
||||
(recur (app + i 1) (app + acc (app * i i)))))))
|
||||
|
||||
|
||||
@@ -23,10 +23,10 @@
|
||||
(params score)
|
||||
(body
|
||||
(let g 0
|
||||
(let g (if (app >= score 60) 1 g)
|
||||
(let g (if (app >= score 70) 2 g)
|
||||
(let g (if (app >= score 80) 3 g)
|
||||
(let g (if (app >= score 90) 4 g)
|
||||
(let g (if (app ge score 60) 1 g)
|
||||
(let g (if (app ge score 70) 2 g)
|
||||
(let g (if (app ge score 80) 3 g)
|
||||
(let g (if (app ge score 90) 4 g)
|
||||
g)))))))
|
||||
|
||||
(fn main
|
||||
|
||||
@@ -45,13 +45,13 @@
|
||||
(body
|
||||
(match rest
|
||||
(case (pat-ctor Nil)
|
||||
(if ok (app == depth 0) false))
|
||||
(if ok (app eq depth 0) false))
|
||||
(case (pat-ctor Cons t more)
|
||||
(match t
|
||||
(case (pat-lit 1)
|
||||
(tail-app scan more (app + depth 1) ok))
|
||||
(case (pat-lit 2)
|
||||
(if (app == depth 0)
|
||||
(if (app eq depth 0)
|
||||
(tail-app scan more depth false)
|
||||
(tail-app scan more (app - depth 1) ok)))
|
||||
(case _
|
||||
|
||||
@@ -0,0 +1,9 @@
|
||||
(module float_compare_smoke
|
||||
(fn main
|
||||
(doc "Float comparison via the named-fn surface that replaces the deleted operator names. Each float_* call lowers to a single fcmp via try_emit_primitive_instance_body.")
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body
|
||||
(seq (app print (app float_eq 1.5 1.5))
|
||||
(seq (app print (app float_lt 1.0 2.0))
|
||||
(app print (app float_eq 1.0 0.0)))))))
|
||||
@@ -27,7 +27,7 @@
|
||||
(params n)
|
||||
(type (fn-type (params (con Int)) (ret (con Int))))
|
||||
(body
|
||||
(if (app <= n 1)
|
||||
(if (app le n 1)
|
||||
1
|
||||
(app * n (app factorial (app - n 1)))))
|
||||
(in (app print (app apply5 factorial)))))))
|
||||
|
||||
@@ -29,7 +29,7 @@
|
||||
(params n)
|
||||
(type (fn-type (params (con Int)) (ret (con Int))))
|
||||
(body
|
||||
(if (app <= n 1)
|
||||
(if (app le n 1)
|
||||
(app + 1 base)
|
||||
(app * n (app factorial_plus (app - n 1)))))
|
||||
(in (app apply5 factorial_plus)))))
|
||||
|
||||
@@ -20,7 +20,7 @@
|
||||
(params i)
|
||||
(type (fn-type (params (con Int)) (ret (con Int))))
|
||||
(body
|
||||
(if (app >= i n)
|
||||
(if (app ge i n)
|
||||
0
|
||||
(app + i (app loop (app + i 1)))))
|
||||
(in (app loop 1)))))
|
||||
|
||||
@@ -17,7 +17,7 @@
|
||||
(params n)
|
||||
(type (fn-type (params (con Int)) (ret (con Int))))
|
||||
(body
|
||||
(if (app <= n 1)
|
||||
(if (app le n 1)
|
||||
1
|
||||
(app * n (app fact (app - n 1)))))
|
||||
(in
|
||||
|
||||
@@ -31,9 +31,9 @@
|
||||
(params i)
|
||||
(type (fn-type (params (con Int)) (ret (con Int))))
|
||||
(body
|
||||
(if (app > i n)
|
||||
(if (app gt i n)
|
||||
0
|
||||
(if (app < i threshold)
|
||||
(if (app lt i threshold)
|
||||
(app + 1 (app loop (app + i 1)))
|
||||
(app loop (app + i 1)))))
|
||||
(in (app loop 1))))))
|
||||
|
||||
@@ -42,9 +42,9 @@
|
||||
(params i)
|
||||
(type (fn-type (params (con Int)) (ret (con Int))))
|
||||
(body
|
||||
(if (app > i n)
|
||||
(if (app gt i n)
|
||||
0
|
||||
(if (app < i threshold)
|
||||
(if (app lt i threshold)
|
||||
(app + 1 (app loop (app + i 1)))
|
||||
(app loop (app + i 1)))))
|
||||
(in (app loop 1)))))))
|
||||
|
||||
@@ -4,6 +4,6 @@
|
||||
(params n)
|
||||
(body
|
||||
(loop (acc (con Int) 0) (i (con Int) 1)
|
||||
(if (app > i n)
|
||||
(if (app gt i n)
|
||||
acc
|
||||
(recur (app + acc i) (app + i 1)))))))
|
||||
|
||||
@@ -9,6 +9,6 @@
|
||||
(params n)
|
||||
(body
|
||||
(loop (acc (con Int) 0) (i (con Int) 1)
|
||||
(if (app > i n)
|
||||
(if (app gt i n)
|
||||
acc
|
||||
(recur (app + acc i) (app + i 1)))))))
|
||||
|
||||
@@ -9,6 +9,6 @@
|
||||
(params n)
|
||||
(body
|
||||
(loop (acc (con Int) 0) (i (con Int) 1)
|
||||
(if (app > i n)
|
||||
(if (app gt i n)
|
||||
acc
|
||||
(recur (app + acc i) (app + i 1)))))))
|
||||
|
||||
@@ -7,7 +7,7 @@ fn main() -> Unit with IO {
|
||||
|
||||
fn sum_to(n: Int) -> Int {
|
||||
loop(acc = 0, i = 1) {
|
||||
if i > n {
|
||||
if gt(i, n) {
|
||||
acc
|
||||
} else {
|
||||
recur(acc + i, i + 1)
|
||||
|
||||
+2
-2
@@ -2,12 +2,12 @@
|
||||
(fn max
|
||||
(type (fn-type (params (con Int) (con Int)) (ret (con Int))))
|
||||
(params a b)
|
||||
(body (if (app > a b) a b)))
|
||||
(body (if (app gt a b) a b)))
|
||||
(fn max3
|
||||
(doc "Demonstriert verschachteltes if (statt max-call) zum Test des Block-Trackings.")
|
||||
(type (fn-type (params (con Int) (con Int) (con Int)) (ret (con Int))))
|
||||
(params a b c)
|
||||
(body (if (app > a b) (if (app > a c) a c) (if (app > b c) b c))))
|
||||
(body (if (app gt a b) (if (app gt a c) a c) (if (app gt b c) b c))))
|
||||
(fn main
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
|
||||
@@ -12,6 +12,6 @@
|
||||
(type (fn-type (params (con Int) (con Int) (con Int)) (ret (con Int))))
|
||||
(params lo hi acc)
|
||||
(body
|
||||
(if (app > lo hi)
|
||||
(if (app gt lo hi)
|
||||
acc
|
||||
(tail-app sum_helper (app + lo 1) hi (app + acc lo))))))
|
||||
|
||||
@@ -12,6 +12,6 @@
|
||||
(type (fn-type (params (con Float) (con Float) (con Float)) (ret (con Float))))
|
||||
(params lo hi acc)
|
||||
(body
|
||||
(if (app > lo hi)
|
||||
(if (app float_gt lo hi)
|
||||
acc
|
||||
(tail-app sum_helper (app + lo 1.0) hi (app + acc lo))))))
|
||||
|
||||
@@ -29,14 +29,14 @@
|
||||
(params i)
|
||||
(type (fn-type (params (con Int)) (ret (con Int))))
|
||||
(body
|
||||
(if (app > i n)
|
||||
(if (app gt i n)
|
||||
0
|
||||
(app +
|
||||
(let-rec inner
|
||||
(params j)
|
||||
(type (fn-type (params (con Int)) (ret (con Int))))
|
||||
(body
|
||||
(if (app > j i)
|
||||
(if (app gt j i)
|
||||
0
|
||||
(app + 1 (app inner (app + j 1)))))
|
||||
(in (app inner 1)))
|
||||
|
||||
@@ -0,0 +1,6 @@
|
||||
(module operator_unbound_check
|
||||
(fn main
|
||||
(doc "Pin fixture. After operator-routing-eq-ord, `(app == 5 5)` must fail typecheck with `unknown variable: ==` — the operator names are no longer in the language. Today this typechecks (== is polymorphic over Int) — RED-first.")
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body (app print (app == 5 5)))))
|
||||
@@ -0,0 +1,27 @@
|
||||
; Smoke fixture for the `lt__Int` / `le__Int` / `gt__Int` /
|
||||
; `ge__Int` / `ne__Int` intercept-arm family (operator-routing-eq-ord.1
|
||||
; Task 13). Forces the mono pass to instantiate each of the five
|
||||
; Ord/Eq free helpers at Int by calling each one once; the linked
|
||||
; pin test (ord_int_intercept_ir_pin.rs) reads the resulting IR and
|
||||
; asserts each body lowers to a single direct `icmp` carrying
|
||||
; `alwaysinline`. The body is not perf-relevant — only the symbol
|
||||
; set and the IR shape are pinned.
|
||||
|
||||
(module ord_int_intercept_smoke
|
||||
|
||||
(fn drive
|
||||
(doc "Touches each of lt/le/gt/ge/ne at Int once. Returns 0 unconditionally; we care only about which mono symbols the call graph forces the unified mono pass to emit.")
|
||||
(type (fn-type (params (con Int) (con Int)) (ret (con Int))))
|
||||
(params a b)
|
||||
(body
|
||||
(let r1 (app lt a b)
|
||||
(let r2 (app le a b)
|
||||
(let r3 (app gt a b)
|
||||
(let r4 (app ge a b)
|
||||
(let r5 (app ne a b)
|
||||
0)))))))
|
||||
|
||||
(fn main
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body (app print (app drive 1 2)))))
|
||||
@@ -43,7 +43,7 @@
|
||||
(params k acc)
|
||||
(type (fn-type (params (con Int) a) (ret a)))
|
||||
(body
|
||||
(if (app == k 0)
|
||||
(if (app eq k 0)
|
||||
acc
|
||||
(app loop (app - k 1) (app f acc))))
|
||||
(in (app loop n x)))))
|
||||
|
||||
+44
-8
@@ -6,27 +6,33 @@
|
||||
(ctor GT))
|
||||
(class Eq
|
||||
(param a)
|
||||
(doc "Structural equality. Ships in milestone 23 alongside Ord. The primitive `==` operator stays as the surface-level comparator this iter; routing `==` through `Eq.eq` is the declared P2 follow-up (see docs/specs/2026-05-10-23-eq-ord-prelude.md, `Out of scope`).")
|
||||
(doc "Structural equality. The class-method `eq` is the surface-level comparator; `==` as a surface name is not part of the language. Primitive instances Eq Int / Bool / Str / Unit are lowered via try_emit_primitive_instance_body in the codegen.")
|
||||
(method eq
|
||||
(type (fn-type (params (borrow a) (borrow a)) (ret (con Bool))))))
|
||||
(instance
|
||||
(class Eq)
|
||||
(type (con Int))
|
||||
(doc "Eq Int. Body lowers to `icmp eq i64` via the existing primitive `==` dispatch in `lower_eq`.")
|
||||
(doc "Eq Int. Body is placeholder for round-trip stability; codegen intercept try_emit_primitive_instance_body::eq__Int emits `icmp eq i64` with the alwaysinline attribute.")
|
||||
(method eq
|
||||
(body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (body (app == x y))))))
|
||||
(body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (body false)))))
|
||||
(instance
|
||||
(class Eq)
|
||||
(type (con Bool))
|
||||
(doc "Eq Bool. Body lowers to `icmp eq i1` via the existing primitive `==` dispatch in `lower_eq`.")
|
||||
(doc "Eq Bool. Body is placeholder for round-trip stability; codegen intercept try_emit_primitive_instance_body::eq__Bool emits `icmp eq i1` with the alwaysinline attribute.")
|
||||
(method eq
|
||||
(body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (body (app == x y))))))
|
||||
(body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (body false)))))
|
||||
(instance
|
||||
(class Eq)
|
||||
(type (con Str))
|
||||
(doc "Eq Str. The lambda body shape mirrors Int/Bool for round-trip stability, but the codegen intercept in `emit_fn` overrides the body to call `@ail_str_eq` directly — see `try_emit_primitive_instance_body` in `crates/ailang-codegen/src/lib.rs`.")
|
||||
(doc "Eq Str. Body is placeholder for round-trip stability; codegen intercept try_emit_primitive_instance_body::eq__Str overrides it with a call to `@ail_str_eq` and attaches the alwaysinline attribute.")
|
||||
(method eq
|
||||
(body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (body (app == x y))))))
|
||||
(body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (body false)))))
|
||||
(instance
|
||||
(class Eq)
|
||||
(type (con Unit))
|
||||
(doc "Eq Unit. Unit is single-inhabitant so all values compare equal. Body is placeholder; codegen intercept try_emit_primitive_instance_body::eq__Unit emits `ret i1 1`.")
|
||||
(method eq
|
||||
(body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (body true)))))
|
||||
(class Ord
|
||||
(param a)
|
||||
(superclass (class Eq) (type a))
|
||||
@@ -113,4 +119,34 @@
|
||||
(doc "Polymorphic console-print helper. `print x` ≡ `do io/print_str (show x)` with an explicit let-binder around `show x` for heap-Str RC discipline per eob.1 Str carve-out. Ships in milestone 24 as the second half of the Show prelude.")
|
||||
(type (forall (vars a) (constraints (constraint Show a)) (fn-type (params (borrow a)) (ret (con Unit)) (effects IO))))
|
||||
(params x)
|
||||
(body (let s (app show x) (do io/print_str s)))))
|
||||
(body (let s (app show x) (do io/print_str s))))
|
||||
(fn float_eq
|
||||
(doc "IEEE Float equality. `float_eq x y` returns true iff both operands are non-NaN and bit-equal. Lowered to `fcmp oeq double` via try_emit_primitive_instance_body::float_eq with alwaysinline. Replaces the milestone-deleted polymorphic `==` on Float.")
|
||||
(type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
|
||||
(params x y)
|
||||
(body false))
|
||||
(fn float_ne
|
||||
(doc "IEEE Float disequality. `float_ne nan nan` returns true (unordered-or-not-equal per IEEE-754). Lowered to `fcmp une double`.")
|
||||
(type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
|
||||
(params x y)
|
||||
(body false))
|
||||
(fn float_lt
|
||||
(doc "IEEE Float strict less-than. `float_lt nan x` returns false for any x (unordered). Lowered to `fcmp olt double`.")
|
||||
(type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
|
||||
(params x y)
|
||||
(body false))
|
||||
(fn float_le
|
||||
(doc "IEEE Float less-than-or-equal. Lowered to `fcmp ole double`.")
|
||||
(type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
|
||||
(params x y)
|
||||
(body false))
|
||||
(fn float_gt
|
||||
(doc "IEEE Float strict greater-than. Lowered to `fcmp ogt double`.")
|
||||
(type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
|
||||
(params x y)
|
||||
(body false))
|
||||
(fn float_ge
|
||||
(doc "IEEE Float greater-than-or-equal. Lowered to `fcmp oge double`.")
|
||||
(type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
|
||||
(params x y)
|
||||
(body false)))
|
||||
|
||||
@@ -7,7 +7,7 @@
|
||||
(doc "Tail-recursive list builder. acc-prepended.")
|
||||
(type (fn-type (params (con Int) (con IntList)) (ret (con IntList))))
|
||||
(params n acc)
|
||||
(body (if (app == n 0) acc (tail-app cons_n_acc (app - n 1) (term-ctor IntList ICons n acc)))))
|
||||
(body (if (app eq n 0) acc (tail-app cons_n_acc (app - n 1) (term-ctor IntList ICons n acc)))))
|
||||
(fn cons_n
|
||||
(doc "Build [1, 2, ..., n] :: IntList. Order is reverse of build but immaterial for head/sum.")
|
||||
(type (fn-type (params (con Int)) (ret (con IntList))))
|
||||
|
||||
@@ -36,7 +36,7 @@
|
||||
(ret (own (con Tree)))))
|
||||
(params d)
|
||||
(body
|
||||
(if (app == d 0)
|
||||
(if (app eq d 0)
|
||||
(term-ctor Tree TLeaf)
|
||||
(term-ctor Tree TNode 1
|
||||
(app build (app - d 1))
|
||||
@@ -66,7 +66,7 @@
|
||||
(ret (con Int))))
|
||||
(params n t)
|
||||
(body
|
||||
(if (app == n 0)
|
||||
(if (app eq n 0)
|
||||
0
|
||||
(let _v (app pin_aliased t)
|
||||
(app loop (app - n 1) t)))))
|
||||
|
||||
@@ -28,7 +28,7 @@
|
||||
(ret (own (con Tree)))))
|
||||
(params d)
|
||||
(body
|
||||
(if (app == d 0)
|
||||
(if (app eq d 0)
|
||||
(term-ctor Tree TLeaf)
|
||||
(term-ctor Tree TNode 1
|
||||
(app build (app - d 1))
|
||||
|
||||
@@ -24,7 +24,7 @@
|
||||
(type (fn-type (params (con Int)) (ret (con Tree))))
|
||||
(params d)
|
||||
(body
|
||||
(if (app == d 0)
|
||||
(if (app eq d 0)
|
||||
(term-ctor Tree TLeaf)
|
||||
(term-ctor Tree TNode 1
|
||||
(app build (app - d 1))
|
||||
@@ -42,7 +42,7 @@
|
||||
(type (fn-type (params (con Int) (con Tree)) (ret (con Int))))
|
||||
(params n t)
|
||||
(body
|
||||
(if (app == n 0)
|
||||
(if (app eq n 0)
|
||||
0
|
||||
(let _v (app pin t)
|
||||
(app loop (app - n 1) t)))))
|
||||
|
||||
@@ -26,7 +26,7 @@
|
||||
(ret (own (con IntList)))))
|
||||
(params n acc)
|
||||
(body
|
||||
(if (app == n 0)
|
||||
(if (app eq n 0)
|
||||
acc
|
||||
(tail-app cons_n_acc
|
||||
(app - n 1)
|
||||
|
||||
+1
-1
@@ -9,7 +9,7 @@
|
||||
(params y xs)
|
||||
(body (match xs
|
||||
(case (pat-ctor Nil) (term-ctor IntList Cons y (term-ctor IntList Nil)))
|
||||
(case (pat-ctor Cons h t) (if (app <= y h) (term-ctor IntList Cons y (term-ctor IntList Cons h t)) (term-ctor IntList Cons h (app insert y t)))))))
|
||||
(case (pat-ctor Cons h t) (if (app le y h) (term-ctor IntList Cons y (term-ctor IntList Cons h t)) (term-ctor IntList Cons h (app insert y t)))))))
|
||||
(fn sort
|
||||
(doc "Insertion sort: build the result by inserting each head into the sorted tail.")
|
||||
(type (fn-type (params (con IntList)) (ret (con IntList))))
|
||||
|
||||
@@ -172,7 +172,7 @@
|
||||
(ret (con List a)))))
|
||||
(params n xs)
|
||||
(body
|
||||
(if (app <= n 0)
|
||||
(if (app le n 0)
|
||||
(term-ctor List Nil)
|
||||
(match xs
|
||||
(case (pat-ctor Nil) (term-ctor List Nil))
|
||||
@@ -188,7 +188,7 @@
|
||||
(ret (con List a)))))
|
||||
(params n xs)
|
||||
(body
|
||||
(if (app <= n 0)
|
||||
(if (app le n 0)
|
||||
xs
|
||||
(match xs
|
||||
(case (pat-ctor Nil) (term-ctor List Nil))
|
||||
|
||||
@@ -24,7 +24,7 @@
|
||||
(doc "Predicate: x mod 2 == 0.")
|
||||
(type (fn-type (params (con Int)) (ret (con Bool))))
|
||||
(params x)
|
||||
(body (app == (app % x 2) 0)))
|
||||
(body (app eq (app % x 2) 0)))
|
||||
|
||||
(fn double
|
||||
(doc "Multiply by 2. Used as the map arg.")
|
||||
|
||||
@@ -17,7 +17,7 @@
|
||||
(ret (con std_list.List (con Int)))))
|
||||
(params n)
|
||||
(body
|
||||
(if (app == n 0)
|
||||
(if (app eq n 0)
|
||||
(term-ctor std_list.List Nil)
|
||||
(term-ctor std_list.List Cons
|
||||
n
|
||||
|
||||
+1
-1
@@ -3,7 +3,7 @@
|
||||
(doc "rekursive Summe 0..=n")
|
||||
(type (fn-type (params (con Int)) (ret (con Int))))
|
||||
(params n)
|
||||
(body (if (app == n 0) 0 (app + n (app sum (app - n 1))))))
|
||||
(body (if (app eq n 0) 0 (app + n (app sum (app - n 1))))))
|
||||
(fn main
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
|
||||
@@ -11,7 +11,7 @@
|
||||
(fn loop
|
||||
(type (fn-type (params (con Int) (con Int)) (ret (con Int))))
|
||||
(params acc i)
|
||||
(body (if (app == i 0) acc (tail-app loop (app + acc i) (app - i 1)))))
|
||||
(body (if (app eq i 0) acc (tail-app loop (app + acc i) (app - i 1)))))
|
||||
(fn main
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
|
||||
@@ -22,7 +22,7 @@
|
||||
(type (fn-type (params (con Int) (con Int)) (ret (con Int))))
|
||||
(params a b)
|
||||
(body
|
||||
(if (app == b 0)
|
||||
(if (app eq b 0)
|
||||
__unreachable__
|
||||
(app / a b))))
|
||||
|
||||
|
||||
Reference in New Issue
Block a user