diff --git a/boot.lua b/boot.lua index 3f82a9e..ac524e5 100644 --- a/boot.lua +++ b/boot.lua @@ -218,8 +218,10 @@ P.GLOBALS["*release*"] = "0.1" -- port release; kernel *version* comes f -- select direct-call vs APP codegen), the file list, and the LuaJIT version/ -- arch (bytecode is not portable across either). SHEN_KERNEL_CACHE=off -- disables; any other value overrides the cache path. -local CACHE_FORMAT = "SHENKC3" -- 3: per-chunk hoisted (declare ...) block + - -- gensym/inference counters +local CACHE_FORMAT = "SHENKC4" -- 4: hoisted declare typeforms evaluated before + -- `declare` (issue #62); 3: per-chunk hoisted + -- (declare ...) block + gensym/inference + -- counters -- LuaJIT's `bit` library drives the FNV-1a hashing behind both the kernel -- bytecode cache and the user fasl cache. PUC Lua has no `bit` (5.3+ has -- native bitwise operators, but this file must stay parseable by 5.1/LuaJIT), @@ -523,6 +525,34 @@ local function is_declare_form(f) and R.is_cons(f[2]) and R.is_cons(f[2][2]) and f[2][2][2] == R.NIL end +-- A declare's type argument is a KL EXPRESSION — in the 41.2 kernel always a +-- pure rcons constructor tree, e.g. (cons number (cons --> (cons number ()))). +-- Running the form inline evaluates it before `declare` sees it; a hoisted +-- declare must do the same, or the signature registered in shen.*sigf* is over +-- the unevaluated AST and never unifies with a real type (issue #62: System S +-- rejected every kernel signature — arithmetic being the visible case). +-- Only literal trees are evaluated here; anything else refuses the hoist so +-- the form runs inline with full KL semantics. Returns the value, or nil to +-- refuse (KL has no nil, so nil is unambiguous). +local function eval_typeform(e) + if R.is_cons(e) then + local h = e[1] + if R.is_symbol(h) and h.name == "cons" + and R.is_cons(e[2]) and R.is_cons(e[2][2]) and e[2][2][2] == R.NIL then + local a = eval_typeform(e[2][1]) + if a == nil then return nil end + local d = eval_typeform(e[2][2][1]) + if d == nil then return nil end + return R.cons(a, d) + elseif R.is_symbol(h) and h.name == "intern" + and R.is_cons(e[2]) and type(e[2][1]) == "string" and e[2][2] == R.NIL then + return R.intern(e[2][1]) + end + return nil + end + return e -- symbol, number, string, boolean, (): self-evaluating +end + -- Split a kernel file's forms into (body, init forms, declares). Only a -- TRAILING run of non-defun top-level forms is ever moved, and it is run -- immediately after the body chunk, so hoisting cannot reorder anything. In @@ -546,7 +576,9 @@ local function hoist_tail(forms) for i = 1, last do kept[i] = forms[i] end for i = last + 1, d0 - 1 do inits[#inits + 1] = forms[i] end for i = d0, #forms do - decls[#decls + 1] = { name = forms[i][2][1], typ = forms[i][2][2][1] } + local tv = eval_typeform(forms[i][2][2][1]) + if tv == nil then return forms, nil, nil end -- non-literal typeform + decls[#decls + 1] = { name = forms[i][2][1], typ = tv } end return kept, (#inits > 0 and inits or nil), (#decls > 0 and decls or nil) end diff --git a/test/system_s_sigf_spec.lua b/test/system_s_sigf_spec.lua new file mode 100644 index 0000000..ec8800f --- /dev/null +++ b/test/system_s_sigf_spec.lua @@ -0,0 +1,65 @@ +-- system_s_sigf_spec.lua : kernel signatures reach System S (issue #62). +-- +-- luajit test/system_s_sigf_spec.lua +-- +-- `declare` registers each kernel signature in shen.*sigf* as a closure that +-- unifies the goal type against the DECLARED type. boot.lua hoists the +-- trailing (declare Name Typeform) block of types.kl out of the kernel chunk +-- (see hoist_tail), and the regression here was passing Typeform — a KL +-- expression like (cons number (cons --> ...)) — to `declare` UNEVALUATED, so +-- every hoisted signature unified against the raw AST and never matched a +-- real type. The native typecheck harvests signatures separately and masked +-- the bug on the shen.typecheck path; a prolog?-driven shen.system-S query +-- (and the legacy typecheck path) consults the real *sigf* closures, which is +-- exactly what this spec exercises. Expected verdicts match shen-go/shen-cl. + +local shen = require("shen") +shen.boot{ quiet = true } + +local pass, fail = 0, 0 +local function check(desc, got, want) + if got == want then pass = pass + 1 + else + fail = fail + 1 + print(string.format("FAIL %s: got %s want %s", desc, tostring(got), tostring(want))) + end +end + +shen.eval([[ +(define system-s-sigf-spec-query + Hyps [X : A] -> (prolog? (shen.system-S [(shen.curry (receive X)) : (receive A)] (receive Hyps)))) +]]) + +local function judge(src) + return shen.eval("(system-s-sigf-spec-query " .. src .. ")") +end + +-- the four judgments from issue #62: arithmetic/comparison signatures come +-- from the hoisted declare block; cons has a dedicated System S rule and +-- never consults *sigf* (the control). +check("[* 2 3] : number", judge("[] [[* 2 3] : number]"), true) +check("[+ 2 3] : number", judge("[] [[+ 2 3] : number]"), true) +check("[> 2 3] : boolean", judge("[] [[> 2 3] : boolean]"), true) +check("[cons 1 []] : (list number)", judge("[] [[cons 1 []] : [list number]]"), true) + +-- partial application resolves through the same hoisted signature closure +check("partial application [* 2] : (number --> number)", + judge("[] [[* 2] : [number --> number]]"), true) + +-- and wrong judgments must still fail +check("[* 2 3] : string fails", judge("[] [[* 2 3] : string]"), false) +check("[> 2 3] : number fails", judge("[] [[> 2 3] : number]"), false) + +-- the legacy sig closure itself (what lookupsig applies): ground unify of the +-- declared type must succeed — this is false when the typeform was registered +-- unevaluated, whatever engine handles prolog? above. +check("*sigf* closure for + unifies its declared type", + shen.eval([==[ +(let Entry (assoc + (value shen.*sigf*)) + (if (cons? Entry) + ((((((tl Entry) [number --> [number --> number]]) (shen.prolog-vector)) (@v true (@v 0 (vector 0)))) 0) (freeze true)) + symbol-plus-not-in-sigf)) +]==]), true) + +print(string.format("system_s_sigf_spec: %d pass, %d fail", pass, fail)) +os.exit(fail == 0 and 0 or 1)