diff --git a/alicorn-utils.lua b/alicorn-utils.lua index fee2992..bf174a9 100644 --- a/alicorn-utils.lua +++ b/alicorn-utils.lua @@ -303,4 +303,47 @@ function M.get_cursor_position(input_file, output_file) return cursor_line, cursor_column end +-- https://gist.github.com/Badgerati/3261142 +-- Returns the Levenshtein distance between the two given strings +function M.levenshtein(str1, str2) + local len1 = string.len(str1) + local len2 = string.len(str2) + local matrix = {} + local cost = 0 + + -- quick cut-offs to save time + if len1 == 0 then + return len2 + elseif len2 == 0 then + return len1 + elseif str1 == str2 then + return 0 + end + + -- initialise the base matrix values + for i = 0, len1, 1 do + matrix[i] = {} + matrix[i][0] = i + end + for j = 0, len2, 1 do + matrix[0][j] = j + end + + -- actual Levenshtein algorithm + for i = 1, len1, 1 do + for j = 1, len2, 1 do + if str1:byte(i) == str2:byte(j) then + cost = 0 + else + cost = 1 + end + + matrix[i][j] = math.min(matrix[i - 1][j] + 1, matrix[i][j - 1] + 1, matrix[i - 1][j - 1] + cost) + end + end + + -- return the last value - this is the Levenshtein distance + return matrix[len1][len2] +end + return M diff --git a/base-env.lua b/base-env.lua index f930b93..792cf7e 100644 --- a/base-env.lua +++ b/base-env.lua @@ -6,6 +6,7 @@ local exprs = require "alicorn-expressions" 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 @@ -30,7 +31,7 @@ end ---handle a let binding ---@type lua_operative -local function let_bind(syntax, env) +local function let_impl(syntax, env) local ok, name, tail = syntax:match({ metalanguage.listtail( metalanguage.accept_handler, @@ -67,7 +68,7 @@ local function let_bind(syntax, env) if not env or not env.get then p(env) - error("env in let_bind isn't an env") + error("env in let_impl isn't an env") end if not name["kind"] then @@ -95,6 +96,122 @@ local function let_bind(syntax, env) env end +---@type lua_operative +local function mk_impl(syntax, env) + local ok, bun = syntax:match({ + metalanguage.listmatch( + metalanguage.accept_handler, + metalanguage.listtail(utils.accept_bundled, metalanguage.issymbol(metalanguage.accept_handler)) + ), + metalanguage.listtail(utils.accept_bundled, metalanguage.issymbol(metalanguage.accept_handler)), + }, metalanguage.failure_handler, nil) + if not ok then + return ok, bun + end + local name, tail = utils.unpack_bundle(bun) + local tuple + ok, tuple, env = tail:match({ + exprs.collect_tuple(metalanguage.accept_handler, exprs.ExpressionArgs.new(terms.expression_goal.infer, env)), + }, metalanguage.failure_handler, nil) + if not ok then + return ok, tuple + end + return ok, terms.inferrable_term.enum_cons(name.str, tuple), env +end + +---@type Matcher +local switch_case_header_matcher = metalanguage.listtail( + metalanguage.accept_handler, + metalanguage.oneof( + metalanguage.accept_handler, + metalanguage.issymbol(utils.accept_bundled), + metalanguage.list_many(metalanguage.accept_handler, metalanguage.issymbol(metalanguage.accept_handler)) + ), + 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 env Environment +local switch_case = metalanguage.reducer(function(syntax, env) + local ok, tag, tail = syntax:match({ switch_case_header_matcher }, metalanguage.failure_handler, nil) + if not ok then + return ok, tag + end + + local names = gen.declare_array(gen.builtin_string)(unwrap_into_string(table.unpack(tag, 2))) + tag = tag[1] + + if not tag then + return false, "missing case tag" + end + local singleton_contents + ok, singleton_contents = tail:match({ + metalanguage.listmatch(metalanguage.accept_handler, metalanguage.any(metalanguage.accept_handler)), + }, metalanguage.failure_handler, nil) + if ok then + tail = singleton_contents + end + --TODO rewrite this to use an environment-splitting operation + env = environment.new_env(env, { + typechecking_context = env.typechecking_context:append( + "#switch-subj", + evaluator.typechecker_state:metavariable(env.typechecking_context):as_value(), + nil, + syntax.start_anchor + ), + }) + 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())) + ) + ok, term, env = tail:match({ + exprs.inferred_expression(metalanguage.accept_handler, env), + }, metalanguage.failure_handler, nil) + if not ok then + return ok, term + end + env, term = env:exit_block(term, shadowed) + term.start_anchor = syntax.start_anchor --TODO figure out where to store/retrieve the anchors correctly + term.end_anchor = syntax.end_anchor + return ok, tag, term, env +end, "switch_case") + +---@type lua_operative +local function switch_impl(syntax, env) + local ok, subj + ok, subj, syntax = syntax:match({ + metalanguage.listtail(metalanguage.accept_handler, exprs.inferred_expression(utils.accept_bundled, env)), + }, metalanguage.failure_handler, nil) + if not ok then + return ok, subj + end + subj, env = table.unpack(subj) + local variants = gen.declare_map(gen.builtin_string, terms.inferrable_term)() + while not syntax:match({ metalanguage.isnil(metalanguage.accept_handler) }, metalanguage.failure_handler, nil) do + local tag, term + ok, tag, syntax = syntax:match({ + metalanguage.listtail(metalanguage.accept_handler, switch_case(utils.accept_bundled, env)), + }, metalanguage.failure_handler, nil) + if not ok then + return ok, tag + end + --TODO rewrite this to collect the branch envs and join them back together: + tag, term = table.unpack(tag) + variants:set(tag.str, term) + end + return true, terms.inferrable_term.enum_case(subj, variants), env +end + ---@param _ any ---@param symbol SyntaxSymbol ---@param exprenv { val:inferrable, env:Environment } @@ -133,7 +250,7 @@ local function record_build(syntax, env) end ---@type lua_operative -local function intrinsic(syntax, env) +local function intrinsic_impl(syntax, env) local ok, str_env, syntax = syntax:match({ metalanguage.listtail( metalanguage.accept_handler, @@ -340,7 +457,7 @@ local function lambda_curry_impl(syntax, env) return true, term, resenv end -local tupleof_ascribed_names_inner = metalanguage.reducer( +local tuple_desc_of_ascribed_names = metalanguage.reducer( ---@param syntax ConstructedSyntax ---@param env Environment ---@return boolean @@ -382,17 +499,17 @@ local tupleof_ascribed_names_inner = metalanguage.reducer( return ok, thread end, - "tupleof_ascribed_names_inner" + "tuple_desc_of_ascribed_names" ) -local tupleof_ascribed_names = metalanguage.reducer( +local tuple_of_ascribed_names = metalanguage.reducer( ---@param syntax ConstructedSyntax ---@param env Environment ---@return boolean ---@return {names: string[], args: inferrable, env: Environment}|string function(syntax, env) local ok, thread = syntax:match({ - tupleof_ascribed_names_inner(metalanguage.accept_handler, env), + tuple_desc_of_ascribed_names(metalanguage.accept_handler, env), }, metalanguage.failure_handler, nil) if not ok then return ok, thread @@ -400,17 +517,17 @@ local tupleof_ascribed_names = metalanguage.reducer( thread.args = terms.inferrable_term.tuple_type(thread.args) return ok, thread end, - "tupleof_ascribed_names" + "tuple_of_ascribed_names" ) -local host_tupleof_ascribed_names = metalanguage.reducer( +local host_tuple_of_ascribed_names = metalanguage.reducer( ---@param syntax ConstructedSyntax ---@param env Environment ---@return boolean ---@return {names: string[], args: inferrable, env: Environment}|string function(syntax, env) local ok, thread = syntax:match({ - tupleof_ascribed_names_inner(metalanguage.accept_handler, env), + tuple_desc_of_ascribed_names(metalanguage.accept_handler, env), }, metalanguage.failure_handler, nil) if not ok then return ok, thread @@ -418,7 +535,7 @@ local host_tupleof_ascribed_names = metalanguage.reducer( thread.args = terms.inferrable_term.host_tuple_type(thread.args) return ok, thread end, - "host_tupleof_ascribed_names" + "host_tuple_of_ascribed_names" ) local ascribed_segment = metalanguage.reducer( @@ -449,7 +566,7 @@ local ascribed_segment = metalanguage.reducer( thread = { names = name, args = type_val, env = type_env } else ok, thread = syntax:match({ - tupleof_ascribed_names(metalanguage.accept_handler, env), + tuple_of_ascribed_names(metalanguage.accept_handler, env), }, metalanguage.failure_handler, nil) if not ok then return ok, thread @@ -490,7 +607,7 @@ local host_ascribed_segment = metalanguage.reducer( thread = { names = name, args = type_val, env = type_env } else ok, thread = syntax:match({ - host_tupleof_ascribed_names(metalanguage.accept_handler, env), + host_tuple_of_ascribed_names(metalanguage.accept_handler, env), }, metalanguage.failure_handler, nil) if not ok then return ok, thread @@ -503,7 +620,7 @@ local host_ascribed_segment = metalanguage.reducer( "host_ascribed_segment" ) -local tuplewrap_ascribed_name_inner = metalanguage.reducer( +local tuple_desc_wrap_ascribed_name = metalanguage.reducer( ---@param syntax ConstructedSyntax ---@param env Environment ---@return boolean @@ -535,46 +652,10 @@ local tuplewrap_ascribed_name_inner = metalanguage.reducer( env = type_env return ok, { names = names, args = args, env = env } end, - "tuplewrap_ascribed_name_inner" -) - -local tuplewrap_ascribed_name = metalanguage.reducer( - ---@param syntax ConstructedSyntax - ---@param env Environment - ---@return boolean - ---@return {names: string[], args: inferrable, env: Environment}|string - function(syntax, env) - local ok, thread = syntax:match({ - tuplewrap_ascribed_name_inner(metalanguage.accept_handler, env), - }, metalanguage.failure_handler, nil) - if not ok then - return ok, thread - end - thread.args = terms.inferrable_term.tuple_type(thread.args) - return ok, thread - end, - "tuplewrap_ascribed_name" -) - -local host_tuplewrap_ascribed_name = metalanguage.reducer( - ---@param syntax ConstructedSyntax - ---@param env Environment - ---@return boolean - ---@return {names: string[], args: inferrable, env: Environment}|string - function(syntax, env) - local ok, thread = syntax:match({ - tuplewrap_ascribed_name_inner(metalanguage.accept_handler, env), - }, metalanguage.failure_handler, nil) - if not ok then - return ok, thread - end - thread.args = terms.inferrable_term.host_tuple_type(thread.args) - return ok, thread - end, - "host_tuplewrap_ascribed_name" + "tuple_desc_wrap_ascribed_name" ) -local ascribed_segment_2 = metalanguage.reducer( +local ascribed_segment_tuple_desc = metalanguage.reducer( ---@param syntax ConstructedSyntax ---@param env Environment ---@return boolean @@ -594,51 +675,40 @@ local ascribed_segment_2 = metalanguage.reducer( if single then ok, thread = syntax:match({ - tuplewrap_ascribed_name(metalanguage.accept_handler, env), + tuple_desc_wrap_ascribed_name(metalanguage.accept_handler, env), }, metalanguage.failure_handler, nil) else ok, thread = syntax:match({ - tupleof_ascribed_names(metalanguage.accept_handler, env), + tuple_desc_of_ascribed_names(metalanguage.accept_handler, env), }, metalanguage.failure_handler, nil) end return ok, thread end, - "ascribed_segment_2" + "ascribed_segment_tuple_desc" ) -local host_ascribed_segment_2 = metalanguage.reducer( - ---@param syntax ConstructedSyntax - ---@param env Environment - ---@return boolean - ---@return {names: string[], args: inferrable, env: Environment}|string - function(syntax, env) - -- check whether syntax looks like a single annotated param - local single, _, _, _ = syntax:match({ - metalanguage.listmatch( - metalanguage.accept_handler, - metalanguage.any(metalanguage.accept_handler), - metalanguage.symbol_exact(metalanguage.accept_handler, ":"), - metalanguage.any(metalanguage.accept_handler) - ), - }, metalanguage.failure_handler, nil) - - local ok, thread - - if single then - ok, thread = syntax:match({ - host_tuplewrap_ascribed_name(metalanguage.accept_handler, env), - }, metalanguage.failure_handler, nil) - else - ok, thread = syntax:match({ - host_tupleof_ascribed_names(metalanguage.accept_handler, env), - }, metalanguage.failure_handler, nil) - end +local ascribed_segment_tuple = metalanguage.reducer(function(syntax, env) + local ok, thread = syntax:match({ + ascribed_segment_tuple_desc(metalanguage.accept_handler, env), + }, metalanguage.failure_handler, nil) + if not ok then + return ok, thread + end + thread.args = terms.inferrable_term.tuple_type(thread.args) + return ok, thread +end, "ascribed_segment_tuple") +local host_ascribed_segment_tuple = metalanguage.reducer(function(syntax, env) + local ok, thread = syntax:match({ + ascribed_segment_tuple_desc(metalanguage.accept_handler, env), + }, metalanguage.failure_handler, nil) + if not ok then return ok, thread - end, - "host_ascribed_segment_2" -) + end + thread.args = terms.inferrable_term.host_tuple_type(thread.args) + return ok, thread +end, "host_ascribed_segment_tuple") -- TODO: abstract so can reuse for func type and host func type local function make_host_func_syntax(effectful) @@ -948,7 +1018,7 @@ end ---@type lua_operative local function lambda_impl(syntax, env) local ok, thread, tail = syntax:match({ - metalanguage.listtail(metalanguage.accept_handler, ascribed_segment_2(metalanguage.accept_handler, env)), + metalanguage.listtail(metalanguage.accept_handler, ascribed_segment_tuple(metalanguage.accept_handler, env)), }, metalanguage.failure_handler, nil) if not ok then return ok, thread @@ -983,7 +1053,7 @@ end ---@type lua_operative local function lambda_prog_impl(syntax, env) local ok, thread, tail = syntax:match({ - metalanguage.listtail(metalanguage.accept_handler, ascribed_segment_2(metalanguage.accept_handler, env)), + metalanguage.listtail(metalanguage.accept_handler, ascribed_segment_tuple(metalanguage.accept_handler, env)), }, metalanguage.failure_handler, nil) if not ok then return ok, thread @@ -1072,7 +1142,7 @@ end ---@type lua_operative local function lambda_annotated_impl(syntax, env) local ok, thread, tail = syntax:match({ - metalanguage.listtail(metalanguage.accept_handler, ascribed_segment_2(metalanguage.accept_handler, env)), + metalanguage.listtail(metalanguage.accept_handler, ascribed_segment_tuple(metalanguage.accept_handler, env)), }, metalanguage.failure_handler, nil) if not ok then return ok, thread @@ -1448,6 +1518,58 @@ local function build_wrapped(body_fn) ) end +---@param env Environment +local enum_variant = metalanguage.reducer(function(syntax, env) + local ok, tag, tail = syntax:match({ + metalanguage.listtail( + metalanguage.accept_handler, + metalanguage.issymbol(metalanguage.accept_handler), + ascribed_segment_tuple_desc(metalanguage.accept_handler, env) + ), + }, metalanguage.failure_handler, nil) + + if not ok then + return ok, tag + end + + if not tag then + return false, "missing enum variant name" + end + + return true, tag.str, terms.inferrable_term.tuple_type(tail.args), env +end, "enum_variant") + +---@type lua_operative +local function enum_impl(syntax, env) + local variants = gen.declare_map(gen.builtin_string, terms.inferrable_term)() + while not syntax:match({ metalanguage.isnil(metalanguage.accept_handler) }, metalanguage.failure_handler, nil) do + local tag, term + + ok, tag, syntax = syntax:match({ + metalanguage.listtail(metalanguage.accept_handler, enum_variant(utils.accept_bundled, env)), + }, metalanguage.failure_handler, nil) + if not ok then + return ok, tag + end + + tag, term = table.unpack(tag) + variants:set(tag, term) + end + + return true, + terms.inferrable_term.enum_type( + terms.inferrable_term.enum_desc_cons( + variants, + terms.inferrable_term.typed( + value.enum_desc_type(value.star(0, 0)), + usage_array(), + typed.literal(value.enum_desc_value(gen.declare_map(gen.builtin_string, terms.value)())) + ) + ) + ), + env +end + local core_operations = { ["+"] = exprs.host_applicative(function(a, b) return a + b @@ -1476,9 +1598,12 @@ local core_operations = { --end, types.tuple {types.number, types.number}, types.cotuple({types.unit, types.unit})), --["do"] = evaluator.host_operative(do_block), - let = exprs.host_operative(let_bind, "let_bind"), - record = exprs.host_operative(record_build, "record_build"), - intrinsic = exprs.host_operative(intrinsic, "intrinsic"), + let = exprs.host_operative(let_impl, "let_impl"), + mk = exprs.host_operative(mk_impl, "mk_impl"), + switch = exprs.host_operative(switch_impl, "switch_impl"), + enum = exprs.host_operative(enum_impl, "enum_impl"), + --record = exprs.host_operative(record_build, "record_build"), + intrinsic = exprs.host_operative(intrinsic_impl, "intrinsic_impl"), ["host-number"] = lit_term(value.host_number_type, value.host_type_type), ["host-type"] = lit_term(value.host_type_type, value.star(1, 1)), ["host-func-type"] = exprs.host_operative(make_host_func_syntax(false), "host_func_type_impl"), @@ -1530,7 +1655,7 @@ local function create() end local base_env = { - tupleof_ascribed_names_inner = tupleof_ascribed_names_inner, + ascribed_segment_tuple_desc = ascribed_segment_tuple_desc, create = create, } local internals_interface = require "internals-interface" diff --git a/evaluator.lua b/evaluator.lua index c59ff63..1c3cf83 100644 --- a/evaluator.lua +++ b/evaluator.lua @@ -235,11 +235,23 @@ enum_desc_srel = setmetatable({ end local use_variants = use:unwrap_enum_desc_value() for name, val_type in val_variants:pairs() do + local use_variant = use_variants:get(name) + if use_variant == nil then + local smallest = 99999999999 + local suggest = "[enum has no variants!]" + for n, _ in use_variants:pairs() do + local d = U.levenshtein(name, n) + if d < smallest then + smallest, suggest = d, n + end + end + error(name .. " is not a valid enum variant! Did you mean " .. suggest .. "?") + end typechecker_state:queue_subtype( lctx, val_type, rctx, - use_variants:get(name) --[[@as value -- please find a better approach]], + use_variant --[[@as value -- please find a better approach]], "enum variant" ) end @@ -400,8 +412,20 @@ local function substitute_inner(val, mappings, context_len) return typed_term.enum_cons(constructor, arg) elseif val:is_enum_type() then local desc = val:unwrap_enum_type() - -- TODO: Handle desc properly, because it's a value. - return typed_term.literal(val) + local desc_sub = substitute_inner(desc, mappings, context_len) + return typed_term.enum_type(desc_sub) + elseif val:is_enum_desc_type() then + local univ = val:unwrap_enum_desc_type() + local univ_sub = substitute_inner(univ, mappings, context_len) + return typed_term.enum_desc_type(univ_sub) + elseif val:is_enum_desc_value() then + local variants = val:unwrap_enum_desc_value() + ---@type MapValue + local variants_sub = string_typed_map() + for k, v in variants:pairs() do + variants_sub:set(k, substitute_inner(v, mappings, context_len)) + end + return typed_term.enum_desc_cons(variants_sub, typed_term.literal(value.enum_desc_value(string_value_map()))) elseif val:is_record_value() then -- TODO: How to deal with a map? error("Records not yet implemented") @@ -2010,7 +2034,7 @@ function infer( local subject_type, subject_usages, subject_term = infer(subject, typechecking_context) local constrain_variants = string_value_map() for k, v in variants:pairs() do - constrain_variants[k] = typechecker_state:metavariable(typechecking_context, false):as_value() + constrain_variants:set(k, typechecker_state:metavariable(typechecking_context, false):as_value()) end typechecker_state:flow( subject_type, @@ -2022,8 +2046,9 @@ function infer( local term_variants = string_typed_map() local result_types = {} for k, v in variants:pairs() do + --TODO figure out where to store/retrieve the anchors correctly local variant_type, variant_usages, variant_term = - infer(v, typechecking_context:append("#variant", constrain_variants:get(k), nil, nil)) --TODO improve + infer(v, typechecking_context:append("#variant", constrain_variants:get(k), nil, v.start_anchor)) --TODO improve term_variants:set(k, variant_term) result_types[#result_types + 1] = variant_type end @@ -2041,6 +2066,33 @@ function infer( "unacceptable enum variant" ) ) + elseif inferrable_term:is_enum_desc_cons() then + local variants, rest = inferrable_term:unwrap_enum_desc_cons() + local result_types = {} + local term_variants = string_typed_map() + for k, v in variants:pairs() do + local variant_type, variant_usages, variant_term = infer(v, typechecking_context) --TODO improve + term_variants:set(k, variant_term) + result_types[#result_types + 1] = variant_type + end + local result_type = result_types[1] + for i = 2, #result_types do + result_type = value.union_type(result_type, result_types[i]) + end + local _, rest_usages, rest_term = infer(rest, typechecking_context) --TODO improve + return value.enum_desc_type(result_type), rest_usages, typed_term.enum_desc_cons(term_variants, rest_term) + elseif inferrable_term:is_enum_type() then + local desc = inferrable_term:unwrap_enum_type() + local desc_type, desc_usages, desc_term = infer(desc, typechecking_context) + local univ_var = typechecker_state:metavariable(typechecking_context, false):as_value() + typechecker_state:flow( + desc_type, + typechecking_context, + value.enum_desc_type(univ_var), + typechecking_context, + "tuple type construction" + ) + 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 local methods = inferrable_term:unwrap_object_cons() local type_data = terms.empty @@ -2541,13 +2593,17 @@ function evaluate(typed_term, runtime_context) local desc = typed_term:unwrap_enum_type() local desc_val = evaluate(desc, runtime_context) return value.enum_type(desc_val) + elseif typed_term:is_enum_desc_type() then + local universe_term = typed_term:unwrap_enum_desc_type() + local universe = evaluate(universe_term, runtime_context) + return terms.value.enum_desc_type(universe) elseif typed_term:is_enum_case() then local target, variants, default = typed_term:unwrap_enum_case() local target_val = evaluate(target, runtime_context) if target_val:is_enum_value() then local variant, arg = target_val:unwrap_enum_value() - if variants[variant] then - return evaluate(variants[variant], runtime_context:append(arg)) + if variants:get(variant) then + return evaluate(variants:get(variant), runtime_context:append(arg)) else return evaluate(default, runtime_context:append(target_val)) end diff --git a/metalanguage.lua b/metalanguage.lua index 58c59fd..6aa9a6e 100644 --- a/metalanguage.lua +++ b/metalanguage.lua @@ -412,6 +412,7 @@ end ---@class ConstructedSyntax ---@field accepters AccepterSet ---@field start_anchor Anchor +---@field end_anchor Anchor local ConstructedSyntax = {} --[[ diff --git a/prelude.alc b/prelude.alc index fa6ca7f..bc894a3 100644 --- a/prelude.alc +++ b/prelude.alc @@ -1282,8 +1282,8 @@ let host-matcher-reducible = lambda ( let accept-handler-type = reducible-handler-type(userdata, result2, result) let accept-handler-desc = tuple-desc-singleton(host-type, accept-handler-type) - let red-param-desc = tuple-desc-concat(host-type, accept-handler-desc, storage) - let red-result-desc = tuple-desc-singleton(host-type, host-matcher(userdata, result)) + # let red-param-desc = tuple-desc-concat(host-type, accept-handler-desc, storage) + # let red-result-desc = tuple-desc-singleton(host-type, host-matcher(userdata, result)) let accept-handler-tuple = host-tuple-of(host-type, accept-handler-desc)(accept-handler) let red-param = host-tuple-concat(host-type, accept-handler-desc, storage, accept-handler-tuple, s) @@ -1303,8 +1303,8 @@ let host-matcher-reducible = lambda ( accept-handler : reducible-handler-type(userdata, result2, result)) let accept-handler-type = reducible-handler-type(userdata, result2, result) let accept-handler-desc = tuple-desc-singleton(host-type, accept-handler-type) - let red-param-desc = tuple-desc-concat(host-type, accept-handler-desc, storage) - let red-result-desc = tuple-desc-singleton(host-type, host-matcher(userdata, result)) + # let red-param-desc = tuple-desc-concat(host-type, accept-handler-desc, storage) + # let red-result-desc = tuple-desc-singleton(host-type, host-matcher(userdata, result)) let accept-handler-tuple = host-tuple-of(host-type, accept-handler-desc)(accept-handler) let red-param = host-tuple-concat(host-type, accept-handler-desc, storage, accept-handler-tuple, s) @@ -1636,40 +1636,40 @@ let do = into-operative(host-unit, host-nil, do-impl) ## tuple-desc operative -let tupleof-ascribed-names-reducer-thread-type = new-host-type(new-host-unique-id("tupleof-ascribed-names-reducer-thread")) -let tupleof-ascribed-names-reducer-thread-type-get-names = intrinsic +let ascribed-segment-tuple-desc-reducer-thread-type = new-host-type(new-host-unique-id("ascribed-segment-tuple-desc-reducer-thread")) +let ascribed-segment-tuple-desc-reducer-thread-type-get-names = intrinsic """" local function get_names(thread) return thread.names end return get_names : - host-func-type ((thread : tupleof-ascribed-names-reducer-thread-type)) -> ((names : terms-gen-array)) -let tupleof-ascribed-names-reducer-thread-type-get-args = intrinsic + host-func-type ((thread : ascribed-segment-tuple-desc-reducer-thread-type)) -> ((names : terms-gen-array)) +let ascribed-segment-tuple-desc-reducer-thread-type-get-args = intrinsic """" local function get_args(thread) return thread.args end return get_args : - host-func-type ((thread : tupleof-ascribed-names-reducer-thread-type)) -> ((args : host-inferrable-term)) -let tupleof-ascribed-names-reducer-thread-type-get-env = intrinsic + host-func-type ((thread : ascribed-segment-tuple-desc-reducer-thread-type)) -> ((args : host-inferrable-term)) +let ascribed-segment-tuple-desc-reducer-thread-type-get-env = intrinsic """" local function get_env(thread) return thread.env end return get_env : - host-func-type ((thread : tupleof-ascribed-names-reducer-thread-type)) -> ((env : host-environment)) + host-func-type ((thread : ascribed-segment-tuple-desc-reducer-thread-type)) -> ((env : host-environment)) -let tupleof-ascribed-names-reducer-storage-desc = tuple-desc-singleton(host-type, host-environment) +let ascribed-segment-tuple-desc-reducer-storage-desc = tuple-desc-singleton(host-type, host-environment) -let tupleof-ascribed-names-reducer-result2-desc = tuple-desc-singleton(host-type, tupleof-ascribed-names-reducer-thread-type) +let ascribed-segment-tuple-desc-reducer-result2-desc = tuple-desc-singleton(host-type, ascribed-segment-tuple-desc-reducer-thread-type) -let tupleof-ascribed-names-match-result-desc = - # read as: (ok : host-bool, _ : host-if(ok, tupleof-ascribed-names-reducer-thread-type, host-lua-error)) +let ascribed-segment-tuple-desc-match-result-desc = + # read as: (ok : host-bool, _ : host-if(ok, ascribed-segment-tuple-desc-reducer-thread-type, host-lua-error)) # or, more logically: (ok : host-bool, ...) where: - # - ok == true: `...` is tupleof-ascribed-names-reducer-thread-type + # - ok == true: `...` is ascribed-segment-tuple-desc-reducer-thread-type # - ok == false: `...` is host-lua-error # technically this should have a third element in the ok == true case, containing host-syntax # but the syntax will always be nil, and the errors are annoying @@ -1679,32 +1679,32 @@ let tupleof-ascribed-names-match-result-desc = lambda () host-bool lambda (ok : host-bool) - host-if(ok, tupleof-ascribed-names-reducer-thread-type, host-lua-error) + host-if(ok, ascribed-segment-tuple-desc-reducer-thread-type, host-lua-error) -# FIXME: tupleof_ascribed_names_inner can only produce tuple descs in star-0 -let tupleof-ascribed-names-reducer = intrinsic "return base_env.tupleof_ascribed_names_inner" : - reducer-type(tupleof-ascribed-names-reducer-storage-desc, tupleof-ascribed-names-reducer-result2-desc) +# FIXME: ascribed_segment_tuple_desc can only produce tuple descs in star-0 +let ascribed-segment-tuple-desc-reducer = intrinsic "return base_env.ascribed_segment_tuple_desc" : + reducer-type(ascribed-segment-tuple-desc-reducer-storage-desc, ascribed-segment-tuple-desc-reducer-result2-desc) -let tupleof-ascribed-names-match-accept-handler = intrinsic "return metalanguage.accept_handler" : - reducible-handler-type(host-unit, tupleof-ascribed-names-reducer-result2-desc, tupleof-ascribed-names-match-result-desc) -let tupleof-ascribed-names-match-failure-handler = intrinsic "return metalanguage.failure_handler" : - failure-handler-type(host-unit, tupleof-ascribed-names-match-result-desc) +let ascribed-segment-tuple-desc-match-accept-handler = intrinsic "return metalanguage.accept_handler" : + reducible-handler-type(host-unit, ascribed-segment-tuple-desc-reducer-result2-desc, ascribed-segment-tuple-desc-match-result-desc) +let ascribed-segment-tuple-desc-match-failure-handler = intrinsic "return metalanguage.failure_handler" : + failure-handler-type(host-unit, ascribed-segment-tuple-desc-match-result-desc) let tuple-desc-impl-type = operative-handler-type(host-unit) let tuple-desc-impl = lambda (syn : host-syntax, env : host-environment, ud : host-unit, goal : host-goal) - let s = host-tuple-of(host-type, tupleof-ascribed-names-reducer-storage-desc)(env) + let s = host-tuple-of(host-type, ascribed-segment-tuple-desc-reducer-storage-desc)(env) - let matcher-t = host-matcher(host-unit, tupleof-ascribed-names-match-result-desc) + let matcher-t = host-matcher(host-unit, ascribed-segment-tuple-desc-match-result-desc) let matcher = host-matcher-reducible host-unit - tupleof-ascribed-names-reducer-storage-desc - tupleof-ascribed-names-reducer-result2-desc - tupleof-ascribed-names-match-result-desc - tupleof-ascribed-names-reducer + ascribed-segment-tuple-desc-reducer-storage-desc + ascribed-segment-tuple-desc-reducer-result2-desc + ascribed-segment-tuple-desc-match-result-desc + ascribed-segment-tuple-desc-reducer s - tupleof-ascribed-names-match-accept-handler + ascribed-segment-tuple-desc-match-accept-handler let matchers = host-array-set @@ -1715,23 +1715,25 @@ let tuple-desc-impl = lambda (syn : host-syntax, env : host-environment, ud : ho let (ok, thread) = match-syntax host-unit - tupleof-ascribed-names-match-result-desc + ascribed-segment-tuple-desc-match-result-desc matchers - tupleof-ascribed-names-match-failure-handler + ascribed-segment-tuple-desc-match-failure-handler syn host-nil - let thread = error-filter(tupleof-ascribed-names-reducer-thread-type, host-lua-error, ok, thread) + let thread = error-filter(ascribed-segment-tuple-desc-reducer-thread-type, host-lua-error, ok, thread) - let (args) = tupleof-ascribed-names-reducer-thread-type-get-args(thread) - let (env) = tupleof-ascribed-names-reducer-thread-type-get-env(thread) + let (args) = ascribed-segment-tuple-desc-reducer-thread-type-get-args(thread) + let (env) = ascribed-segment-tuple-desc-reducer-thread-type-get-env(thread) let (args) = goalify-inferrable(goal, args) tuple-of(host-type, operative-result-desc(goal))(args, env) -#let (tuple-desc-op-type, tuple-desc-op) = new-operative(host-unit, host-nil, tuple-desc-impl) -let tuple-desc-op = into-operative(host-unit, host-nil, tuple-desc-impl) +#let (tuple-desc-op-type, tuple-desc) = new-operative(host-unit, host-nil, tuple-desc-impl) +let tuple-desc = into-operative(host-unit, host-nil, tuple-desc-impl) +# tuple-desc for single-element tuples currently require an extra pair of parens, like lambdas used to. +# This should eventually be fixed the same way lambdas were fixed. let terms-gen-map = new-host-type(new-host-unique-id("terms-gen-map")) @@ -1776,3 +1778,11 @@ let listtail-reducer = # aa # aa # a + +let host-arith-binop = (host-func-type (a : host-number, b : host-number) -> ((c : host-number))) +let host-mul = (intrinsic "return function(a, b) return a * b end" : host-arith-binop) +let mul = lambda (a : host-number, b : host-number) + let (c) = host-mul(a, b) + c +let _*_ = mul + diff --git a/terms.lua b/terms.lua index e7e002d..905520a 100644 --- a/terms.lua +++ b/terms.lua @@ -391,6 +391,10 @@ inferrable_term:define_enum("inferrable", { "constructor", gen.builtin_string, "arg", inferrable_term, } }, + { "enum_desc_cons", { + "variants", map(gen.builtin_string, inferrable_term), + "rest", inferrable_term, +} }, { "enum_elim", { "subject", inferrable_term, "mechanism", inferrable_term, @@ -405,6 +409,7 @@ inferrable_term:define_enum("inferrable", { "target", inferrable_term, "debug", gen.builtin_string, } }, + { "object_cons", { "methods", map(gen.builtin_string, inferrable_term) } }, { "object_elim", { "subject", inferrable_term, @@ -639,6 +644,9 @@ typed_term:define_enum("typed", { "variants", map(gen.builtin_string, typed_term), "rest", typed_term, } }, + { "enum_desc_type", { + "univ", typed_term + } }, { "enum_type", { "desc", typed_term } }, { "enum_case", { "target", typed_term, diff --git a/testlist.json b/testlist.json index 7ef7f84..b7e0447 100644 --- a/testlist.json +++ b/testlist.json @@ -12,5 +12,7 @@ "tests/implicit.alc": "success", "tests/operative-do.alc": "success", "tests/operative-tuple-desc.alc": "success", + "tests/switch-fail.alc": "termgen", + "tests/switch-test.alc": "success", "tests/tuples.alc": "success" } \ No newline at end of file diff --git a/tests/arith.alc b/tests/arith.alc index 9d8d841..e5caee3 100644 --- a/tests/arith.alc +++ b/tests/arith.alc @@ -1,4 +1,3 @@ -let host-arith-binop = (host-func-type (a : host-number, b : host-number) -> ((c : host-number))) let host-sub = (intrinsic "return function(a, b) return a - b end" : host-arith-binop) #let host-sub = (intrinsic "return function(a, b) return a - b end" : (host-func-type (a : host-number, b : host-number) -> ((c : host-number)))) @@ -6,12 +5,6 @@ let host-sub = (intrinsic "return function(a, b) return a - b end" : host-arith- #let foo = (record (bar = 5) (baz = 6)) #let subbed = host-sub foo.bar y -let host-mul = (intrinsic "return function(a, b) return a * b end" : host-arith-binop) -let mul = lambda (a : host-number, b : host-number) - let (c) = host-mul(a, b) - c -let _*_ = mul - let sqr = lambda (x) x * x sqr 6 diff --git a/tests/bad-types.alc b/tests/bad-types.alc index fec3da3..5a3aefa 100644 --- a/tests/bad-types.alc +++ b/tests/bad-types.alc @@ -1,8 +1,3 @@ -let host-mul = (intrinsic "return function(a, b) return a * b end" : host-arith-binop) -let mul = lambda (a : host-number, b : host-number) - let (c) = host-mul(a, b) - c -let _*_ = mul # FIXME: this super duper should be failing let sqr_overcomplicated = lambda_annotated (t, x : t) : host-string diff --git a/tests/basic-annotated.alc b/tests/basic-annotated.alc index 229ff7c..7d9cc1d 100644 --- a/tests/basic-annotated.alc +++ b/tests/basic-annotated.alc @@ -1,11 +1,3 @@ -let host-arith-binop = (host-func-type (a : host-number, b : host-number) -> ((c : host-number))) - let host-string-wrap = intrinsic "return terms.value.host_string_type" : wrapped(host-type) let host-string = unwrap(host-string-wrap) - -let host-mul = (intrinsic "return function(a, b) return a * b end" : host-arith-binop) -let mul = lambda (a : host-number, b : host-number) - let (c) = host-mul(a, b) - c -let _*_ = mul diff --git a/tests/implicit.alc b/tests/implicit.alc index 624efc9..170ab93 100644 --- a/tests/implicit.alc +++ b/tests/implicit.alc @@ -2,10 +2,10 @@ let id = lambda_implicit (T : type_(10, 0)) lambda (x : T) x -# TODO: test this when tuple-desc-op can do more than just star-0 +# TODO: test this when tuple-desc can do more than just star-0 #let point = lambda_implicit (U : type_(10)) # lambda (T : U) -# tuple-type(tuple-desc-op(x : T, y : T)) +# tuple-type(tuple-desc(x : T, y : T)) # #let mkpoint = lambda_implicit (U : type_(10), T : U) # lambda (x : T, y : T) diff --git a/tests/operative-tuple-desc.alc b/tests/operative-tuple-desc.alc index dc7ab88..a5e4e31 100644 --- a/tests/operative-tuple-desc.alc +++ b/tests/operative-tuple-desc.alc @@ -1,3 +1,12 @@ -let my-tuple-desc = tuple-desc-op(x : host-number, y : host-number) +let my-tuple-desc = tuple-desc(x : host-number, y : host-number) let my-tuple-type = tuple-type-explicit(type_(0, 0), my-tuple-desc) -my-tuple-type + +the my-tuple-type tuple-of-implicit(3, 4) + +let symbol-exact = + intrinsic "return metalanguage.symbol_exact" : + reducer-type(tuple-desc(s : host-string), tuple-desc()) + +let inferrable-enum-cons = + intrinsic "return terms.inferrable_term.enum_cons" : + host-func-type (name : host-string, arg : host-inferrable-term) -> ((res : host-inferrable-term)) diff --git a/tests/switch-fail.alc b/tests/switch-fail.alc new file mode 100644 index 0000000..91b1933 --- /dev/null +++ b/tests/switch-fail.alc @@ -0,0 +1,12 @@ +let Result = lambda (T, E) + enum + Ok(x : T) + Err(e : E) + +let switchtest_ascribed = lambda (x : Result(host-number, host-number)) + switch x + Ok(x) -> x + Err(a) -> -1 + +switchtest_ascribed(mk Ok(5)) +switchtest_ascribed(mk Er(3)) \ No newline at end of file diff --git a/tests/switch-test.alc b/tests/switch-test.alc new file mode 100644 index 0000000..be208c9 --- /dev/null +++ b/tests/switch-test.alc @@ -0,0 +1,29 @@ +let sqr = lambda (x) + x * x + +let switchtest = lambda (x) + switch x + none -> 2 + inj1(a) -> sqr(a) + inj2(a, b) -> sqr(a) * b + +tuple-of-implicit + switchtest(mk none) + switchtest(mk inj1 5) + switchtest(mk inj2 3 5) + switchtest(mk inj2(3, 5)) + switchtest(mk inj2 sqr(2) 5) + +let Result = lambda (T, E) + enum + Ok(x : T) + Err(e : E) + +let switchtest_ascribed = lambda (x : Result(host-number, host-number)) + switch x + Ok(x) -> x * x + Err(a) -> a + +switchtest_ascribed(mk Ok(5)) +switchtest_ascribed(mk Err(3)) + \ No newline at end of file diff --git a/types/inferrable.lua b/types/inferrable.lua index 5df80f1..e165660 100644 --- a/types/inferrable.lua +++ b/types/inferrable.lua @@ -71,6 +71,12 @@ function inferrable:unwrap_enum_cons() end ---@return boolean, string, inferrable function inferrable:as_enum_cons() end ---@return boolean +function inferrable:is_enum_desc_cons() end +---@return MapValue, inferrable +function inferrable:unwrap_enum_desc_cons() end +---@return boolean, MapValue, inferrable +function inferrable:as_enum_desc_cons() end +---@return boolean function inferrable:is_enum_elim() end ---@return inferrable, inferrable function inferrable:unwrap_enum_elim() end @@ -83,6 +89,12 @@ function inferrable:unwrap_enum_type() end ---@return boolean, inferrable function inferrable:as_enum_type() end ---@return boolean +function inferrable:is_enum_desc_cons() end +---@return MapValue, inferrable +function inferrable:unwrap_enum_desc_cons() end +---@return boolean, MapValue, inferrable +function inferrable:as_enum_desc_cons() end +---@return boolean function inferrable:is_enum_case() end ---@return inferrable, MapValue function inferrable:unwrap_enum_case() end @@ -258,8 +270,10 @@ function inferrable:as_program_type() end ---@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_desc_cons fun(variants: MapValue, rest: inferrable): inferrable ---@field enum_elim fun(subject: inferrable, mechanism: inferrable): inferrable ---@field enum_type fun(desc: inferrable): inferrable +---@field enum_desc_cons fun(variants: MapValue, rest: inferrable): inferrable ---@field enum_case fun(target: inferrable, variants: MapValue): inferrable ---@field enum_absurd fun(target: inferrable, debug: string): inferrable ---@field object_cons fun(methods: MapValue): inferrable diff --git a/types/typed.lua b/types/typed.lua index a7a0b80..1135777 100644 --- a/types/typed.lua +++ b/types/typed.lua @@ -149,6 +149,12 @@ function typed:unwrap_enum_desc_cons() end ---@return boolean, MapValue, typed function typed:as_enum_desc_cons() end ---@return boolean +function typed:is_enum_desc_type() end +---@return typed +function typed:unwrap_enum_desc_type() end +---@return boolean, typed +function typed:as_enum_desc_type() end +---@return boolean function typed:is_enum_type() end ---@return typed function typed:unwrap_enum_type() end @@ -391,6 +397,7 @@ function typed:as_constrained_type() end ---@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 +---@field enum_desc_type fun(univ: typed): typed ---@field enum_type fun(desc: typed): typed ---@field enum_case fun(target: typed, variants: MapValue, default: typed): typed ---@field enum_absurd fun(target: typed, debug: string): typed