go: Phase 7 generics closed — types 102/102, +30 cleared, total 556/556 [shapes-static-types-bidirectional]
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 53s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 53s
Canonical generic functions: Map, Filter, Reduce, First end-to-end type-check + run. Plus 20+ typer-only shape tests covering Apply, Compose, ToMap, Swap, Box, Triple, ToSlice, Take, Send, Fill, Eq, Values, Pair, Inspect, etc. Index synth (slice/array/map → element type) added to typer. v0 limitations stamped in tests: SX `/` is float (no int mod emulation), `var r []T` indistinguishable from unbound, single-name constraints opaque (no type-set arithmetic). Shape locked in: "the parser recognizes shapes, the validator recognizes roles." Same AST + different role-validators = different guest semantics. Diary documents this as the lemma the kit should extract — three deliverables (binding-groups, control-flow sentinels, index synthesis) now all instantiate it. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This commit is contained in:
@@ -265,6 +265,19 @@
|
||||
;; (:composite TYPE-OR-EXPR ELEMS) — composite literal
|
||||
(and (list? expr) (= (first expr) :composite))
|
||||
(go-synth-composite ctx (nth expr 1) (nth expr 2))
|
||||
;; (:index OBJ IDX) — slice/map/array element. v0: element type
|
||||
;; is the slice/array element type, or the map value type.
|
||||
(and (list? expr) (= (first expr) :index))
|
||||
(let ((obj-ty (go-synth ctx (nth expr 1))))
|
||||
(cond
|
||||
(go-type-error? obj-ty) obj-ty
|
||||
(and (list? obj-ty) (= (first obj-ty) :ty-slice))
|
||||
(nth obj-ty 1)
|
||||
(and (list? obj-ty) (= (first obj-ty) :ty-array))
|
||||
(nth obj-ty 2)
|
||||
(and (list? obj-ty) (= (first obj-ty) :ty-map))
|
||||
(nth obj-ty 2)
|
||||
:else (list :type-error :index-not-indexable obj-ty)))
|
||||
:else (list :type-error :unsupported-synth expr))))
|
||||
|
||||
(define
|
||||
|
||||
Reference in New Issue
Block a user