summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/resolve/hir.rs
blob: 9256425bd657db7a341e7e7860432e4d88f7ab81 (plain)
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
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
use crate::error::TypeError;
use crate::semantics::{type_with, NameEnv, Nir, NzEnv, Tir, TyEnv, Type};
use crate::syntax::{Expr, ExprKind, Span, V};
use crate::ToExprOptions;

/// Stores an alpha-normalized variable.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct AlphaVar {
    idx: usize,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub enum HirKind {
    /// A resolved variable (i.e. a DeBruijn index)
    Var(AlphaVar),
    /// Result of resolving an import.
    Import(Hir, Type),
    // Forbidden ExprKind variants: Var, Import, Completion
    Expr(ExprKind<Hir>),
}

// An expression with resolved variables and imports.
#[derive(Debug, Clone)]
pub struct Hir {
    kind: Box<HirKind>,
    span: Span,
}

impl AlphaVar {
    pub fn new(idx: usize) -> Self {
        AlphaVar { idx }
    }
    pub fn idx(self) -> usize {
        self.idx
    }
}

impl Hir {
    pub fn new(kind: HirKind, span: Span) -> Self {
        Hir {
            kind: Box::new(kind),
            span,
        }
    }

    pub fn kind(&self) -> &HirKind {
        &*self.kind
    }
    pub fn span(&self) -> Span {
        self.span.clone()
    }

    /// Converts a closed Hir expr back to the corresponding AST expression.
    pub fn to_expr(&self, opts: ToExprOptions) -> Expr {
        hir_to_expr(self, opts, &mut NameEnv::new())
    }
    /// Converts a closed Hir expr back to the corresponding AST expression.
    pub fn to_expr_noopts(&self) -> Expr {
        let opts = ToExprOptions { alpha: false };
        self.to_expr(opts)
    }
    pub fn to_expr_tyenv(&self, env: &TyEnv) -> Expr {
        let opts = ToExprOptions { alpha: false };
        let mut env = env.as_nameenv().clone();
        hir_to_expr(self, opts, &mut env)
    }

    /// Typecheck the Hir.
    pub fn typecheck<'hir>(
        &'hir self,
        env: &TyEnv,
    ) -> Result<Tir<'hir>, TypeError> {
        type_with(env, self, None)
    }
    pub fn typecheck_noenv<'hir>(&'hir self) -> Result<Tir<'hir>, TypeError> {
        self.typecheck(&TyEnv::new())
    }

    /// Eval the Hir. It will actually get evaluated only as needed on demand.
    pub fn eval(&self, env: impl Into<NzEnv>) -> Nir {
        Nir::new_thunk(env.into(), self.clone())
    }
    /// Eval a closed Hir (i.e. without free variables). It will actually get evaluated only as
    /// needed on demand.
    pub fn eval_closed_expr(&self) -> Nir {
        self.eval(NzEnv::new())
    }
}

fn hir_to_expr(hir: &Hir, opts: ToExprOptions, env: &mut NameEnv) -> Expr {
    let kind = match hir.kind() {
        HirKind::Var(v) if opts.alpha => ExprKind::Var(V("_".into(), v.idx())),
        HirKind::Var(v) => ExprKind::Var(env.label_var(*v)),
        HirKind::Import(hir, _) => {
            return hir_to_expr(hir, opts, &mut NameEnv::new())
        }
        HirKind::Expr(e) => {
            let e = e.map_ref_maybe_binder(|l, hir| {
                if let Some(l) = l {
                    env.insert_mut(l);
                }
                let e = hir_to_expr(hir, opts, env);
                if l.is_some() {
                    env.remove_mut();
                }
                e
            });

            match e {
                ExprKind::Lam(_, t, e) if opts.alpha => {
                    ExprKind::Lam("_".into(), t, e)
                }
                ExprKind::Pi(_, t, e) if opts.alpha => {
                    ExprKind::Pi("_".into(), t, e)
                }
                e => e,
            }
        }
    };
    Expr::new(kind, hir.span())
}

impl std::cmp::PartialEq for Hir {
    fn eq(&self, other: &Self) -> bool {
        self.kind == other.kind
    }
}
impl std::cmp::Eq for Hir {}