Skip to content

Commit

Permalink
add unwrap
Browse files Browse the repository at this point in the history
  • Loading branch information
ErikMcClure committed Jan 15, 2025
1 parent 775ef04 commit 10379d0
Show file tree
Hide file tree
Showing 2 changed files with 31 additions and 32 deletions.
56 changes: 24 additions & 32 deletions prelude.alc
Original file line number Diff line number Diff line change
Expand Up @@ -11,13 +11,6 @@ let universe = type_(9, 1)
lambda (x : T)
wrap T x

let foo = debug-track
lambda_implicit (a : type)
lambda_implicit (b : type)
lambda (c : a, d : b)
c
let test = foo(1, 2)

let implicit-wrap = lambda_curry ((T : type_(10, 0)))
lambda (x : T)
wrap T x
Expand Down Expand Up @@ -153,29 +146,28 @@ let _&_ =
wrapped (forall (a : U, b : U) -> (res : U))

let covariant =
debug-track
lambda_curry (U : type_(9, 1), a : U)
unwrap
intrinsic
""""
local string_array = terms_gen.declare_array(terms_gen.builtin_string)
return terms.value.closure(
"#covariant-args",
terms.typed_term.tuple_elim(
string_array("base"),
terms.typed_term.bound_variable(1),
1,
terms.typed_term.variance_cons(
terms.typed_term.literal(
terms.value.host_value(true)
),
terms.typed_term.bound_variable(2)
)
),
terms.runtime_context()
)
:
wrapped (forall ((rel : srel(a))) -> (res : variance(a)))
lambda_curry (U : type_(9, 1), a : U)
unwrap
intrinsic
""""
local string_array = terms_gen.declare_array(terms_gen.builtin_string)
return terms.value.closure(
"#covariant-args",
terms.typed_term.tuple_elim(
string_array("base"),
terms.typed_term.bound_variable(1),
1,
terms.typed_term.variance_cons(
terms.typed_term.literal(
terms.value.host_value(true)
),
terms.typed_term.bound_variable(2)
)
),
terms.runtime_context()
)
:
wrapped (forall ((rel : srel(a))) -> (res : variance(a)))

let contravariant =
lambda_curry (U : type_(9, 1), a : U)
Expand Down Expand Up @@ -327,7 +319,7 @@ let new-host-type-family = lambda (unique-id : host-unique-id, signature : type_
signature_ : wrapped(type_(1, 0)),
variance_ : wrapped(host-family-sig-variances(unwrap(signature_))))
->
((family : wrapped(signature)))
(family : wrapped(unwrap(signature_)))
let (family) = inner(unique-id, wrap(signature), wrap(variance))
unwrap(family)
let new-host-type = lambda (unique-id : host-unique-id)
Expand All @@ -338,7 +330,7 @@ let new-host-type = lambda (unique-id : host-unique-id)

let host-array-type = new-host-type-family new-host-unique-id("array")
forall ((T : host-type)) -> (T : host-type)
tuple-of-implicit debug-track(covariant(subtyping))
tuple-of-implicit covariant(subtyping)

let host-array-new = lambda (T : host-type)
let inner = intrinsic
Expand Down
7 changes: 7 additions & 0 deletions tests/implicit.alc
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,13 @@ let id = lambda_implicit (T : type_(10, 0))
lambda (x : T)
x

let foo =
lambda_implicit (a : type)
lambda_implicit (b : type)
lambda (c : a, d : b)
c
let test = foo(1, 2)

# TODO: test this when tuple-desc can do more than just star-0
#let point = lambda_implicit (U : type_(10))
# lambda (T : U)
Expand Down

0 comments on commit 10379d0

Please sign in to comment.