From b3732ca82e2eecb1bdf6f8344cb1eedfe3ea4094 Mon Sep 17 00:00:00 2001 From: Dusk Banks Date: Mon, 13 Jan 2025 17:11:47 -0800 Subject: [PATCH] [WIP] comprehensively use a `Symbol` type --- alicorn-expressions.lua | 178 ++++++++++++++---------------------- base-env.lua | 170 +++++++++++++++++----------------- core-operatives.lua | 7 +- environment.lua | 28 +++--- evaluator.lua | 85 +++++++++-------- format-adapter.lua | 9 +- format.lua | 113 ++++++++++++++++++----- metalanguage.lua | 19 ++-- modules.lua | 2 +- runtest.lua | 4 +- syntax-schema.lua | 69 +++++++------- terms-pretty.lua | 36 ++++---- terms.lua | 98 +++++++++++--------- test-fitsinto.lua | 19 ++-- test.lua | 3 +- types/binding.lua | 22 +++-- types/checkable.lua | 6 +- types/inferrable.lua | 28 ++++-- types/neutral_value.lua | 6 +- types/placeholder_debug.lua | 2 +- types/typed.lua | 18 ++-- types/value.lua | 18 ++-- unformatter.lua | 4 +- 23 files changed, 503 insertions(+), 441 deletions(-) diff --git a/alicorn-expressions.lua b/alicorn-expressions.lua index 8fe2c644..dfe11fce 100644 --- a/alicorn-expressions.lua +++ b/alicorn-expressions.lua @@ -24,7 +24,7 @@ local inferrable_array = array(inferrable_term) local typed_array = array(typed_term) local value_array = array(value) local usage_array = array(gen.builtin_number) -local name_array = array(gen.builtin_string) +local name_array = terms.symbol_array local param_info_implicit = value.param_info(value.visibility(visibility.implicit)) local param_info_explicit = value.param_info(value.visibility(visibility.explicit)) @@ -37,7 +37,10 @@ local infer = evaluator.infer --local typechecker_state = evaluator.typechecker_state local format = require "format" -local NIL_ANCHOR = format.create_anchor(0, 0, "") +local create_symbol = format.create_symbol +local is_symbol = format.is_symbol +local internal_symbols = format.internal_symbols +local nil_anchor = format.nil_anchor local U = require "alicorn-utils" @@ -212,12 +215,11 @@ local infix_data = { -- # is the comment character and is forbidden here } ----@param symbol SyntaxSymbol +---@param symbol Symbol ---@return boolean ----@return SyntaxSymbol | string +---@return Symbol | string local function shunting_yard_prefix_handler(_, symbol) - assert(symbol and symbol["kind"]) - + assert(is_symbol(symbol)) if not prefix_data[(symbol.str):sub(1, 1)] or (symbol.str):find("_") then return false, "symbol was provided in a prefix operator place, but the symbol isn't a valid prefix operator: " @@ -226,16 +228,16 @@ local function shunting_yard_prefix_handler(_, symbol) return true, symbol end ----@param symbol SyntaxSymbol +---@param symbol Symbol ---@param a ConstructedSyntax ---@param b ConstructedSyntax ---@return boolean ---@return boolean|string ----@return SyntaxSymbol? +---@return Symbol? ---@return ConstructedSyntax? ---@return ConstructedSyntax? local function shunting_yard_infix_handler(_, symbol, a, b) - assert(symbol and symbol["kind"]) + assert(is_symbol(symbol)) if not infix_data[(symbol.str):sub(1, 1)] or (symbol.str):find("_") then return false, "symbol was provided in an infix operator place, but the symbol isn't a valid infix operator: " @@ -252,7 +254,7 @@ end ---@class (exact) TaggedOperator ---@field type OperatorType ----@field symbol SyntaxSymbol +---@field symbol Symbol ---@param yard { n: integer, [integer]: TaggedOperator } ---@param output { n: integer, [integer]: ConstructedSyntax } @@ -295,11 +297,11 @@ local function shunting_yard_pop(yard, output, start_anchor, end_anchor) end end ----@param new_symbol SyntaxSymbol +---@param new_symbol Symbol ---@param yard_operator TaggedOperator ---@return boolean local function shunting_yard_should_pop(new_symbol, yard_operator) - assert(new_symbol and new_symbol["kind"]) + assert(is_symbol(new_symbol)) -- new_symbol is always infix, as we never pop while adding a prefix operator -- prefix operators always have higher precedence than infix operators @@ -350,7 +352,7 @@ local function shunting_yard(a, b, yard, output, start_anchor, end_anchor) -- first, collect all prefix operators local is_prefix, prefix_symbol = a:match({ metalanguage.issymbol(shunting_yard_prefix_handler) }, metalanguage.failure_handler, nil) - ---@cast prefix_symbol SyntaxSymbol + ---@cast prefix_symbol Symbol if is_prefix then local ok, next_a, next_b = b:match({ metalanguage.ispair(metalanguage.accept_handler) }, metalanguage.failure_handler, nil) @@ -382,7 +384,7 @@ local function shunting_yard(a, b, yard, output, start_anchor, end_anchor) return ok, more end if infix_symbol then - assert(infix_symbol["kind"]) + assert(is_symbol(infix_symbol)) end if not more then while yard.n > 0 do @@ -401,7 +403,7 @@ local function shunting_yard(a, b, yard, output, start_anchor, end_anchor) return shunting_yard(next_a, next_b, yard, output, start_anchor, end_anchor) end ----@param symbol SyntaxSymbol +---@param symbol Symbol ---@param arg ConstructedSyntax ---@return boolean ---@return OperatorType|string @@ -416,7 +418,7 @@ local function expression_prefix_handler(_, symbol, arg) end ---@param left ConstructedSyntax ----@param symbol SyntaxSymbol +---@param symbol Symbol ---@param right ConstructedSyntax ---@return boolean ---@return OperatorType|string @@ -424,7 +426,7 @@ end ---@return ConstructedSyntax? ---@return ConstructedSyntax? local function expression_infix_handler(_, left, symbol, right) - assert(symbol and symbol["kind"]) + assert(is_symbol(symbol)) if not infix_data[(symbol.str):sub(1, 1)] or (symbol.str):find("_") then return false, @@ -444,7 +446,7 @@ local function speculate_pi_type(env, metaval) param_mv:as_value(), param_info_implicit, value.closure( - "#spec-pi", + internal_symbols["#spec-pi"], typed_term.literal(result_mv:as_value()), env.typechecking_context.runtime_context ), @@ -460,7 +462,7 @@ local function speculate_pi_type(env, metaval) env.typechecking_context, pi, env.typechecking_context, - terms.constraintcause.primitive("Speculating on pi type", NIL_ANCHOR, NIL_ANCHOR) + terms.constraintcause.primitive("Speculating on pi type", nil_anchor, nil_anchor) ) return pi @@ -475,7 +477,7 @@ local function speculate_pi_type(env, metaval) param_mv:as_value(), param_info_explicit, value.closure( - "#spec-pi", + internal_symbols["#spec-pi"], typed_term.literal(result_mv:as_value()), env.typechecking_context.runtime_context ), @@ -491,7 +493,7 @@ local function speculate_pi_type(env, metaval) env.typechecking_context, pi, env.typechecking_context, - terms.constraintcause.primitive("Speculating on pi type", NIL_ANCHOR, NIL_ANCHOR) + terms.constraintcause.primitive("Speculating on pi type", nil_anchor, nil_anchor) ) return pi @@ -809,44 +811,32 @@ local function expression_pairhandler(args, a, b) return false, "unknown type for pairhandler " .. type_of_term.kind, env end ----@param symbol SyntaxSymbol ----@return SyntaxSymbol ----@return SyntaxSymbol? +---@param symbol Symbol +---@return Symbol +---@return Symbol? local function split_dot_accessors(symbol) - if symbol then - local split_dot_pos = (symbol.str):find("%.") - - if split_dot_pos then - local first, second = (symbol.str):match("([^.]+)%.(.+)") - - local first_end_anchor = symbol.end_anchor - first_end_anchor.char = symbol.start_anchor.char + split_dot_pos - - local firstsymbol = { - kind = "symbol", - str = first, - start_anchor = symbol.start_anchor, - end_anchor = first_end_anchor, - } - - -- we can assume it is on the same line. - local second_start_anchor = symbol.start_anchor - second_start_anchor.char = second_start_anchor.char + split_dot_pos - - local secondsymbol = { - kind = "symbol", - str = second, - start_anchor = second_start_anchor, - end_anchor = symbol.end_anchor, - } - - return firstsymbol, secondsymbol - end + local split_dot_pos = (symbol.str):find("%.") + + if split_dot_pos then + local first, second = (symbol.str):match("([^.]+)%.(.+)") + + local first_end_anchor = symbol.end_anchor + first_end_anchor.char = symbol.start_anchor.char + split_dot_pos + local first_symbol = create_symbol(first, symbol.start_anchor, first_end_anchor) + + -- we can assume it is on the same line. + local second_start_anchor = symbol.start_anchor + second_start_anchor.char = second_start_anchor.char + split_dot_pos + local second_symbol = create_symbol(second, second_start_anchor, symbol.end_anchor) + + return first_symbol, second_symbol + else + return symbol end end ---@param args ExpressionArgs ----@param name SyntaxSymbol +---@param name Symbol ---@return boolean ---@return inferrable | checkable | string ---@return Environment? @@ -857,58 +847,24 @@ local function expression_symbolhandler(args, name) --print(name, split_dot_accessors(name)) local front, rest = split_dot_accessors(name) - assert(name["kind"]) - - if front then - assert(front["kind"]) - end - - if not front then - local ok, val = env:get(name.str) - if not ok then - ---@cast val string - return ok, val, env - end - ---@cast val -string - if goal:is_check() then - return true, checkable_term.inferrable(val), env - end - return ok, val, env - else - local ok, part = env:get(front.str) - if not ok then - ---@cast part string - return false, part, env - end - ---@cast part -string - while front do - name = rest - front, rest = split_dot_accessors(name) - assert(front.str) - local namearray - if front then - assert(front["kind"]) - end - - if front and front.str then - namearray = front.str - else - assert(name) - assert(name.str) - namearray = name.str - end - - part = inferrable_term.record_elim( - part, - name_array(namearray), - inferrable_term.bound_variable(env.typechecking_context:len() + 1) - ) - end - if goal:is_check() then - return true, checkable_term.inferrable(part), env - end + local ok, part = env:get(front.str) + if not ok then + ---@cast part string return ok, part, env end + ---@cast part -string + while rest do + front, rest = split_dot_accessors(rest) + part = inferrable_term.record_elim( + part, + name_array(front), + inferrable_term.bound_variable(env.typechecking_context:len() + 1) + ) + end + if goal:is_check() then + return true, checkable_term.inferrable(part), env + end + return ok, part, env end ---@param args ExpressionArgs @@ -1079,15 +1035,15 @@ local function host_operative(fn, name) end local tuple_conv = typed_term.tuple_cons(tuple_conv_elements) local host_tuple_conv = typed_term.host_tuple_cons(host_tuple_conv_elements) - local param_names = name_array("#syntax", "#env", "#userdata", "#goal") + local param_names = name_array(internal_symbols["#syntax"], internal_symbols["#env"], internal_symbols["#userdata"], internal_symbols["#goal"]) local tuple_to_host_tuple = typed_term.tuple_elim(param_names, typed_term.bound_variable(1), nparams, host_tuple_conv) local tuple_to_host_tuple_fn = typed_term.application(typed_host_fn, tuple_to_host_tuple) - local result_names = name_array("#term", "#env") + local result_names = name_array(internal_symbols["#term"], internal_symbols["#env"]) local tuple_to_tuple_fn = typed_term.tuple_elim(result_names, tuple_to_host_tuple_fn, 2, tuple_conv) -- 3: wrap it in a closure with an empty capture, not a typed lambda -- this ensures variable 1 is the argument tuple - local value_fn = value.closure("#OPERATIVE_PARAM", tuple_to_tuple_fn, runtime_context()) + local value_fn = value.closure(internal_symbols["#OPERATIVE_PARAM"], tuple_to_tuple_fn, runtime_context()) local userdata_type = value.tuple_type(terms.empty) return inferrable_term.typed( @@ -1166,7 +1122,7 @@ collect_tuple = metalanguage.reducer( desc = terms.cons( desc, value.closure( - "#collect-tuple-param", + internal_symbols["#collect-tuple-param"], typed_term.literal(value.singleton(next_elem_type, next_val)), env.typechecking_context.runtime_context ) @@ -1205,7 +1161,7 @@ collect_tuple = metalanguage.reducer( env.typechecking_context, goal_type, env.typechecking_context, - terms.constraintcause.primitive("tuple type in collect_tuple", NIL_ANCHOR, NIL_ANCHOR) + terms.constraintcause.primitive("tuple type in collect_tuple", nil_anchor, nil_anchor) ) return true, checkable_term.tuple_cons(collected_terms), env else @@ -1251,7 +1207,7 @@ collect_host_tuple = metalanguage.reducer( desc = terms.cons( desc, value.closure( - "#collect-host-tuple-param", + internal_symbols["#collect-host-tuple-param"], typed_term.literal(value.singleton(next_elem_type, next_val)), env.typechecking_context.runtime_context ) @@ -1286,7 +1242,7 @@ collect_host_tuple = metalanguage.reducer( env.typechecking_context, goal_type, env.typechecking_context, - terms.constraintcause.primitive("host tuple type in collect_host_tuple", NIL_ANCHOR, NIL_ANCHOR) + terms.constraintcause.primitive("host tuple type in collect_host_tuple", nil_anchor, nil_anchor) ) return true, checkable_term.host_tuple_cons(collected_terms), env else diff --git a/base-env.lua b/base-env.lua index 391849a6..1f4b9d02 100644 --- a/base-env.lua +++ b/base-env.lua @@ -9,7 +9,9 @@ local evaluator = require "evaluator" local U = require "alicorn-utils" local format = require "format" -local NIL_ANCHOR = format.create_anchor(0, 0, "") +local create_symbol = format.create_symbol +local internal_symbols = format.internal_symbols +local nil_anchor = format.nil_anchor local value = terms.value local typed = terms.typed_term @@ -74,24 +76,20 @@ local function let_impl(syntax, env) error("env in let_impl isn't an env") end - if not name["kind"] then + if format.is_symbol(name) then + env = env:bind_local(terms.binding.let(name, expr, syntax.start_anchor, syntax.end_anchor)) + else --print("binding destructuring with let") --p(name) local tupletype = gen.declare_array(gen.builtin_string) local names = {} for _, v in ipairs(name) do - table.insert(names, v.str) - if v.kind == nil then - error("v.kind is nil") - end + assert(format.is_symbol(v), "let_impl: v is not a Symbol") + table.insert(names, v) end - env = env:bind_local(terms.binding.tuple_elim(tupletype(table.unpack(names)), expr)) - else - if name["kind"] == nil then - error("name['kind'] is nil") - end - env = env:bind_local(terms.binding.let(name.str, expr)) + require("lldebugger").requestBreak() + env = env:bind_local(terms.binding.tuple_elim(terms.symbol_array(table.unpack(names)), expr, syntax.start_anchor, syntax.end_anchor)) end return true, @@ -123,7 +121,7 @@ local function mk_impl(syntax, env) if not ok then return ok, tuple end - return ok, terms.inferrable_term.enum_cons(name.str, tuple), env + return ok, terms.inferrable_term.enum_cons(name, tuple), env end ---@type Matcher @@ -137,16 +135,6 @@ local switch_case_header_matcher = metalanguage.listtail( metalanguage.symbol_exact(metalanguage.accept_handler, "->") ) ----@param ... SyntaxSymbol ----@return ... -local function unwrap_into_string(...) - local args = { ... } - for i, v in ipairs(args) do - args[i] = v.str - end - return table.unpack(args) -end - ---@param syntax ConstructedSyntax ---@param env Environment local switch_case = metalanguage.reducer(function(syntax, env) @@ -155,7 +143,7 @@ local switch_case = metalanguage.reducer(function(syntax, env) return ok, tag end - local names = gen.declare_array(gen.builtin_string)(unwrap_into_string(table.unpack(tag, 2))) + local names = terms.symbol_array(table.unpack(tag, 2)) tag = tag[1] if not tag then @@ -181,7 +169,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(), syntax.start_anchor, syntax.end_anchor), syntax.start_anchor, syntax.end_anchor) ) ok, term, env = tail:match({ exprs.inferred_expression(metalanguage.accept_handler, env), @@ -216,20 +204,20 @@ local function switch_impl(syntax, env) end --TODO rewrite this to collect the branch envs and join them back together: tag, term = table.unpack(tag) - variants:set(tag.str, term) + variants:set(tag, term) end return true, terms.inferrable_term.enum_case(subj, variants), env end ---@param _ any ----@param symbol SyntaxSymbol +---@param symbol Symbol ---@param exprenv { val:inferrable, env:Environment } ---@return boolean ----@return { name:string, expr:inferrable } +---@return { name: Symbol, expr:inferrable } ---@return Environment local function record_threaded_element_acceptor(_, symbol, exprenv) local expr, env = utils.unpack_val_env(exprenv) - return true, { name = symbol.str, expr = expr }, env + return true, { name = symbol, expr = expr }, env end ---@param env Environment @@ -251,9 +239,9 @@ local function record_build(syntax, env) if not ok then return ok, defs end - local map = gen.declare_map(gen.builtin_string, terms.inferrable_term)() + local map = gen.declare_map(terms.symbol_type, terms.inferrable_term)() for _, v in ipairs(defs) do - map[v.name] = v.expr + map:set(v.name, v.expr) end return true, terms.inferrable_term.record_cons(map), env end @@ -311,7 +299,7 @@ local pure_ascribed_name = metalanguage.reducer( ---@param syntax ConstructedSyntax ---@param env Environment ---@return boolean - ---@return string + ---@return Symbol ---@return inferrable? ---@return Environment? function(syntax, env) @@ -346,7 +334,7 @@ local pure_ascribed_name = metalanguage.reducer( typed.literal(type_mv:as_value()) ) end - return true, name.str, type, env + return true, name, type, env end, "pure_ascribed_name" ) @@ -371,7 +359,7 @@ local ascribed_name = metalanguage.reducer( shadowed, env = env:enter_block(terms.block_purity.pure) env = env:bind_local( terms.binding.annotated_lambda( - "#prev", + internal_symbols["#prev"], prev, syntax.start_anchor, syntax.end_anchor, @@ -379,12 +367,12 @@ local ascribed_name = metalanguage.reducer( literal_purity_pure ) ) - local ok, prev_binding = env:get("#prev") + local ok, prev_binding = env:get(internal_symbols["#prev"]) if not ok then error "#prev should always be bound, was just added" end ---@cast prev_binding -string - env = env:bind_local(terms.binding.tuple_elim(names, prev_binding)) + env = env:bind_local(terms.binding.tuple_elim(names, prev_binding, syntax.start_anchor, syntax.end_anchor)) local ok, name, val, env = syntax:match({ pure_ascribed_name(metalanguage.accept_handler, env) }, metalanguage.failure_handler, nil) if not ok then @@ -749,26 +737,27 @@ local function make_host_func_syntax(effectful) local shadowed 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 host func type if needed + local start_anchor, end_anchor = tail.start_anchor or syntax.start_anchor, tail.end_anchor or syntax.end_anchor -- TODO: use correct name in lambda parameter instead of adding an extra let env = env:bind_local( terms.binding.annotated_lambda( - "#host-func-arguments", + internal_symbols["#host-func-arguments"], params_args, - tail.start_anchor or syntax.start_anchor, - tail.end_anchor or syntax.end_anchor, + start_anchor, + end_anchor, terms.visibility.explicit, literal_purity_pure ) ) - local ok, arg = env:get("#host-func-arguments") + local ok, arg = env:get(internal_symbols["#host-func-arguments"]) if not ok then error("wtf") end ---@cast arg -string if params_single then - env = env:bind_local(terms.binding.let(params_names, arg)) + env = env:bind_local(terms.binding.let(params_names, arg, start_anchor, end_anchor)) else - env = env:bind_local(terms.binding.tuple_elim(params_names, arg)) + env = env:bind_local(terms.binding.tuple_elim(params_names, arg, start_anchor, end_anchor)) end local ok, results_thread = tail:match({ @@ -845,26 +834,27 @@ local function forall_impl(syntax, env) local shadowed 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 + local start_anchor, end_anchor = tail.start_anchor or syntax.start_anchor, tail.end_anchor or syntax.end_anchor -- TODO: use correct name in lambda parameter instead of adding an extra let env = env:bind_local( terms.binding.annotated_lambda( - "#forall-arguments", + internal_symbols["#forall-arguments"], params_args, - tail.start_anchor or syntax.start_anchor, - tail.end_anchor or syntax.end_anchor, + start_anchor, + end_anchor, terms.visibility.explicit, literal_purity_pure ) ) - local ok, arg = env:get("#forall-arguments") + local ok, arg = env:get(internal_symbols["#forall-arguments"]) if not ok then error("wtf") end ---@cast arg -string if params_single then - env = env:bind_local(terms.binding.let(params_names, arg)) + env = env:bind_local(terms.binding.let(params_names, arg, start_anchor, end_anchor)) else - env = env:bind_local(terms.binding.tuple_elim(params_names, arg)) + env = env:bind_local(terms.binding.tuple_elim(params_names, arg, start_anchor, end_anchor)) end local ok, results_thread = tail:match({ @@ -987,7 +977,7 @@ local function apply_operative_impl(syntax, env) env.typechecking_context, spec_type, env.typechecking_context, - terms.constraintcause.primitive("apply", NIL_ANCHOR, NIL_ANCHOR) + terms.constraintcause.primitive("apply", nil_anchor, nil_anchor) ) local ok, args_inferrable_term = tail:match({ @@ -1040,11 +1030,12 @@ local function lambda_impl(syntax, env) end local args, names, env = thread.args, thread.names, thread.env + ---@cast env Environment local shadow, inner_env = env:enter_block(terms.block_purity.pure) inner_env = inner_env:bind_local( terms.binding.annotated_lambda( - "#lambda-arguments", + internal_symbols["#lambda-arguments"], args, syntax.start_anchor, syntax.end_anchor, @@ -1052,13 +1043,14 @@ local function lambda_impl(syntax, env) literal_purity_pure ) ) - local _, arg = inner_env:get("#lambda-arguments") - inner_env = inner_env:bind_local(terms.binding.tuple_elim(names, arg)) + local _, arg = inner_env:get(internal_symbols["#lambda-arguments"]) + inner_env = inner_env:bind_local(terms.binding.tuple_elim(names, arg, syntax.start_anchor, syntax.end_anchor)) local ok, expr, env = tail:match( { exprs.block(metalanguage.accept_handler, exprs.ExpressionArgs.new(terms.expression_goal.infer, inner_env)) }, metalanguage.failure_handler, nil ) + ---@cast env Environment if not ok then return ok, expr end @@ -1076,11 +1068,12 @@ local function lambda_prog_impl(syntax, env) end local args, names, env = thread.args, thread.names, thread.env + ---@cast env Environment local shadow, inner_env = env:enter_block(terms.block_purity.effectful) inner_env = inner_env:bind_local( terms.binding.annotated_lambda( - "#lambda-arguments", + internal_symbols["#lambda-arguments"], args, syntax.start_anchor, syntax.end_anchor, @@ -1088,13 +1081,15 @@ local function lambda_prog_impl(syntax, env) literal_purity_effectful ) ) - local _, arg = inner_env:get("#lambda-arguments") - inner_env = inner_env:bind_local(terms.binding.tuple_elim(names, arg)) + local _, arg = inner_env:get(internal_symbols["#lambda-arguments"]) + require("lldebugger").requestBreak() + inner_env = inner_env:bind_local(terms.binding.tuple_elim(names, arg, syntax.start_anchor, syntax.end_anchor)) local ok, expr, env = tail:match( { exprs.block(metalanguage.accept_handler, exprs.ExpressionArgs.new(terms.expression_goal.infer, inner_env)) }, metalanguage.failure_handler, nil ) + ---@cast env Environment if not ok then return ok, expr end @@ -1179,7 +1174,8 @@ local function lambda_annotated_impl(syntax, env) ) ) local _, arg = inner_env:get("#lambda-arguments") - inner_env = inner_env:bind_local(terms.binding.tuple_elim(names, arg)) + require("lldebugger").requestBreak() + inner_env = inner_env:bind_local(terms.binding.tuple_elim(names, arg, syntax.start_anchor, syntax.end_anchor)) local ok, ann_expr_env, tail = tail:match({ metalanguage.listtail( @@ -1252,15 +1248,15 @@ local function host_term_of_inner(goal) end local host_term_of_inner_type = value.host_function_type( value.host_tuple_type( - terms.tuple_desc(value.closure("#htoit-empty", typed.literal(terms.host_goal_type), terms.runtime_context())) + terms.tuple_desc(value.closure(internal_symbols["#htoit-empty"], typed.literal(terms.host_goal_type), terms.runtime_context())) ), value.closure( - "#htoit-params", + internal_symbols["#htoit-params"], typed.literal( value.host_tuple_type( terms.tuple_desc( value.closure( - "#htoit-empty", + internal_symbols["#htoit-empty"], typed.host_wrapped_type(typed.literal(value.host_type_type)), terms.runtime_context() ) @@ -1291,20 +1287,19 @@ end ---@return value local function operative_handler_type(ud_type) local teees = gen.declare_array(typed) - local names = gen.declare_array(gen.builtin_string) - local namesp4 = names( - "#operative_handler_type-syn", - "#operative_handler_type-env", - "#operative_handler_type-ud", - "#operative_handler_type-goal" + local namesp4 = terms.symbol_array( + internal_symbols["#operative_handler_type-syn"], + internal_symbols["#operative_handler_type-env"], + internal_symbols["#operative_handler_type-ud"], + internal_symbols["#operative_handler_type-goal"] ) - local pnamep0 = "#operative_handler_type-empty" - local pnamep1 = "#operative_handler_type-syn" - local pnamep2 = "#operative_handler_type-syn-env" - local pnamep3 = "#operative_handler_type-syn-env-ud" - local pnamer = "#operative_handler_type-params" - local pnamer0 = "#operative_handler_type-result-empty" - local pnamer1 = "#operative_handler_type-result-term" + local pnamep0 = internal_symbols["#operative_handler_type-empty"] + local pnamep1 = internal_symbols["#operative_handler_type-syn"] + local pnamep2 = internal_symbols["#operative_handler_type-syn-env"] + local pnamep3 = internal_symbols["#operative_handler_type-syn-env-ud"] + local pnamer = internal_symbols["#operative_handler_type-params"] + local pnamer0 = internal_symbols["#operative_handler_type-result-empty"] + local pnamer1 = internal_symbols["#operative_handler_type-result-term"] return value.pi( value.tuple_type( terms.tuple_desc( @@ -1409,12 +1404,12 @@ end ---@param type_fn fun(typed): typed ---@return inferrable local function build_wrap(body_fn, type_fn) - local names = gen.declare_array(gen.builtin_string) + local names = terms.symbol_array local names0 = names() - local names1 = names("#wrap-TODO1") - local names2 = names("#wrap-TODO1", "#wrap-TODO2") - local pname_arg = "#wrap-arguments" - local pname_type = "#wrap-prev" + local names1 = names(internal_symbols["#wrap-TODO1"]) + local names2 = names(internal_symbols["#wrap-TODO1"], internal_symbols["#wrap-TODO2"]) + local pname_arg = internal_symbols["#wrap-arguments"] + local pname_type = internal_symbols["#wrap-prev"] return lit_term( value.closure( pname_arg, @@ -1457,12 +1452,12 @@ end ---@param type_fn fun(typed): typed ---@return inferrable local function build_unwrap(body_fn, type_fn) - local names = gen.declare_array(gen.builtin_string) + local names = terms.symbol_array local names0 = names() - local names1 = names("#unwrap-TODO1") - local names2 = names("#unwrap-TODO1", "#unwrap-TODO2") - local pname_arg = "#unwrap-arguments" - local pname_type = "#unwrap-prev" + local names1 = names(internal_symbols["#unwrap-TODO1"]) + local names2 = names(internal_symbols["#unwrap-TODO1"], internal_symbols["#unwrap-TODO2"]) + local pname_arg = internal_symbols["#unwrap-arguments"] + local pname_type = internal_symbols["#unwrap-prev"] return lit_term( value.closure( pname_arg, @@ -1504,11 +1499,11 @@ end ---@param body_fn fun(typed): typed ---@return inferrable local function build_wrapped(body_fn) - local names = gen.declare_array(gen.builtin_string) + local names = terms.symbol_array local names0 = names() - local names1 = names("#wrapped-TODO1") - local pname_arg = "#wrapped-arguments" - local pname_type = "#wrapped-prev" + local names1 = names(internal_symbols["#wrapped-TODO1"]) + local pname_arg = internal_symbols["#wrapped-arguments"] + local pname_type = internal_symbols["#wrapped-prev"] return lit_term( value.closure( pname_arg, @@ -1536,6 +1531,7 @@ local function build_wrapped(body_fn) ) end +---@param syntax ConstructedSyntax ---@param env Environment local enum_variant = metalanguage.reducer(function(syntax, env) local ok, tag, tail = syntax:match({ @@ -1554,7 +1550,7 @@ local enum_variant = metalanguage.reducer(function(syntax, env) return false, "missing enum variant name" end - return true, tag.str, terms.inferrable_term.tuple_type(tail.args), env + return true, tag, terms.inferrable_term.tuple_type(tail.args), env end, "enum_variant") ---@type lua_operative diff --git a/core-operatives.lua b/core-operatives.lua index af05d52b..e176611e 100644 --- a/core-operatives.lua +++ b/core-operatives.lua @@ -2,6 +2,7 @@ local metalanguage = require "metalanguage" local alicorn = require "alicorn-evaluator" local conexpr = require "contextual-exprs" local environment = require "environment" +local format = require "format" local val = metalanguage.primitive_operative(function(syntax, env) local ok, name, expr, nextenv = syntax:match({ @@ -19,10 +20,10 @@ local val = metalanguage.primitive_operative(function(syntax, env) return false, name end local binder, envres - if not name["kind"] then - binder = conexpr.bindtuple(name) - elseif type(name) == "string" then + if type(name) == "string" then binder = conexpr.bindval(name) + elseif not (name["kind"] or format.is_symbol(name)) then + binder = conexpr.bindtuple(name) else error "names had an invalid value?" end diff --git a/environment.lua b/environment.lua index f27af1f3..d751d26b 100644 --- a/environment.lua +++ b/environment.lua @@ -10,7 +10,7 @@ local module_mt = {} local evaluator = require "evaluator" local format = require "format" local infer = evaluator.infer -local NIL_ANCHOR = format.create_anchor(0, 0, "") +local nil_anchor = format.nil_anchor local environment_mt @@ -57,18 +57,18 @@ local environment = {} ---@class ShadowEnvironment ---@field shadowed Environment ----@param name string +---@param name Symbol ---@return boolean ---@return inferrable|string function environment:get(name) - local present, binding = self.in_scope:get(name) + local present, binding = self.in_scope:get(name.str) if not present then - return false, 'symbol "' .. name .. '" is not in scope' + return false, 'symbol "' .. tostring(name) .. '" is not in scope' end if binding == nil then return false, 'symbol "' - .. name + .. tostring(name) .. '" is marked as present but with no data; this indicates a bug in the environment or something violating encapsulation' end return true, binding @@ -95,7 +95,7 @@ function environment:bind_local(binding) error("nyi environment dependent purity") end if binding:is_let() then - local name, expr = binding:unwrap_let() + local name, expr, start_anchor, end_anchor = binding:unwrap_let() local expr_type, expr_usages, expr_term = infer(expr, self.typechecking_context) if terms.value.value_check(expr_type) ~= true then print("expr", expr) @@ -103,7 +103,7 @@ function environment:bind_local(binding) end local n = self.typechecking_context:len() local term = inferrable_term.bound_variable(n + 1) - local locals = self.locals:put(name, term) + local locals = self.locals:put(name.str, term) local evaled = evaluator.evaluate(expr_term, self.typechecking_context.runtime_context) -- print "doing let binding" -- print(expr:pretty_print()) @@ -116,7 +116,7 @@ function environment:bind_local(binding) typechecking_context = typechecking_context, }) elseif binding:is_tuple_elim() then - local names, subject = binding:unwrap_tuple_elim() + local names, subject, start_anchor, end_anchor = binding:unwrap_tuple_elim() local subject_type, subject_usages, subject_term = infer(subject, self.typechecking_context) --local subject_qty, subject_type = subject_type:unwrap_qtype() --DEBUG: @@ -139,7 +139,7 @@ function environment:bind_local(binding) -- self.typechecking_context, -- spec_type, -- self.typechecking_context, - -- terms.constraintcause.primitive("environment tuple-elim", NIL_ANCHOR, NIL_ANCHOR) + -- terms.constraintcause.primitive("environment tuple-elim", nil_anchor, nil_anchor) -- ) U.tag( "flow", @@ -150,7 +150,7 @@ function environment:bind_local(binding) self.typechecking_context, spec_type, self.typechecking_context, - terms.constraintcause.primitive("environment tuple-elim", NIL_ANCHOR, NIL_ANCHOR) + terms.constraintcause.primitive("environment tuple-elim", nil_anchor, nil_anchor) ) -- evaluating the subject is necessary for inferring the type of the body @@ -393,11 +393,11 @@ function environment:exit_block(term, shadowed) error "missing binding" end if binding:is_let() then - local name, expr = binding:unwrap_let() - wrapped = terms.inferrable_term.let(name, expr, wrapped) + local name, expr, start_anchor, end_anchor = binding:unwrap_let() + wrapped = terms.inferrable_term.let(name, expr, wrapped, start_anchor, end_anchor) elseif binding:is_tuple_elim() then - local names, subject = binding:unwrap_tuple_elim() - wrapped = terms.inferrable_term.tuple_elim(names, subject, wrapped) + local names, subject, start_anchor, end_anchor = binding:unwrap_tuple_elim() + wrapped = terms.inferrable_term.tuple_elim(names, subject, wrapped, start_anchor, end_anchor) elseif binding:is_annotated_lambda() then local name, annotation, start_anchor, end_anchor, visible, purity = binding:unwrap_annotated_lambda() wrapped = terms.inferrable_term.annotated_lambda(name, annotation, wrapped, start_anchor, end_anchor, visible, purity) diff --git a/evaluator.lua b/evaluator.lua index d746628c..df49a0f0 100644 --- a/evaluator.lua +++ b/evaluator.lua @@ -3,6 +3,7 @@ local metalanguage = require "metalanguage" local U = require "alicorn-utils" local utils = require "alicorn-utils" local format = require "format" +local create_symbol = format.create_symbol local runtime_context = terms.runtime_context local s = require "pretty-printer".s --local new_typechecking_context = terms.typechecking_context @@ -20,6 +21,7 @@ local host_environment_type = terms.host_environment_type local host_typed_term_type = terms.host_typed_term_type local host_goal_type = terms.host_goal_type local host_inferrable_term_type = terms.host_inferrable_term_type +local symbol_type = terms.symbol_type local diff = require "traits".diff @@ -46,10 +48,11 @@ local result_info_pure = value.result_info(result_info(purity.pure)) local OMEGA = 9 local typechecker_state local evaluate, infer, check, apply_value -local name_array = string_array +local name_array = terms.symbol_array local typed = terms.typed_term -local NIL_ANCHOR = format.create_anchor(0, 0, "") +local internal_symbols = format.internal_symbols +local nil_anchor = format.nil_anchor ---@param luafunc function ---@return value @@ -60,12 +63,13 @@ local function luatovalue(luafunc) local new_body = typed_array() for i = 1, len do - parameters:append(debug.getlocal(luafunc, i)) + local parameter_name, parameter_value = debug.getlocal(luafunc, i) + parameters:append(create_symbol(parameter_name, nil_anchor, nil_anchor), parameter_value) new_body:append(typed.bound_variable(i + 1)) end return value.closure( - "#luatovalue-args", + internal_symbols["#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)) @@ -338,7 +342,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(internal_symbols["#CONST_PARAM"], typed_term.bound_variable(1), runtime_context():append(v)) end ---@param t value @@ -678,10 +682,14 @@ end --for substituting a single var at index ---@param val value ---@param index integer ----@param param_name string? +---@param param_name Symbol? ---@return value function substitute_type_variables(val, index, param_name) - param_name = param_name and "#sub-" .. param_name or "#sub-param" + if param_name then + param_name = create_symbol("#sub-" .. param_name.str, param_name.start_anchor, param_name.end_anchor) + else + param_name = internal_symbols["#sub-param"] + end --print("value before substituting (val): (value term follows)") --print(val) local substituted = substitute_inner(val, { @@ -947,12 +955,12 @@ add_comparer("value.enum_type", "value.tuple_desc_type", function(lctx, a, rctx, value.tuple_value( value_array( value.enum_value(terms.DescCons.empty, value.tuple_value(value_array())), - value.closure("#prefix", typed_term.literal(b), rctx.runtime_context) + value.closure(internal_symbols["#prefix"], typed_term.literal(b), rctx.runtime_context) ) ) ), value.closure( - "#prefix", + internal_symbols["#prefix"], typed_term.tuple_elim( string_array("prefix-desc"), typed_term.bound_variable(#rctx + 2), @@ -1003,12 +1011,12 @@ add_comparer("value.tuple_desc_type", "value.enum_type", function(lctx, a, rctx, value.tuple_value( value_array( value.enum_value(terms.DescCons.empty, value.tuple_value(value_array())), - value.closure("#prefix", typed_term.literal(a), rctx.runtime_context) + value.closure(internal_symbols["#prefix"], typed_term.literal(a), rctx.runtime_context) ) ) ), value.closure( - "#prefix", + internal_symbols["#prefix"], typed_term.tuple_elim( string_array("prefix-desc"), typed_term.bound_variable(#rctx + 2), @@ -1487,7 +1495,7 @@ function check( typechecking_context, goal_type, typechecking_context, - terms.constraintcause.primitive("inferrable", NIL_ANCHOR, NIL_ANCHOR) + terms.constraintcause.primitive("inferrable", nil_anchor, nil_anchor) ) end @@ -1511,7 +1519,7 @@ function check( desc = terms.cons( desc, value.closure( - "#check-tuple-cons-param", + internal_symbols["#check-tuple-cons-param"], typed_term.literal(value.singleton(el_type, el_val)), typechecking_context.runtime_context ) @@ -1523,7 +1531,7 @@ function check( typechecking_context, goal_type, typechecking_context, - terms.constraintcause.primitive("checkable_term:is_tuple_cons", NIL_ANCHOR, NIL_ANCHOR) + terms.constraintcause.primitive("checkable_term:is_tuple_cons", nil_anchor, nil_anchor) ) return usages, typed_term.tuple_cons(new_elements) @@ -1546,7 +1554,7 @@ function check( desc = terms.cons( desc, value.closure( - "#check-tuple-cons-param", + internal_symbols["#check-tuple-cons-param"], typed_term.literal(value.singleton(el_type, el_val)), typechecking_context.runtime_context ) @@ -1558,7 +1566,7 @@ function check( typechecking_context, goal_type, typechecking_context, - terms.constraintcause.primitive("checkable_term:is_host_tuple_cons", NIL_ANCHOR, NIL_ANCHOR) + terms.constraintcause.primitive("checkable_term:is_host_tuple_cons", nil_anchor, nil_anchor) ) return usages, typed_term.host_tuple_cons(new_elements) @@ -1914,7 +1922,7 @@ function infer_impl( typechecking_context, result_type_param_type, typechecking_context, - terms.constraintcause.primitive("inferrable pi term", NIL_ANCHOR, NIL_ANCHOR) + terms.constraintcause.primitive("inferrable pi term", nil_anchor, nil_anchor) ) local result_type_result_type_result = apply_value(result_type_result_type, evaluate(param_type_term, typechecking_context.runtime_context)) @@ -2036,7 +2044,7 @@ function infer_impl( end return value.host_tuple_type(type_data), usages, typed_term.host_tuple_cons(new_elements) elseif inferrable_term:is_tuple_elim() then - local names, subject, body = inferrable_term:unwrap_tuple_elim() + local names, subject, body, start_anchor, end_anchor = inferrable_term:unwrap_tuple_elim() local subject_type, subject_usages, subject_term = infer(subject, typechecking_context) -- evaluating the subject is necessary for inferring the type of the body @@ -2051,13 +2059,14 @@ function infer_impl( local spec_type = terms.value.tuple_type(desc) local host_spec_type = terms.value.host_tuple_type(desc) + require("lldebugger").requestBreak() local ok, tupletypes, n_elements = typechecker_state:speculate(function() typechecker_state:flow( subject_type, typechecking_context, spec_type, typechecking_context, - terms.constraintcause.primitive("tuple elimination", NIL_ANCHOR, NIL_ANCHOR) + terms.constraintcause.primitive("tuple elimination", start_anchor, end_anchor) ) return infer_tuple_type(spec_type, subject_value) end) @@ -2069,7 +2078,7 @@ function infer_impl( typechecking_context, host_spec_type, typechecking_context, - terms.constraintcause.primitive("host tuple elimination", NIL_ANCHOR, NIL_ANCHOR) + terms.constraintcause.primitive("host tuple elimination", start_anchor, end_anchor) ) return infer_tuple_type(host_spec_type, subject_value) end) @@ -2101,7 +2110,7 @@ function infer_impl( typechecking_context, value.tuple_desc_type(univ_var), typechecking_context, - terms.constraintcause.primitive("tuple type construction", NIL_ANCHOR, NIL_ANCHOR) + terms.constraintcause.primitive("tuple type construction", nil_anchor, nil_anchor) ) return value.union_type(terms.value.star(0, 0), univ_var), desc_usages, terms.typed_term.tuple_type(desc_term) elseif inferrable_term:is_record_cons() then @@ -2226,7 +2235,7 @@ function infer_impl( typechecking_context, value.enum_type(value.enum_desc_value(constrain_variants)), typechecking_context, - terms.constraintcause.primitive("enum case matching", NIL_ANCHOR, NIL_ANCHOR) + terms.constraintcause.primitive("enum case matching", nil_anchor, nil_anchor) ) local term_variants = string_typed_map() ---@type {[integer]: value} @@ -2279,7 +2288,7 @@ function infer_impl( typechecking_context, value.enum_desc_type(univ_var), typechecking_context, - terms.constraintcause.primitive("tuple type construction", NIL_ANCHOR, NIL_ANCHOR) + terms.constraintcause.primitive("tuple type construction", nil_anchor, nil_anchor) ) return value.union_type(terms.value.star(0, 0), univ_var), desc_usages, terms.typed_term.enum_type(desc_term) elseif inferrable_term:is_object_cons() then @@ -2312,7 +2321,7 @@ function infer_impl( typechecking_context, op_userdata_type, typechecking_context, - terms.constraintcause.primitive("operative userdata", NIL_ANCHOR, NIL_ANCHOR) + terms.constraintcause.primitive("operative userdata", nil_anchor, nil_anchor) ) end local operative_usages = usage_array() @@ -2407,14 +2416,14 @@ function infer_impl( typechecking_context, restype, typechecking_context, - terms.constraintcause.primitive("inferred host if consequent", NIL_ANCHOR, NIL_ANCHOR) + terms.constraintcause.primitive("inferred host if consequent", nil_anchor, nil_anchor) ) typechecker_state:flow( atype, typechecking_context, restype, typechecking_context, - terms.constraintcause.primitive("inferred host if alternate", NIL_ANCHOR, NIL_ANCHOR) + terms.constraintcause.primitive("inferred host if alternate", nil_anchor, nil_anchor) ) local result_usages = usage_array() @@ -2425,7 +2434,7 @@ function infer_impl( return restype, result_usages, typed_term.host_if(sterm, cterm, aterm) elseif inferrable_term:is_let() then -- print(inferrable_term:pretty_print()) - local name, expr, body = inferrable_term:unwrap_let() + local name, expr, body, start_anchor, end_anchor = inferrable_term:unwrap_let() local exprtype, exprusages, exprterm = infer(expr, typechecking_context) typechecking_context = typechecking_context:append(name, exprtype, evaluate(exprterm, typechecking_context.runtime_context)) @@ -2478,7 +2487,7 @@ function infer_impl( typechecking_context, value.tuple_desc_type(value.host_type_type), typechecking_context, - terms.constraintcause.primitive("tuple type construction", NIL_ANCHOR, NIL_ANCHOR) + terms.constraintcause.primitive("tuple type construction", nil_anchor, nil_anchor) ) return terms.value.star(0, 0), desc_usages, terms.typed_term.host_tuple_type(desc_term) elseif inferrable_term:is_program_sequence() then @@ -2785,7 +2794,7 @@ function evaluate_impl(typed_term, runtime_context) if mechanism_value:is_object_value() then local constructor, arg = subject_value:unwrap_enum_value() local methods, capture = mechanism_value:unwrap_object_value() - local this_method = value.closure("#ENUM_PARAM", methods[constructor], capture) + local this_method = value.closure(internal_symbols["#ENUM_PARAM"], methods[constructor], capture) return apply_value(this_method, arg) elseif mechanism_value:is_neutral() then -- objects and enums are categorical duals @@ -2862,7 +2871,7 @@ function evaluate_impl(typed_term, runtime_context) if mechanism_value:is_enum_value() then local methods, capture = subject_value:unwrap_object_value() local constructor, arg = mechanism_value:unwrap_enum_value() - local this_method = value.closure("#OBJECT_PARAM", methods[constructor], capture) + local this_method = value.closure(internal_symbols["#OBJECT_PARAM"], methods[constructor], capture) return apply_value(this_method, arg) elseif mechanism_value:is_neutral() then -- objects and enums are categorical duals @@ -3723,7 +3732,7 @@ function Reachability:constrain_transitivity(edge, edge_id, queue) edge.rel, edge.right, math.min(edge.shallowest_block, l2.shallowest_block), - terms.constraintcause.composition(i, edge_id, NIL_ANCHOR, NIL_ANCHOR) + terms.constraintcause.composition(i, edge_id, nil_anchor, nil_anchor) ) ) end @@ -3739,7 +3748,7 @@ function Reachability:constrain_transitivity(edge, edge_id, queue) edge.rel, r2.right, math.min(edge.shallowest_block, r2.shallowest_block), - terms.constraintcause.composition(edge_id, i, NIL_ANCHOR, NIL_ANCHOR) + terms.constraintcause.composition(edge_id, i, nil_anchor, nil_anchor) ) ) end @@ -4179,7 +4188,7 @@ function TypeCheckerState:constrain_leftcall_compose_1(edge, edge_id) r2.rel, r2.right, math.min(edge.shallowest_block, r2.shallowest_block), - terms.constraintcause.leftcall_discharge(i, edge_id, NIL_ANCHOR, NIL_ANCHOR) + terms.constraintcause.leftcall_discharge(i, edge_id, nil_anchor, nil_anchor) ) ) end @@ -4204,7 +4213,7 @@ function TypeCheckerState:constrain_on_left_meet(edge, edge_id) edge.rel, edge.right, math.min(edge.shallowest_block, r.shallowest_block), - terms.constraintcause.composition(i, edge_id, NIL_ANCHOR, NIL_ANCHOR) + terms.constraintcause.composition(i, edge_id, nil_anchor, nil_anchor) ) ) end @@ -4229,7 +4238,7 @@ function TypeCheckerState:constrain_on_right_meet(edge, edge_id) edge.rel, l.right, math.min(edge.shallowest_block, l.shallowest_block), - terms.constraintcause.composition(edge_id, i, NIL_ANCHOR, NIL_ANCHOR) + terms.constraintcause.composition(edge_id, i, nil_anchor, nil_anchor) ) ) end @@ -4256,7 +4265,7 @@ function TypeCheckerState:constrain_leftcall_compose_2(edge, edge_id) edge.rel, l2.right, math.min(edge.shallowest_block, l2.shallowest_block), - terms.constraintcause.leftcall_discharge(edge_id, i, NIL_ANCHOR, NIL_ANCHOR) + terms.constraintcause.leftcall_discharge(edge_id, i, nil_anchor, nil_anchor) ) ) end @@ -4283,7 +4292,7 @@ function TypeCheckerState:rightcall_constrain_compose_2(edge, edge_id) l2.right, l2.arg, math.min(edge.shallowest_block, l2.shallowest_block), - terms.constraintcause.rightcall_discharge(edge_id, i, NIL_ANCHOR, NIL_ANCHOR) + terms.constraintcause.rightcall_discharge(edge_id, i, nil_anchor, nil_anchor) ) ) end @@ -4310,7 +4319,7 @@ function TypeCheckerState:rightcall_constrain_compose_1(edge, edge_id) r2.right, edge.arg, math.min(edge.shallowest_block, r2.shallowest_block), - terms.constraintcause.rightcall_discharge(i, edge_id, NIL_ANCHOR, NIL_ANCHOR) + terms.constraintcause.rightcall_discharge(i, edge_id, nil_anchor, nil_anchor) ) ) end diff --git a/format-adapter.lua b/format-adapter.lua index 9301063f..ab3e3438 100644 --- a/format-adapter.lua +++ b/format-adapter.lua @@ -1,8 +1,12 @@ local metalanguage = require "metalanguage" local format = require "format" +local is_symbol = format.is_symbol local function syntax_convert(tree) - if tree.kind == "list" then + if is_symbol(tree) then + ---@cast tree Symbol + return metalanguage.symbol(tree) + elseif tree.kind == "list" then local res = metalanguage.nilval for i = #tree.elements, 1, -1 do local elem = syntax_convert(tree.elements[i]) @@ -11,9 +15,6 @@ local function syntax_convert(tree) end end return res - elseif tree.kind == "symbol" then - assert(tree["kind"]) - return metalanguage.symbol(tree.start_anchor, tree.end_anchor, tree) elseif tree.kind == "literal" then return metalanguage.value( tree.start_anchor, diff --git a/format.lua b/format.lua index 1fb59425..a39f3405 100644 --- a/format.lua +++ b/format.lua @@ -21,27 +21,104 @@ end ---@field sourceid string local Anchor = {} +---@type Anchor +local nil_anchor local anchor_mt = { __lt = function(fst, snd) - return snd.line > fst.line or (snd.line == fst.line and snd.char > fst.char) + return snd.line > fst.line or (snd.line == fst.line and snd.char > fst.char) or (snd.char == fst.char and snd.sourceid < fst.sourceid) end, __le = function(fst, snd) return fst < snd or fst == snd end, __eq = function(fst, snd) - return (snd.line == fst.line and snd.char == fst.char) + return (snd.line == fst.line and snd.char == fst.char and snd.sourceid == fst.sourceid) end, __tostring = function(self) - return "file " - .. tostring(self.sourceid) - .. ", line " - .. tostring(self.line) - .. " character " - .. tostring(self.char) + if rawequal(self, nil_anchor) then + return "🗋" + else + return "file " + .. tostring(self.sourceid) + .. ", line " + .. tostring(self.line) + .. " character " + .. tostring(self.char) + end end, __index = Anchor, } +---@param line integer +---@param char integer +---@param sourceid string +---@return Anchor +local function create_anchor(line, char, sourceid) + return setmetatable({ + line = line, + char = char, + sourceid = sourceid, + }, anchor_mt) +end + +nil_anchor = create_anchor(0, 0, "") + +---@class Symbol +---@field str string +---@field start_anchor Anchor +---@field end_anchor Anchor +local Symbol = {} + +local symbol_mt = { + __lt = function(fst, snd) + return snd.str > fst.str + end, + __le = function(fst, snd) + return fst < snd or fst == snd + end, + __eq = function(fst, snd) + return (snd.str == fst.str) + end, + __tostring = function(self) + if self.start_anchor == self.end_anchor then + return tostring(self.str) .. "@(" .. tostring(self.start_anchor) .. ")" + else + return tostring(self.str) .. "@(" .. tostring(self.start_anchor) .. ")–(" .. tostring(self.end_anchor) .. ")" + end + end, + __index = Symbol, +} + +---@param str string +---@param start_anchor Anchor +---@param end_anchor Anchor +---@return Symbol +local function create_symbol(str, start_anchor, end_anchor) + return setmetatable({ + str = str, + start_anchor = start_anchor, + end_anchor = end_anchor, + }, symbol_mt) +end + +---@param symbol any +---@return Symbol? +local function is_symbol(symbol) + if getmetatable(symbol) == symbol_mt then + return symbol + else + return nil + end +end + +---@type {[string]: Symbol} +local internal_symbols = setmetatable({}, { + __index = function (self, str) + local symbol = create_symbol(str, nil_anchor, nil_anchor) + rawset(self, str, symbol) + return symbol + end +}) + lpeg.locale(lpeg) local function element(kind, pattern) @@ -49,7 +126,9 @@ local function element(kind, pattern) end local function symbol(value) - return element("symbol", Cg(value, "str") * Cg(V "anchor", "end_anchor")) + return Cmt(V "anchor" * Cg(value) * V "anchor", function (_, _, start_anchor, str, end_anchor) + return true, create_symbol(str, start_anchor, end_anchor) + end) end local function space_tokens(pattern) @@ -179,20 +258,6 @@ local function erase(pattern) return pattern / {} end ----@param line integer ----@param char integer ----@param sourceid string ----@return Anchor -local function create_anchor(line, char, sourceid) - local new_anchor = { - line = line, - char = char, - sourceid = sourceid, - } - setmetatable(new_anchor, anchor_mt) - return new_anchor -end - ---@class LinePosition ---@field line integer ---@field pos integer @@ -579,4 +644,4 @@ local function parse(input, filename) return ast end -return { parse = parse, anchor_mt = anchor_mt, create_anchor = create_anchor } +return { parse = parse, anchor_mt = anchor_mt, symbol_mt = symbol_mt, create_anchor = create_anchor, create_symbol = create_symbol, internal_symbols = internal_symbols, is_symbol = is_symbol, nil_anchor = nil_anchor } diff --git a/metalanguage.lua b/metalanguage.lua index 92013b3d..018369ea 100644 --- a/metalanguage.lua +++ b/metalanguage.lua @@ -39,16 +39,11 @@ local MatcherKind = --[[@enum MatcherKind]] ---@field handler SymbolFunc | PairFunc | NilFunc | ValueFunc | ReducibleFunc ---@field reducible Reducible? ----@class SyntaxSymbol ----@field start_anchor Anchor ----@field end_anchor Anchor ----@field str string - --[[ issymbol : forall implicit userdata : type implicit results : tuple-desc - handler : (forall (u : userdata, s : SyntaxSymbol) -> res : tuple-type(results))) + handler : (forall (u : userdata, s : Symbol) -> res : tuple-type(results))) -> Matcher(userdata, results) --]] @@ -327,14 +322,14 @@ local function reducer(func, name) end ---@param expected string ----@param symbol SyntaxSymbol +---@param symbol Symbol ---@return boolean ---@return string? local function symbolexacthandler(expected, symbol) if symbol.str == expected then return true else - return false, "symbol is expected to be exactly " .. expected .. " but was instead " .. symbol.str + return false, "symbol is expected to be exactly " .. tostring(expected) .. " but was instead " .. tostring(symbol) end end @@ -505,12 +500,10 @@ local symbol_accepters = { end, } ----@param start_anchor Anchor ----@param end_anchor Anchor ----@param syntaxsymbol SyntaxSymbol +---@param syntax_symbol Symbol ---@return ConstructedSyntax -local function symbol(start_anchor, end_anchor, syntaxsymbol) - return cons_syntax(symbol_accepters, start_anchor, end_anchor, syntaxsymbol) +local function symbol(syntax_symbol) + return cons_syntax(symbol_accepters, syntax_symbol.start_anchor, syntax_symbol.end_anchor, syntax_symbol) end local value_accepters = { diff --git a/modules.lua b/modules.lua index 1eb4df0f..a447e6db 100644 --- a/modules.lua +++ b/modules.lua @@ -98,7 +98,7 @@ local function get_op_impl(syntax, env) if not ok then return ok, modval end - print("module get", ok, modval, env, symbol.str) + print("module get", ok, modval, env, tostring(symbol)) if not modval.type == module_type then return false, "first argument of module get must be a module" end diff --git a/runtest.lua b/runtest.lua index 4864113c..353a57ca 100644 --- a/runtest.lua +++ b/runtest.lua @@ -286,7 +286,7 @@ local function execute_alc_file(bound_expr, log) local set = gen.declare_set local unique_id = gen.builtin_table - local NIL_ANCHOR = format.create_anchor(0, 0, "") + local nil_anchor = format.nil_anchor local ok, err = pcall(function() evaluator.typechecker_state:flow( @@ -297,7 +297,7 @@ local function execute_alc_file(bound_expr, log) evaluator.typechecker_state:metavariable(terms.typechecking_context()):as_value() ), nil, - terms.constraintcause.primitive("final flow check", NIL_ANCHOR, NIL_ANCHOR) + terms.constraintcause.primitive("final flow check", nil_anchor, nil_anchor) ) end) diff --git a/syntax-schema.lua b/syntax-schema.lua index aa88af05..98e18fbe 100644 --- a/syntax-schema.lua +++ b/syntax-schema.lua @@ -12,6 +12,12 @@ S:struct "anchor" "The source position information attached to a node" { schema.u32 "char"(2) "the offset within the line", } +S:struct "symbol" "A string from the source" { + schema.text "str"(0) "the string", + S.export.anchor "start_anchor"(1), + S.export.anchor "end_anchor"(2), +} + local element = S:addstruct("element") element:define { @@ -21,52 +27,49 @@ element:define { schema.list(element) "elements"(3), S.export.anchor "end_anchor"(4), }, - schema.variant "symbol"(5) { - schema.text "str"(6), - }, - schema.variant "string"(7) { - schema.list(element) "elements"(8) "A string contains a list of elements corresponding to parts of the literal. Every splice becomes a separate element, and the region between them is a literal byte buffer element", - S.export.anchor "end_anchor"(9), + schema.variant "string"(5) { + schema.list(element) "elements"(6) "A string contains a list of elements corresponding to parts of the literal. Every splice becomes a separate element, and the region between them is a literal byte buffer element", + S.export.anchor "end_anchor"(7), }, - schema.variant "literal"(10) { - schema.union "literaltype"(11) { - schema.variant "u8"(12) { - schema.u8 "val"(13), + schema.variant "literal"(8) { + schema.union "literaltype"(9) { + schema.variant "u8"(10) { + schema.u8 "val"(11), }, - schema.variant "i8"(14) { - schema.i8 "val"(15), + schema.variant "i8"(12) { + schema.i8 "val"(13), }, - schema.variant "u16"(16) { - schema.u16 "val"(17), + schema.variant "u16"(14) { + schema.u16 "val"(15), }, - schema.variant "i16"(18) { - schema.i16 "val"(19), + schema.variant "i16"(16) { + schema.i16 "val"(17), }, - schema.variant "u32"(20) { - schema.u32 "val"(21), + schema.variant "u32"(18) { + schema.u32 "val"(19), }, - schema.variant "i32"(22) { - schema.i32 "val"(23), + schema.variant "i32"(20) { + schema.i32 "val"(21), }, - schema.variant "u64"(24) { - schema.u64 "val"(25), + schema.variant "u64"(22) { + schema.u64 "val"(23), }, - schema.variant "i64"(26) { - schema.i64 "val"(27), + schema.variant "i64"(24) { + schema.i64 "val"(25), }, - schema.variant "f16"(28) { - schema.f16 "val"(29), + schema.variant "f16"(26) { + schema.f16 "val"(27), }, - schema.variant "f32"(30) { - schema.f32 "val"(31), + schema.variant "f32"(28) { + schema.f32 "val"(29), }, - schema.variant "f64"(32) { - schema.f64 "val"(33), + schema.variant "f64"(30) { + schema.f64 "val"(31), }, - schema.variant "bytes"(34) { - schema.list(schema.u8) "val"(35), + schema.variant "bytes"(32) { + schema.list(schema.u8) "val"(33), }, - schema.variant "unit"(36) {}, + schema.variant "unit"(34) {}, }, }, }, diff --git a/terms-pretty.lua b/terms-pretty.lua index 198f27b5..5569488c 100644 --- a/terms-pretty.lua +++ b/terms-pretty.lua @@ -119,7 +119,7 @@ local function tuple_elim_helper(pp, names, subject, context) pp:unit(pp:_resetcolor()) for i, name in names:ipairs() do - inner_context = inner_context:append(name) + inner_context = inner_context:append(tostring(name)) if i > 1 then pp:unit(pp:_color()) @@ -216,10 +216,10 @@ end local function inferrable_let_or_tuple_elim(pp, term, context) pp:_enter() - local name, expr, names, subject + local name, expr, names, subject, start_anchor, end_anchor while true do if term:is_let() then - name, expr, term = term:unwrap_let() + name, expr, term, start_anchor, end_anchor = term:unwrap_let() -- rear-loading prefix to cheaply handle first loop not needing prefix pp:unit(pp:_color()) @@ -229,7 +229,7 @@ local function inferrable_let_or_tuple_elim(pp, term, context) pp:unit("\n") pp:_prefix() elseif term:is_tuple_elim() then - names, subject, term = term:unwrap_tuple_elim() + names, subject, term, start_anchor, end_anchor = term:unwrap_tuple_elim() pp:unit(pp:_color()) pp:unit("inferrable.let ") @@ -291,6 +291,8 @@ end ---@return (string | ArrayValue)? ---@return inferrable ---@return PrettyPrintingContext +---@return Anchor? +---@return Anchor? local function inferrable_destructure_helper(term, context) if term:is_let() then -- destructuring with a let effectively just renames the parameter @@ -299,25 +301,25 @@ local function inferrable_destructure_helper(term, context) -- but some operatives that are generic over lets and tuple-elims do this -- e.g. forall, lambda -- so we pretty this anyway - local name, expr, body = term:unwrap_let() + local name, expr, body, start_anchor, end_anchor = term:unwrap_let() local ok, index = expr:as_bound_variable() local is_destructure = ok and index == context:len() if is_destructure then context = context:append(name) - return true, true, name, body, context + return true, true, name, body, context, start_anchor, end_anchor end elseif term:is_tuple_elim() then - local names, subject, body = term:unwrap_tuple_elim() + local names, subject, body, start_anchor, end_anchor = term:unwrap_tuple_elim() local ok, index = subject:as_bound_variable() local is_destructure = ok and index == context:len() if is_destructure then for _, name in names:ipairs() do context = context:append(name) end - return true, false, names, body, context + return true, false, names, body, context, start_anchor, end_anchor end end - return false, false, nil, term, context + return false, false, nil, term, context, nil, nil end ---@param term typed @@ -380,7 +382,7 @@ local function inferrable_tuple_type_flatten(desc, context) return false end local inner_context = context:append(param_name) - local _, _, names, body, inner_context = inferrable_destructure_helper(body, inner_context) + local _, _, names, body, inner_context, start_anchor, end_anchor = inferrable_destructure_helper(body, inner_context) ---@cast names ArrayValue local ok, prev, n = inferrable_tuple_type_flatten(desc, context) if not ok then @@ -660,7 +662,7 @@ end ---@param pp PrettyPrint ---@param context AnyContext function binding_override_pretty:let(pp, context) - local name, expr = self:unwrap_let() + local name, expr, start_anchor, end_anchor = self:unwrap_let() context = ensure_context(context) pp:_enter() @@ -690,7 +692,7 @@ end ---@param pp PrettyPrint ---@param context AnyContext function binding_override_pretty:tuple_elim(pp, context) - local names, subject = self:unwrap_tuple_elim() + local names, subject, start_anchor, end_anchor = self:unwrap_tuple_elim() context = ensure_context(context) pp:_enter() @@ -751,7 +753,7 @@ function inferrable_term_override_pretty:annotated_lambda(pp, context) context = ensure_context(context) local inner_context = context:append(param_name) local is_tuple_type, desc = as_any_tuple_type(param_annotation) - local is_destructure, is_rename, names, body, inner_context = inferrable_destructure_helper(body, inner_context) + local is_destructure, is_rename, names, body, inner_context, start_anchor, end_anchor = inferrable_destructure_helper(body, inner_context) if is_rename then ---@cast names string param_name = names @@ -951,10 +953,10 @@ function inferrable_term_override_pretty:pi(pp, context) local result_context = context local param_is_tuple_type, param_desc = as_any_tuple_type(param_type) local result_is_readable, param_name, _, result_body, _ = result_type:as_annotated_lambda() - local result_is_destructure, result_is_rename, param_names, result_is_tuple_type, result_desc + local result_is_destructure, result_is_rename, param_names, result_is_tuple_type, result_desc, result_start_anchor, result_end_anchor if result_is_readable then result_context = result_context:append(param_name) - result_is_destructure, result_is_rename, param_names, result_body, result_context = + result_is_destructure, result_is_rename, param_names, result_body, result_context, result_start_anchor, result_end_anchor = inferrable_destructure_helper(result_body, result_context) if result_is_rename then ---@cast param_names string @@ -1056,10 +1058,10 @@ function inferrable_term_override_pretty:host_function_type(pp, context) local result_context = context local param_is_tuple_type, param_desc = param_type:as_host_tuple_type() local result_is_readable, param_name, _, result_body, _ = result_type:as_annotated_lambda() - local result_is_destructure, result_is_rename, param_names, result_is_tuple_type, result_desc + local result_is_destructure, result_is_rename, param_names, result_is_tuple_type, result_desc, result_start_anchor, result_end_anchor if result_is_readable then result_context = result_context:append(param_name) - result_is_destructure, result_is_rename, param_names, result_body, result_context = + result_is_destructure, result_is_rename, param_names, result_body, result_context, result_start_anchor, result_end_anchor = inferrable_destructure_helper(result_body, result_context) if result_is_rename then ---@cast param_names string diff --git a/terms.lua b/terms.lua index 0113666b..2962857a 100644 --- a/terms.lua +++ b/terms.lua @@ -16,6 +16,8 @@ local traits = require "traits" local format = require "format" +local nil_anchor = format.nil_anchor + local map = gen.declare_map local array = gen.declare_array local set = gen.declare_set @@ -60,6 +62,9 @@ local metavariable_mt = { __index = Metavariable } local metavariable_type = gen.declare_foreign(gen.metatable_equality(metavariable_mt), "Metavariable") local anchor_type = gen.declare_foreign(gen.metatable_equality(format.anchor_mt), "Anchor") +local symbol_type = gen.declare_foreign(gen.metatable_equality(format.symbol_mt), "Symbol") + +local symbol_array = array(symbol_type) ---@class RuntimeContext ---@field bindings FibonacciBuffer @@ -210,15 +215,15 @@ function TypecheckingContext:get_runtime_context() return self.runtime_context end ----@param name string +---@param name Symbol ---@param type value ---@param val value? ---@param start_anchor Anchor? ---@param end_anchor Anchor? ---@return TypecheckingContext function TypecheckingContext:append(name, type, val, start_anchor, end_anchor) - if gen.builtin_string.value_check(name) ~= true then - error("TypecheckingContext:append parameter 'name' must be a string") + if symbol_type.value_check(name) ~= true then + error("TypecheckingContext:append parameter 'name' must be a Symbol") end if value.value_check(type) ~= true then print("type", type) @@ -322,15 +327,19 @@ expression_goal:define_enum("expression_goal", { -- stylua: ignore binding:define_enum("binding", { { "let", { - "name", gen.builtin_string, - "expr", inferrable_term, + "name", symbol_type, + "expr", inferrable_term, + "start_anchor", anchor_type, + "end_anchor", anchor_type, } }, { "tuple_elim", { - "names", array(gen.builtin_string), + "names", symbol_array, "subject", inferrable_term, + "start_anchor", anchor_type, + "end_anchor", anchor_type, } }, { "annotated_lambda", { - "param_name", gen.builtin_string, + "param_name", symbol_type, "param_annotation", inferrable_term, "start_anchor", anchor_type, "end_anchor", anchor_type, @@ -351,7 +360,7 @@ checkable_term:define_enum("checkable", { { "tuple_cons", { "elements", array(checkable_term) } }, { "host_tuple_cons", { "elements", array(checkable_term) } }, { "lambda", { - "param_name", gen.builtin_string, + "param_name", symbol_type, "body", checkable_term, } }, }) @@ -365,7 +374,7 @@ inferrable_term:define_enum("inferrable", { "typed_term", typed_term, } }, { "annotated_lambda", { - "param_name", gen.builtin_string, + "param_name", symbol_type, "param_annotation", inferrable_term, "body", inferrable_term, "start_anchor", anchor_type, @@ -385,23 +394,25 @@ inferrable_term:define_enum("inferrable", { } }, { "tuple_cons", { "elements", array(inferrable_term) } }, { "tuple_elim", { - "names", array(gen.builtin_string), + "names", symbol_array, "subject", inferrable_term, "body", inferrable_term, + "start_anchor", anchor_type, + "end_anchor", anchor_type, } }, { "tuple_type", { "desc", inferrable_term } }, - { "record_cons", { "fields", map(gen.builtin_string, inferrable_term) } }, + { "record_cons", { "fields", map(symbol_type, inferrable_term) } }, { "record_elim", { "subject", inferrable_term, - "field_names", array(gen.builtin_string), + "field_names", symbol_array, "body", inferrable_term, } }, { "enum_cons", { - "constructor", gen.builtin_string, + "constructor", symbol_type, "arg", inferrable_term, } }, { "enum_desc_cons", { - "variants", map(gen.builtin_string, inferrable_term), + "variants", map(symbol_type, inferrable_term), "rest", inferrable_term, } }, { "enum_elim", { @@ -411,7 +422,7 @@ inferrable_term:define_enum("inferrable", { { "enum_type", { "desc", inferrable_term } }, { "enum_case", { "target", inferrable_term, - "variants", map(gen.builtin_string, inferrable_term), + "variants", map(symbol_type, inferrable_term), --"default", inferrable_term, } }, { "enum_absurd", { @@ -419,15 +430,17 @@ inferrable_term:define_enum("inferrable", { "debug", gen.builtin_string, } }, - { "object_cons", { "methods", map(gen.builtin_string, inferrable_term) } }, + { "object_cons", { "methods", map(symbol_type, inferrable_term) } }, { "object_elim", { "subject", inferrable_term, "mechanism", inferrable_term, } }, { "let", { - "name", gen.builtin_string, - "expr", inferrable_term, - "body", inferrable_term, + "name", symbol_type, + "expr", inferrable_term, + "body", inferrable_term, + "start_anchor", anchor_type, + "end_anchor", anchor_type, } }, { "operative_cons", { "operative_type", inferrable_term, @@ -599,7 +612,7 @@ typed_term:define_enum("typed", { { "bound_variable", { "index", gen.builtin_number } }, { "literal", { "literal_value", value } }, { "lambda", { - "param_name", gen.builtin_string, + "param_name", symbol_type, "body", typed_term, } }, { "pi", { @@ -613,7 +626,7 @@ typed_term:define_enum("typed", { "arg", typed_term, } }, { "let", { - "name", gen.builtin_string, + "name", symbol_type, "expr", typed_term, "body", typed_term, } }, @@ -629,7 +642,7 @@ typed_term:define_enum("typed", { { "tuple_cons", { "elements", array(typed_term) } }, --{"tuple_extend", {"base", typed_term, "fields", array(typed_term)}}, -- maybe? { "tuple_elim", { - "names", array(gen.builtin_string), + "names", symbol_array, "subject", typed_term, "length", gen.builtin_number, "body", typed_term, @@ -640,19 +653,19 @@ typed_term:define_enum("typed", { } }, { "tuple_type", { "desc", typed_term } }, { "tuple_desc_type", { "universe", typed_term } }, - { "record_cons", { "fields", map(gen.builtin_string, typed_term) } }, + { "record_cons", { "fields", map(symbol_type, typed_term) } }, { "record_extend", { "base", typed_term, - "fields", map(gen.builtin_string, typed_term), + "fields", map(symbol_type, typed_term), } }, { "record_elim", { "subject", typed_term, - "field_names", array(gen.builtin_string), + "field_names", symbol_array, "body", typed_term, } }, --TODO record elim { "enum_cons", { - "constructor", gen.builtin_string, + "constructor", symbol_type, "arg", typed_term, } }, { "enum_elim", { @@ -664,7 +677,7 @@ typed_term:define_enum("typed", { "mechanism", typed_term, } }, { "enum_desc_cons", { - "variants", map(gen.builtin_string, typed_term), + "variants", map(symbol_type, typed_term), "rest", typed_term, } }, { "enum_desc_type", { @@ -673,15 +686,15 @@ typed_term:define_enum("typed", { { "enum_type", { "desc", typed_term } }, { "enum_case", { "target", typed_term, - "variants", map(gen.builtin_string, typed_term), + "variants", map(symbol_type, typed_term), "default", typed_term, } }, { "enum_absurd", { "target", typed_term, "debug", gen.builtin_string, } }, - { "object_cons", { "methods", map(gen.builtin_string, typed_term) } }, - { "object_corec_cons", { "methods", map(gen.builtin_string, typed_term) } }, + { "object_cons", { "methods", map(symbol_type, typed_term) } }, + { "object_corec_cons", { "methods", map(symbol_type, typed_term) } }, { "object_elim", { "subject", typed_term, "mechanism", typed_term, @@ -780,7 +793,7 @@ typed_term:define_enum("typed", { -- stylua: ignore placeholder_debug:define_record("placeholder_debug", { - "name", gen.builtin_string, + "name", symbol_type, "start_anchor", anchor_type, "end_anchor", anchor_type, }) @@ -887,7 +900,7 @@ value:define_enum("value", { -- closure is a type that contains a typed term corresponding to the body -- and a runtime context representng the bound context where the closure was created { "closure", { - "param_name", gen.builtin_string, + "param_name", symbol_type, "code", typed_term, "capture", runtime_context_type, } }, @@ -916,7 +929,7 @@ value:define_enum("value", { --{"typechecker_monad_value", }, -- TODO --{"typechecker_monad_type", {"wrapped_type", value}}, { "name_type" }, - { "name", { "name", gen.builtin_string } }, + { "name", { "name", symbol_type } }, { "operative_value", { "userdata", value } }, { "operative_type", { "handler", value, @@ -928,21 +941,21 @@ value:define_enum("value", { { "tuple_type", { "desc", value } }, { "tuple_desc_type", { "universe", value } }, { "enum_value", { - "constructor", gen.builtin_string, + "constructor", symbol_type, "arg", value, } }, { "enum_type", { "desc", value } }, { "enum_desc_type", { "universe", value } }, - { "enum_desc_value", { "variants", gen.declare_map(gen.builtin_string, value) } }, - { "record_value", { "fields", map(gen.builtin_string, value) } }, + { "enum_desc_value", { "variants", gen.declare_map(symbol_type, value) } }, + { "record_value", { "fields", map(symbol_type, value) } }, { "record_type", { "desc", value } }, { "record_desc_type", { "universe", value } }, { "record_extend_stuck", { "base", neutral_value, - "extension", map(gen.builtin_string, value), + "extension", map(symbol_type, value), } }, { "object_value", { - "methods", map(gen.builtin_string, typed_term), + "methods", map(symbol_type, typed_term), "capture", runtime_context_type, } }, { "object_type", { "desc", value } }, @@ -1049,7 +1062,7 @@ neutral_value:define_enum("neutral_value", { } }, { "record_field_access_stuck", { "subject", neutral_value, - "field_name", gen.builtin_string, + "field_name", symbol_type, } }, { "host_application_stuck", { "function", gen.any_lua_type, @@ -1088,8 +1101,8 @@ local host_lua_error_type = value.host_user_defined_type({ name = "lua_error_typ ---@class DescConsContainer local DescCons = --[[@enum DescCons]] { - cons = "cons", - empty = "empty", + cons = format.internal_symbols["cons"], + empty = format.internal_symbols["empty"], } local value_array = array(value) @@ -1134,6 +1147,9 @@ local TCState = local lua_prog = effect_id(effect_registry:register("lua_prog", "running effectful lua code"), set(unique_id)()) local terms = { + anchor_type = anchor_type, + symbol_type = symbol_type, + symbol_array = symbol_array, metavariable_mt = metavariable_mt, checkable_term = checkable_term, -- {} inferrable_term = inferrable_term, -- {} diff --git a/test-fitsinto.lua b/test-fitsinto.lua index 5b8f6edc..864e6a32 100644 --- a/test-fitsinto.lua +++ b/test-fitsinto.lua @@ -3,9 +3,10 @@ local terms = require "terms" local gen = require "terms-generators" local evaluator = require "evaluator" -local value = terms.value -local typed = terms.typed_term local fitsinto = evaluator.fitsinto +local internal_symbols = require("format").internal_symbols +local typed = terms.typed_term +local value = terms.value local val_array = gen.declare_array(value) @@ -124,7 +125,7 @@ local passed, failed, total = (require "tap")(function(test) test("tuple type decl", function(expect) -- fitsinto needs to handle tuple type by applying the closures on prior element (from right side always) -- not by blindly applying closure like it is right now - local names = gen.declare_array(gen.builtin_string) + local names = terms.symbol_array local decl_a = value.tuple_type( val_desc_elem( val_tup_cons( @@ -132,16 +133,16 @@ local passed, failed, total = (require "tap")(function(test) val_tup_cons( val_desc_empty, value.closure( - "#A", + internal_symbols["#A"], typed.tuple_elim(names(), typed.bound_variable(1), 0, typed.star(1)), terms.runtime_context() ) ) ), value.closure( - "#B", + internal_symbols["#B"], terms.typed_term.tuple_elim( - names("#FOO"), + names(internal_symbols["#FOO"]), terms.typed_term.bound_variable(1), 1, typed.bound_variable(2) @@ -158,16 +159,16 @@ local passed, failed, total = (require "tap")(function(test) val_tup_cons( val_desc_empty, value.closure( - "#C", + internal_symbols["#C"], typed.tuple_elim(names(), typed.bound_variable(1), 0, typed.star(1)), terms.runtime_context() ) ) ), value.closure( - "#D", + internal_symbols["#D"], terms.typed_term.tuple_elim( - names("#BAR"), + names(internal_symbols["#BAR"]), terms.typed_term.bound_variable(1), 1, typed.bound_variable(2) diff --git a/test.lua b/test.lua index ba8c6a80..8b5d21e7 100644 --- a/test.lua +++ b/test.lua @@ -17,7 +17,8 @@ local function simplify_list(list) else if list.kind == "literal" then return list.val - elseif list.kind == "symbol" then + elseif format.is_symbol(list) then + ---@cast list Symbol return list.str elseif list.kind == "comment" then return list.val diff --git a/types/binding.lua b/types/binding.lua index a032213a..2c16b555 100644 --- a/types/binding.lua +++ b/types/binding.lua @@ -6,25 +6,33 @@ binding = {} ---@return boolean function binding:is_let() end ----@return string name +---@return Symbol name ---@return inferrable expr +---@return Anchor start_anchor +---@return Anchor end_anchor function binding:unwrap_let() end ---@return boolean ----@return string name +---@return Symbol name ---@return inferrable expr +---@return Anchor start_anchor +---@return Anchor end_anchor function binding:as_let() end ---@return boolean function binding:is_tuple_elim() end ---@return ArrayValue names ---@return inferrable subject +---@return Anchor start_anchor +---@return Anchor end_anchor function binding:unwrap_tuple_elim() end ---@return boolean ---@return ArrayValue names ---@return inferrable subject +---@return Anchor start_anchor +---@return Anchor end_anchor function binding:as_tuple_elim() end ---@return boolean function binding:is_annotated_lambda() end ----@return string param_name +---@return Symbol param_name ---@return inferrable param_annotation ---@return Anchor start_anchor ---@return Anchor end_anchor @@ -32,7 +40,7 @@ function binding:is_annotated_lambda() end ---@return checkable pure function binding:unwrap_annotated_lambda() end ---@return boolean ----@return string param_name +---@return Symbol param_name ---@return inferrable param_annotation ---@return Anchor start_anchor ---@return Anchor end_anchor @@ -53,8 +61,8 @@ function binding:as_program_sequence() end ---@class (exact) bindingType: EnumType ---@field define_enum fun(self: bindingType, name: string, variants: Variants): bindingType ----@field let fun(name: string, expr: inferrable): binding ----@field tuple_elim fun(names: ArrayValue, subject: inferrable): binding ----@field annotated_lambda fun(param_name: string, param_annotation: inferrable, start_anchor: Anchor, end_anchor: Anchor, visible: visibility, pure: checkable): binding +---@field let fun(name: Symbol, expr: inferrable, start_anchor: Anchor, end_anchor: Anchor): binding +---@field tuple_elim fun(names: ArrayValue, subject: inferrable, start_anchor: Anchor, end_anchor: Anchor): binding +---@field annotated_lambda fun(param_name: Symbol, param_annotation: inferrable, start_anchor: Anchor, end_anchor: Anchor, visible: visibility, pure: checkable): binding ---@field program_sequence fun(first: inferrable, start_anchor: Anchor, end_anchor: Anchor): binding return {} diff --git a/types/checkable.lua b/types/checkable.lua index f711baad..1bcfd31b 100644 --- a/types/checkable.lua +++ b/types/checkable.lua @@ -27,11 +27,11 @@ function checkable:unwrap_host_tuple_cons() end function checkable:as_host_tuple_cons() end ---@return boolean function checkable:is_lambda() end ----@return string param_name +---@return Symbol param_name ---@return checkable body function checkable:unwrap_lambda() end ---@return boolean ----@return string param_name +---@return Symbol param_name ---@return checkable body function checkable:as_lambda() end @@ -40,5 +40,5 @@ function checkable:as_lambda() end ---@field inferrable fun(inferrable_term: inferrable): checkable ---@field tuple_cons fun(elements: ArrayValue): checkable ---@field host_tuple_cons fun(elements: ArrayValue): checkable ----@field lambda fun(param_name: string, body: checkable): checkable +---@field lambda fun(param_name: Symbol, body: checkable): checkable return {} diff --git a/types/inferrable.lua b/types/inferrable.lua index fe8fa946..860c7640 100644 --- a/types/inferrable.lua +++ b/types/inferrable.lua @@ -24,7 +24,7 @@ function inferrable:unwrap_typed() end function inferrable:as_typed() end ---@return boolean function inferrable:is_annotated_lambda() end ----@return string param_name +---@return Symbol param_name ---@return inferrable param_annotation ---@return inferrable body ---@return Anchor start_anchor @@ -33,7 +33,7 @@ function inferrable:is_annotated_lambda() end ---@return checkable pure function inferrable:unwrap_annotated_lambda() end ---@return boolean ----@return string param_name +---@return Symbol param_name ---@return inferrable param_annotation ---@return inferrable body ---@return Anchor start_anchor @@ -75,11 +75,15 @@ function inferrable:is_tuple_elim() end ---@return ArrayValue names ---@return inferrable subject ---@return inferrable body +---@return Anchor start_anchor +---@return Anchor end_anchor function inferrable:unwrap_tuple_elim() end ---@return boolean ---@return ArrayValue names ---@return inferrable subject ---@return inferrable body +---@return Anchor start_anchor +---@return Anchor end_anchor function inferrable:as_tuple_elim() end ---@return boolean function inferrable:is_tuple_type() end @@ -108,11 +112,11 @@ function inferrable:unwrap_record_elim() end function inferrable:as_record_elim() end ---@return boolean function inferrable:is_enum_cons() end ----@return string constructor +---@return Symbol constructor ---@return inferrable arg function inferrable:unwrap_enum_cons() end ---@return boolean ----@return string constructor +---@return Symbol constructor ---@return inferrable arg function inferrable:as_enum_cons() end ---@return boolean @@ -176,14 +180,18 @@ function inferrable:unwrap_object_elim() end function inferrable:as_object_elim() end ---@return boolean function inferrable:is_let() end ----@return string name +---@return Symbol name ---@return inferrable expr ---@return inferrable body +---@return Anchor start_anchor +---@return Anchor end_anchor function inferrable:unwrap_let() end ---@return boolean ----@return string name +---@return Symbol name ---@return inferrable expr ---@return inferrable body +---@return Anchor start_anchor +---@return Anchor end_anchor function inferrable:as_let() end ---@return boolean function inferrable:is_operative_cons() end @@ -374,15 +382,15 @@ function inferrable:as_program_type() end ---@field define_enum fun(self: inferrableType, name: string, variants: Variants): inferrableType ---@field bound_variable fun(index: number): 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, end_anchor: Anchor, visible: visibility, pure: checkable): inferrable +---@field annotated_lambda fun(param_name: Symbol, param_annotation: inferrable, body: inferrable, start_anchor: Anchor, end_anchor: Anchor, visible: visibility, pure: checkable): inferrable ---@field pi fun(param_type: inferrable, param_info: checkable, result_type: inferrable, result_info: checkable): inferrable ---@field application fun(f: inferrable, arg: checkable): inferrable ---@field tuple_cons fun(elements: ArrayValue): inferrable ----@field tuple_elim fun(names: ArrayValue, subject: inferrable, body: inferrable): inferrable +---@field tuple_elim fun(names: ArrayValue, subject: inferrable, body: inferrable, start_anchor: Anchor, end_anchor: Anchor): inferrable ---@field tuple_type fun(desc: inferrable): inferrable ---@field record_cons fun(fields: MapValue): inferrable ---@field record_elim fun(subject: inferrable, field_names: ArrayValue, body: inferrable): inferrable ----@field enum_cons fun(constructor: string, arg: inferrable): inferrable +---@field enum_cons fun(constructor: Symbol, arg: inferrable): inferrable ---@field enum_desc_cons fun(variants: MapValue, rest: inferrable): inferrable ---@field enum_elim fun(subject: inferrable, mechanism: inferrable): inferrable ---@field enum_type fun(desc: inferrable): inferrable @@ -390,7 +398,7 @@ function inferrable:as_program_type() end ---@field enum_absurd fun(target: inferrable, debug: string): inferrable ---@field object_cons fun(methods: MapValue): inferrable ---@field object_elim fun(subject: inferrable, mechanism: inferrable): inferrable ----@field let fun(name: string, expr: inferrable, body: inferrable): inferrable +---@field let fun(name: Symbol, expr: inferrable, body: inferrable, start_anchor: Anchor, end_anchor: Anchor): inferrable ---@field operative_cons fun(operative_type: inferrable, userdata: inferrable): inferrable ---@field operative_type_cons fun(handler: checkable, userdata_type: inferrable): inferrable ---@field level_type inferrable diff --git a/types/neutral_value.lua b/types/neutral_value.lua index 440ac9bb..3539c63e 100644 --- a/types/neutral_value.lua +++ b/types/neutral_value.lua @@ -59,11 +59,11 @@ function neutral_value:as_tuple_element_access_stuck() end ---@return boolean function neutral_value:is_record_field_access_stuck() end ---@return neutral_value subject ----@return string field_name +---@return Symbol field_name function neutral_value:unwrap_record_field_access_stuck() end ---@return boolean ---@return neutral_value subject ----@return string field_name +---@return Symbol field_name function neutral_value:as_record_field_access_stuck() end ---@return boolean function neutral_value:is_host_application_stuck() end @@ -130,7 +130,7 @@ function neutral_value:as_host_unwrap_stuck() end ---@field enum_rec_elim_stuck fun(handler: value, subject: neutral_value): neutral_value ---@field object_elim_stuck fun(mechanism: value, subject: neutral_value): neutral_value ---@field tuple_element_access_stuck fun(subject: neutral_value, index: number): neutral_value ----@field record_field_access_stuck fun(subject: neutral_value, field_name: string): neutral_value +---@field record_field_access_stuck fun(subject: neutral_value, field_name: Symbol): neutral_value ---@field host_application_stuck fun(function: any, arg: neutral_value): neutral_value ---@field host_tuple_stuck fun(leading: ArrayValue, stuck_element: neutral_value, trailing: ArrayValue): neutral_value ---@field host_if_stuck fun(subject: neutral_value, consequent: value, alternate: value): neutral_value diff --git a/types/placeholder_debug.lua b/types/placeholder_debug.lua index 4ce05c4f..e8719761 100644 --- a/types/placeholder_debug.lua +++ b/types/placeholder_debug.lua @@ -4,7 +4,7 @@ ---@class (exact) placeholder_debug: RecordValue placeholder_debug = {} ----@return string +---@return Symbol ---@return Anchor ---@return Anchor function placeholder_debug:unwrap_placeholder_debug() end diff --git a/types/typed.lua b/types/typed.lua index 7bed3527..57ca87f0 100644 --- a/types/typed.lua +++ b/types/typed.lua @@ -20,11 +20,11 @@ function typed:unwrap_literal() end function typed:as_literal() end ---@return boolean function typed:is_lambda() end ----@return string param_name +---@return Symbol param_name ---@return typed body function typed:unwrap_lambda() end ---@return boolean ----@return string param_name +---@return Symbol param_name ---@return typed body function typed:as_lambda() end ---@return boolean @@ -51,12 +51,12 @@ function typed:unwrap_application() end function typed:as_application() end ---@return boolean function typed:is_let() end ----@return string name +---@return Symbol name ---@return typed expr ---@return typed body function typed:unwrap_let() end ---@return boolean ----@return string name +---@return Symbol name ---@return typed expr ---@return typed body function typed:as_let() end @@ -176,11 +176,11 @@ function typed:unwrap_record_elim() end function typed:as_record_elim() end ---@return boolean function typed:is_enum_cons() end ----@return string constructor +---@return Symbol constructor ---@return typed arg function typed:unwrap_enum_cons() end ---@return boolean ----@return string constructor +---@return Symbol constructor ---@return typed arg function typed:as_enum_cons() end ---@return boolean @@ -524,10 +524,10 @@ function typed:as_constrained_type() end ---@field define_enum fun(self: typedType, name: string, variants: Variants): typedType ---@field bound_variable fun(index: number): typed ---@field literal fun(literal_value: value): typed ----@field lambda fun(param_name: string, body: typed): typed +---@field lambda fun(param_name: Symbol, body: typed): typed ---@field pi fun(param_type: typed, param_info: typed, result_type: typed, result_info: typed): typed ---@field application fun(f: typed, arg: typed): typed ----@field let fun(name: string, expr: typed, body: typed): typed +---@field let fun(name: Symbol, expr: typed, body: typed): typed ---@field level_type typed ---@field level0 typed ---@field level_suc fun(previous_level: typed): typed @@ -542,7 +542,7 @@ function typed:as_constrained_type() end ---@field record_cons fun(fields: MapValue): typed ---@field record_extend fun(base: typed, fields: MapValue): typed ---@field record_elim fun(subject: typed, field_names: ArrayValue, body: typed): typed ----@field enum_cons fun(constructor: string, arg: typed): typed +---@field enum_cons fun(constructor: Symbol, arg: typed): typed ---@field enum_elim fun(subject: typed, mechanism: typed): typed ---@field enum_rec_elim fun(subject: typed, mechanism: typed): typed ---@field enum_desc_cons fun(variants: MapValue, rest: typed): typed diff --git a/types/value.lua b/types/value.lua index e1fe9c39..6be9290f 100644 --- a/types/value.lua +++ b/types/value.lua @@ -58,12 +58,12 @@ function value:unwrap_pi() end function value:as_pi() end ---@return boolean function value:is_closure() end ----@return string param_name +---@return Symbol param_name ---@return typed code ---@return RuntimeContext capture function value:unwrap_closure() end ---@return boolean ----@return string param_name +---@return Symbol param_name ---@return typed code ---@return RuntimeContext capture function value:as_closure() end @@ -86,10 +86,10 @@ function value:unwrap_name_type() end function value:as_name_type() end ---@return boolean function value:is_name() end ----@return string name +---@return Symbol name function value:unwrap_name() end ---@return boolean ----@return string name +---@return Symbol name function value:as_name() end ---@return boolean function value:is_operative_value() end @@ -130,11 +130,11 @@ function value:unwrap_tuple_desc_type() end function value:as_tuple_desc_type() end ---@return boolean function value:is_enum_value() end ----@return string constructor +---@return Symbol constructor ---@return value arg function value:unwrap_enum_value() end ---@return boolean ----@return string constructor +---@return Symbol constructor ---@return value arg function value:as_enum_value() end ---@return boolean @@ -450,16 +450,16 @@ function value:as_union_type() end ---@field result_info_type value ---@field result_info fun(result_info: result_info): value ---@field pi fun(param_type: value, param_info: value, result_type: value, result_info: value): value ----@field closure fun(param_name: string, code: typed, capture: RuntimeContext): value +---@field closure fun(param_name: Symbol, code: typed, capture: RuntimeContext): value ---@field range fun(lower_bounds: ArrayValue, upper_bounds: ArrayValue, relation: value): value ---@field name_type value ----@field name fun(name: string): value +---@field name fun(name: Symbol): value ---@field operative_value fun(userdata: value): value ---@field operative_type fun(handler: value, userdata_type: value): value ---@field tuple_value fun(elements: ArrayValue): value ---@field tuple_type fun(desc: value): value ---@field tuple_desc_type fun(universe: value): value ----@field enum_value fun(constructor: string, arg: value): value +---@field enum_value fun(constructor: Symbol, arg: value): value ---@field enum_type fun(desc: value): value ---@field enum_desc_type fun(universe: value): value ---@field enum_desc_value fun(variants: MapValue): value diff --git a/unformatter.lua b/unformatter.lua index 8bc1f687..a57e58ad 100644 --- a/unformatter.lua +++ b/unformatter.lua @@ -2,6 +2,8 @@ -- put tokens on a new line if their line number is greater than the current line -- this is not a format tool it's a lisp-ifier for the format +local is_symbol = require("format").is_symbol + local indentation_char = "\t" ---@param ast FormatList @@ -34,7 +36,7 @@ local function unformat_list(ast, prev_line, indentation) acc = acc .. ")" elseif ast.kind == "literal" then acc = acc .. tostring(ast.val) - elseif ast.kind == "symbol" then + elseif is_symbol(ast) then acc = acc .. ast.str elseif ast.kind == "comment" then indentation = indentation + 1