parse prim-function-type

alicorn-expressions.lua

@@ -190,7 +190,7 @@ local function inferred_expression_pairhandler(env, a, b)
 		if not inferrable_term.value_check(data) then
 			error "tried to handle something that was not an inferrable term"
 		end
-		p("Inferring!", data.kind, env.typechecking_context)
+		--p("Inferring!", data.kind, env.typechecking_context)
 
 		local resulting_type, usage_counts, term = infer(data, env.typechecking_context)
 

base-env.lua

@@ -111,14 +111,14 @@ local function intrinsic(syntax, env)
 		return ok, str_env
 	end
 	env = str_env.env
-	local str = str_env.val
+	local str = terms.checkable_term.inferrable(str_env.val) -- workaround for not having exprs.checked_expression yet
 	local ok, type, env = syntax:match({
 		metalang.listmatch(metalang.accept_handler, exprs.inferred_expression(metalang.accept_handler, env)),
 	}, metalang.failure_handler, nil)
 	if not ok then
 		return ok, type
 	end
-	return true, terms.inferrable_term.prim_intrinsic(str, type), env
+	return true, terms.inferrable_term.prim_intrinsic(str, terms.checkable_term.inferrable(type)), env
 end
 
 local basic_fn_kind = {
@@ -277,15 +277,17 @@ local prim_func_type_impl_reducer = metalang.reducer(function(syntax, env)
 	end
 	local empty = terms.inferrable_term.enum_cons(terms.value.tuple_defn_type, "empty", tup_cons())
 	local args = empty
+
+	local unrestricted_term = terms.inferrable_term.typed(
+		terms.value.quantity_type,
+		usage_array(),
+		terms.typed_term.literal(
+			terms.value.quantity(terms.quantity.unrestricted)))
 
 	local function build_type_term(args)
 		return
 			terms.inferrable_term.qtype(
-				terms.inferrable_term.typed(
-					terms.value.quantity_type,
-					usage_array(),
-					terms.typed_term.literal(
-						terms.value.quantity(terms.quantity.unrestricted))),
+				unrestricted_term,
 				terms.inferrable_term.tuple_type(args)
 			)
 	end
@@ -310,6 +312,9 @@ local prim_func_type_impl_reducer = metalang.reducer(function(syntax, env)
 		print(env.get)
 		print(env.enter_block)
 
+		print "args in loop is"
+		print(args:pretty_print())
+
 		ok, continue, name, type_val, type_env = head:match({
 			metalang.symbol_exact(function()
 				return true, false
@@ -339,7 +344,8 @@ local prim_func_type_impl_reducer = metalang.reducer(function(syntax, env)
 	ok, continue = true, true
 	local shadowed, env = env:enter_block()
 	env = env:bind_local(terms.binding.annotated_lambda("#arg", build_type_term(args)))
-	env = env:bind_local(terms.binding.tuple_elim(names, build_type_term(args)))
+	local ok, arg = env:get("#arg")
+	env = env:bind_local(terms.binding.tuple_elim(names, arg))
 	names = gen.declare_array(gen.builtin_string)()
 	local results = empty
 	while ok and continue do
@@ -366,24 +372,26 @@ local prim_func_type_impl_reducer = metalang.reducer(function(syntax, env)
 			names:append(name)
 		end
 
+		if not ok then
+			return false, continue
+		end
+
 		syntax = tail
 	end
-	if not ok then
-		return false, continue
-	end
 
-	local fn_type_term = terms.value.qtype(terms.quantity.unrestricted, terms.value.prim_function_type(args, results))
-
+	local fn_type_term = terms.inferrable_term.qtype(unrestricted_term, terms.inferrable_term.prim_function_type(args, results))
+	print("reached end of function type construction")
 	return true, fn_type_term, env
 end, "prim_func_type_impl")
 
 -- TODO: abstract so can reuse for func type and prim func type
 local function prim_func_type_impl(syntax, env)
 	print("in prim_func_type_impl")
-	local result =
+	local ok, fn_type_term, env =
 		syntax:match({ prim_func_type_impl_reducer(metalang.accept_handler, env) }, metalang.failure_handler, env)
-	p(result)
-	error "NYI"
+	print("finished matching prim_func_type_impl")
+	if not ok then return ok, fn_type_term end
+	return ok, fn_type_term, env
 	-- parse sequence of ascribed names, arrow, then sequence of ascribed names
 	-- for each ascribed name:
 	-- enter a block, perform lambda binding, perform tuple destrucutring binding, parse out the type of the ascription

environment.lua

@@ -70,7 +70,7 @@ environment_mt = {
 			elseif binding:is_tuple_elim() then
 				local names, subject = binding:unwrap_tuple_elim()
 				local subject_type, subject_usages, subject_term = infer(subject, self.typechecking_context)
-				local subject_qty, subject_type = subject_type:unwrap_qtype()
+				--local subject_qty, subject_type = subject_type:unwrap_qtype()
 				--DEBUG:
 				if subject_type:is_enum_value() then print "bad subject infer" ; print(subject:pretty_print()) end
 

evaluator.lua

@@ -569,6 +569,10 @@ local function make_inner_context(decls, tupletypes, make_prefix)
 end
 
 local function infer_tuple_type(subject_type, subject_value)
+	if not subject_type:is_qtype() then
+		print("missing qtype wrapping tuple type")
+		print(subject_type:pretty_print())
+	end
 	-- define how the type of each tuple element should be evaluated
 	local qty, base = subject_type:unwrap_qtype()
 	local decls, make_prefix = make_tuple_prefix(base, subject_value)
@@ -577,6 +581,7 @@ local function infer_tuple_type(subject_type, subject_value)
 	return inner_context, n_elements
 end
 
+---@return unknown, unknown, unknow
 function infer(
 	inferrable_term, -- constructed from inferrable
 	typechecking_context -- todo
@@ -609,7 +614,7 @@ function infer(
 		-- TODO: also handle neutral values, for inference of qtype
 		local param_quantity, param_type = param_value:unwrap_qtype()
 		local param_quantity = param_quantity:unwrap_quantity()
-		local inner_context = typechecking_context:append(param_name, param_type)
+		local inner_context = typechecking_context:append(param_name, param_value)
 		local body_type, body_usages, body_term = infer(body, inner_context)
 		local result_type = substitute_type_variables(body_type, #inner_context, 0)
 		local body_usages_param = body_usages[#body_usages]
@@ -640,6 +645,9 @@ function infer(
 		add_arrays(qtype_usages, type_usages)
 		local qtype = typed_term.qtype(quantity_term, type_term)
 		local qtype_type = value.qtype_type(get_level(type_type))
+		-- print("inferring a qtype")
+		-- print(inferrable_term:pretty_print())
+		-- print(qtype:pretty_print())
 		return qtype_type, qtype_usages, qtype
 	elseif inferrable_term:is_pi() then
 		error("infer: nyi")
@@ -752,8 +760,7 @@ function infer(
 		if definition_type ~= terms.value.tuple_defn_type then
 			error "argument to tuple_type is not a tuple_defn"
 		end
-		return unrestricted(terms.value.star(0)), definition_usages,
-			unrestricted_typed(terms.typed_term.tuple_type(definition_term))
+		return unrestricted(terms.value.star(0)), definition_usages, terms.typed_term.tuple_type(definition_term)
 	elseif inferrable_term:is_record_cons() then
 		local fields = inferrable_term:unwrap_record_cons()
 		-- type_data is either "empty", an empty tuple,
@@ -1013,12 +1020,20 @@ function infer(
 	elseif inferrable_term:is_level_max() then
 		local arg_type_a, arg_term_a = infer(inferrable_term.level_a, typechecking_context)
 		local arg_type_b, arg_term_b = infer(inferrable_term.level_b, typechecking_context)
-		return value.level_type, typed_term.level_max(arg_term_a, arg_term_b)
+		return value.level_type, usage_array(), typed_term.level_max(arg_term_a, arg_term_b)
 	elseif inferrable_term:is_level_suc() then
-		local arg_type, arg_term = infer(inferrable_term.previous_level, typechecking_context)
-		return value.level_type, typed_term.level_suc(arg_term)
+		local arg_type, arg_usages, arg_term = infer(inferrable_term.previous_level, typechecking_context)
+		return value.level_type, usage_array(), typed_term.level_suc(arg_term)
 	elseif inferrable_term:is_level0() then
-		return value.level_type, typed_term.level0
+		return value.level_type, usage_array(), typed_term.level0
+	elseif inferrable_term:is_prim_function_type() then
+		local args, returns = inferrable_term:unwrap_prim_function_type()
+		local arg_type, arg_usages, arg_term = infer(args, typechecking_context)
+		local return_type, return_usages, return_term = infer(args, typechecking_context)
+		local res_usages = usage_array()
+		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)
 	else
 		error("infer: unknown kind: " .. inferrable_term.kind)
 	end
@@ -1297,6 +1312,11 @@ function evaluate(typed_term, runtime_context)
 		else
 			error "Tried to load an intrinsic with something that isn't a string"
 		end
+	elseif typed_term:is_prim_function_type() then
+		local args, returns = typed_term:unwrap_prim_function_type()
+		local args_val = evaluate(args, runtime_context)
+		local returns_val = evaluate(returns, runtime_context)
+		return value.prim_function_type(args_val, returns_val)
 	elseif typed_term:is_level0() then
 		return value.level(0)
 	elseif typed_term:is_level_suc() then

terms.lua

@@ -429,6 +429,17 @@ inferrable_term:define_enum("inferrable", {
 			array(inferrable_term), -- prim
 		},
 	},
+	{
+		"prim_function_type",
+		{
+			"param_type",
+			inferrable_term, -- must be a prim_tuple_type
+			-- primitive functions can only have explicit arguments
+			"result_type",
+			inferrable_term, -- must be a prim_tuple_type
+			-- primitive functions can only be pure for now
+		},
+	},
 	{ "prim_boxed_type", { "type", inferrable_term } },
 	{ "prim_box", { "content", inferrable_term } },
 	{ "prim_unbox", { "container", inferrable_term } },
@@ -570,6 +581,17 @@ typed_term:define_enum("typed", {
 			array(typed_term), -- prim
 		},
 	},
+	{
+		"prim_function_type",
+		{
+			"param_type",
+			typed_term, -- must be a prim_tuple_type
+			-- primitive functions can only have explicit arguments
+			"result_type",
+			typed_term, -- must be a prim_tuple_type
+			-- primitive functions can only be pure for now
+		},
+	},
 	{ "prim_boxed_type", { "type", typed_term } },
 	{ "prim_box", { "content", typed_term } },
 	{ "prim_unbox", { "container", typed_term } },

testfile.alc

@@ -1,8 +1,9 @@
 let x = 621
 let y = 926
-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 prim-arith-binop = (prim-func-type (a : prim-number) (b : prim-number) -> (c : prim-number))
+#let prim-sub = (intrinsic "return function(a, b) return a - b end" : prim-arith-binop)
 let foo = (record (bar = 5) (baz = 6))
-let subbed = prim-sub foo.bar y
+#let subbed = prim-sub foo.bar y
 
 let (val) =
 	+ x 1