use lib {}

// Bool tests

#[test]
def test_bool_true : Bool :=
    if true then true else false

#[test]
def test_bool_false : Bool :=
    if false then false else true

#[test]
def test_bool_not_true : Bool :=
    if not true then false else true

#[test]
def test_bool_not_false : Bool :=
    if not false then true else false

#[test]
def test_bool_and : Bool :=
    true && true

#[test]
def test_bool_and_false : Bool :=
    if true && false then false else true

#[test]
def test_bool_or : Bool :=
    if false || true then true else false

#[test]
def test_bool_or_false : Bool :=
    if false || false then false else true

// Numeric literal tests

#[test]
def test_hex_literal_i64 : Bool :=
    0xFF == 255

#[test]
def test_hex_literal_u32_suffix : Bool :=
    0xBADBEEFu32 == 195935983u32

#[test]
def test_hex_literal_negative : Bool :=
    -0x10 == -16

#[test]
def test_hex_literal_uppercase_prefix : Bool :=
    0XCAFE == 51966

// I64 tests

#[test]
def test_i64_add : Bool :=
    1 + 2 == 3

#[test]
def test_i64_sub : Bool :=
    5 - 3 == 2

#[test]
def test_i64_mul : Bool :=
    4 * 3 == 12

#[test]
def test_i64_div : Bool :=
    10 / 2 == 5

#[test]
def test_i64_add_zero : Bool :=
    0 + 0 == 0

#[test]
def test_i64_mul_zero : Bool :=
    42 * 0 == 0

#[test]
def test_i64_sub_order : Bool :=
    10 - 3 == 7

// List tests

def empty_list : List I64 :=
    List.empty

#[test]
def test_list_empty : Bool :=
    match empty_list {
        empty => true,
        cons _ _ => false
    }

#[test]
def test_list_not_empty : Bool :=
    not (List.is_empty [1, 2, 3])

#[test]
def test_get_0 : Bool :=
    some 1 == (List.get 0 [1, 2, 3])

#[test]
def test_get_1 : Bool :=
    some 2 == (List.get 1 [1, 2, 3])

#[test]
def test_get_2 : Bool :=
    some 3 == (List.get 2 [1, 2, 3])

#[test]
def test_get_max : Bool :=
    none == (List.get 4 [1, 2, 3])

#[test]
def test_get_neg1 : Bool :=
    none == (List.get (-1) [1, 2, 3])

#[test]
def test_get_empty : Bool :=
    none == (List.get 0 ([] : List I64))

def first_of_empty : Option I64 :=
    List.first List.empty

#[test]
def test_list_first_none : Bool :=
    match first_of_empty {
        some _ => false,
        none => true
    }

#[test]
def test_list_single : Bool :=
    not (List.is_empty [42])

// Option tests

def none_opt : Option I64 :=
    none

#[test]
def test_option_none : Bool :=
    match none_opt {
        some _ => false,
        none => true
    }

#[test]
def test_option_get_or_default_some : Bool :=
    Option.get_or_default 0 (some 42) == 42

#[test]
def test_option_get_or_default_none : Bool :=
    Option.get_or_default 99 none_opt == 99

// Result tests

def err_val : Result String I64 :=
    err "fail"

#[test]
def test_result_err : Bool :=
    match err_val {
        ok _ => false,
        err _ => true
    }

// String tests

#[test]
def test_string_length : Bool :=
    String.length "hello" == 5

#[test]
def test_string_empty_length : Bool :=
    String.length "" == 0

#[test]
def test_string_is_empty : Bool :=
    String.is_empty ""

#[test]
def test_string_not_empty : Bool :=
    not (String.is_empty "hello")

// Nat tests

#[test]
def test_nat_zero : Bool :=
    match Nat.zero {
        zero => true,
        succ _ => false
    }

#[test]
def test_nat_succ : Bool :=
    match Nat.succ Nat.zero {
        zero => false,
        succ n => match n {
            zero => true,
            succ _ => false
        }
    }

// Operator tests

#[test]
def test_pipe_forward : Bool :=
    5 |> fn x => x + 1 |> fn x => x == 6

def double (x : I64) : I64 :=
    x * 2

#[test]
def test_apply_back : Bool :=
    double 3 == 6

// String slice/drop tests

#[test]
def test_string_slice_basic : Bool :=
    String.slice "hello" 0 3 == "hel"

#[test]
def test_string_slice_middle : Bool :=
    String.slice "hello" 1 3 == "ell"

#[test]
def test_string_slice_past_end : Bool :=
    String.slice "hi" 0 10 == "hi"

#[test]
def test_string_drop_basic : Bool :=
    String.drop 3 "hello" == "lo"

#[test]
def test_string_drop_none : Bool :=
    String.drop 0 "hello" == "hello"

#[test]
def test_string_drop_all : Bool :=
    String.drop 10 "hi" == ""

// String starts_with tests

#[test]
def test_string_starts_with : Bool :=
    String.starts_with "hel" "hello"

#[test]
def test_string_not_starts_with : Bool :=
    not (String.starts_with "world" "hello")

#[test]
def test_string_starts_with_empty : Bool :=
    String.starts_with "" "hello"

#[test]
def test_empty_starts_with_empty : Bool :=
    String.starts_with "" ""

// Unit tests

#[test]
def test_unit : Bool :=
    match unit {
        unit => true
    }

// Struct tests

struct Point {
    x: I64,
    y: I64,
}

#[test]
def test_struct_construct_and_match : Bool :=
    let pt : Point := { x := 1, y := 2 } in
    match pt {
        mk x y => true
    }



#[test]
def test_eq_in_plain_match : Bool :=
    match List.cons 5 List.empty {
        cons x _ => x == 5
    }

#[test]
def test_struct_eq_in_match : Bool :=
    let pt : Point := { x := 1, y := 2 } in
    match pt {
        mk x y => x + y == 3
    }

#[test]
def test_struct_wildcard : Bool :=
    let pt : Point := { x := 10, y := 20 } in
    match pt {
        mk x _ => x == 10
    }

struct DefaultedBox {
    w: I64,
    h: I64 := 100,
}

#[test]
def test_struct_default_value : Bool :=
    let r : DefaultedBox := { w := 50 } in
    match r {
        mk w h => h == 100
    }

#[test]
def test_struct_update_syntax : Bool :=
    let p1 : Point := { x := 1, y := 2 } in
    let p2 : Point := { p1 with x := 10 } in
    match p2 {
        mk x y => x == 10 && y == 2
    }

// Optics/indexed-monad tests: `Lens`/`IndexedMonad` compiling at all is
// already exercised for free by every OTHER test in this file (any real
// checker regression in either would fail the whole file to load, not
// just one isolated test) -- `optics_tests.mo` is where `Lens`'s actual
// behavior (get/set/over) gets real, non-trivial runtime coverage.

// Nat arithmetic tests

#[test]
def test_nat_add_zero : Bool :=
    Nat.eq (Nat.add Nat.zero Nat.zero) Nat.zero

#[test]
def test_nat_add_one_one : Bool :=
    let one := Nat.succ Nat.zero in
    let two := Nat.succ (Nat.succ Nat.zero) in
    Nat.eq (Nat.add one one) two

#[test]
def test_nat_sub_self : Bool :=
    let one := Nat.succ Nat.zero in
    Nat.eq (Nat.sub one one) Nat.zero

#[test]
def test_nat_eq_false : Bool :=
    Bool.not (Nat.eq Nat.zero (Nat.succ Nat.zero))

// Vec dependent type tests

#[test]
def test_vec_nil_match : Bool :=
    match Vec.nil {
        nil => true
    }

#[test]
def test_vec_nil_type : Bool :=
    let v : Vec Nat.zero I64 := Vec.nil in
    match v {
        nil => true
    }

#[test]
def test_vec_cons_type : Bool :=
    let v : Vec (Nat.succ Nat.zero) I64 := Vec.cons 42 Vec.nil in
    match v {
        cons h t => h == 42
    }

#[test]
def test_vec_cons_pattern : Bool :=
    let v : Vec (Nat.succ Nat.zero) I64 := Vec.cons 42 Vec.nil in
    match v {
        cons h t => h == 42
    }

#[test]
def test_vec_cons_head : Bool :=
    match Vec.cons 42 Vec.nil {
        cons h t => h == 42
    }

#[test]
def test_vec_cons_tail_nil : Bool :=
    match Vec.cons 42 Vec.nil {
        cons h t =>
            match t {
                nil => true
            }
    }

// Tuple tests
//
// No separate "construct only" tests here -- `test_tuple_pair_match`/
// `test_tuple_triple_nested_match` below build the exact same tuples and
// additionally verify their contents via `match`, so a construct-only
// twin would check strictly less while covering nothing new.

#[test]
def test_tuple_pair_match : Bool :=
    let t : Pair I64 Bool := (1, true) in
    match t {
        Pair.pair a b => (a == 1) && (b == true)
    }

#[test]
def test_tuple_triple_nested_match : Bool :=
    let t : Pair I64 (Pair Bool String) := (1, true, "hi") in
    match t {
        Pair.pair a rest =>
            match rest {
                Pair.pair b c => (a == 1) && (b == true) && (c == "hi")
            }
    }

#[test]
def test_tuple_parens_expr : Bool :=
    let x := (1 + 2) in
    x == 3

#[test]
def test_tuple_nested_expr : Bool :=
    let t : Pair I64 Bool := (1 + 1, 2 == 2) in
    match t {
        Pair.pair a b => (a == 2) && b
    }

#[test]
def test_match_wildcard : Bool :=
    match Option.some 42 {
        some x => x == 42,
        _ => false
    }

#[test]
def test_match_wildcard_fallback : Bool :=
    match Option.none {
        some x => false,
        _ => true
    }

#[test]
def test_match_wildcard_only : Bool :=
    match Option.some 1 {
        _ => true
    }

#[test]
def test_match_wildcard_exact_first : Bool :=
    match Option.some 5 {
        some x => x == 5,
        _ => false
    }

#[test]
def test_match_wildcard_discard_arg : Bool :=
    match Option.some 99 {
        some _ => true,
        _ => false
    }

// -- Id monad tests --

#[test]
def test_id_unwrap : Bool :=
    match Id.run (Id.id true) { true => true, false => false }

#[test]
def test_id_unwrap_false : Bool :=
    match Id.run (Id.id false) { true => false, false => true }

// `Eq.refl`/`Sort`/`Prop`/`Type`-as-value tests below are genuinely
// type-checking-only: `Eq`'s only inhabitant is `refl` and a `Sort`
// value carries no runtime-observable structure at all (see
// `lower_core_ir.rs`'s `IrLit::Sort` -- deliberately opaque), so there is
// nothing further to inspect once construction/annotation type-checks;
// `true` here is the correct body, not a stand-in for a missing
// assertion, the same way a `#[test]` that only needs to confirm "this
// compiles" legitimately can be.

#[test]
def test_eq_refl_apply : Bool :=
    let refx := Eq.refl 1 in
    true

#[test]
def test_eq_refl_apply_str : Bool :=
    let refx := Eq.refl "hello" in
    true

#[test]
def test_eq_refl_type : Bool :=
    let refx : Eq I64 1 1 := Eq.refl 1 in
    true

// -- Sort universe tests —

#[test]
def test_sort_formation : Bool :=
    let _type : Sort 2 := Sort 1 in
    true

#[test]
def test_sort_cumulativity : Bool :=
    let t : Sort 1 := Sort 0 in
    true

#[test]
def test_pi_universe : Bool :=
    let _f : (Sort 1 -> Sort 2) := fn x => x in
    true

// -- Prop/Type/Pred in value position —

#[test]
def test_type_as_value_arg : Bool :=
    let _x : Sort 1 := get_sort Type in
    true

#[test]
def test_prop_as_value_arg : Bool :=
    let _x : Sort 1 := get_sort Prop in
    true

#[test]
def test_pred_as_value_arg : Bool :=
    let _x : Sort 1 := get_sort Pred in
    true

#[test]
def test_id_type_with_prop : Bool :=
    let _x : Sort 0 := get_identity Prop in
    true

#[test]
def test_id_type_with_pred : Bool :=
    let _x : Sort 0 := get_identity Pred in
    true

#[test]
def test_prop_nested_inference : Bool :=
    let _x : Sort 1 := get_identity (get_sort Prop) in
    true

def get_sort {A : Sort 1} (x : Sort 1) : Sort 1 := x

def get_identity {A : Sort 1} (x : A) : A := x

// BOrd Bool tests

#[test]
def test_bord_bool_lt_false_true : Bool :=
    BOrd.lt false true

#[test]
def test_bord_bool_lt_true_false : Bool :=
    Bool.not (BOrd.lt true false)

#[test]
def test_bord_bool_lt_false_false : Bool :=
    Bool.not (BOrd.lt false false)

#[test]
def test_bord_bool_lt_true_true : Bool :=
    Bool.not (BOrd.lt true true)

#[test]
def test_bord_bool_gt_true_false : Bool :=
    BOrd.gt true false

#[test]
def test_bord_bool_gt_false_true : Bool :=
    Bool.not (BOrd.gt false true)

#[test]
def test_bord_bool_gt_true_true : Bool :=
    Bool.not (BOrd.gt true true)

#[test]
def test_bord_bool_gt_false_false : Bool :=
    Bool.not (BOrd.gt false false)

// -- Type propagation tests --

#[test]
def test_match_with_let_annotation : Bool :=
    let result : Option I64 := Option.some 42 in
    match result {
        Option.some x => true,
        Option.none => false
    }

#[test]
def test_do_bind_with_match : IO Bool := do {
    let x <- IO.pure (Option.some 42);
    match x {
        Option.some _ => IO.pure true,
        Option.none => IO.pure false
    }
}

// -- Type inference tests (without annotations) --

#[test]
def test_let_match_no_annotation : Bool :=
    let result := Option.some 42 in
    match result {
        Option.some _ => true,
        Option.none => false
    }

// -- Comonad tests --

#[test]
def test_comonad_id_extract : Bool :=
    Comonad.extract (Id.id 42) == 42

#[test]
def test_comonad_id_duplicate_is_the_same_context_twice : Bool :=
    Id.run (Id.run (Comonad.duplicate (Id.id 42))) == 42

// The lambda parameter is annotated -- its carrier is only known from the
// call's SECOND argument, which the checker has not inferred yet when it
// checks this one, so an unannotated `a` stays a hole and `+` resolves
// against the wildcard-headed `instance [Add A] HAdd A A A` bridge, which
// then calls itself until the driver dies by signal (the same class of bug
// `app_arg_expected_type_from_callee`'s doc comment records for
// `Foldable.foldr`).
#[test]
def test_comonad_id_extend_maps_over_the_context : Bool :=
    Id.run (Comonad.extend (fn (a : Id I64) => Id.run a + 1) (Id.id 41)) == 42

#[test]
def test_comonad_pair_extract_is_the_second_component : Bool :=
    Comonad.extract (Pair.pair 10 3) == 3

#[test]
def test_comonad_pair_duplicate_carries_the_environment_into_both : Bool :=
    match Comonad.duplicate (Pair.pair 10 3) {
        Pair.pair e inner => match inner {
            Pair.pair e2 a => e == 10 && e2 == 10 && a == 3
        }
    }

// Same reason as `test_comonad_id_extend_maps_over_the_context` above: the
// lambda parameter needs an explicit annotation.
#[test]
def test_comonad_pair_extend_applies_with_the_environment_in_scope : Bool :=
    match Comonad.extend (fn (w : Pair I64 I64) => Comonad.extract w + 1) (Pair.pair 10 3) {
        Pair.pair e b => e == 10 && b == 4
    }