From ec3ddf121a11b54e6f390aa567fe1b0ff9b53e98 Mon Sep 17 00:00:00 2001 From: Jesin Date: Mon, 7 Oct 2024 01:58:12 -0700 Subject: [PATCH 01/25] comment out some unused locals --- testfile.alc | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/testfile.alc b/testfile.alc index 23c84ec8..261a1736 100644 --- a/testfile.alc +++ b/testfile.alc @@ -1062,8 +1062,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) @@ -1083,8 +1083,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) From ff6e09cd277fb078d4f20c4e76a0c474deb874e9 Mon Sep 17 00:00:00 2001 From: Jesin Date: Tue, 8 Oct 2024 02:17:30 -0700 Subject: [PATCH 02/25] fix variance annotations --- testfile.alc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/testfile.alc b/testfile.alc index 261a1736..ef7fa6df 100644 --- a/testfile.alc +++ b/testfile.alc @@ -1022,7 +1022,7 @@ let host-matcher-is-value = lambda (userdata : host-type, result : tuple-desc-ty let reducer-type = new-host-type-family new-host-unique-id("host-reducer") forall (storage : tuple-desc-type(host-type), result2 : tuple-desc-type(host-type)) -> (T : host-type) - tuple-of-implicit covariant(tuple-desc-relation) contravariant(tuple-desc-relation) + tuple-of-implicit contravariant(tuple-desc-relation) covariant(tuple-desc-relation) let reducible-handler-type = lambda (userdata : host-type, result2 : tuple-desc-type(host-type), result : tuple-desc-type(host-type)) # prepend userdata to result2 From 9f3910883307287620207f9523935a75aa32f557 Mon Sep 17 00:00:00 2001 From: Jesin Date: Tue, 8 Oct 2024 02:28:51 -0700 Subject: [PATCH 03/25] rename tuple-desc-op to tuple-desc --- testfile.alc | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/testfile.alc b/testfile.alc index ef7fa6df..145ea5ca 100644 --- a/testfile.alc +++ b/testfile.alc @@ -1512,10 +1512,10 @@ let tuple-desc-impl = lambda (syn : host-syntax, env : host-environment, ud : ho 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) -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 @@ -1576,10 +1576,10 @@ let id = lambda_implicit (T : type_(10, 0)) 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) From b3ba09a59225b30848f9f9e3c82b89c75117f0ee Mon Sep 17 00:00:00 2001 From: Jesin Date: Wed, 16 Oct 2024 13:47:24 -0700 Subject: [PATCH 04/25] Create enum-constructor operative named mk --- base-env.lua | 33 ++++++++++++++++++++++++++++++++- testfile.alc | 29 ++++++++++++++++------------- 2 files changed, 48 insertions(+), 14 deletions(-) diff --git a/base-env.lua b/base-env.lua index e78e985e..0ab1ed6e 100644 --- a/base-env.lua +++ b/base-env.lua @@ -88,6 +88,36 @@ local function let_bind(syntax, env) env end +local mk_inner = metalanguage.reducer(function(syntax, env) + local ok, name, tail = syntax:match({ + metalanguage.listtail(metalanguage.accept_handler, metalanguage.issymbol(metalanguage.accept_handler)), + }, metalanguage.failure_handler, nil) + if not ok then + return ok, name + end + 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, tuple), env } +end, "mk_inner") + +---@type lua_operative +local function mk(syntax, env) + local inner_matcher = mk_inner(metalanguage.accept_handler, env) + local ok, rest = syntax:match({ + inner_matcher, + metalanguage.listtail(metalanguage.accept_handler, inner_matcher), + }, metalanguage.failure_handler, nil) + if not ok then + return ok, rest + end + return ok, table.unpack(rest) +end + ---@param _ any ---@param name string ---@param exprenv { val:inferrable, env:Environment } @@ -1464,7 +1494,8 @@ local core_operations = { --["do"] = evaluator.host_operative(do_block), let = exprs.host_operative(let_bind, "let_bind"), - record = exprs.host_operative(record_build, "record_build"), + mk = exprs.host_operative(mk, "mk"), + --record = exprs.host_operative(record_build, "record_build"), intrinsic = exprs.host_operative(intrinsic, "intrinsic"), ["host-number"] = lit_term(value.host_number_type, value.host_type_type), ["host-type"] = lit_term(value.host_type_type, value.star(1, 1)), diff --git a/testfile.alc b/testfile.alc index 145ea5ca..ebabc52f 100644 --- a/testfile.alc +++ b/testfile.alc @@ -1514,10 +1514,20 @@ let tuple-desc-impl = lambda (syn : host-syntax, env : host-environment, ud : ho #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 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)) let host-if-2-type = forall ( result : host-type, @@ -1613,17 +1623,6 @@ y let terms-gen-map = new-host-type(new-host-unique-id("terms-gen-map")) -let listtail-accepter-result = lambda (( result : tuple-desc-type(host-type) )) - tuple-desc-concat(host-type, result, tuple-desc-singleton(host-type, host-syntax)) - -let listtail-reducer = - lambda_implicit ( userdata : host-type ) - lambda_implicit ( result : tuple-desc-type(host-type) ) - lambda (( matcher : host-matcher(userdata, result) )) - intrinsic "return metalanguage.listtail" : - reducer-type((tuple-desc-empty host-type), result) - - #### # ---@alias URect userdata let URect = new-host-type(new-host-unique-id("URect")) @@ -1886,4 +1885,8 @@ sqr 6 # FIXME: this super duper should be failing let sqr_overcomplicated = lambda_annotated (t, x : t) : host-string x * x -sqr_overcomplicated(host-number, 6) +tuple-of-implicit + mk None + mk None() + mk inj1 6 sqr(6) + mk inj2(7, sqr(7)) From 627ec4ba720f3c720c10fa16ef7c7b060f2ea73a Mon Sep 17 00:00:00 2001 From: Jesin Date: Sun, 3 Nov 2024 23:49:08 -0800 Subject: [PATCH 05/25] use a slightly nicer accept handler --- base-env.lua | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/base-env.lua b/base-env.lua index 0ab1ed6e..a7040a2d 100644 --- a/base-env.lua +++ b/base-env.lua @@ -102,12 +102,12 @@ local mk_inner = metalanguage.reducer(function(syntax, env) if not ok then return ok, tuple end - return ok, { terms.inferrable_term.enum_cons(name, tuple), env } + return ok, terms.inferrable_term.enum_cons(name, tuple), env end, "mk_inner") ---@type lua_operative local function mk(syntax, env) - local inner_matcher = mk_inner(metalanguage.accept_handler, env) + local inner_matcher = mk_inner(utils.accept_bundled, env) local ok, rest = syntax:match({ inner_matcher, metalanguage.listtail(metalanguage.accept_handler, inner_matcher), From e75472282c8ab49ea4554139316a36234bc9af35 Mon Sep 17 00:00:00 2001 From: Jesin Date: Fri, 8 Nov 2024 05:31:36 -0800 Subject: [PATCH 06/25] switch statement (not working) --- base-env.lua | 67 ++++++++++++++++++++++++++++++++++++++++++++++++++++ testfile.alc | 15 ++++++++---- 2 files changed, 78 insertions(+), 4 deletions(-) diff --git a/base-env.lua b/base-env.lua index a7040a2d..b02871b7 100644 --- a/base-env.lua +++ b/base-env.lua @@ -118,6 +118,72 @@ local function mk(syntax, env) return ok, table.unpack(rest) end +---@param env Environment +local switch_case = metalanguage.reducer(function(syntax, env) + local ok, tag + ok, tag, syntax = syntax:match({ + 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, "->") + ), + }, metalanguage.failure_handler, nil) + if not ok then + return ok, tag + end + local names = gen.declare_array(gen.builtin_string)(table.unpack(tag, 2)) + tag = tag[1] + local singleton_contents + ok, singleton_contents = syntax:match({ + metalanguage.listmatch(metalanguage.accept_handler, metalanguage.any(metalanguage.accept_handler)), + }, metalanguage.failure_handler, nil) + if ok then + syntax = singleton_contents + end + 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() + 1)) + ) + ok, term, env = syntax: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) + return ok, tag, term, env +end, "switch_case") + +---@type lua_operative +local function switch(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:match({ + metalanguage.listtail(metalanguage.accept_handler, switch_case(utils.accept_bundled, env)), + }, metalanguage.failure_handler, nil) + if not ok then + return ok, tag + end + tag, term, env = table.unpack(tag) + variants:set(tag, term) + end + return true, terms.inferrable_term.enum_case(subj, variants), env +end + ---@param _ any ---@param name string ---@param exprenv { val:inferrable, env:Environment } @@ -1495,6 +1561,7 @@ local core_operations = { --["do"] = evaluator.host_operative(do_block), let = exprs.host_operative(let_bind, "let_bind"), mk = exprs.host_operative(mk, "mk"), + switch = exprs.host_operative(switch, "switch"), --record = exprs.host_operative(record_build, "record_build"), intrinsic = exprs.host_operative(intrinsic, "intrinsic"), ["host-number"] = lit_term(value.host_number_type, value.host_type_type), diff --git a/testfile.alc b/testfile.alc index ebabc52f..af690ec6 100644 --- a/testfile.alc +++ b/testfile.alc @@ -1885,8 +1885,15 @@ sqr 6 # FIXME: this super duper should be failing let sqr_overcomplicated = lambda_annotated (t, x : t) : host-string x * x +sqr_overcomplicated(host-number, 6) + +let switchtest = lambda (x) + switch x + none -> 2 + inj1(a) -> sqr(a) + inj2(a, b) -> sqr(a) + b + tuple-of-implicit - mk None - mk None() - mk inj1 6 sqr(6) - mk inj2(7, sqr(7)) + switchtest(mk none) + switchtest(mk inj1 5) + switchtest(mk inj2 6 4) From 4ac976b8d780d2aa93dec88264d3a4c8d0a049cd Mon Sep 17 00:00:00 2001 From: Jesin Date: Tue, 12 Nov 2024 01:04:58 -0800 Subject: [PATCH 07/25] fix type annotation of TypecheckingContext:append --- terms.lua | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/terms.lua b/terms.lua index 200d9837..df6c5381 100644 --- a/terms.lua +++ b/terms.lua @@ -143,7 +143,7 @@ function TypecheckingContext:get_runtime_context() end ---@param name string ----@param type any +---@param type value ---@param val value? ---@param anchor Anchor? ---@return TypecheckingContext From fae0f3306e501308d6e9b61047027e470a7d110d Mon Sep 17 00:00:00 2001 From: Jesin Date: Tue, 12 Nov 2024 02:10:14 -0800 Subject: [PATCH 08/25] switch seems closer to correct but now hangs --- base-env.lua | 47 ++++++++++++++++++++++++++++++----------------- 1 file changed, 30 insertions(+), 17 deletions(-) diff --git a/base-env.lua b/base-env.lua index b02871b7..7f9551a6 100644 --- a/base-env.lua +++ b/base-env.lua @@ -118,38 +118,50 @@ local function mk(syntax, env) return ok, table.unpack(rest) 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 env Environment local switch_case = metalanguage.reducer(function(syntax, env) - local ok, tag - ok, tag, syntax = syntax:match({ - 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, "->") - ), - }, metalanguage.failure_handler, nil) + 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)(table.unpack(tag, 2)) tag = tag[1] + if not tag then + return false, "missing case tag" + end local singleton_contents - ok, singleton_contents = syntax:match({ + ok, singleton_contents = tail:match({ metalanguage.listmatch(metalanguage.accept_handler, metalanguage.any(metalanguage.accept_handler)), }, metalanguage.failure_handler, nil) if ok then - syntax = singleton_contents + tail = singleton_contents end + -- This should eventually be rewritten 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.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() + 1)) + terms.binding.tuple_elim(names, terms.inferrable_term.bound_variable(env.typechecking_context:len())) ) - ok, term, env = syntax:match({ + ok, term, env = tail:match({ exprs.inferred_expression(metalanguage.accept_handler, env), }, metalanguage.failure_handler, nil) if not ok then @@ -178,7 +190,8 @@ local function switch(syntax, env) if not ok then return ok, tag end - tag, term, env = table.unpack(tag) + -- This should eventually be rewritten to collect the branch envs and join them back together: + tag, term = table.unpack(tag) variants:set(tag, term) end return true, terms.inferrable_term.enum_case(subj, variants), env From d0042581b9e635b59d2f373643ff09bd4b4d0c38 Mon Sep 17 00:00:00 2001 From: Jesin Date: Tue, 12 Nov 2024 05:53:22 -0800 Subject: [PATCH 09/25] fix infinite loop in switch operative --- base-env.lua | 2 +- testfile.alc | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/base-env.lua b/base-env.lua index 7f9551a6..06c3bd51 100644 --- a/base-env.lua +++ b/base-env.lua @@ -184,7 +184,7 @@ local function switch(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:match({ + ok, tag, syntax = syntax:match({ metalanguage.listtail(metalanguage.accept_handler, switch_case(utils.accept_bundled, env)), }, metalanguage.failure_handler, nil) if not ok then diff --git a/testfile.alc b/testfile.alc index af690ec6..092a8efd 100644 --- a/testfile.alc +++ b/testfile.alc @@ -1891,9 +1891,9 @@ let switchtest = lambda (x) switch x none -> 2 inj1(a) -> sqr(a) - inj2(a, b) -> sqr(a) + b + inj2(a, b) -> sqr(a) * b tuple-of-implicit switchtest(mk none) switchtest(mk inj1 5) - switchtest(mk inj2 6 4) + switchtest(mk inj2 3 5) From 835758cdb1928c1b6fe6b5da0e4753f0ece69733 Mon Sep 17 00:00:00 2001 From: Jesin Date: Tue, 12 Nov 2024 06:01:25 -0800 Subject: [PATCH 10/25] use set method instead of disallowed index assignment --- evaluator.lua | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/evaluator.lua b/evaluator.lua index e7a608a0..c8d18714 100644 --- a/evaluator.lua +++ b/evaluator.lua @@ -1983,7 +1983,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, From d137eb49295f41fef8f6b4fe514f976994871f24 Mon Sep 17 00:00:00 2001 From: Jesin Date: Wed, 13 Nov 2024 05:28:28 -0800 Subject: [PATCH 11/25] feed typechecking_context:append the anchors it demands --- base-env.lua | 5 +++-- evaluator.lua | 3 ++- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/base-env.lua b/base-env.lua index 06c3bd51..abdd369f 100644 --- a/base-env.lua +++ b/base-env.lua @@ -147,7 +147,7 @@ local switch_case = metalanguage.reducer(function(syntax, env) if ok then tail = singleton_contents end - -- This should eventually be rewritten to use an environment-splitting operation: + --TODO rewrite this to use an environment-splitting operation env = environment.new_env(env, { typechecking_context = env.typechecking_context:append( "#switch-subj", @@ -168,6 +168,7 @@ local switch_case = metalanguage.reducer(function(syntax, env) return ok, term end env, term = env:exit_block(term, shadowed) + term.anchor = syntax.anchor --TODO figure out where to store/retrieve the anchors correctly return ok, tag, term, env end, "switch_case") @@ -190,7 +191,7 @@ local function switch(syntax, env) if not ok then return ok, tag end - -- This should eventually be rewritten to collect the branch envs and join them back together: + --TODO rewrite this to collect the branch envs and join them back together: tag, term = table.unpack(tag) variants:set(tag, term) end diff --git a/evaluator.lua b/evaluator.lua index c8d18714..13dee198 100644 --- a/evaluator.lua +++ b/evaluator.lua @@ -1995,8 +1995,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.anchor)) --TODO improve term_variants:set(k, variant_term) result_types[#result_types + 1] = variant_type end From 5a67298eefb6e888dbff10154f0bdd9f3a97efcb Mon Sep 17 00:00:00 2001 From: Jesin Date: Thu, 14 Nov 2024 02:26:51 -0800 Subject: [PATCH 12/25] using MapValue:get() instead of [] passes the test! --- evaluator.lua | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/evaluator.lua b/evaluator.lua index 13dee198..3f5da8c8 100644 --- a/evaluator.lua +++ b/evaluator.lua @@ -2510,8 +2510,8 @@ function evaluate(typed_term, runtime_context) 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 From 0fdbca03f8f67d44fc41384163581940e4c96673 Mon Sep 17 00:00:00 2001 From: AstroSnail Date: Sun, 17 Nov 2024 02:57:33 +0000 Subject: [PATCH 13/25] Refactor mk to match syntax variants before invoking collect_tuple makes expression errors inside mk easier to find --- base-env.lua | 27 ++++++++++----------------- testfile.alc | 2 ++ 2 files changed, 12 insertions(+), 17 deletions(-) diff --git a/base-env.lua b/base-env.lua index 67975a77..02bdf43c 100644 --- a/base-env.lua +++ b/base-env.lua @@ -88,13 +88,19 @@ local function let_bind(syntax, env) env end -local mk_inner = metalanguage.reducer(function(syntax, env) - local ok, name, tail = syntax:match({ - metalanguage.listtail(metalanguage.accept_handler, metalanguage.issymbol(metalanguage.accept_handler)), +---@type lua_operative +local function mk(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, name + 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)), @@ -103,19 +109,6 @@ local mk_inner = metalanguage.reducer(function(syntax, env) return ok, tuple end return ok, terms.inferrable_term.enum_cons(name, tuple), env -end, "mk_inner") - ----@type lua_operative -local function mk(syntax, env) - local inner_matcher = mk_inner(utils.accept_bundled, env) - local ok, rest = syntax:match({ - inner_matcher, - metalanguage.listtail(metalanguage.accept_handler, inner_matcher), - }, metalanguage.failure_handler, nil) - if not ok then - return ok, rest - end - return ok, table.unpack(rest) end ---@type Matcher diff --git a/testfile.alc b/testfile.alc index 4469cd30..b3115548 100644 --- a/testfile.alc +++ b/testfile.alc @@ -1896,3 +1896,5 @@ 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) From 33f01fb7411e514579ce868e929bdc5dad93120d Mon Sep 17 00:00:00 2001 From: Jesin Date: Wed, 20 Nov 2024 18:45:58 -0800 Subject: [PATCH 14/25] Unify lua_operative naming conventions --- base-env.lua | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/base-env.lua b/base-env.lua index 02bdf43c..08d0e542 100644 --- a/base-env.lua +++ b/base-env.lua @@ -30,7 +30,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 +67,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 type(name) == "table" then @@ -89,7 +89,7 @@ local function let_bind(syntax, env) end ---@type lua_operative -local function mk(syntax, env) +local function mk_impl(syntax, env) local ok, bun = syntax:match({ metalanguage.listmatch( metalanguage.accept_handler, @@ -166,7 +166,7 @@ local switch_case = metalanguage.reducer(function(syntax, env) end, "switch_case") ---@type lua_operative -local function switch(syntax, env) +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)), @@ -229,7 +229,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, @@ -1566,11 +1566,11 @@ 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"), - mk = exprs.host_operative(mk, "mk"), - switch = exprs.host_operative(switch, "switch"), + let = exprs.host_operative(let_impl, "let_impl"), + mk = exprs.host_operative(mk_impl, "mk_impl"), + switch = exprs.host_operative(switch_impl, "switch_impl"), --record = exprs.host_operative(record_build, "record_build"), - intrinsic = exprs.host_operative(intrinsic, "intrinsic"), + 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"), From 3b68272d463c21b86139be699c52ddbb7fe12eb9 Mon Sep 17 00:00:00 2001 From: Jesin Date: Tue, 26 Nov 2024 18:14:52 -0800 Subject: [PATCH 15/25] use start_anchor and (sometimes) end_anchor per #126 --- base-env.lua | 7 ++++--- evaluator.lua | 2 +- metalanguage.lua | 1 + 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/base-env.lua b/base-env.lua index a11bb033..0bd8c951 100644 --- a/base-env.lua +++ b/base-env.lua @@ -146,7 +146,7 @@ local switch_case = metalanguage.reducer(function(syntax, env) "#switch-subj", evaluator.typechecker_state:metavariable(env.typechecking_context):as_value(), nil, - syntax.anchor + syntax.start_anchor ), }) local shadowed, term @@ -161,7 +161,8 @@ local switch_case = metalanguage.reducer(function(syntax, env) return ok, term end env, term = env:exit_block(term, shadowed) - term.anchor = syntax.anchor --TODO figure out where to store/retrieve the anchors correctly + 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") @@ -1181,7 +1182,7 @@ local function lambda_annotated_impl(syntax, env) terms.binding.annotated_lambda( "#lambda-arguments", args, - syntax.anchor, + syntax.start_anchor, terms.visibility.explicit, literal_purity_pure ) diff --git a/evaluator.lua b/evaluator.lua index 319487fc..ce0341a0 100644 --- a/evaluator.lua +++ b/evaluator.lua @@ -2012,7 +2012,7 @@ function infer( 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, v.anchor)) --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 diff --git a/metalanguage.lua b/metalanguage.lua index c2c006d8..55263e36 100644 --- a/metalanguage.lua +++ b/metalanguage.lua @@ -407,6 +407,7 @@ end ---@class ConstructedSyntax ---@field accepters AccepterSet ---@field start_anchor Anchor +---@field end_anchor Anchor local ConstructedSyntax = {} --[[ From 7b28381c8d27215874d480264acc1fa4937aab5f Mon Sep 17 00:00:00 2001 From: Erik McClure Date: Fri, 3 Jan 2025 08:38:56 -0800 Subject: [PATCH 16/25] Apply .str refactor and move test to own file --- base-env.lua | 19 ++++++++++++++++--- prelude.alc | 18 ++++++------------ testlist.json | 1 + tests/arith.alc | 7 ------- tests/bad-types.alc | 5 ----- tests/basic-annotated.alc | 8 -------- tests/implicit.alc | 4 ++-- tests/operative-tuple-desc.alc | 13 +++++++++++-- tests/switch-test.alc | 15 +++++++++++++++ 9 files changed, 51 insertions(+), 39 deletions(-) create mode 100644 tests/switch-test.alc diff --git a/base-env.lua b/base-env.lua index 2537b0bc..d3c56afa 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 @@ -115,7 +116,7 @@ local function mk_impl(syntax, env) if not ok then return ok, tuple end - return ok, terms.inferrable_term.enum_cons(name, tuple), env + return ok, terms.inferrable_term.enum_cons(name.str, tuple), env end ---@type Matcher @@ -129,14 +130,26 @@ 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 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)(table.unpack(tag, 2)) + + 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 @@ -194,7 +207,7 @@ 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, term) + variants:set(tag.str, term) end return true, terms.inferrable_term.enum_case(subj, variants), env end diff --git a/prelude.alc b/prelude.alc index 8a3a4ad0..932582b1 100644 --- a/prelude.alc +++ b/prelude.alc @@ -1779,15 +1779,9 @@ let listtail-reducer = # aa # a -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 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/testlist.json b/testlist.json index 7ef7f848..c0e250e8 100644 --- a/testlist.json +++ b/testlist.json @@ -12,5 +12,6 @@ "tests/implicit.alc": "success", "tests/operative-do.alc": "success", "tests/operative-tuple-desc.alc": "success", + "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 9d8d8410..e5caee3a 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 fec3da3c..5a3aefa3 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 229ff7c9..7d9cc1db 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 624efc91..170ab938 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 dc7ab88e..52c80b62 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)) \ No newline at end of file diff --git a/tests/switch-test.alc b/tests/switch-test.alc new file mode 100644 index 00000000..72a56ca3 --- /dev/null +++ b/tests/switch-test.alc @@ -0,0 +1,15 @@ +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) From 07fe82512d48b2be5f142ffd2167d687e7f4d637 Mon Sep 17 00:00:00 2001 From: Erik McClure Date: Sat, 4 Jan 2025 05:11:13 -0800 Subject: [PATCH 17/25] Make enums almost work --- base-env.lua | 51 +++++++++++++++++++++++++++++++++++++++++++ evaluator.lua | 15 +++++++++++++ terms.lua | 5 +++++ tests/switch-test.alc | 5 +++++ types/inferrable.lua | 7 ++++++ 5 files changed, 83 insertions(+) diff --git a/base-env.lua b/base-env.lua index d3c56afa..69f6a84e 100644 --- a/base-env.lua +++ b/base-env.lua @@ -1565,6 +1565,56 @@ 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), + tupleof_ascribed_names_inner(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_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 @@ -1596,6 +1646,7 @@ local core_operations = { 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), diff --git a/evaluator.lua b/evaluator.lua index f5bc834c..ddd92df5 100644 --- a/evaluator.lua +++ b/evaluator.lua @@ -2042,6 +2042,21 @@ 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_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_term = infer(rest, typechecking_context) --TODO improve + return value.enum_desc_type(result_type), usage_array(), typed_term.enum_desc_cons(term_variants, rest_term) elseif inferrable_term:is_object_cons() then local methods = inferrable_term:unwrap_object_cons() local type_data = terms.empty diff --git a/terms.lua b/terms.lua index e7e002d3..5c12f654 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, diff --git a/tests/switch-test.alc b/tests/switch-test.alc index 72a56ca3..74fd8e01 100644 --- a/tests/switch-test.alc +++ b/tests/switch-test.alc @@ -13,3 +13,8 @@ tuple-of-implicit 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) \ No newline at end of file diff --git a/types/inferrable.lua b/types/inferrable.lua index 5df80f13..29c743a7 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 @@ -258,6 +264,7 @@ 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_case fun(target: inferrable, variants: MapValue): inferrable From 99108e23b39ac4d8846a09af56d11e71233df02a Mon Sep 17 00:00:00 2001 From: Alex Iverson Date: Sat, 4 Jan 2025 20:12:07 -0800 Subject: [PATCH 18/25] add substitution cases --- evaluator.lua | 16 ++++++++++++++-- terms.lua | 7 +++++++ types/inferrable.lua | 7 +++++++ types/typed.lua | 7 +++++++ 4 files changed, 35 insertions(+), 2 deletions(-) diff --git a/evaluator.lua b/evaluator.lua index ddd92df5..1bf43ae2 100644 --- a/evaluator.lua +++ b/evaluator.lua @@ -400,8 +400,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") diff --git a/terms.lua b/terms.lua index 5c12f654..024aa88b 100644 --- a/terms.lua +++ b/terms.lua @@ -400,6 +400,10 @@ inferrable_term:define_enum("inferrable", { "mechanism", inferrable_term, } }, { "enum_type", { "desc", inferrable_term } }, + { "enum_desc_cons", { + "variants", map(gen.builtin_string, inferrable_term), + "rest", inferrable_term, + } }, { "enum_case", { "target", inferrable_term, "variants", map(gen.builtin_string, inferrable_term), @@ -644,6 +648,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/types/inferrable.lua b/types/inferrable.lua index 29c743a7..e165660c 100644 --- a/types/inferrable.lua +++ b/types/inferrable.lua @@ -89,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 @@ -267,6 +273,7 @@ function inferrable:as_program_type() end ---@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 a7a0b80f..11357772 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 From 04014228a4a483431532ad695fa864094b7641de Mon Sep 17 00:00:00 2001 From: Erik McClure Date: Sun, 5 Jan 2025 00:18:27 -0800 Subject: [PATCH 19/25] value leaking into type comparison??? --- evaluator.lua | 4 ++++ prelude.alc | 20 ++++++++++++++++++++ terms.lua | 4 ---- 3 files changed, 24 insertions(+), 4 deletions(-) diff --git a/evaluator.lua b/evaluator.lua index 1bf43ae2..908a1cfd 100644 --- a/evaluator.lua +++ b/evaluator.lua @@ -2569,6 +2569,10 @@ 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) diff --git a/prelude.alc b/prelude.alc index 932582b1..6a3b78b1 100644 --- a/prelude.alc +++ b/prelude.alc @@ -55,6 +55,25 @@ let host-inferrable-term = unwrap(host-inferrable-term-wrap) let host-checkable-term = unwrap(host-checkable-term-wrap) let host-lua-error = unwrap(host-lua-error-wrap) +# TEMPORARY TEST: MOVE TO TEST FILE BEFORE FINALIZING PR + +let Result = lambda (T, E) + enum + Ok(x : T) + Err(e : E) + +let sqr = lambda (x) + x + +let switchtest = lambda (x : Result(host-number, host-number)) + switch x + Ok(x) -> x + Err(a) -> -1 + +switchtest(mk Ok(5)) +switchtest(mk Err(3)) + + let host-srel-type = lambda_implicit (U : type_(10, 0)) unwrap @@ -1785,3 +1804,4 @@ 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 024aa88b..905520a1 100644 --- a/terms.lua +++ b/terms.lua @@ -400,10 +400,6 @@ inferrable_term:define_enum("inferrable", { "mechanism", inferrable_term, } }, { "enum_type", { "desc", inferrable_term } }, - { "enum_desc_cons", { - "variants", map(gen.builtin_string, inferrable_term), - "rest", inferrable_term, - } }, { "enum_case", { "target", inferrable_term, "variants", map(gen.builtin_string, inferrable_term), From 043de523aa5c854eb1bc3a421226227395f11e4d Mon Sep 17 00:00:00 2001 From: Erik McClure Date: Sun, 5 Jan 2025 01:06:25 -0800 Subject: [PATCH 20/25] Actually return enum_type --- base-env.lua | 14 ++++++++------ evaluator.lua | 18 +++++++++++++++--- 2 files changed, 23 insertions(+), 9 deletions(-) diff --git a/base-env.lua b/base-env.lua index 69f6a84e..7eec8ab3 100644 --- a/base-env.lua +++ b/base-env.lua @@ -1604,12 +1604,14 @@ local function enum_impl(syntax, env) end return true, - 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)())) + 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 diff --git a/evaluator.lua b/evaluator.lua index 908a1cfd..361eba9b 100644 --- a/evaluator.lua +++ b/evaluator.lua @@ -2059,7 +2059,7 @@ function infer( local result_types = {} local term_variants = string_typed_map() for k, v in variants:pairs() do - local variant_type, _, variant_term = infer(v, typechecking_context) --TODO improve + 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 @@ -2067,8 +2067,20 @@ function infer( for i = 2, #result_types do result_type = value.union_type(result_type, result_types[i]) end - local _, _, rest_term = infer(rest, typechecking_context) --TODO improve - return value.enum_desc_type(result_type), usage_array(), typed_term.enum_desc_cons(term_variants, rest_term) + 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 From 744ea1b267fc43cdb2696e4663505501ae708752 Mon Sep 17 00:00:00 2001 From: AstroSnail Date: Sun, 5 Jan 2025 11:16:48 +0000 Subject: [PATCH 21/25] Refactor the ascribed-names reducers --- base-env.lua | 127 ++++++++++++++++----------------------------------- 1 file changed, 40 insertions(+), 87 deletions(-) diff --git a/base-env.lua b/base-env.lua index 7eec8ab3..ed02b1a4 100644 --- a/base-env.lua +++ b/base-env.lua @@ -457,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 @@ -499,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 @@ -517,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 @@ -535,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( @@ -566,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 @@ -607,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 @@ -620,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 @@ -652,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" + "tuple_desc_wrap_ascribed_name" ) -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" -) - -local ascribed_segment_2 = metalanguage.reducer( +local ascribed_segment_tuple_desc = metalanguage.reducer( ---@param syntax ConstructedSyntax ---@param env Environment ---@return boolean @@ -711,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) @@ -1065,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 @@ -1100,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 @@ -1189,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 @@ -1571,7 +1524,7 @@ local enum_variant = metalanguage.reducer(function(syntax, env) metalanguage.listtail( metalanguage.accept_handler, metalanguage.issymbol(metalanguage.accept_handler), - tupleof_ascribed_names_inner(metalanguage.accept_handler, env) + tuple_desc_of_ascribed_names(metalanguage.accept_handler, env) ), }, metalanguage.failure_handler, nil) @@ -1702,7 +1655,7 @@ local function create() end local base_env = { - tupleof_ascribed_names_inner = tupleof_ascribed_names_inner, + tupleof_ascribed_names_inner = tuple_desc_of_ascribed_names, create = create, } local internals_interface = require "internals-interface" From d7429753dc1dcb88e34f167bd653576e7304320b Mon Sep 17 00:00:00 2001 From: AstroSnail Date: Sun, 5 Jan 2025 11:23:41 +0000 Subject: [PATCH 22/25] Change tuple-desc and enum operatives to use ascribed_segment_tuple_desc --- base-env.lua | 4 +-- prelude.alc | 64 +++++++++++++++++----------------- tests/operative-tuple-desc.alc | 4 +-- 3 files changed, 36 insertions(+), 36 deletions(-) diff --git a/base-env.lua b/base-env.lua index ed02b1a4..b4a3ab29 100644 --- a/base-env.lua +++ b/base-env.lua @@ -1524,7 +1524,7 @@ local enum_variant = metalanguage.reducer(function(syntax, env) metalanguage.listtail( metalanguage.accept_handler, metalanguage.issymbol(metalanguage.accept_handler), - tuple_desc_of_ascribed_names(metalanguage.accept_handler, env) + ascribed_segment_tuple_desc(metalanguage.accept_handler, env) ), }, metalanguage.failure_handler, nil) @@ -1655,7 +1655,7 @@ local function create() end local base_env = { - tupleof_ascribed_names_inner = tuple_desc_of_ascribed_names, + ascribed_segment_tuple_desc = ascribed_segment_tuple_desc, create = create, } local internals_interface = require "internals-interface" diff --git a/prelude.alc b/prelude.alc index 6a3b78b1..ab9293f6 100644 --- a/prelude.alc +++ b/prelude.alc @@ -1655,40 +1655,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 @@ -1698,32 +1698,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 @@ -1734,16 +1734,16 @@ 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) diff --git a/tests/operative-tuple-desc.alc b/tests/operative-tuple-desc.alc index 52c80b62..a5e4e315 100644 --- a/tests/operative-tuple-desc.alc +++ b/tests/operative-tuple-desc.alc @@ -5,8 +5,8 @@ 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()) + 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)) \ No newline at end of file + host-func-type (name : host-string, arg : host-inferrable-term) -> ((res : host-inferrable-term)) From 7f42fc5beedfdde4b6f213643338f20dc9a97c76 Mon Sep 17 00:00:00 2001 From: AstroSnail Date: Sun, 5 Jan 2025 11:27:13 +0000 Subject: [PATCH 23/25] Fix unpack --- base-env.lua | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/base-env.lua b/base-env.lua index b4a3ab29..792cf7e4 100644 --- a/base-env.lua +++ b/base-env.lua @@ -137,7 +137,7 @@ local function unwrap_into_string(...) for i, v in ipairs(args) do args[i] = v.str end - return unpack(args) + return table.unpack(args) end ---@param env Environment From b6d3e8676fe66e280247794c0bdb82579322f949 Mon Sep 17 00:00:00 2001 From: Erik McClure Date: Sun, 5 Jan 2025 03:50:47 -0800 Subject: [PATCH 24/25] Finalize tests, make error not stupid. --- evaluator.lua | 6 +++++- prelude.alc | 19 ------------------- testlist.json | 1 + tests/switch-fail.alc | 12 ++++++++++++ tests/switch-test.alc | 11 ++++++++++- 5 files changed, 28 insertions(+), 21 deletions(-) create mode 100644 tests/switch-fail.alc diff --git a/evaluator.lua b/evaluator.lua index 361eba9b..f9903d97 100644 --- a/evaluator.lua +++ b/evaluator.lua @@ -235,11 +235,15 @@ 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 + error(name .. " is not a valid enum variant! Is this a typo?") + 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 diff --git a/prelude.alc b/prelude.alc index ab9293f6..bc894a36 100644 --- a/prelude.alc +++ b/prelude.alc @@ -55,25 +55,6 @@ let host-inferrable-term = unwrap(host-inferrable-term-wrap) let host-checkable-term = unwrap(host-checkable-term-wrap) let host-lua-error = unwrap(host-lua-error-wrap) -# TEMPORARY TEST: MOVE TO TEST FILE BEFORE FINALIZING PR - -let Result = lambda (T, E) - enum - Ok(x : T) - Err(e : E) - -let sqr = lambda (x) - x - -let switchtest = lambda (x : Result(host-number, host-number)) - switch x - Ok(x) -> x - Err(a) -> -1 - -switchtest(mk Ok(5)) -switchtest(mk Err(3)) - - let host-srel-type = lambda_implicit (U : type_(10, 0)) unwrap diff --git a/testlist.json b/testlist.json index c0e250e8..b7e0447f 100644 --- a/testlist.json +++ b/testlist.json @@ -12,6 +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/switch-fail.alc b/tests/switch-fail.alc new file mode 100644 index 00000000..91b1933a --- /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 index 74fd8e01..be208c9f 100644 --- a/tests/switch-test.alc +++ b/tests/switch-test.alc @@ -17,4 +17,13 @@ tuple-of-implicit let Result = lambda (T, E) enum Ok(x : T) - Err(e : E) \ No newline at end of file + 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 From 738a7375c5855437a8c20c6953462aa5f5b57c4b Mon Sep 17 00:00:00 2001 From: Erik McClure Date: Sun, 5 Jan 2025 04:18:58 -0800 Subject: [PATCH 25/25] Add levenshtein algorithm --- alicorn-utils.lua | 43 +++++++++++++++++++++++++++++++++++++++++++ evaluator.lua | 10 +++++++++- 2 files changed, 52 insertions(+), 1 deletion(-) diff --git a/alicorn-utils.lua b/alicorn-utils.lua index fee29923..bf174a96 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/evaluator.lua b/evaluator.lua index f9903d97..1c3cf83b 100644 --- a/evaluator.lua +++ b/evaluator.lua @@ -237,7 +237,15 @@ enum_desc_srel = setmetatable({ for name, val_type in val_variants:pairs() do local use_variant = use_variants:get(name) if use_variant == nil then - error(name .. " is not a valid enum variant! Is this a typo?") + 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,