fieldtest: canonical-type-names — 5 examples, 9 findings
This commit is contained in:
@@ -0,0 +1 @@
|
||||
{"defs":[{"ctors":[{"fields":[],"name":"INil"},{"fields":[{"k":"con","name":"Int"},{"k":"con","name":"IntList"}],"name":"ICons"}],"doc":"Local Int-list ADT; nothing fancy.","kind":"type","name":"IntList"},{"body":{"arms":[{"body":{"args":[{"lit":{"kind":"int","value":0},"t":"lit"},{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"-","t":"var"},"t":"app"},"pat":{"ctor":"LT","fields":[],"p":"ctor"}},{"body":{"lit":{"kind":"int","value":0},"t":"lit"},"pat":{"ctor":"EQ","fields":[],"p":"ctor"}},{"body":{"lit":{"kind":"int","value":1},"t":"lit"},"pat":{"ctor":"GT","fields":[],"p":"ctor"}}],"scrutinee":{"args":[{"name":"n","t":"var"},{"lit":{"kind":"int","value":0},"t":"lit"}],"fn":{"name":"compare","t":"var"},"t":"app"},"t":"match"},"doc":"Map an Int to -1/0/+1 via prelude.compare. Returns the sign as an Int.","kind":"fn","name":"signum","params":["n"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"}],"ret":{"k":"con","name":"Int"}}},{"body":{"arms":[{"body":{"lit":{"kind":"unit"},"t":"lit"},"pat":{"ctor":"INil","fields":[],"p":"ctor"}},{"body":{"lhs":{"args":[{"args":[{"name":"h","t":"var"}],"fn":{"name":"signum","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"args":[{"name":"t","t":"var"}],"fn":{"name":"drain","t":"var"},"t":"app","tail":true},"t":"seq"},"pat":{"ctor":"ICons","fields":[{"name":"h","p":"var"},{"name":"t","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Print signum of every element of xs, in list order.","kind":"fn","name":"drain","params":["xs"],"type":{"effects":["IO"],"k":"fn","params":[{"k":"con","name":"IntList"}],"ret":{"k":"con","name":"Unit"}}},{"body":{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":0},"t":"lit"},{"lit":{"kind":"int","value":3},"t":"lit"}],"fn":{"name":"-","t":"var"},"t":"app"},{"args":[{"lit":{"kind":"int","value":0},"t":"lit"},{"args":[{"lit":{"kind":"int","value":7},"t":"lit"},{"args":[{"args":[{"lit":{"kind":"int","value":0},"t":"lit"},{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"-","t":"var"},"t":"app"},{"args":[{"lit":{"kind":"int","value":2},"t":"lit"},{"args":[],"ctor":"INil","t":"ctor","type":"IntList"}],"ctor":"ICons","t":"ctor","type":"IntList"}],"ctor":"ICons","t":"ctor","type":"IntList"}],"ctor":"ICons","t":"ctor","type":"IntList"}],"ctor":"ICons","t":"ctor","type":"IntList"}],"ctor":"ICons","t":"ctor","type":"IntList"}],"fn":{"name":"drain","t":"var"},"t":"app"},"kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[],"name":"ct_1_ordering_signum","schema":"ailang/v0"}
|
||||
@@ -0,0 +1,55 @@
|
||||
; Fieldtest — canonical-type-names, axis 4: canonical happy path.
|
||||
;
|
||||
; Reduce a list of Int to a 'sign profile': for each element, print
|
||||
; -1, 0, or +1 according to its compare-to-zero result. Exercises:
|
||||
; - cross-module reference to prelude.Ordering at use site
|
||||
; - pattern match against prelude.Ordering's three constructors LT/EQ/GT
|
||||
; - returning a freshly chosen Int from each arm
|
||||
; - simple recursion over a local List ADT
|
||||
;
|
||||
; Expected stdout (one per line):
|
||||
; -1 ; signum -3
|
||||
; 0 ; signum 0
|
||||
; 1 ; signum 7
|
||||
; -1 ; signum -1
|
||||
; 1 ; signum 2
|
||||
|
||||
(module ct_1_ordering_signum
|
||||
|
||||
(data IntList
|
||||
(doc "Local Int-list ADT; nothing fancy.")
|
||||
(ctor INil)
|
||||
(ctor ICons (con Int) (con IntList)))
|
||||
|
||||
(fn signum
|
||||
(doc "Map an Int to -1/0/+1 via prelude.compare. Returns the sign as an Int.")
|
||||
(type (fn-type (params (con Int)) (ret (con Int))))
|
||||
(params n)
|
||||
(body
|
||||
(match (app compare n 0)
|
||||
(case (pat-ctor LT) (app - 0 1))
|
||||
(case (pat-ctor EQ) 0)
|
||||
(case (pat-ctor GT) 1))))
|
||||
|
||||
(fn drain
|
||||
(doc "Print signum of every element of xs, in list order.")
|
||||
(type (fn-type (params (con IntList)) (ret (con Unit)) (effects IO)))
|
||||
(params xs)
|
||||
(body
|
||||
(match xs
|
||||
(case (pat-ctor INil) (lit-unit))
|
||||
(case (pat-ctor ICons h t)
|
||||
(seq (do io/print_int (app signum h))
|
||||
(tail-app drain t))))))
|
||||
|
||||
(fn main
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body
|
||||
(app drain
|
||||
(term-ctor IntList ICons (app - 0 3)
|
||||
(term-ctor IntList ICons 0
|
||||
(term-ctor IntList ICons 7
|
||||
(term-ctor IntList ICons (app - 0 1)
|
||||
(term-ctor IntList ICons 2
|
||||
(term-ctor IntList INil))))))))))
|
||||
@@ -0,0 +1 @@
|
||||
{"defs":[{"body":{"name":"m","t":"var"},"doc":"Identity over Maybe<Int>; signature uses bare `Maybe` instead of `std_maybe.Maybe`.","kind":"fn","name":"classify","params":["m"],"type":{"effects":[],"k":"fn","params":[{"args":[{"k":"con","name":"Int"}],"k":"con","name":"Maybe"}],"ret":{"args":[{"k":"con","name":"Int"}],"k":"con","name":"Maybe"}}},{"body":{"args":[{"args":[{"lit":{"kind":"int","value":99},"t":"lit"},{"args":[{"args":[{"lit":{"kind":"int","value":7},"t":"lit"}],"ctor":"Just","t":"ctor","type":"std_maybe.Maybe"}],"fn":{"name":"classify","t":"var"},"t":"app"}],"fn":{"name":"std_maybe.from_maybe","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[{"module":"std_maybe"}],"name":"ct_2_bare_cross_module","schema":"ailang/v0"}
|
||||
@@ -0,0 +1,31 @@
|
||||
; Fieldtest — canonical-type-names, axis 1: BareCrossModuleTypeRef.
|
||||
;
|
||||
; A consumer of std_maybe deliberately writes a BARE `Maybe` in its
|
||||
; fn signature instead of `std_maybe.Maybe`. Per ct.1's load-time
|
||||
; validator, the canonical form requires cross-module type refs to
|
||||
; be qualified. Expected: workspace-load error
|
||||
; `BareCrossModuleTypeRef` naming the type and listing the qualified
|
||||
; form as a candidate.
|
||||
;
|
||||
; This is what an LLM author would write if they forgot the
|
||||
; cross-module-qualification rule — the rule fires here at load
|
||||
; time, not deep inside the typechecker.
|
||||
|
||||
(module ct_2_bare_cross_module
|
||||
|
||||
(import std_maybe)
|
||||
|
||||
(fn classify
|
||||
(doc "Identity over Maybe<Int>; signature uses bare `Maybe` instead of `std_maybe.Maybe`.")
|
||||
(type
|
||||
(fn-type
|
||||
(params (con Maybe (con Int)))
|
||||
(ret (con Maybe (con Int)))))
|
||||
(params m)
|
||||
(body m))
|
||||
|
||||
(fn main
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body
|
||||
(do io/print_int (app std_maybe.from_maybe 99 (app classify (term-ctor std_maybe.Maybe Just 7)))))))
|
||||
@@ -0,0 +1 @@
|
||||
{"defs":[{"body":{"name":"w","t":"var"},"doc":"Identity at mystery.Widget — but `mystery` is not a workspace module.","kind":"fn","name":"passthrough","params":["w"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"mystery.Widget"}],"ret":{"k":"con","name":"mystery.Widget"}}},{"body":{"args":[{"lit":{"kind":"str","value":"unreachable"},"t":"lit"}],"op":"io/print_str","t":"do"},"kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[],"name":"ct_3_bad_qualified","schema":"ailang/v0"}
|
||||
@@ -0,0 +1,22 @@
|
||||
; Fieldtest — canonical-type-names, axis 2: BadCrossModuleTypeRef.
|
||||
;
|
||||
; A consumer references a fully qualified type `mystery.Widget`
|
||||
; where the module `mystery` does not exist in the workspace.
|
||||
; Per ct.1's load-time validator, this should be rejected with
|
||||
; `BadCrossModuleTypeRef` naming the unknown owner.
|
||||
|
||||
(module ct_3_bad_qualified
|
||||
|
||||
(fn passthrough
|
||||
(doc "Identity at mystery.Widget — but `mystery` is not a workspace module.")
|
||||
(type
|
||||
(fn-type
|
||||
(params (con mystery.Widget))
|
||||
(ret (con mystery.Widget))))
|
||||
(params w)
|
||||
(body w))
|
||||
|
||||
(fn main
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body (do io/print_str "unreachable"))))
|
||||
@@ -0,0 +1 @@
|
||||
{"defs":[{"body":{"name":"w","t":"var"},"doc":"Identity at std_maybe.Widget — `std_maybe` is real, but `Widget` is not in it.","kind":"fn","name":"passthrough","params":["w"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"std_maybe.Widget"}],"ret":{"k":"con","name":"std_maybe.Widget"}}},{"body":{"args":[{"lit":{"kind":"str","value":"unreachable"},"t":"lit"}],"op":"io/print_str","t":"do"},"kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[{"module":"std_maybe"}],"name":"ct_3b_bad_qualified_known_module","schema":"ailang/v0"}
|
||||
@@ -0,0 +1,23 @@
|
||||
; Fieldtest — canonical-type-names, axis 2 (variant b): BadCrossModuleTypeRef
|
||||
; — known module, unknown type. Author qualifies as `std_maybe.Widget`
|
||||
; where `std_maybe` IS a workspace module but does not declare a
|
||||
; `Widget` type. Per ct.1's load-time validator, this should be
|
||||
; rejected with `BadCrossModuleTypeRef`.
|
||||
|
||||
(module ct_3b_bad_qualified_known_module
|
||||
|
||||
(import std_maybe)
|
||||
|
||||
(fn passthrough
|
||||
(doc "Identity at std_maybe.Widget — `std_maybe` is real, but `Widget` is not in it.")
|
||||
(type
|
||||
(fn-type
|
||||
(params (con std_maybe.Widget))
|
||||
(ret (con std_maybe.Widget))))
|
||||
(params w)
|
||||
(body w))
|
||||
|
||||
(fn main
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body (do io/print_str "unreachable"))))
|
||||
@@ -0,0 +1 @@
|
||||
{"defs":[{"ctors":[{"fields":[{"k":"con","name":"Int"}],"name":"MkBox"}],"doc":"A trivial Int wrapper.","kind":"type","name":"Box"},{"class":"prelude.Eq","kind":"instance","methods":[{"body":{"body":{"arms":[{"body":{"arms":[{"body":{"args":[{"name":"a","t":"var"},{"name":"b","t":"var"}],"fn":{"name":"==","t":"var"},"t":"app"},"pat":{"ctor":"MkBox","fields":[{"name":"b","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"y","t":"var"},"t":"match"},"pat":{"ctor":"MkBox","fields":[{"name":"a","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"x","t":"var"},"t":"match"},"effects":[],"paramTypes":[{"k":"con","name":"Box"},{"k":"con","name":"Box"}],"params":["x","y"],"retType":{"k":"con","name":"Bool"},"t":"lam"},"name":"eq"}],"type":{"k":"con","name":"Box"}}],"imports":[],"name":"ct_4_qualified_class","schema":"ailang/v0"}
|
||||
@@ -0,0 +1,26 @@
|
||||
; Fieldtest — canonical-type-names, axis 3: QualifiedClassName.
|
||||
;
|
||||
; A consumer defines a local Box type and writes an instance for
|
||||
; `prelude.Eq` instead of bare `Eq`. Per ct.1's load-time validator,
|
||||
; class names are NOT module-scoped (they remain workspace-flat,
|
||||
; with MethodNameCollision enforcing uniqueness), so a qualified
|
||||
; class name in an InstanceDef.class field is a schema violation.
|
||||
|
||||
(module ct_4_qualified_class
|
||||
|
||||
(data Box
|
||||
(doc "A trivial Int wrapper.")
|
||||
(ctor MkBox (con Int)))
|
||||
|
||||
(instance
|
||||
(class prelude.Eq)
|
||||
(type (con Box))
|
||||
(method eq
|
||||
(body
|
||||
(lam (params (typed x (con Box)) (typed y (con Box))) (ret (con Bool))
|
||||
(body
|
||||
(match x
|
||||
(case (pat-ctor MkBox a)
|
||||
(match y
|
||||
(case (pat-ctor MkBox b)
|
||||
(app == a b)))))))))))
|
||||
Reference in New Issue
Block a user