diff options
Diffstat (limited to 'dhall/src/semantics/resolve/hir.rs')
-rw-r--r-- | dhall/src/semantics/resolve/hir.rs | 135 |
1 files changed, 135 insertions, 0 deletions
diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs new file mode 100644 index 0000000..2f3464a --- /dev/null +++ b/dhall/src/semantics/resolve/hir.rs @@ -0,0 +1,135 @@ +use crate::error::TypeError; +use crate::semantics::{type_with, NameEnv, Nir, NzEnv, Tir, TyEnv, Type}; +use crate::syntax::{Expr, ExprKind, Span, V}; +use crate::{NormalizedExpr, ToExprOptions}; + +/// Stores an alpha-normalized variable. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +pub struct AlphaVar { + idx: usize, +} + +#[derive(Debug, Clone, PartialEq, Eq)] +pub(crate) 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(crate) struct Hir { + kind: Box<HirKind>, + span: Span, +} + +impl AlphaVar { + pub(crate) fn new(idx: usize) -> Self { + AlphaVar { idx } + } + pub(crate) 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) -> NormalizedExpr { + 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) -> NormalizedExpr { + let opts = ToExprOptions { alpha: false }; + self.to_expr(opts) + } + pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr { + 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) + } + + /// 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()) + } + /// Eval a closed Hir fully and recursively; + pub fn rec_eval_closed_expr(&self) -> Nir { + let val = self.eval_closed_expr(); + val.normalize(); + val + } +} + +fn hir_to_expr( + hir: &Hir, + opts: ToExprOptions, + env: &mut NameEnv, +) -> NormalizedExpr { + 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 let Some(_) = l { + 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 {} |