From 8c072186ccc768f42e1f6053c7750077545d0177 Mon Sep 17 00:00:00 2001
From: Alex Iverson <alexjiverson@gmail.com>
Date: Mon, 4 Dec 2023 17:17:28 -0800
Subject: [PATCH] add prim-type to env and try making an array

---
 base-env.lua |  1 +
 runtest.lua  |  1 +
 terms.lua    |  2 +-
 testfile.alc | 26 +++++++++++++++++++++-----
 4 files changed, 24 insertions(+), 6 deletions(-)

diff --git a/base-env.lua b/base-env.lua
index f3f32bda..7bffed95 100644
--- a/base-env.lua
+++ b/base-env.lua
@@ -478,6 +478,7 @@ local core_operations = {
 	record = exprs.primitive_operative(record_build),
 	intrinsic = exprs.primitive_operative(intrinsic),
 	["prim-number"] = lit_term(value.qtype(value.quantity(terms.quantity.unrestricted), value.prim_number_type), value.prim_type_type),
+	["prim-type"] = lit_term(value.qtype(value.quantity(terms.quantity.unrestricted), value.prim_type_type), value.star(1)),
 	["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/runtest.lua b/runtest.lua
index 3b0912b8..ba447406 100644
--- a/runtest.lua
+++ b/runtest.lua
@@ -30,6 +30,7 @@ local env, bound_expr = env:exit_block(expr, shadowed)
 
 print("Inferring")
 local type, usages, term = evaluator.infer(bound_expr, terms.typechecking_context())
+print("Inferred!")
 print(type:pretty_print())
 p(usages)
 print(term:pretty_print())
diff --git a/terms.lua b/terms.lua
index 6d5462b3..1ce08d61 100644
--- a/terms.lua
+++ b/terms.lua
@@ -39,7 +39,7 @@
 -- when binding to another metavariable bind the one with a greater index to the lesser index
 
 local metalang = require "./metalanguage"
-local types = require "./typesystem"
+--local types = require "./typesystem"
 
 local fibbuf = require "./fibonacci-buffer"
 
diff --git a/testfile.alc b/testfile.alc
index fb38b1f4..a858ed49 100644
--- a/testfile.alc
+++ b/testfile.alc
@@ -2,16 +2,31 @@
 #let y = 926
 #let prim-add = +
 
-# FIXME: let binding here errors due to type mismatch (qtype_type vs actual qtype wrapping prim_number_type)
-#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 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)
 
-# 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 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 subbed = prim-sub foo.bar y
 
+# this should error becaused prim-type is not a prim-type and therefore can't be an arg to a prim-func-type
+# but it doesn't.
+let array-type =
+	intrinsic
+		""""
+			local terms = require './terms'
+			local value = terms.value
+			local gens = require './terms-generators'
+			local value_array = gens.declare_array(value)
+			local id = {name = "array"}
+			local function mktype(elem)
+				return value.prim_boxed_type(id, value_array(elem))
+			end
+			return mktype
+		:
+		prim-func-type (T : prim-type) -> (array : prim-type)
+
 #let (val) =
 #	+ x 5
 
@@ -22,3 +37,4 @@ let prim-sub = (intrinsic "return function(a, b) return a - b end" : (prim-func-
 
 let (val) = (prim-sub 5 1)
 prim-sub val 3
+