summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/hir.rs112
-rw-r--r--dhall/src/semantics/mod.rs2
-rw-r--r--dhall/src/semantics/nze/normalize.rs4
-rw-r--r--dhall/src/semantics/nze/value.rs10
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs70
5 files changed, 133 insertions, 65 deletions
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<Hir, Normalized>),
+}
+
+// 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 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<Value, Normalized>,
) -> 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<Type>, 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");
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 01:24:15 +0000