From 27031b3739ff9f2043e64130a4c5699d0f9233e8 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 9 Feb 2020 11:23:59 +0000 Subject: Add Hir as untyped alternative to TyExpr --- dhall/src/semantics/hir.rs | 112 +++++++++++++++++++++++++++++++++++ dhall/src/semantics/mod.rs | 2 + dhall/src/semantics/nze/normalize.rs | 4 +- dhall/src/semantics/nze/value.rs | 10 ++-- dhall/src/semantics/tck/tyexpr.rs | 70 ++++------------------ 5 files changed, 133 insertions(+), 65 deletions(-) create mode 100644 dhall/src/semantics/hir.rs (limited to 'dhall/src') diff --git a/dhall/src/semantics/hir.rs b/dhall/src/semantics/hir.rs new file mode 100644 index 0000000..2784ecb --- /dev/null +++ b/dhall/src/semantics/hir.rs @@ -0,0 +1,112 @@ +#![allow(dead_code)] +use crate::semantics::{rc, NameEnv, NzEnv, TyEnv, Value}; +use crate::syntax::{ExprKind, Span, V}; +use crate::{Normalized, NormalizedExpr, ToExprOptions}; + +/// Stores an alpha-normalized variable. +#[derive(Debug, Clone, Copy)] +pub struct AlphaVar { + idx: usize, +} + +#[derive(Debug, Clone)] +pub(crate) enum HirKind { + Var(AlphaVar), + // Forbidden ExprKind variants: Var, Import, Embed + 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()) + } + 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) + } + + /// Eval the Hir. It will actually get evaluated only as needed on demand. + pub fn eval(&self, env: &NzEnv) -> Value { + // Value::new_thunk(env, self.clone()) + todo!() + } + /// 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) -> Value { + self.eval(&NzEnv::new()) + } + /// Eval a closed Hir fully and recursively (TODO: ish, need to fix under lambdas) + pub fn rec_eval_closed_expr(&self) -> Value { + let mut val = self.eval_closed_expr(); + val.normalize_mut(); + val + } +} + +fn hir_to_expr( + hir: &Hir, + opts: ToExprOptions, + env: &mut NameEnv, +) -> NormalizedExpr { + rc(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, + } + } + }) +} diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs index 98fdf5a..a8c0659 100644 --- a/dhall/src/semantics/mod.rs +++ b/dhall/src/semantics/mod.rs @@ -1,8 +1,10 @@ pub mod builtins; +pub mod hir; pub mod nze; pub mod parse; pub mod resolve; pub mod tck; pub(crate) use self::builtins::*; +pub(crate) use self::hir::*; pub(crate) use self::nze::*; pub(crate) use self::tck::*; diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs index c660fce..b5949f5 100644 --- a/dhall/src/semantics/nze/normalize.rs +++ b/dhall/src/semantics/nze/normalize.rs @@ -3,8 +3,8 @@ use std::collections::HashMap; use crate::semantics::NzEnv; use crate::semantics::{ - Binder, BuiltinClosure, Closure, TextLit, TyExpr, TyExprKind, Value, - ValueKind, + Binder, BuiltinClosure, Closure, Hir, HirKind, TextLit, TyExpr, TyExprKind, + Value, ValueKind, }; use crate::syntax::{BinOp, Builtin, ExprKind, InterpolatedTextContents}; use crate::Normalized; diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index 47c50a4..d4213bc 100644 --- a/dhall/src/semantics/nze/value.rs +++ b/dhall/src/semantics/nze/value.rs @@ -5,8 +5,8 @@ use crate::error::{TypeError, TypeMessage}; use crate::semantics::nze::lazy; use crate::semantics::{ apply_any, normalize_one_layer, normalize_tyexpr_whnf, squash_textlit, - type_with, Binder, BuiltinClosure, NzEnv, NzVar, TyEnv, TyExpr, TyExprKind, - VarEnv, + type_with, Binder, BuiltinClosure, Hir, NzEnv, NzVar, TyEnv, TyExpr, + TyExprKind, VarEnv, }; use crate::syntax::{ BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, @@ -461,19 +461,19 @@ impl ValueKind { } impl Thunk { - pub fn new(env: &NzEnv, body: TyExpr) -> Self { + fn new(env: &NzEnv, body: TyExpr) -> Self { Thunk::Thunk { env: env.clone(), body, } } - pub fn from_partial_expr( + fn from_partial_expr( env: NzEnv, expr: ExprKind, ) -> Self { Thunk::PartialExpr { env, expr } } - pub fn eval(self) -> ValueKind { + fn eval(self) -> ValueKind { match self { Thunk::Thunk { env, body } => normalize_tyexpr_whnf(&body, &env), Thunk::PartialExpr { env, expr } => normalize_one_layer(expr, &env), diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index 1886646..fa578c0 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,17 +1,13 @@ use crate::error::{TypeError, TypeMessage}; -use crate::semantics::{rc, NameEnv, NzEnv, TyEnv, Value}; +use crate::semantics::{ + rc, AlphaVar, Hir, HirKind, NameEnv, NzEnv, TyEnv, Value, +}; use crate::syntax::{ExprKind, Span, V}; use crate::Normalized; use crate::{NormalizedExpr, ToExprOptions}; pub(crate) type Type = Value; -/// Stores an alpha-normalized variable. -#[derive(Debug, Clone, Copy)] -pub struct AlphaVar { - idx: usize, -} - #[derive(Debug, Clone)] pub(crate) enum TyExprKind { Var(AlphaVar), @@ -27,15 +23,6 @@ pub(crate) struct TyExpr { span: Span, } -impl AlphaVar { - pub(crate) fn new(idx: usize) -> Self { - AlphaVar { idx } - } - pub(crate) fn idx(&self) -> usize { - self.idx - } -} - impl TyExpr { pub fn new(kind: TyExprKind, ty: Option, span: Span) -> Self { TyExpr { @@ -58,17 +45,19 @@ impl TyExpr { } } + pub fn to_hir(&self) -> Hir { + let kind = match self.kind() { + TyExprKind::Var(v) => HirKind::Var(v.clone()), + TyExprKind::Expr(e) => HirKind::Expr(e.map_ref(|tye| tye.to_hir())), + }; + Hir::new(kind, self.span()) + } /// Converts a value back to the corresponding AST expression. pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { - tyexpr_to_expr(self, opts, &mut NameEnv::new()) + self.to_hir().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(); - tyexpr_to_expr(self, opts, &mut env) + self.to_hir().to_expr_tyenv(env) } /// Eval the TyExpr. It will actually get evaluated only as needed on demand. @@ -88,41 +77,6 @@ impl TyExpr { } } -fn tyexpr_to_expr<'a>( - tyexpr: &'a TyExpr, - opts: ToExprOptions, - env: &mut NameEnv, -) -> NormalizedExpr { - rc(match tyexpr.kind() { - TyExprKind::Var(v) if opts.alpha => { - ExprKind::Var(V("_".into(), v.idx())) - } - TyExprKind::Var(v) => ExprKind::Var(env.label_var(v)), - TyExprKind::Expr(e) => { - let e = e.map_ref_maybe_binder(|l, tye| { - if let Some(l) = l { - env.insert_mut(l); - } - let e = tyexpr_to_expr(tye, 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, - } - } - }) -} - impl std::fmt::Debug for TyExpr { fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { let mut x = fmt.debug_struct("TyExpr"); -- cgit v1.2.3