From cba843eae58616dc104a0b7ff4ae0483dad8cf14 Mon Sep 17 00:00:00 2001 From: Erik McClure Date: Tue, 14 Jan 2025 19:37:00 -0800 Subject: [PATCH] Add more debug information --- base-env.lua | 85 +++++++++++++++++++-------------- environment.lua | 9 ++-- evaluator.lua | 47 +++++++++++-------- format.lua | 24 +++++++--- terms-generators.lua | 8 +++- terms-pretty.lua | 109 +++++++++++++++++++++++++++++++++++++------ terms.lua | 4 +- test-fitsinto.lua | 13 +++--- types/inferrable.lua | 4 +- types/typed.lua | 4 +- 10 files changed, 219 insertions(+), 88 deletions(-) diff --git a/base-env.lua b/base-env.lua index 4d62b83c..ebb8b27d 100644 --- a/base-env.lua +++ b/base-env.lua @@ -177,7 +177,7 @@ local switch_case = metalanguage.reducer(function(syntax, env) local shadowed, term shadowed, env = env:enter_block(terms.block_purity.inherit) env = env:bind_local( - terms.binding.tuple_elim(names, terms.inferrable_term.bound_variable(env.typechecking_context:len())) + terms.binding.tuple_elim(names, terms.inferrable_term.bound_variable(env.typechecking_context:len(), U.here())) ) ok, term, env = tail:match({ exprs.inferred_expression(metalanguage.accept_handler, env), @@ -365,15 +365,7 @@ local ascribed_name = metalanguage.reducer( -- print(env.enter_block) local shadowed shadowed, env = env:enter_block(terms.block_purity.pure) - local prev_name = "#prev - " - .. syntax.start_anchor.sourceid - .. ":" - .. syntax.start_anchor.line - .. "[" - .. syntax.start_anchor.char - .. "-" - .. syntax.end_anchor.char - .. "]" + local prev_name = "#prev - " .. tostring(syntax.start_anchor) env = env:bind_local( terms.binding.annotated_lambda( prev_name, @@ -848,16 +840,17 @@ local function forall_impl(syntax, env) shadowed, env = env:enter_block(terms.block_purity.pure) -- tail.start_anchor can be nil so we fall back to the start_anchor for this forall type if needed -- TODO: use correct name in lambda parameter instead of adding an extra let + local inner_name = "forall(" .. table.concat(params_names, ", ") .. ")" env = env:bind_local( terms.binding.annotated_lambda( - "#forall-arguments", + inner_name, params_args, tail.start_anchor or syntax.start_anchor, terms.visibility.explicit, literal_purity_pure ) ) - local ok, arg = env:get("#forall-arguments") + local ok, arg = env:get(inner_name) if not ok then error("wtf") end @@ -1041,18 +1034,18 @@ local function lambda_impl(syntax, env) end local args, names, env = thread.args, thread.names, thread.env - local shadow, inner_env = env:enter_block(terms.block_purity.pure) + local inner_name = "λ(" .. table.concat(names, ",") .. ")" inner_env = inner_env:bind_local( terms.binding.annotated_lambda( - "#lambda-arguments", + inner_name, args, syntax.start_anchor, terms.visibility.explicit, literal_purity_pure ) ) - local _, arg = inner_env:get("#lambda-arguments") + local _, arg = inner_env:get(inner_name) inner_env = inner_env:bind_local(terms.binding.tuple_elim(names, arg)) local ok, expr, env = tail:match( { exprs.block(metalanguage.accept_handler, exprs.ExpressionArgs.new(terms.expression_goal.infer, inner_env)) }, @@ -1076,18 +1069,19 @@ local function lambda_prog_impl(syntax, env) end local args, names, env = thread.args, thread.names, thread.env + local inner_name = "λ-prog(" .. table.concat(names, ",") .. ")" local shadow, inner_env = env:enter_block(terms.block_purity.effectful) inner_env = inner_env:bind_local( terms.binding.annotated_lambda( - "#lambda-arguments", + inner_name, args, syntax.start_anchor, terms.visibility.explicit, literal_purity_effectful ) ) - local _, arg = inner_env:get("#lambda-arguments") + local _, arg = inner_env:get(inner_name) inner_env = inner_env:bind_local(terms.binding.tuple_elim(names, arg)) local ok, expr, env = tail:match( { exprs.block(metalanguage.accept_handler, exprs.ExpressionArgs.new(terms.expression_goal.infer, inner_env)) }, @@ -1165,18 +1159,19 @@ local function lambda_annotated_impl(syntax, env) end local args, names, env = thread.args, thread.names, thread.env + local inner_name = "λ-named(" .. table.concat(names, ",") .. ")" local shadow, inner_env = env:enter_block(terms.block_purity.pure) inner_env = inner_env:bind_local( terms.binding.annotated_lambda( - "#lambda-arguments", + inner_name, args, syntax.start_anchor, terms.visibility.explicit, literal_purity_pure ) ) - local _, arg = inner_env:get("#lambda-arguments") + local _, arg = inner_env:get(inner_name) inner_env = inner_env:bind_local(terms.binding.tuple_elim(names, arg)) local ok, ann_expr_env, tail = tail:match({ @@ -1281,7 +1276,7 @@ local function host_term_of(goal, context_len) t, typed.application(typed.literal(value.host_value(host_term_of_inner)), typed.host_tuple_cons(teees(goal))), 1, - typed.host_unwrap(typed.bound_variable(context_len + 1)) + typed.host_unwrap(typed.bound_variable(context_len + 1, U.here())) ) end @@ -1317,7 +1312,7 @@ local function operative_handler_type(ud_type) pnamer, typed.tuple_elim( namesp4, - typed.bound_variable(1), + typed.bound_variable(1, U.here()), 4, typed.tuple_type( typed.enum_cons( @@ -1329,7 +1324,7 @@ local function operative_handler_type(ud_type) typed.tuple_cons( teees( typed.enum_cons(terms.DescCons.empty, typed.tuple_cons(teees())), - typed.lambda(pnamer0, host_term_of(typed.bound_variable(5), 6)) + typed.lambda(pnamer0, host_term_of(typed.bound_variable(5, U.here()), 6)) ) ) ), @@ -1416,7 +1411,7 @@ local function build_wrap(body_fn, type_fn) return lit_term( value.closure( pname_arg, - typed.tuple_elim(names2, typed.bound_variable(1), 2, body_fn(typed.bound_variable(3))), + typed.tuple_elim(names2, typed.bound_variable(1, U.here()), 2, body_fn(typed.bound_variable(3, U.here()))), terms.runtime_context() ), value.pi( @@ -1424,16 +1419,21 @@ local function build_wrap(body_fn, type_fn) terms.tuple_desc( value.closure( pname_type, - typed.tuple_elim(names0, typed.bound_variable(1), 0, typed.star(evaluator.OMEGA + 1, 0)), + typed.tuple_elim( + names0, + typed.bound_variable(1, U.here()), + 0, + typed.star(evaluator.OMEGA + 1, 0) + ), terms.runtime_context() ), value.closure( pname_type, terms.typed_term.tuple_elim( names1, - terms.typed_term.bound_variable(1), + terms.typed_term.bound_variable(1, U.here()), 1, - typed.bound_variable(2) + typed.bound_variable(2, U.here()) ), terms.runtime_context() ) @@ -1442,7 +1442,12 @@ local function build_wrap(body_fn, type_fn) param_info_explicit, value.closure( pname_type, - typed.tuple_elim(names2, typed.bound_variable(1), 2, type_fn(typed.bound_variable(2))), + typed.tuple_elim( + names2, + typed.bound_variable(1, U.here()), + 2, + type_fn(typed.bound_variable(2, U.here())) + ), terms.runtime_context() ), result_info_pure @@ -1464,7 +1469,7 @@ local function build_unwrap(body_fn, type_fn) return lit_term( value.closure( pname_arg, - typed.tuple_elim(names2, typed.bound_variable(1), 2, body_fn(typed.bound_variable(3))), + typed.tuple_elim(names2, typed.bound_variable(1, U.here()), 2, body_fn(typed.bound_variable(3, U.here()))), terms.runtime_context() ), value.pi( @@ -1472,16 +1477,21 @@ local function build_unwrap(body_fn, type_fn) terms.tuple_desc( value.closure( pname_type, - typed.tuple_elim(names0, typed.bound_variable(1), 0, typed.star(evaluator.OMEGA + 1, 0)), + typed.tuple_elim( + names0, + typed.bound_variable(1, U.here()), + 0, + typed.star(evaluator.OMEGA + 1, 0) + ), terms.runtime_context() ), value.closure( pname_type, terms.typed_term.tuple_elim( names1, - terms.typed_term.bound_variable(1), + terms.typed_term.bound_variable(1, U.here()), 1, - type_fn(typed.bound_variable(2)) + type_fn(typed.bound_variable(2, U.here())) ), terms.runtime_context() ) @@ -1490,7 +1500,7 @@ local function build_unwrap(body_fn, type_fn) param_info_explicit, value.closure( pname_type, - typed.tuple_elim(names2, typed.bound_variable(1), 2, typed.bound_variable(2)), + typed.tuple_elim(names2, typed.bound_variable(1, U.here()), 2, typed.bound_variable(2, U.here())), terms.runtime_context() ), result_info_pure @@ -1510,7 +1520,7 @@ local function build_wrapped(body_fn) return lit_term( value.closure( pname_arg, - typed.tuple_elim(names1, typed.bound_variable(1), 1, body_fn(typed.bound_variable(2))), + typed.tuple_elim(names1, typed.bound_variable(1, U.here()), 1, body_fn(typed.bound_variable(2, U.here()))), terms.runtime_context() ), value.pi( @@ -1518,7 +1528,12 @@ local function build_wrapped(body_fn) terms.tuple_desc( value.closure( pname_type, - typed.tuple_elim(names0, typed.bound_variable(1), 0, typed.star(evaluator.OMEGA + 1, 0)), + typed.tuple_elim( + names0, + typed.bound_variable(1, U.here()), + 0, + typed.star(evaluator.OMEGA + 1, 0) + ), terms.runtime_context() ) ) @@ -1526,7 +1541,7 @@ local function build_wrapped(body_fn) param_info_explicit, value.closure( pname_type, - typed.tuple_elim(names1, typed.bound_variable(1), 1, typed.literal(value.host_type_type)), + typed.tuple_elim(names1, typed.bound_variable(1, U.here()), 1, typed.literal(value.host_type_type)), terms.runtime_context() ), result_info_pure diff --git a/environment.lua b/environment.lua index bdcf8f10..4fb55240 100644 --- a/environment.lua +++ b/environment.lua @@ -101,7 +101,7 @@ function environment:bind_local(binding) error("infer returned a bad type for expr in bind_local") end local n = self.typechecking_context:len() - local term = inferrable_term.bound_variable(n + 1) + local term = inferrable_term.bound_variable(n + 1, U.here()) local locals = self.locals:put(name, term) local evaled = evaluator.evaluate(expr_term, self.typechecking_context.runtime_context) -- print "doing let binding" @@ -188,7 +188,7 @@ function environment:bind_local(binding) -- if constructor ~= "cons" then -- error("todo: this error message") -- end - local term = inferrable_term.bound_variable(n + i) + local term = inferrable_term.bound_variable(n + i, U.here()) locals = locals:put(v, term) local evaled = evaluator.index_tuple_value(subject_value, i) @@ -250,7 +250,8 @@ function environment:bind_local(binding) --print(annotation_term:pretty_print(self.typechecking_context)) local evaled = evaluator.evaluate(annotation_term, self.typechecking_context.runtime_context) local bindings = self.bindings:append(binding) - local locals = self.locals:put(param_name, inferrable_term.bound_variable(self.typechecking_context:len() + 1)) + local locals = + self.locals:put(param_name, inferrable_term.bound_variable(self.typechecking_context:len() + 1, U.here())) local typechecking_context = self.typechecking_context:append(param_name, evaled, nil, start_anchor) return update_env(self, { locals = locals, @@ -270,7 +271,7 @@ function environment:bind_local(binding) local first_effect_sig, first_base_type = first_type:unwrap_program_type() --print("FOUND EFFECTFUL BINDING", first_base_type, "produced by ", first_type) local n = self.typechecking_context:len() - local term = inferrable_term.bound_variable(n + 1) + local term = inferrable_term.bound_variable(n + 1, U.here()) local locals = self.locals:put("#program-sequence", term) local typechecking_context = self.typechecking_context:append("#program-sequence", first_base_type, nil, start_anchor) diff --git a/evaluator.lua b/evaluator.lua index 309cd69e..ffb56210 100644 --- a/evaluator.lua +++ b/evaluator.lua @@ -1,7 +1,6 @@ local terms = require "terms" local metalanguage = require "metalanguage" local U = require "alicorn-utils" -local utils = require "alicorn-utils" local format = require "format" local runtime_context = terms.runtime_context local s = require "pretty-printer".s @@ -61,14 +60,14 @@ local function luatovalue(luafunc) for i = 1, len do parameters:append(debug.getlocal(luafunc, i)) - new_body:append(typed.bound_variable(i + 1)) + new_body:append(typed.bound_variable(i + 1, U.here())) end return value.closure( "#luatovalue-args", typed.application( typed.literal(value.host_value(luafunc)), - typed.tuple_elim(parameters, typed.bound_variable(1), len, typed.host_tuple_cons(new_body)) + typed.tuple_elim(parameters, typed.bound_variable(1, U.here()), len, typed.host_tuple_cons(new_body)) ), runtime_context() ) @@ -91,9 +90,12 @@ local function FunctionRelation(srel) end), constrain = luatovalue(function(lctx, val, rctx, use, cause) local inner_info = { - debug = "FunctionRelation(" .. srel.debug_name .. ").constrain " .. utils.here() .. " " .. tostring( - cause - ), + debug = "FunctionRelation(" + .. srel.debug_name + .. ").constrain " + .. U.here() + .. " caused by: " + .. U.strip_ansi(tostring(cause)), } local u = value.neutral(neutral_value.free(free.unique(inner_info))) @@ -308,10 +310,11 @@ local TupleDescRelation = setmetatable({ -- i have considered exploiting the linked-list structure of tuple desc for recursive -- checking, but doing it naively won't work because the unique (representing the tuple -- value) should be the same across the whole desc - local unique = { debug = "TupleDescRelation.constrain" .. utils.here() } + local unique = { debug = "TupleDescRelation.constrain" .. U.here() } local placeholder = value.neutral(neutral_value.free(free.unique(unique))) local tuple_types_val, tuple_types_use, tuple_vals, n = infer_tuple_type_unwrapped2(value.tuple_type(val), value.tuple_type(use), placeholder) + for i = 1, n do typechecker_state:queue_subtype( lctx, @@ -344,7 +347,7 @@ end ---@param v value ---@return value local function const_combinator(v) - return value.closure("#CONST_PARAM", typed_term.bound_variable(1), runtime_context():append(v)) + return value.closure("#CONST_PARAM", typed_term.bound_variable(1, U.here()), runtime_context():append(v)) end ---@param t value @@ -385,7 +388,7 @@ local function substitute_inner_impl(val, mappings, context_len) return typed_term.pi(param_type, param_info, result_type, result_info) elseif val:is_closure() then local param_name, code, capture = val:unwrap_closure() - local unique = { debug = "substitute_inner, val:is_closure" .. utils.here() } + local unique = { debug = "substitute_inner, val:is_closure" .. U.here() } local arg = value.neutral(neutral_value.free(free.unique(unique))) val = apply_value(val, arg) --print("applied closure during substitution: (value term follows)") @@ -394,7 +397,7 @@ local function substitute_inner_impl(val, mappings, context_len) -- Here we need to add the new arg placeholder to a map of things to substitute -- otherwise it would be left as a free.unique in the result local new_mappings = U.shallow_copy(mappings) - new_mappings[unique] = typed_term.bound_variable(context_len + 1) + new_mappings[unique] = typed_term.bound_variable(context_len + 1, U.here()) local val_typed = substitute_inner(val, new_mappings, context_len + 1) -- FIXME: this results in more captures every time we substitute a closure -> @@ -692,7 +695,7 @@ function substitute_type_variables(val, index, param_name) --print("value before substituting (val): (value term follows)") --print(val) local substituted = substitute_inner(val, { - [index] = typed_term.bound_variable(1), + [index] = typed_term.bound_variable(1, U.here()), }, 1) --print("typed term after substitution (substituted): (typed term follows)") --print(substituted:pretty_print(typechecking_context)) @@ -962,12 +965,15 @@ add_comparer("value.enum_type", "value.tuple_desc_type", function(lctx, a, rctx, "#prefix", typed_term.tuple_elim( string_array("prefix-desc"), - typed_term.bound_variable(#rctx + 2), + typed_term.bound_variable(#rctx + 2, U.here()), 1, typed_term.pi( - typed_term.tuple_type(typed_term.bound_variable(#rctx + 3)), + typed_term.tuple_type(typed_term.bound_variable(#rctx + 3, U.here())), typed.literal(value.param_info(value.visibility(terms.visibility.explicit))), - typed.lambda("#arg" .. tostring(#rctx + 1), typed_term.bound_variable(#rctx + 1)), + typed.lambda( + "#arg" .. tostring(#rctx + 1), + typed_term.bound_variable(#rctx + 1, U.here()) + ), typed.literal(value.result_info(terms.result_info(terms.purity.pure))) ) ), @@ -1018,12 +1024,15 @@ add_comparer("value.tuple_desc_type", "value.enum_type", function(lctx, a, rctx, "#prefix", typed_term.tuple_elim( string_array("prefix-desc"), - typed_term.bound_variable(#rctx + 2), + typed_term.bound_variable(#rctx + 2, U.here()), 1, typed_term.pi( - typed_term.tuple_type(typed_term.bound_variable(#rctx + 3)), + typed_term.tuple_type(typed_term.bound_variable(#rctx + 3, U.here())), typed.literal(value.param_info(value.visibility(terms.visibility.explicit))), - typed.lambda("#arg" .. tostring(#rctx + 1), typed_term.bound_variable(#rctx + 1)), + typed.lambda( + "#arg" .. tostring(#rctx + 1), + typed_term.bound_variable(#rctx + 1, U.here()) + ), typed.literal(value.result_info(terms.result_info(terms.purity.pure))) ) ), @@ -1865,7 +1874,7 @@ function infer_impl( usage_counts:append(0) end usage_counts[index] = 1 - local bound = typed_term.bound_variable(index) + local bound = typed_term.bound_variable(index, U.here()) return typeof_bound, usage_counts, bound elseif inferrable_term:is_annotated() then local checkable_term, inferrable_goal_type = inferrable_term:unwrap_annotated() @@ -2253,7 +2262,7 @@ function infer_impl( subject_term, term_variants, typed_term.enum_absurd( - typed_term.bound_variable(typechecking_context:len() + 1), + typed_term.bound_variable(typechecking_context:len() + 1, U.here()), "unacceptable enum variant" ) ) diff --git a/format.lua b/format.lua index 1fb59425..374a1719 100644 --- a/format.lua +++ b/format.lua @@ -21,6 +21,23 @@ end ---@field sourceid string local Anchor = {} +---comment +---@param stop Anchor? +---@return string +function Anchor:display(stop) + if stop == nil then + return tostring(self) + end + + return tostring(self.sourceid) + .. ":" + .. tostring(self.line) + .. ":" + .. tostring(self.char) + .. "-" + .. tostring(stop.char) +end + local anchor_mt = { __lt = function(fst, snd) return snd.line > fst.line or (snd.line == fst.line and snd.char > fst.char) @@ -32,12 +49,7 @@ local anchor_mt = { return (snd.line == fst.line and snd.char == fst.char) end, __tostring = function(self) - return "file " - .. tostring(self.sourceid) - .. ", line " - .. tostring(self.line) - .. " character " - .. tostring(self.char) + return tostring(self.sourceid) .. ":" .. tostring(self.line) .. ":" .. tostring(self.char) end, __index = Anchor, } diff --git a/terms-generators.lua b/terms-generators.lua index d05a0a66..6576aa61 100644 --- a/terms-generators.lua +++ b/terms-generators.lua @@ -745,7 +745,13 @@ local function gen_array_index_fns(self, value_type) -- so we should make sure to use the :ipairs() method instead if key < 1 or key > val.n then p(key, val.n) - error("key passed to array indexing is out of bounds (read code comment above)") + error( + "key passed to array indexing is out of bounds (read code comment above): " + .. tostring(key) + .. "is not within [1," + .. tostring(val.n) + .. "]" + ) end return val.array[key] end diff --git a/terms-pretty.lua b/terms-pretty.lua index 16b86328..a7882e1e 100644 --- a/terms-pretty.lua +++ b/terms-pretty.lua @@ -1,5 +1,6 @@ local fibbuf = require "fibonacci-buffer" local gen = require "terms-generators" +local U = require "alicorn-utils" local typechecking_context_type local runtime_context_type local DescCons @@ -401,14 +402,14 @@ end local function inferrable_tuple_type_hydraulicpress(desc) local ok, constructor, arg = desc:as_enum_cons() if not ok then - return { "" }, 1 + return { " " .. U.here() }, 1 end if constructor == DescCons.empty then return {}, 0 elseif constructor == DescCons.cons then local elements = arg:unwrap_tuple_cons() if elements:len() ~= 2 then - return { "" }, 1 + return { " " .. U.here() }, 1 end local desc = elements[1] local f = elements[2] @@ -417,7 +418,7 @@ local function inferrable_tuple_type_hydraulicpress(desc) prev[n] = f return prev, n else - return { "" }, 1 + return { " " .. U.here() }, 1 end end @@ -466,14 +467,14 @@ end local function typed_tuple_type_hydraulicpress(desc) local ok, constructor, arg = desc:as_enum_cons() if not ok then - return { "" }, 1 + return { " " .. U.here() }, 1 end if constructor == DescCons.empty then return {}, 0 elseif constructor == DescCons.cons then local elements = arg:unwrap_tuple_cons() if elements:len() ~= 2 then - return { "" }, 1 + return { " " .. U.here() }, 1 end local desc = elements[1] local f = elements[2] @@ -482,7 +483,7 @@ local function typed_tuple_type_hydraulicpress(desc) prev[n] = f return prev, n else - return { "" }, 1 + return { " " .. U.here() }, 1 end end @@ -532,7 +533,7 @@ local function value_tuple_type_hydraulicpress(desc) elseif constructor == DescCons.cons then local elements = arg:unwrap_tuple_value() if elements:len() ~= 2 then - return { "" }, 1 + return { " " .. U.here() }, 1 end local desc = elements[1] local f = elements[2] @@ -541,7 +542,7 @@ local function value_tuple_type_hydraulicpress(desc) prev[n] = f return prev, n else - return { "" }, 1 + return { " " .. U.here() }, 1 end end @@ -720,13 +721,13 @@ end ---@param pp PrettyPrint ---@param context AnyContext function binding_override_pretty:annotated_lambda(pp, context) - local param_name, param_annotation, _, visible, pure = self:unwrap_annotated_lambda() + local param_name, param_annotation, anchor, visible, pure = self:unwrap_annotated_lambda() context = ensure_context(context) pp:_enter() pp:unit(pp:_color()) - pp:unit("binding.λ <") + pp:unit("binding.λ [" .. tostring(anchor) .. "] <") pp:any(visible) pp:unit(", ") pp:any(pure) @@ -747,7 +748,7 @@ end ---@param pp PrettyPrint ---@param context AnyContext function inferrable_term_override_pretty:annotated_lambda(pp, context) - local param_name, param_annotation, body, _, visible, pure = self:unwrap_annotated_lambda() + local param_name, param_annotation, body, anchor, visible, pure = self:unwrap_annotated_lambda() context = ensure_context(context) local inner_context = context:append(param_name) local is_tuple_type, desc = as_any_tuple_type(param_annotation) @@ -766,7 +767,7 @@ function inferrable_term_override_pretty:annotated_lambda(pp, context) pp:_enter() pp:unit(pp:_color()) - pp:unit("inferrable.λ <") + pp:unit("inferrable.λ [" .. tostring(anchor) .. "] <") pp:any(visible) pp:unit(", ") pp:any(pure) @@ -886,6 +887,78 @@ function typed_term_override_pretty:lambda(pp, context) pp:_exit() end +---@param pp PrettyPrint +function value_override_pretty:enum_value(pp) + local constructor, arg = self:unwrap_enum_value() + + pp:_enter() + + if constructor == "empty" then + pp:unit(pp:_color()) + pp:unit("enum[]") + pp:unit(pp:_resetcolor()) + else + pp:unit(pp:_color()) + pp:unit("enum[") + pp:unit(pp:_resetcolor()) + + pp:any(arg) + + pp:unit(pp:_color()) + pp:unit("]") + pp:unit(pp:_resetcolor()) + end + + pp:_exit() +end + +---@param pp PrettyPrint +function value_override_pretty:star(pp) + local level, depth = self:unwrap_star() + + pp:_enter() + + pp:unit(pp:_color()) + pp:unit("✪ " .. level .. "|" .. depth) + pp:unit(pp:_resetcolor()) + + pp:_exit() +end + +---@param pp PrettyPrint +function value_override_pretty:visibility(pp) + local v = self:unwrap_visibility() + pp:_enter() + + pp:unit(pp:_color()) + if v:is_implicit() then + pp:unit("implicit") + elseif v:is_explicit() then + pp:unit("explicit") + else + pp:any(v) + end + pp:unit(pp:_resetcolor()) + + pp:_exit() +end + +function value_override_pretty:param_info(pp) + local v = self:unwrap_param_info() + + pp:_enter() + pp:any(v) + pp:_exit() +end + +function value_override_pretty:result_info(pp) + local purity = self:unwrap_result_info():unwrap_result_info() + + pp:_enter() + pp:any(purity) + pp:_exit() +end + ---@param pp PrettyPrint function value_override_pretty:closure(pp) local param_name, code, capture = self:unwrap_closure() @@ -978,9 +1051,19 @@ function inferrable_term_override_pretty:pi(pp, context) pp:unit(pp:_color()) pp:unit("inferrable.Π <") - pp:any(param_info) + pp:unit(pp:_resetcolor()) + if param_info:unwrap_param_info():is_explicit() then + pp:unit("explicit") + elseif param_info:unwrap_param_info():is_implicit() then + pp:unit("implicit") + else + pp:any(param_info) + end + pp:unit(pp:_color()) pp:unit(", ") + pp:unit(pp:_resetcolor()) pp:any(result_info) + pp:unit(pp:_color()) pp:unit("> ") pp:unit(pp:_resetcolor()) diff --git a/terms.lua b/terms.lua index 3a2c9218..56eef829 100644 --- a/terms.lua +++ b/terms.lua @@ -350,7 +350,7 @@ checkable_term:define_enum("checkable", { -- inferrable terms can have their type inferred / don't need a goal type -- stylua: ignore inferrable_term:define_enum("inferrable", { - { "bound_variable", { "index", gen.builtin_number } }, + { "bound_variable", { "index", gen.builtin_number, "debug", gen.builtin_string } }, { "typed", { "type", value, "usage_counts", array(gen.builtin_number), @@ -581,7 +581,7 @@ local unique_id = gen.builtin_table -- typed terms have been typechecked but do not store their type internally -- stylua: ignore typed_term:define_enum("typed", { - { "bound_variable", { "index", gen.builtin_number } }, + { "bound_variable", { "index", gen.builtin_number, "debug", gen.builtin_string } }, { "literal", { "literal_value", value } }, { "lambda", { "param_name", gen.builtin_string, diff --git a/test-fitsinto.lua b/test-fitsinto.lua index 5b8f6edc..e4165b7b 100644 --- a/test-fitsinto.lua +++ b/test-fitsinto.lua @@ -2,6 +2,7 @@ local traits = require "traits" local terms = require "terms" local gen = require "terms-generators" local evaluator = require "evaluator" +local U = require "alicorn-utils" local value = terms.value local typed = terms.typed_term @@ -133,7 +134,7 @@ local passed, failed, total = (require "tap")(function(test) val_desc_empty, value.closure( "#A", - typed.tuple_elim(names(), typed.bound_variable(1), 0, typed.star(1)), + typed.tuple_elim(names(), typed.bound_variable(1, U.here()), 0, typed.star(1)), terms.runtime_context() ) ) @@ -142,9 +143,9 @@ local passed, failed, total = (require "tap")(function(test) "#B", terms.typed_term.tuple_elim( names("#FOO"), - terms.typed_term.bound_variable(1), + terms.typed_term.bound_variable(1, U.here()), 1, - typed.bound_variable(2) + typed.bound_variable(2, U.here()) ), terms.runtime_context() ) @@ -159,7 +160,7 @@ local passed, failed, total = (require "tap")(function(test) val_desc_empty, value.closure( "#C", - typed.tuple_elim(names(), typed.bound_variable(1), 0, typed.star(1)), + typed.tuple_elim(names(), typed.bound_variable(1, U.here()), 0, typed.star(1)), terms.runtime_context() ) ) @@ -168,9 +169,9 @@ local passed, failed, total = (require "tap")(function(test) "#D", terms.typed_term.tuple_elim( names("#BAR"), - terms.typed_term.bound_variable(1), + terms.typed_term.bound_variable(1, U.here()), 1, - typed.bound_variable(2) + typed.bound_variable(2, U.here()) ), terms.runtime_context() ) diff --git a/types/inferrable.lua b/types/inferrable.lua index 22b07989..1694c6aa 100644 --- a/types/inferrable.lua +++ b/types/inferrable.lua @@ -7,9 +7,11 @@ inferrable = {} ---@return boolean function inferrable:is_bound_variable() end ---@return number index +---@return string debug function inferrable:unwrap_bound_variable() end ---@return boolean ---@return number index +---@return string debug function inferrable:as_bound_variable() end ---@return boolean function inferrable:is_typed() end @@ -366,7 +368,7 @@ function inferrable:as_program_type() end ---@class (exact) inferrableType: EnumType ---@field define_enum fun(self: inferrableType, name: string, variants: Variants): inferrableType ----@field bound_variable fun(index: number): inferrable +---@field bound_variable fun(index: number, debug: string): inferrable ---@field typed fun(type: value, usage_counts: ArrayValue, typed_term: typed): inferrable ---@field annotated_lambda fun(param_name: string, param_annotation: inferrable, body: inferrable, start_anchor: Anchor, visible: visibility, pure: checkable): inferrable ---@field pi fun(param_type: inferrable, param_info: checkable, result_type: inferrable, result_info: checkable): inferrable diff --git a/types/typed.lua b/types/typed.lua index abdd0e1f..b3779cdd 100644 --- a/types/typed.lua +++ b/types/typed.lua @@ -7,9 +7,11 @@ typed = {} ---@return boolean function typed:is_bound_variable() end ---@return number index +---@return string debug function typed:unwrap_bound_variable() end ---@return boolean ---@return number index +---@return string debug function typed:as_bound_variable() end ---@return boolean function typed:is_literal() end @@ -520,7 +522,7 @@ function typed:as_constrained_type() end ---@class (exact) typedType: EnumType ---@field define_enum fun(self: typedType, name: string, variants: Variants): typedType ----@field bound_variable fun(index: number): typed +---@field bound_variable fun(index: number, debug: string): typed ---@field literal fun(literal_value: value): typed ---@field lambda fun(param_name: string, body: typed): typed ---@field pi fun(param_type: typed, param_info: typed, result_type: typed, result_info: typed): typed