blr-lang 0.1.0

use expect_test::{Expect, expect};
use test_log::test;

use super::{builder::ExprBuilder, items::ItemSource, *};

use crate::{compiler::parse, debug_alt, runtime::binary};

fn test_convert(src: &str, expect: Expect) {
    let module = parse(src).expect("source should parse");
    debug_alt!(module, "ast");
    let mut item_source = ItemSource::default();
    binary::register_binary_operator_functions(&mut item_source);
    let semantic = super::lower(module, &mut item_source, "main");
    expect.assert_debug_eq(&semantic);
}

fn test_infer(src: &str, expect: Expect) {
    let module = parse_module(src).expect("source should parse");
    let mut item_source = ItemSource::default();
    binary::register_binary_operator_functions(&mut item_source);
    let typed = super::type_infer_with_items(item_source, module);
    expect.assert_debug_eq(&typed);
}

#[test]
fn precedence_01() {
    test_convert(
        "1 + 2 * 3",
        expect![[r#"
            (mod
              (pub
                main
                (abs
                  0
                  (app
                    (itm (id 0) (symbol std::ops +))
                    (i 1)
                    (app (itm (id 2) (symbol std::ops *)) (i 2) (i 3))))
                (tsh (fn (unit) (tvar 0)) row typ (tvar 0))))
        "#]],
    );
}

#[test]
fn precedence_30() {
    test_convert(
        "let a = 1;
        let b = 2;
        let c = 3;
        a .. b >> c()",
        expect![[r#"
            (mod
              (pub
                main
                (abs
                  0
                  (app
                    (abs
                      1
                      (app
                        (abs 2 (app (abs 3 (app (var 3) (cat (var 1) (var 2)))) (i 3)))
                        (i 2)))
                    (i 1)))
                (tsh (fn (unit) (tvar 0)) row typ (tvar 0))))
        "#]],
    );
}

#[test]
fn label_unlabel() {
    test_convert(
        "{a:1,b:3}.a",
        expect![[r#"
            (mod
              (pub
                main
                (abs 0 (ulb a (prj (cat (lbl a (i 1)) (lbl b (i 3))))))
                (tsh (fn (unit) (tvar 0)) row typ (tvar 0))))
        "#]],
    );
}

#[test]
fn abstraction_0() {
    test_convert(
        "fn (x) => x",
        expect![[r#"
            (mod (pub main (abs 0 1 (var 1)) (tsh (fn (unit) (tvar 0)) row typ (tvar 0))))
        "#]],
    );
}
#[test]
fn abstraction_1() {
    test_convert(
        "fn (x, y, z) => x",
        expect![[r#"
            (mod
              (pub main (abs 0 1 2 3 (var 1)) (tsh (fn (unit) (tvar 0)) row typ (tvar 0))))
        "#]],
    );
}

#[test]
fn products_0() {
    test_convert(
        "let r = {a:1, b:1}; r.b",
        expect![[r#"
            (mod
              (pub
                main
                (abs
                  0
                  (app (abs 1 (ulb b (prj (var 1)))) (cat (lbl a (i 1)) (lbl b (i 1)))))
                (tsh (fn (unit) (tvar 0)) row typ (tvar 0))))
        "#]],
    );
}
#[test]
#[ignore]
fn polymorphic_add() {
    test_infer(
        "(mod (pub main (app (abs 0
            (app (itm 0 std_ops add) (f 1.0) (f 1.0)))
            (app (itm 0 std_ops add) (i 1) (i 1)))))",
        expect![[r#"
            Ok(
                └─┐tmd
                  └─┐tni 0  main
                    ├─┐sch
                    │ ├─ tvs
                    │ ├─ rows
                    │ ├─ evs
                    │ └─ typ flt
                    └─┐app n11
                      ├─┐abs n5
                      │ ├─┐tdv
                      │ │ ├─ var n5 v0
                      │ │ └─ typ int
                      │ └─┐app n4
                      │   ├─┐app n3
                      │   │ ├─ itm n0 0 std_ops add
                      │   │ └─ 1 n1
                      │   └─ 1 n2
                      └─┐app n10
                        ├─┐app n9
                        │ ├─ itm n6 0 std_ops add
                        │ └─ 1 n7
                        └─ 1 n8
    
                ,
            )
        "#]],
    );
}

#[test]
#[ignore]
fn infer_products_0() {
    test_infer(
        "(mod (pub main (app (abs 0 (ulb b (prj (var 0)))) (cat (lbl a (i 1)) (lbl b (i 1))))))",
        expect![[r#"
            Ok(
                └─┐tmd
                  └─┐tni 0  main
                    ├─┐sch
                    │ ├─ tvs
                    │ ├─ rows
                    │ ├─ evs
                    │ └─ typ int
                    └─┐app n9
                      ├─┐abs n3
                      │ ├─┐tdv
                      │ │ ├─ var n3 v0
                      │ │ └─┐typ
                      │ │   └─┐prd
                      │ │     └─┐row
                      │ │       └─┐cld
                      │ │         ├─┐a
                      │ │         │ └─ typ int
                      │ │         └─┐b
                      │ │           └─ typ int
                      │ └─┐ubl n2 b
                      │   └─┐prj n1
                      │     └─┐tdv
                      │       ├─ var n0 v0
                      │       └─┐typ
                      │         └─┐prd
                      │           └─┐row
                      │             └─┐cld
                      │               ├─┐a
                      │               │ └─ typ int
                      │               └─┐b
                      │                 └─ typ int
                      └─┐cat n8
                        ├─┐lbl n5 a
                        │ └─ 1 n4
                        └─┐lbl n7 b
                          └─ 1 n6
    
                ,
            )
        "#]],
    );
}

macro_rules! set {
        () => {{ BTreeSet::new() }};
        ($($ele:expr),*) => {{
            let mut tmp = BTreeSet::new();
            $(tmp.insert($ele);)*
            tmp
        }};
    }

//#[test]
//fn infers_k_combinator() {
//    let x = Var(0);
//    let y = Var(1);
//    let b = ExprBuilder::default();
//    let expr = b.funs([x, y], b.var(x));
//
//    let ty_chk = type_infer(expr).expect("Type inference to succeed");
//
//    let a = TypeVar(0);
//    let b = TypeVar(1);
//    assert_eq!(
//        ty_chk.scheme,
//        TypeScheme {
//            unbound_tys: set![a, b],
//            unbound_rows: set![],
//            evidence: vec![],
//            ty: Type::fun(Type::Var(a), Type::fun(Type::Var(b), Type::Var(a))),
//        }
//    );
//}
//
//#[test]
//fn infers_s_combinator() {
//    let x = Var(0);
//    let y = Var(1);
//    let z = Var(2);
//    let b = ExprBuilder::default();
//    let expr = b.funs(
//        [x, y, z],
//        b.app(b.app(b.var(x), b.var(z)), b.app(b.var(y), b.var(z))),
//    );
//
//    let ty_chk = type_infer(expr).expect("Type inference to succeed");
//
//    let a = TypeVar(0);
//    let b = TypeVar(1);
//    let c = TypeVar(2);
//    let x_ty = Type::fun(Type::Var(a), Type::fun(Type::Var(b), Type::Var(c)));
//    let y_ty = Type::fun(Type::Var(a), Type::Var(b));
//    assert_eq!(
//        ty_chk.scheme,
//        TypeScheme {
//            unbound_tys: set![a, b, c],
//            unbound_rows: set![],
//            evidence: vec![],
//            ty: Type::fun(x_ty, Type::fun(y_ty, Type::fun(Type::Var(a), Type::Var(c)))),
//        }
//    )
//}
//
//#[test]
//fn type_infer_fails() {
//    let x = Var(0);
//    let b = ExprBuilder::default();
//    let expr = b.locals([(x, b.int(1))], b.app(b.var(x), b.int(3)));
//
//    let ty_chk_res = type_infer(expr);
//
//    assert_eq!(
//        ty_chk_res,
//        Err(TypeError {
//            kind: TypeErrorKind::TypeNotEqual((
//                Type::fun(Type::Int, Type::Unifier(TypeUniVar { id: 1 })),
//                Type::Int
//            )),
//            node_id: NodeId(1)
//        })
//    );
//}

//#[test]
//#[ignore]
//fn test_wand_combinator() {
//    let b = ExprBuilder::default();
//    let expr = b.make_funs(|[m, n]| b.unlabel(b.project(b.concatenate(b.var(m), b.var(n))), "x"));
//
//    let ty_chk = type_infer(expr).expect("Type inference to succeed");
//
//    let m = RowVar(0);
//    let n = RowVar(1);
//    let goal = RowVar(2);
//    let a = TypeVar(0);
//    assert_eq!(
//        ty_chk.scheme,
//        TypeScheme {
//            unbound_rows: set![n, RowVar(3), m, goal],
//            unbound_tys: set![a],
//            evidence: vec![
//                Evidence::RowEquation {
//                    left: Row::Open(m),
//                    right: Row::Open(n),
//                    goal: Row::Open(goal)
//                },
//                Evidence::RowEquation {
//                    left: Row::Closed(single_row("x", Type::Var(a))),
//                    right: Row::Open(RowVar(3)),
//                    goal: Row::Open(goal)
//                }
//            ],
//            ty: Type::fun(
//                Type::Prod(Row::Open(m)),
//                Type::fun(Type::Prod(Row::Open(n)), Type::Var(a))
//            )
//        }
//    );
//}

#[test]
fn type_check_items() {
    let b = ExprBuilder::default();
    let expr = b.make_funs(|[m, n]| b.unlabel(b.project(b.concatenate(b.var(m), b.var(n))), "x"));

    let r = RowVar(0);
    let s = RowVar(1);
    let w = RowVar(2);
    let a = TypeVar(0);
    let scheme = TypeScheme {
        unbound_rows: set![r, s, w, RowVar(3)],
        unbound_tys: set![a],
        evidence: vec![
            Evidence::RowEquation {
                left: Row::Open(r),
                right: Row::Open(s),
                goal: Row::Open(w),
            },
            Evidence::RowEquation {
                left: Row::single("x", Type::Var(a)),
                right: Row::Open(RowVar(3)),
                goal: Row::Open(w),
            },
        ],
        typ: Type::abstraction(
            Type::Prod(Row::Open(r)),
            Type::abstraction(Type::Prod(Row::Open(s)), Type::Var(a)),
        ),
    };

    let out = type_check(expr, scheme);

    assert!(out.is_ok());
}

#[test]
fn type_check_item_fails() {
    let a = TypeVar(0);

    let b = ExprBuilder::default();
    let expr = b.make_funs(|[x, y]| b.app(b.var(y), b.var(x)));
    let signature = TypeScheme {
        unbound_tys: set![a],
        unbound_rows: set![],
        evidence: vec![],
        typ: Type::abstraction(
            Type::Var(a),
            Type::abstraction(Type::abstraction(Type::Int, Type::Int), Type::Int),
        ),
    };

    let out = type_check(expr, signature);

    assert_eq!(
        out,
        Err(TypeError {
            kind: TypeErrorKind::TypeNotEqual((Type::Var(a), Type::Int)),
            node_id: NodeId(0),
        })
    );
}

#[test]
fn product_as_parameter() {
    let module = parse_module(
        "(mod (pub main (app (abs 0 (cat (lbl a (ulb x (prj (var 0)))) (lbl b (ulb y (prj (var 0)))))) (cat (lbl x (i 2)) (lbl y (i 1)))) (tsh (prd (cld a (int) b (int))) row typ)))",
    )
    .unwrap();

    let out = type_infer_with_items(ItemSource::default(), module);
    expect![[r#"
        Ok(
            (typed_mod
              ((id 4)
                (pub
                  main
                  (app
                    (abs
                      (var 0)
                      (cat (lbl a (ulb x (prj (var 0)))) (lbl b (ulb y (prj (var 0))))))
                    (cat (lbl x (i 2)) (lbl y (i 1))))
                  (tsh (prd (cld a (int) b (int))) row typ)
                  row_to_ev
                  ((nid 1) (equation (cld x (int)) (cld y (int)) (cld x (int) y (int))))
                  ((nid 5) (equation (cld y (int)) (cld x (int)) (cld x (int) y (int))))
                  ((nid 8) (equation (cld a (int)) (cld b (int)) (cld a (int) b (int))))
                  ((nid 14) (equation (cld x (int)) (cld y (int)) (cld x (int) y (int))))
                  branch_to_ret
                  wrappers))),
        )
    "#]]
    .assert_debug_eq(&out);
}

#[test]
fn product_parameter_func() {
    let module = parse_module(
        "(mod (pub main (app (abs 0 1 (app (var 0) (var 1))) (abs 0 (cat (lbl a (ulb x (prj (var 0)))) (lbl b (ulb y (prj (var 0)))))) (cat (lbl x (i 2)) (lbl y (i 1)))) (tsh (prd (cld a (int) b (int))) row typ)))",
    )
    .unwrap();

    let out = type_infer_with_items(ItemSource::default(), module);
    expect![[r#"
        Ok(
            (typed_mod
              ((id 4)
                (pub
                  main
                  (app
                    (abs (var 0) (var 1) (app (var 0) (var 1)))
                    (abs
                      (var 0)
                      (cat (lbl a (ulb x (prj (var 0)))) (lbl b (ulb y (prj (var 0))))))
                    (cat (lbl x (i 2)) (lbl y (i 1))))
                  (tsh (prd (cld a (int) b (int))) row typ)
                  row_to_ev
                  ((nid 6) (equation (cld x (int)) (cld y (int)) (cld x (int) y (int))))
                  ((nid 10) (equation (cld y (int)) (cld x (int)) (cld x (int) y (int))))
                  ((nid 13) (equation (cld a (int)) (cld b (int)) (cld a (int) b (int))))
                  ((nid 19) (equation (cld x (int)) (cld y (int)) (cld x (int) y (int))))
                  branch_to_ret
                  wrappers))),
        )
    "#]]
    .assert_debug_eq(&out);
}