add prim-type to env and try making an array

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

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

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"
 

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
+