From 8264df65c21b5ad508c5faf96c4a1f9d732449cc Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 17 Feb 2020 17:50:22 +0000 Subject: Move hir and resolve into a module --- dhall/src/semantics/resolve/hir.rs | 130 +++++++++++++++++++++++++++++++++++++ 1 file changed, 130 insertions(+) create mode 100644 dhall/src/semantics/resolve/hir.rs (limited to 'dhall/src/semantics/resolve/hir.rs') diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs new file mode 100644 index 0000000..b5db66f --- /dev/null +++ b/dhall/src/semantics/resolve/hir.rs @@ -0,0 +1,130 @@ +use crate::error::TypeError; +use crate::semantics::{type_with, NameEnv, NzEnv, TyEnv, TyExpr, Value}; +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, Hash)] +pub(crate) enum HirKind { + /// A resolved variable (i.e. a DeBruijn index) + Var(AlphaVar), + // Forbidden ExprKind variants: Var, Import, Completion + Expr(ExprKind), +} + +// An expression with resolved variables and imports. +#[derive(Debug, Clone)] +pub(crate) struct Hir { + kind: Box, + 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 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 HIR expr back to the corresponding AST expression. + pub fn to_expr_noopts(&self) -> NormalizedExpr { + let opts = ToExprOptions { + normalize: false, + alpha: false, + }; + self.to_expr(opts) + } + pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr { + let opts = ToExprOptions { + normalize: true, + alpha: false, + }; + let mut env = env.as_nameenv().clone(); + hir_to_expr(self, opts, &mut env) + } + + /// Typecheck the Hir. + pub fn typecheck(&self, env: &TyEnv) -> Result { + 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) -> Value { + Value::new_thunk(env.into(), self.clone()) + } +} + +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::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 {} +impl std::hash::Hash for Hir { + fn hash(&self, state: &mut H) + where + H: std::hash::Hasher, + { + self.kind.hash(state) + } +} -- cgit v1.2.3 From 2f65c02a995f6b6d4c755197fc074782f6bb100d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 17 Feb 2020 18:12:44 +0000 Subject: Rename TyExpr to Tir --- dhall/src/semantics/resolve/hir.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'dhall/src/semantics/resolve/hir.rs') diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs index b5db66f..ae65fff 100644 --- a/dhall/src/semantics/resolve/hir.rs +++ b/dhall/src/semantics/resolve/hir.rs @@ -1,5 +1,5 @@ use crate::error::TypeError; -use crate::semantics::{type_with, NameEnv, NzEnv, TyEnv, TyExpr, Value}; +use crate::semantics::{type_with, NameEnv, NzEnv, Tir, TyEnv, Value}; use crate::syntax::{Expr, ExprKind, Span, V}; use crate::{NormalizedExpr, ToExprOptions}; @@ -70,7 +70,7 @@ impl Hir { } /// Typecheck the Hir. - pub fn typecheck(&self, env: &TyEnv) -> Result { + pub fn typecheck(&self, env: &TyEnv) -> Result { type_with(env, self, None) } -- cgit v1.2.3 From cd5e172002ce724be7bdd52883e121efa8817f20 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 17 Feb 2020 18:22:06 +0000 Subject: Rename Value to Nir --- dhall/src/semantics/resolve/hir.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'dhall/src/semantics/resolve/hir.rs') diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs index ae65fff..346abbf 100644 --- a/dhall/src/semantics/resolve/hir.rs +++ b/dhall/src/semantics/resolve/hir.rs @@ -1,5 +1,5 @@ use crate::error::TypeError; -use crate::semantics::{type_with, NameEnv, NzEnv, Tir, TyEnv, Value}; +use crate::semantics::{type_with, NameEnv, Nir, NzEnv, Tir, TyEnv}; use crate::syntax::{Expr, ExprKind, Span, V}; use crate::{NormalizedExpr, ToExprOptions}; @@ -75,8 +75,8 @@ impl Hir { } /// Eval the Hir. It will actually get evaluated only as needed on demand. - pub fn eval(&self, env: impl Into) -> Value { - Value::new_thunk(env.into(), self.clone()) + pub fn eval(&self, env: impl Into) -> Nir { + Nir::new_thunk(env.into(), self.clone()) } } -- cgit v1.2.3 From ebe43bd6f1fd6feb1564ab9837399de7808b67b5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 18 Feb 2020 18:39:10 +0000 Subject: Borrow relevant Hir from Tir --- dhall/src/semantics/resolve/hir.rs | 20 +++++++++++++++++--- 1 file changed, 17 insertions(+), 3 deletions(-) (limited to 'dhall/src/semantics/resolve/hir.rs') diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs index 346abbf..d421718 100644 --- a/dhall/src/semantics/resolve/hir.rs +++ b/dhall/src/semantics/resolve/hir.rs @@ -48,11 +48,11 @@ impl Hir { self.span.clone() } - /// Converts a HIR expr back to the corresponding AST expression. + /// 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 HIR expr back to the corresponding AST expression. + /// Converts a closed Hir expr back to the corresponding AST expression. pub fn to_expr_noopts(&self) -> NormalizedExpr { let opts = ToExprOptions { normalize: false, @@ -70,7 +70,10 @@ impl Hir { } /// Typecheck the Hir. - pub fn typecheck(&self, env: &TyEnv) -> Result { + pub fn typecheck<'hir>( + &'hir self, + env: &TyEnv, + ) -> Result, TypeError> { type_with(env, self, None) } @@ -78,6 +81,17 @@ impl Hir { pub fn eval(&self, env: impl Into) -> 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( -- cgit v1.2.3 From 50a9dc4b9af19a35a983fe17108453d1d82d80ed Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 18 Feb 2020 18:46:26 +0000 Subject: Remove useless `normalize` option from ToExprOptions --- dhall/src/semantics/resolve/hir.rs | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) (limited to 'dhall/src/semantics/resolve/hir.rs') diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs index d421718..d0bec5a 100644 --- a/dhall/src/semantics/resolve/hir.rs +++ b/dhall/src/semantics/resolve/hir.rs @@ -54,17 +54,11 @@ impl Hir { } /// Converts a closed Hir expr back to the corresponding AST expression. pub fn to_expr_noopts(&self) -> NormalizedExpr { - let opts = ToExprOptions { - normalize: false, - alpha: false, - }; + let opts = ToExprOptions { alpha: false }; self.to_expr(opts) } pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr { - let opts = ToExprOptions { - normalize: true, - alpha: false, - }; + let opts = ToExprOptions { alpha: false }; let mut env = env.as_nameenv().clone(); hir_to_expr(self, opts, &mut env) } -- cgit v1.2.3 From a3990858840a737d7831be45953b38bd67361fb7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 18 Feb 2020 19:08:53 +0000 Subject: Discard import headers while we don't use them --- dhall/src/semantics/resolve/hir.rs | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) (limited to 'dhall/src/semantics/resolve/hir.rs') diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs index d0bec5a..73fc371 100644 --- a/dhall/src/semantics/resolve/hir.rs +++ b/dhall/src/semantics/resolve/hir.rs @@ -9,7 +9,7 @@ pub struct AlphaVar { idx: usize, } -#[derive(Debug, Clone, PartialEq, Eq, Hash)] +#[derive(Debug, Clone, PartialEq, Eq)] pub(crate) enum HirKind { /// A resolved variable (i.e. a DeBruijn index) Var(AlphaVar), @@ -128,11 +128,3 @@ impl std::cmp::PartialEq for Hir { } } impl std::cmp::Eq for Hir {} -impl std::hash::Hash for Hir { - fn hash(&self, state: &mut H) - where - H: std::hash::Hasher, - { - self.kind.hash(state) - } -} -- cgit v1.2.3 From 7cbfc1a0d32766a383d1f48902502adaa2234d2f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 18 Feb 2020 19:12:31 +0000 Subject: Avoid re-typechecking after import --- dhall/src/semantics/resolve/hir.rs | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'dhall/src/semantics/resolve/hir.rs') diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs index 73fc371..2f3464a 100644 --- a/dhall/src/semantics/resolve/hir.rs +++ b/dhall/src/semantics/resolve/hir.rs @@ -1,5 +1,5 @@ use crate::error::TypeError; -use crate::semantics::{type_with, NameEnv, Nir, NzEnv, Tir, TyEnv}; +use crate::semantics::{type_with, NameEnv, Nir, NzEnv, Tir, TyEnv, Type}; use crate::syntax::{Expr, ExprKind, Span, V}; use crate::{NormalizedExpr, ToExprOptions}; @@ -13,6 +13,8 @@ pub struct AlphaVar { 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), } @@ -96,6 +98,9 @@ fn hir_to_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 { -- cgit v1.2.3