intrinsic can infer and call

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
 

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),

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, {

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

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",
 		{

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