1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88

use crate::lang::env::Env;
use crate::lang::env::EnvEntry::*;
use crate::lang::error::TypeError;
use crate::lang::ValueOrigin::FreeSub;
use crate::lang::{PartialExpr, TcEnv};
use crate::lang::UnionIndex;
use std::collections::HashMap;

impl TcEnv {
    /// Expect `io` to be equal to `Type`.
    pub fn expect_beq_type(&mut self, io: UnionIndex, s: &Env) {
        let (i, s) = self.beta_reduce_head(io, s.clone());
        match self.values[i.0] {
            PartialExpr::Type => {}
            PartialExpr::Free => {
                self.values[i.0] = PartialExpr::Type;
                if !self.handle_constraints(i, &s) {
                    self.errors.push(TypeError::ExpectType(io));
                }
            }
            _ => {
                self.errors.push(TypeError::ExpectType(io));
            }
        }
        self.toxic_values.clear();
    }

    /// Expect `f` to be a function type with argument type `i_at` both valid in `s`.
    /// `rt` should be free.
    pub fn expect_beq_fn_type(&mut self, ft: UnionIndex, at: UnionIndex, rt: UnionIndex, s: &Env) {
        let (fr, sr) = self.beta_reduce_head(ft, s.clone());
        
        match self.values[fr.0] {
            PartialExpr::FnType(f_at, f_rt) => {
                if !self.expect_beq_internal((f_at, &sr, &mut HashMap::new()), (at, s, &mut HashMap::new())) {
                    self.errors.push(TypeError::ExpectFnArg {
                        function_type: ft,
                        function_arg_type: f_at,
                        arg_type: at,
                    })
                }

                let mut var_map1 = HashMap::new();
                let mut var_map2 = HashMap::new();
                let id = self.new_tc_id();
                var_map1.insert(id, sr.len());
                var_map2.insert(id, s.len());
                let is_beq_free = self.expect_beq_free(
                    (f_rt, &sr.cons(RType(id)), &mut var_map1),
                    (rt, &s.cons(RType(id)), &mut var_map2),
                );
                debug_assert!(is_beq_free);
            }
            PartialExpr::Free => {
                let f_at = self.store(PartialExpr::Free, FreeSub(fr));
                let f_rt = self.store(PartialExpr::Free, FreeSub(fr));
                self.values[fr.0] = PartialExpr::FnType(f_at, f_rt);

                // TODO this won't give good errors :c
                // Figure out a way to keep the context of this constraint, maybe using tokio?
                if !self.handle_constraints(fr, &sr) {
                    self.errors.push(TypeError::ExpectFnArg {
                        function_type: ft,
                        function_arg_type: f_at,
                        arg_type: at,
                    })
                }

                let is_beq_free = self.expect_beq_free((at, s, &mut HashMap::new()), (f_at, &sr, &mut HashMap::new()));
                debug_assert!(is_beq_free);

                let mut var_map1 = HashMap::new();
                let mut var_map2 = HashMap::new();
                let id = self.new_tc_id();
                var_map1.insert(id, sr.len());
                var_map2.insert(id, s.len());
                let is_beq_free = self.expect_beq_free(
                    (f_rt, &sr.cons(RType(id)), &mut var_map1),
                    (rt, &s.cons(RType(id)), &mut var_map2),
                );
                debug_assert!(is_beq_free);
            }
            _ => self.errors.push(TypeError::ExpectFn(ft)),
        }

        self.toxic_values.clear();
    }
}