summaryrefslogtreecommitdiff
path: root/dhall/src/semantics
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics')
-rw-r--r--dhall/src/semantics/core/value.rs87
-rw-r--r--dhall/src/semantics/core/var.rs18
-rw-r--r--dhall/src/semantics/mod.rs3
-rw-r--r--dhall/src/semantics/phase/mod.rs10
-rw-r--r--dhall/src/semantics/tck/mod.rs2
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs83
-rw-r--r--dhall/src/semantics/to_expr.rs101
7 files changed, 176 insertions, 128 deletions
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index 8b3ada1..a1125cd 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -7,10 +7,12 @@ use crate::semantics::core::context::TyCtx;
use crate::semantics::core::var::{AlphaVar, Binder};
use crate::semantics::phase::normalize::{apply_any, normalize_whnf};
use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value};
-use crate::semantics::phase::{Normalized, NormalizedExpr, Typed};
-use crate::semantics::to_expr;
+use crate::semantics::phase::{
+ Normalized, NormalizedExpr, ToExprOptions, Typed,
+};
+use crate::semantics::{TyExpr, TyExprKind};
use crate::syntax::{
- Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
+ BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
NaiveDouble, Natural, Span,
};
@@ -159,11 +161,12 @@ impl Value {
}
/// Converts a value back to the corresponding AST expression.
- pub(crate) fn to_expr(
- &self,
- opts: to_expr::ToExprOptions,
- ) -> NormalizedExpr {
- to_expr::value_to_expr(self, opts, &vec![])
+ pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
+ if opts.normalize {
+ self.normalize_nf();
+ }
+
+ self.to_tyexpr().to_expr(opts)
}
pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind<Value> {
self.as_whnf().clone()
@@ -283,6 +286,10 @@ impl Value {
// }
// }
// }
+
+ pub fn to_tyexpr(&self) -> TyExpr {
+ value_to_tyexpr(self)
+ }
}
impl ValueInternal {
@@ -510,6 +517,70 @@ impl<V> ValueKind<V> {
}
}
+fn value_to_tyexpr(val: &Value) -> TyExpr {
+ let val_kind = val.as_kind();
+ let val_ty = val.as_internal().ty.clone();
+ let val_span = val.as_internal().span.clone();
+ if let ValueKind::Var(v) = &*val_kind {
+ return TyExpr::new(TyExprKind::Var(*v), val_ty, val_span);
+ }
+
+ // TODO: properly recover intermediate types; `None` is a time-bomb here.
+ let rc = |expr| TyExpr::new(TyExprKind::Expr(expr), None, Span::Artificial);
+
+ let val_kind = val_kind.map_ref(|v| v.to_tyexpr());
+ let expr = match val_kind {
+ ValueKind::Var(_) => unreachable!(),
+ ValueKind::Lam(x, t, e) => ExprKind::Lam(x.to_label(), t, e),
+ ValueKind::Pi(x, t, e) => ExprKind::Pi(x.to_label(), t, e),
+ ValueKind::AppliedBuiltin(b, args) => args
+ .into_iter()
+ .fold(ExprKind::Builtin(b), |acc, v| ExprKind::App(rc(acc), v)),
+ ValueKind::Const(c) => ExprKind::Const(c),
+ ValueKind::BoolLit(b) => ExprKind::BoolLit(b),
+ ValueKind::NaturalLit(n) => ExprKind::NaturalLit(n),
+ ValueKind::IntegerLit(n) => ExprKind::IntegerLit(n),
+ ValueKind::DoubleLit(n) => ExprKind::DoubleLit(n),
+ ValueKind::EmptyOptionalLit(n) => {
+ ExprKind::App(rc(ExprKind::Builtin(Builtin::OptionalNone)), n)
+ }
+ ValueKind::NEOptionalLit(n) => ExprKind::SomeLit(n),
+ ValueKind::EmptyListLit(n) => ExprKind::EmptyListLit(rc(
+ ExprKind::App(rc(ExprKind::Builtin(Builtin::List)), n),
+ )),
+ ValueKind::NEListLit(elts) => ExprKind::NEListLit(elts),
+ ValueKind::RecordLit(kvs) => {
+ ExprKind::RecordLit(kvs.into_iter().collect())
+ }
+ ValueKind::RecordType(kts) => {
+ ExprKind::RecordType(kts.into_iter().collect())
+ }
+ ValueKind::UnionType(kts) => {
+ ExprKind::UnionType(kts.into_iter().collect())
+ }
+ ValueKind::UnionConstructor(l, kts) => ExprKind::Field(
+ rc(ExprKind::UnionType(kts.into_iter().collect())),
+ l,
+ ),
+ ValueKind::UnionLit(l, v, kts) => ExprKind::App(
+ rc(ExprKind::Field(
+ rc(ExprKind::UnionType(kts.into_iter().collect())),
+ l,
+ )),
+ v,
+ ),
+ ValueKind::TextLit(elts) => {
+ ExprKind::TextLit(elts.into_iter().collect())
+ }
+ ValueKind::Equivalence(x, y) => {
+ ExprKind::BinOp(BinOp::Equivalence, x, y)
+ }
+ ValueKind::PartialExpr(e) => e,
+ };
+
+ TyExpr::new(TyExprKind::Expr(expr), val_ty, val_span)
+}
+
// TODO: use Rc comparison to shortcut on identical pointers
impl std::cmp::PartialEq for Value {
fn eq(&self, other: &Self) -> bool {
diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index b336c66..0aa86d5 100644
--- a/dhall/src/semantics/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -1,7 +1,7 @@
use crate::syntax::{Label, V};
/// Stores an alpha-normalized variable.
-#[derive(Clone, Eq)]
+#[derive(Clone, Copy, PartialEq, Eq)]
pub struct AlphaVar {
alpha: V<()>,
}
@@ -36,28 +36,12 @@ impl Binder {
pub(crate) fn new(name: Label) -> Self {
Binder { name }
}
- pub(crate) fn to_label_maybe_alpha(&self, alpha: bool) -> Label {
- if alpha {
- "_".into()
- } else {
- self.to_label()
- }
- }
pub(crate) fn to_label(&self) -> Label {
self.clone().into()
}
- pub(crate) fn name(&self) -> &Label {
- &self.name
- }
}
/// Equality up to alpha-equivalence
-impl std::cmp::PartialEq for AlphaVar {
- fn eq(&self, other: &Self) -> bool {
- self.alpha == other.alpha
- }
-}
-/// Equality up to alpha-equivalence
impl std::cmp::PartialEq for Binder {
fn eq(&self, _other: &Self) -> bool {
true
diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs
index 3ef1aba..63f74ee 100644
--- a/dhall/src/semantics/mod.rs
+++ b/dhall/src/semantics/mod.rs
@@ -1,4 +1,5 @@
pub mod core;
pub mod phase;
-pub mod to_expr;
+pub mod tck;
pub(crate) use self::core::*;
+pub(crate) use self::tck::*;
diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs
index 6afed88..4dc91e7 100644
--- a/dhall/src/semantics/phase/mod.rs
+++ b/dhall/src/semantics/phase/mod.rs
@@ -4,7 +4,6 @@ use std::path::Path;
use crate::error::{EncodeError, Error, ImportError, TypeError};
use crate::semantics::core::value::Value;
use crate::semantics::core::value::ValueKind;
-use crate::semantics::to_expr::ToExprOptions;
use crate::syntax::binary;
use crate::syntax::{Builtin, Const, Expr};
use resolve::ImportRoot;
@@ -38,6 +37,15 @@ pub struct Typed(Value);
#[derive(Debug, Clone)]
pub struct Normalized(Typed);
+/// Controls conversion from `Value` to `Expr`
+#[derive(Copy, Clone)]
+pub(crate) struct ToExprOptions {
+ /// Whether to convert all variables to `_`
+ pub(crate) alpha: bool,
+ /// Whether to normalize before converting
+ pub(crate) normalize: bool,
+}
+
impl Parsed {
pub fn parse_file(f: &Path) -> Result<Parsed, Error> {
parse::parse_file(f)
diff --git a/dhall/src/semantics/tck/mod.rs b/dhall/src/semantics/tck/mod.rs
new file mode 100644
index 0000000..407605d
--- /dev/null
+++ b/dhall/src/semantics/tck/mod.rs
@@ -0,0 +1,2 @@
+pub mod tyexpr;
+pub(crate) use tyexpr::*;
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
new file mode 100644
index 0000000..a8b8e58
--- /dev/null
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -0,0 +1,83 @@
+#![allow(dead_code)]
+use crate::semantics::core::var::AlphaVar;
+use crate::semantics::phase::typecheck::rc;
+use crate::semantics::phase::Normalized;
+use crate::semantics::phase::{NormalizedExpr, ToExprOptions};
+use crate::semantics::Value;
+use crate::syntax::{ExprKind, Label, Span, V};
+
+pub(crate) type Type = Value;
+
+// An expression with inferred types at every node and resolved variables.
+pub(crate) struct TyExpr {
+ kind: Box<TyExprKind>,
+ ty: Option<Type>,
+ span: Span,
+}
+
+pub(crate) enum TyExprKind {
+ Var(AlphaVar),
+ // Forbidden ExprKind variants: Var
+ Expr(ExprKind<TyExpr, Normalized>),
+}
+
+impl TyExpr {
+ pub fn new(kind: TyExprKind, ty: Option<Type>, span: Span) -> Self {
+ TyExpr {
+ kind: Box::new(kind),
+ ty,
+ span,
+ }
+ }
+
+ pub fn kind(&self) -> &TyExprKind {
+ &*self.kind
+ }
+
+ /// Converts a value back to the corresponding AST expression.
+ pub fn to_expr<'a>(&'a self, opts: ToExprOptions) -> NormalizedExpr {
+ tyexpr_to_expr(self, opts, &Vec::new())
+ }
+}
+
+// TODO: mutate context once map_ref gets simplified
+fn tyexpr_to_expr<'a>(
+ tyexpr: &'a TyExpr,
+ opts: ToExprOptions,
+ ctx: &Vec<&'a Label>,
+) -> NormalizedExpr {
+ rc(match tyexpr.kind() {
+ TyExprKind::Var(v) if opts.alpha => {
+ ExprKind::Var(V("_".into(), v.idx()))
+ }
+ TyExprKind::Var(v) => {
+ let name = ctx[ctx.len() - 1 - v.idx()];
+ let mut idx = 0;
+ for l in ctx.iter().rev().take(v.idx()) {
+ if *l == name {
+ idx += 1;
+ }
+ }
+ ExprKind::Var(V(name.clone(), idx))
+ }
+ TyExprKind::Expr(e) => {
+ let e = e.map_ref_with_special_handling_of_binders(
+ |tye| tyexpr_to_expr(tye, opts, ctx),
+ |l, tye| {
+ let ctx = ctx.iter().copied().chain(Some(l)).collect();
+ tyexpr_to_expr(tye, opts, &ctx)
+ },
+ );
+
+ 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/to_expr.rs b/dhall/src/semantics/to_expr.rs
deleted file mode 100644
index 612f794..0000000
--- a/dhall/src/semantics/to_expr.rs
+++ /dev/null
@@ -1,101 +0,0 @@
-use crate::semantics::core::var::Binder;
-use crate::semantics::phase::typecheck::rc;
-use crate::semantics::phase::NormalizedExpr;
-use crate::semantics::{Value, ValueKind};
-use crate::syntax;
-use crate::syntax::{Builtin, ExprKind, V};
-
-/// Controls conversion from `Value` to `Expr`
-#[derive(Copy, Clone)]
-pub(crate) struct ToExprOptions {
- /// Whether to convert all variables to `_`
- pub(crate) alpha: bool,
- /// Whether to normalize before converting
- pub(crate) normalize: bool,
-}
-
-/// Converts a value back to the corresponding AST expression.
-pub(crate) fn value_to_expr<'a>(
- val: &'a Value,
- opts: ToExprOptions,
- ctx: &Vec<&'a Binder>,
-) -> NormalizedExpr {
- if opts.normalize {
- val.normalize_whnf();
- }
-
- let kind = val.as_kind();
- let kind = kind.map_ref_with_special_handling_of_binders(
- |v| value_to_expr(v, opts, ctx),
- |b, _, v| {
- let mut ctx = ctx.clone();
- ctx.push(b);
- value_to_expr(v, opts, &ctx)
- },
- );
- match kind {
- ValueKind::Var(v) if opts.alpha => {
- rc(ExprKind::Var(V("_".into(), v.idx())))
- }
- ValueKind::Var(v) => {
- let name = ctx[ctx.len() - 1 - v.idx()].to_label();
- let mut idx = 0;
- for b in ctx.iter().rev().take(v.idx()) {
- if b.name() == &name {
- idx += 1;
- }
- }
- rc(ExprKind::Var(V(name, idx)))
- }
- ValueKind::Lam(x, t, e) => {
- rc(ExprKind::Lam(x.to_label_maybe_alpha(opts.alpha), t, e))
- }
- ValueKind::AppliedBuiltin(b, args) => args
- .into_iter()
- .fold(rc(ExprKind::Builtin(b)), |acc, v| rc(ExprKind::App(acc, v))),
- ValueKind::Pi(x, t, e) => {
- rc(ExprKind::Pi(x.to_label_maybe_alpha(opts.alpha), t, e))
- }
- ValueKind::Const(c) => rc(ExprKind::Const(c)),
- ValueKind::BoolLit(b) => rc(ExprKind::BoolLit(b)),
- ValueKind::NaturalLit(n) => rc(ExprKind::NaturalLit(n)),
- ValueKind::IntegerLit(n) => rc(ExprKind::IntegerLit(n)),
- ValueKind::DoubleLit(n) => rc(ExprKind::DoubleLit(n)),
- ValueKind::EmptyOptionalLit(n) => rc(ExprKind::App(
- rc(ExprKind::Builtin(Builtin::OptionalNone)),
- n,
- )),
- ValueKind::NEOptionalLit(n) => rc(ExprKind::SomeLit(n)),
- ValueKind::EmptyListLit(n) => rc(ExprKind::EmptyListLit(rc(
- ExprKind::App(rc(ExprKind::Builtin(Builtin::List)), n),
- ))),
- ValueKind::NEListLit(elts) => rc(ExprKind::NEListLit(elts)),
- ValueKind::RecordLit(kvs) => {
- rc(ExprKind::RecordLit(kvs.into_iter().collect()))
- }
- ValueKind::RecordType(kts) => {
- rc(ExprKind::RecordType(kts.into_iter().collect()))
- }
- ValueKind::UnionType(kts) => {
- rc(ExprKind::UnionType(kts.into_iter().collect()))
- }
- ValueKind::UnionConstructor(l, kts) => rc(ExprKind::Field(
- rc(ExprKind::UnionType(kts.into_iter().collect())),
- l,
- )),
- ValueKind::UnionLit(l, v, kts) => rc(ExprKind::App(
- rc(ExprKind::Field(
- rc(ExprKind::UnionType(kts.into_iter().collect())),
- l,
- )),
- v,
- )),
- ValueKind::TextLit(elts) => {
- rc(ExprKind::TextLit(elts.into_iter().collect()))
- }
- ValueKind::Equivalence(x, y) => {
- rc(ExprKind::BinOp(syntax::BinOp::Equivalence, x, y))
- }
- ValueKind::PartialExpr(e) => rc(e),
- }
-}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 18:12:51 +0000