Skip to content

Commit

Permalink
add lambda operative!
Browse files Browse the repository at this point in the history
  • Loading branch information
@aiverson
aiverson committed Dec 10, 2023
1 parent a52dbbb commit 87cd317
Show file tree
Hide file tree
Showing 5 changed files with 354 additions and 28 deletions.
306 changes: 289 additions & 17 deletions base-env.lua
View file
Original file line number Diff line number Diff line change
Expand Up @@ -135,21 +135,6 @@ local function intrinsic(syntax, env)
return true, terms.inferrable_term.prim_intrinsic(str, type--[[terms.checkable_term.inferrable(type)]]), env
end

local basic_fn_kind = {
kind_name = "basic_fn_kind",
type_name = function()
return "basic_fn"
end,
duplicable = function()
return true
end,
discardable = function()
return true
end,
}

local basic_fn_type = { kind = basic_fn_kind, params = {} }

--evaluator.define_operate(
-- basic_fn_kind,
-- function(self, operands, env)
Expand Down Expand Up @@ -418,9 +403,9 @@ end, "prim_func_type_impl")
-- TODO: abstract so can reuse for func type and prim func type
---@param syntax any
---@param env Environment
---@return boolean
---@return unknown
---@return unknown
---@return unknown
---@return unknown|nil
local function prim_func_type_impl(syntax, env)
print("in prim_func_type_impl")
local ok, fn_type_term, env =
Expand All @@ -439,11 +424,294 @@ local function prim_func_type_impl(syntax, env)
--local ok,
end

local forall_type_impl_reducer = metalang.reducer(function(syntax, env)
local value_array = gen.declare_array(terms.value)
local inf_array = gen.declare_array(terms.inferrable_term)
local usage_array = gen.declare_array(gen.builtin_number)
local function tup_cons(...)
return terms.inferrable_term.tuple_cons(inf_array(...))
end
local function cons(...)
return terms.inferrable_term.enum_cons(terms.value.tuple_defn_type, "cons", tup_cons(...))
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(
unrestricted_term,
terms.inferrable_term.tuple_type(args)
)
end

local names = gen.declare_array(gen.builtin_string)()
print("is env an environment? (before loop)")
--p(env)
print(env.get)
print(env.enter_block)
if not env.enter_block then
error "env isn't an environment in prim_func_type_impl_reducer"
end

local head, tail, name, type_val, type_env
local ok, continue = true, true
while ok and continue do
ok, head, tail = syntax:match({ metalang.ispair(metalang.accept_handler) }, metalang.failure_handler, env)
print(env)
if not ok then
break
end

print("is env an environment? (in loop)")
--p(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
end, "->"),
ascribed_name(function(ok, ...)
return ok, true, ...
end, env, build_type_term(args), names),
}, metalang.failure_handler, env)

if continue then
-- type_env:bind_local(terms.binding.let(name, type_val))
-- local arg = nil
-- args = cons(args, arg)
end
if ok and continue then
env = type_env
args = cons(args, type_val)
names = names:copy()
names:append(name)
end
print("arg", ok, continue, name, type_val, type_env)
--error "TODO use ascribed_name results"

syntax = tail
end
print("moving on to return type")
ok, continue = true, true
local shadowed, env = env:enter_block()
env = env:bind_local(terms.binding.annotated_lambda("#arg", 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
ok, head, tail = syntax:match({ metalang.ispair(metalang.accept_handler) }, metalang.failure_handler, env)
print(env)
if not ok then
break
end

ok, continue, name, type_val, type_env = head:match({
metalang.isnil(function()
return true, false
end),
ascribed_name(function(ok, ...)
return ok, true, ...
end, env, build_type_term(results), names),
}, metalang.failure_handler, env)
print("result", ok, continue, name, type_val, type_env)

if ok and continue then
env = type_env
results = cons(results, type_val)
names = names:copy()
names:append(name)
end

if not ok then
return false, continue
end

syntax = tail
end

local env, fn_res_term = env:exit_block(build_type_term(results), shadowed)
local fn_type_term = terms.inferrable_term.qtype(
unrestricted_term,
terms.inferrable_term.pi(
build_type_term(args),
terms.inferrable_term.typed(
terms.value.param_info_type,
usage_array(),
terms.typed_term.literal(
terms.value.param_info(
terms.value.visibility(
terms.visibility.explicit
)
)
)
),
fn_res_term,
terms.inferrable_term.typed(
terms.value.result_info_type,
usage_array(),
terms.typed_term.literal(
terms.value.result_info(
terms.value.purity(
terms.purity.pure
)
)
)
)
)
)
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"
end
return true, fn_type_term, env
end, "forall_type_impl")

-- TODO: abstract so can reuse for func type and prim func type
---@param syntax any
---@param env Environment
---@return boolean
---@return unknown
---@return unknown|nil
local function forall_type_impl(syntax, env)
print("in forall_type_impl")
local ok, fn_type_term, env =
syntax:match({ forall_type_impl_reducer(metalang.accept_handler, env) }, metalang.failure_handler, env)
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"
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

--local ok,
end

---@param syntax any
---@param env Environment
---@return boolean
---@return unknown
---@return unknown|nil
local function lambda_impl(syntax, env)
local value_array = gen.declare_array(terms.value)
local inf_array = gen.declare_array(terms.inferrable_term)
local usage_array = gen.declare_array(gen.builtin_number)
local string_array = gen.declare_array(gen.builtin_string)
local function tup_cons(...)
return terms.inferrable_term.tuple_cons(inf_array(...))
end
local function cons(...)
return terms.inferrable_term.enum_cons(terms.value.tuple_defn_type, "cons", tup_cons(...))
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(
unrestricted_term,
terms.inferrable_term.tuple_type(args)
)
end

local ok, params_group, tail = syntax:match(
{
metalang.listtail(
function(_, thr, tail, ...)
return true, {names = thr.names, types = build_type_term(thr.args), env = thr.env}, tail
end,
metalang.list_many_threaded(
function(_, col, thr)
return true, thr
end,
function(thread)
return ascribed_name(
function(_, name, typ, env)
local names = thread.names:copy()
names:append(name)
return true, {name = name, type = typ}, {
names = names,
args = cons(thread.args, typ),
env = env
}
end,
thread.env,
build_type_term(thread.args),
thread.names
)
end, {
names = string_array(),
args = empty,
env = env
})
)
},
metalang.failure_handler,
nil
)
if not ok then return ok, params_group end

local shadow, inner_env = env:enter_block()
inner_env = inner_env:bind_local(terms.binding.annotated_lambda("#arg", params_group.types))
local _, arg = inner_env:get("#arg")
inner_env = inner_env:bind_local(terms.binding.tuple_elim(params_group.names, arg))
local ok, expr, env = tail:match({exprs.block(metalang.accept_handler, inner_env)}, metalang.failure_handler, nil)
if not ok then return ok, expr end
local resenv, term = env:exit_block(expr, shadow)
return true, term, resenv
end


local value = terms.value
local typed = terms.typed_term

local usage_array = gen.declare_array(gen.builtin_number)
local val_array = gen.declare_array(value)
local function startype_impl(syntax, env)
local ok, level_val = syntax:match(
{
metalang.listmatch(
metalang.isvalue(metalang.accept_handler)
)
}
)
if not ok then return ok, level_val end
if level_val.type ~= "f64" then
return false, "literal must be a number for type levels"
end
if level_val.val % 1 ~= 0 then
return false, "literal must be an integer for type levels"
end
local term = terms.inferrable_term.typed(
terms.typed_term.star(level_val.val + 1),
usage_array(),
terms.typed_term.star(level_val.val)
)

return true, term, env
end

local function lit_term(val, typ)
return terms.inferrable_term.typed(typ, usage_array(), terms.typed_term.literal(val))
end
Expand Down Expand Up @@ -497,6 +765,10 @@ local core_operations = {
unrestricted(value.prim_type_type),
unrestricted(value.star(1))),
["prim-func-type"] = exprs.primitive_operative(prim_func_type_impl),
type = lit_term(value.star(1), value.star(0)),
type_ = exprs.primitive_operative(startype_impl),
["forall"] = exprs.primitive_operative(forall_type_impl),
lambda = exprs.primitive_operative(lambda_impl),
box = lit_term(
value.closure(
typed.tuple_elim(
Expand Down
Loading

0 comments on commit 87cd317

Please sign in to comment.