From e6958c336b4cac71dc918e373fd4e0e2fe769be8 Mon Sep 17 00:00:00 2001 From: Alex Iverson Date: Sun, 26 Nov 2023 10:02:00 -0800 Subject: [PATCH] intrinsic can infer and call --- alicorn-expressions.lua | 7 ++++++- base-env.lua | 17 +++++++++++++---- environment.lua | 2 ++ evaluator.lua | 17 ++++++++++++++++- terms.lua | 5 ++++- testfile.alc | 14 +++++++------- 6 files changed, 48 insertions(+), 14 deletions(-) diff --git a/alicorn-expressions.lua b/alicorn-expressions.lua index ad52baa7..54173949 100644 --- a/alicorn-expressions.lua +++ b/alicorn-expressions.lua @@ -228,7 +228,12 @@ local function inferred_expression_pairhandler(env, a, b) return true, inferrable_term.application(inferrable_term.typed(type_of_term, usage_count, term), tuple), env end - p(type_of_term) + print("!!! about to fail of invalid type") + print(combiner:pretty_print()) + print("infers to") + print(type_of_term:pretty_print()) + print("in") + env.typechecking_context:dump_names() return false, "unknown type for pairhandler " .. type_of_term.kind, env end diff --git a/base-env.lua b/base-env.lua index 956af2b6..f3f32bda 100644 --- a/base-env.lua +++ b/base-env.lua @@ -132,7 +132,7 @@ local function intrinsic(syntax, env) if not env then error "env nil in base-env.intrinsic" end - return true, terms.inferrable_term.prim_intrinsic(str, terms.checkable_term.inferrable(type)), env + return true, terms.inferrable_term.prim_intrinsic(str, type--[[terms.checkable_term.inferrable(type)]]), env end local basic_fn_kind = { @@ -308,6 +308,13 @@ local prim_func_type_impl_reducer = metalang.reducer(function(syntax, env) terms.inferrable_term.tuple_type(args) ) end + local function build_prim_type_term(args) + return + terms.inferrable_term.qtype( + unrestricted_term, + terms.inferrable_term.prim_tuple_type(args) + ) + end local names = gen.declare_array(gen.builtin_string)() print("is env an environment? (before loop)") @@ -399,7 +406,8 @@ local prim_func_type_impl_reducer = metalang.reducer(function(syntax, env) syntax = tail end - local env, fn_type_term = env:exit_block(terms.inferrable_term.qtype(unrestricted_term, terms.inferrable_term.prim_function_type(args, results)), shadowed) + local env, fn_res_term = env:exit_block(build_prim_type_term(results), shadowed) + local fn_type_term = terms.inferrable_term.qtype(unrestricted_term, terms.inferrable_term.prim_function_type(build_prim_type_term(args), fn_res_term)) print("reached end of function type construction") if not env.enter_block then error "env isn't an environment at end in prim_func_type_impl_reducer" @@ -417,7 +425,8 @@ local function prim_func_type_impl(syntax, env) print("in prim_func_type_impl") local ok, fn_type_term, env = syntax:match({ prim_func_type_impl_reducer(metalang.accept_handler, env) }, metalang.failure_handler, env) - print("finished matching prim_func_type_impl") + print("finished matching prim_func_type_impl and got") + print(fn_type_term:pretty_print()) if not ok then return ok, fn_type_term end if not env.enter_block then error "env isn't an environment at end in prim_func_type_impl" @@ -468,7 +477,7 @@ local core_operations = { let = exprs.primitive_operative(let_bind), record = exprs.primitive_operative(record_build), intrinsic = exprs.primitive_operative(intrinsic), - ["prim-number"] = lit_term(value.prim_number_type, value.prim_type_type), + ["prim-number"] = lit_term(value.qtype(value.quantity(terms.quantity.unrestricted), value.prim_number_type), value.prim_type_type), ["prim-func-type"] = exprs.primitive_operative(prim_func_type_impl), --["dump-env"] = evaluator.primitive_operative(function(syntax, env) print(environment.dump_env(env)); return true, types.unit_val, env end), --["basic-fn"] = evaluator.primitive_operative(basic_fn), diff --git a/environment.lua b/environment.lua index a819a69b..1855fc7f 100644 --- a/environment.lua +++ b/environment.lua @@ -71,6 +71,8 @@ function environment:bind_local(binding) local term = inferrable_term.bound_variable(n + 1) local locals = self.locals:put(name, term) local evaled = eval.evaluate(expr_term, self.typechecking_context.runtime_context) + -- print "doing let binding" + -- print(expr:pretty_print()) local typechecking_context = self.typechecking_context:append(name, expr_type, evaled) local bindings = self.bindings:append(binding) return update_env(self, { diff --git a/evaluator.lua b/evaluator.lua index 4c0f94b3..98c7cf40 100644 --- a/evaluator.lua +++ b/evaluator.lua @@ -1033,7 +1033,13 @@ function infer( elseif inferrable_term:is_prim_intrinsic() then local source, type = inferrable_term:unwrap_prim_intrinsic() local source_type, source_usages, source_term = check(source, typechecking_context, unrestricted(value.prim_string_type)) - local type_type, type_usages, type_term = check(type, typechecking_context, value.qtype_type(0)) + local type_type, type_usages, type_term = infer(type, typechecking_context) --check(type, typechecking_context, value.qtype_type(0)) + + print "prim intrinsic is inferring" + print(type:pretty_print()) + print("lowers to") + print(type_term:pretty_print()) + --error "weird type" -- FIXME: type_type, source_type are ignored, need checked? local type_val = evaluate(type_term, typechecking_context.runtime_context) return type_val, source_usages, typed_term.prim_intrinsic(source_term) @@ -1054,6 +1060,11 @@ function infer( add_arrays(res_usages, arg_usages) add_arrays(res_usages, return_usages) return value.prim_type_type, res_usages, typed_term.prim_function_type(arg_term, return_term) + elseif inferrable_term:is_prim_tuple_type() then + local decls = inferrable_term:unwrap_prim_tuple_type() + local decl_type, decl_usages, decl_term = infer(decls, typechecking_context) + if not decl_type:is_tuple_defn_type() then error "must be a tuple defn" end + return value.star(0), decl_usages, typed_term.prim_tuple_type(decl_term) else error("infer: unknown kind: " .. inferrable_term.kind) end @@ -1362,6 +1373,10 @@ function evaluate(typed_term, runtime_context) return value.star(typed_term.level) elseif typed_term:is_prop() then return value.prop(typed_term.level) + elseif typed_term:is_prim_tuple_type() then + local decl = typed_term:unwrap_prim_tuple_type() + local decl_val = evaluate(decl, runtime_context) + return value.prim_tuple_type(decl_val) else error("evaluate: unknown kind: " .. typed_term.kind) end diff --git a/terms.lua b/terms.lua index 0093ac89..6d5462b3 100644 --- a/terms.lua +++ b/terms.lua @@ -243,6 +243,7 @@ function TypecheckingContext:append(name, type, val) -- value is optional if name == nil or type == nil then error("bug!!!") end + if type:is_closure() then error "BUG!!!" end local copy = { bindings = self.bindings:append({ name = name, type = type }), runtime_context = self.runtime_context:append( @@ -444,6 +445,7 @@ inferrable_term:define_enum("inferrable", { array(inferrable_term), -- prim }, }, + { "prim_tuple_type", { "decls", inferrable_term } }, -- just like an ordinary tuple type but can only hold prims { "prim_function_type", { @@ -473,7 +475,7 @@ inferrable_term:define_enum("inferrable", { "source", checkable_term, "type", - checkable_term, + inferrable_term, --checkable_term, } }, }) -- typed terms have been typechecked but do not store their type internally @@ -596,6 +598,7 @@ typed_term:define_enum("typed", { array(typed_term), -- prim }, }, + { "prim_tuple_type", { "decls", typed_term } }, -- just like an ordinary tuple type but can only hold prims { "prim_function_type", { diff --git a/testfile.alc b/testfile.alc index c7ac5f4f..24f83656 100644 --- a/testfile.alc +++ b/testfile.alc @@ -1,5 +1,5 @@ -let x = 621 -let y = 926 +#let x = 621 +#let y = 926 #let prim-add = + # FIXME: let binding here errors due to type mismatch (qtype_type vs actual qtype wrapping prim_number_type) @@ -9,15 +9,15 @@ let y = 926 # FIXME: calling intrinsic here errors due to error in fits into (probably same root cause of qtype_type vs actual qtype wrapping prim_number_type) let prim-sub = (intrinsic "return function(a, b) return a - b end" : (prim-func-type (a : prim-number) (b : prim-number) -> (c : prim-number))) -let foo = (record (bar = 5) (baz = 6)) +#let foo = (record (bar = 5) (baz = 6)) #let subbed = prim-sub foo.bar y -let (val) = - + x 5 +#let (val) = +# + x 5 #let (val) = # + val y -#+ foo.bar val +#prim-sub foo.bar val -#prim-sub +prim-sub 5 1