summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/nze
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics/nze')
-rw-r--r--dhall/src/semantics/nze/env.rs76
-rw-r--r--dhall/src/semantics/nze/lazy.rs64
-rw-r--r--dhall/src/semantics/nze/mod.rs9
-rw-r--r--dhall/src/semantics/nze/normalize.rs421
-rw-r--r--dhall/src/semantics/nze/value.rs656
-rw-r--r--dhall/src/semantics/nze/var.rs36
6 files changed, 1262 insertions, 0 deletions
diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs
new file mode 100644
index 0000000..0b22a8b
--- /dev/null
+++ b/dhall/src/semantics/nze/env.rs
@@ -0,0 +1,76 @@
+use crate::semantics::{AlphaVar, Value, ValueKind};
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub(crate) enum NzVar {
+ /// Reverse-debruijn index: counts number of binders from the bottom of the stack.
+ Bound(usize),
+ /// Fake fresh variable generated for expression equality checking.
+ Fresh(usize),
+}
+
+#[derive(Debug, Clone)]
+enum NzEnvItem {
+ // Variable is bound with given type
+ Kept(Value),
+ // Variable has been replaced by corresponding value
+ Replaced(Value),
+}
+
+#[derive(Debug, Clone)]
+pub(crate) struct NzEnv {
+ items: Vec<NzEnvItem>,
+}
+
+impl NzVar {
+ pub fn new(idx: usize) -> Self {
+ NzVar::Bound(idx)
+ }
+ pub fn fresh() -> Self {
+ use std::sync::atomic::{AtomicUsize, Ordering};
+ // Global counter to ensure uniqueness of the generated id.
+ static FRESH_VAR_COUNTER: AtomicUsize = AtomicUsize::new(0);
+ let id = FRESH_VAR_COUNTER.fetch_add(1, Ordering::SeqCst);
+ NzVar::Fresh(id)
+ }
+ /// Get index of bound variable.
+ /// Panics on a fresh variable.
+ pub fn idx(&self) -> usize {
+ match self {
+ NzVar::Bound(i) => *i,
+ NzVar::Fresh(_) => panic!(
+ "Trying to use a fresh variable outside of equality checking"
+ ),
+ }
+ }
+}
+
+impl NzEnv {
+ pub fn new() -> Self {
+ NzEnv { items: Vec::new() }
+ }
+
+ pub fn insert_type(&self, t: Value) -> Self {
+ let mut env = self.clone();
+ env.items.push(NzEnvItem::Kept(t));
+ env
+ }
+ pub fn insert_value(&self, e: Value) -> Self {
+ let mut env = self.clone();
+ env.items.push(NzEnvItem::Replaced(e));
+ env
+ }
+ pub fn lookup_val(&self, var: &AlphaVar) -> ValueKind {
+ let idx = self.items.len() - 1 - var.idx();
+ match &self.items[idx] {
+ NzEnvItem::Kept(_) => ValueKind::Var(NzVar::new(idx)),
+ NzEnvItem::Replaced(x) => x.kind().clone(),
+ }
+ }
+ pub fn lookup_ty(&self, var: &AlphaVar) -> Value {
+ let idx = self.items.len() - 1 - var.idx();
+ match &self.items[idx] {
+ NzEnvItem::Kept(ty) => ty.clone(),
+ NzEnvItem::Replaced(x) => x.get_type().unwrap(),
+ }
+ }
+}
diff --git a/dhall/src/semantics/nze/lazy.rs b/dhall/src/semantics/nze/lazy.rs
new file mode 100644
index 0000000..d361313
--- /dev/null
+++ b/dhall/src/semantics/nze/lazy.rs
@@ -0,0 +1,64 @@
+use once_cell::unsync::OnceCell;
+use std::cell::Cell;
+use std::fmt::Debug;
+use std::ops::Deref;
+
+pub trait Eval<Tgt> {
+ fn eval(self) -> Tgt;
+}
+
+/// A value which is initialized from a `Src` on the first access.
+pub struct Lazy<Src, Tgt> {
+ /// Exactly one of `src` of `tgt` must be set at a given time.
+ /// Once `src` is unset and `tgt` is set, we never go back.
+ src: Cell<Option<Src>>,
+ tgt: OnceCell<Tgt>,
+}
+
+impl<Src, Tgt> Lazy<Src, Tgt>
+where
+ Src: Eval<Tgt>,
+{
+ /// Creates a new lazy value with the given initializing value.
+ pub fn new(src: Src) -> Self {
+ Lazy {
+ src: Cell::new(Some(src)),
+ tgt: OnceCell::new(),
+ }
+ }
+ /// Creates a new lazy value with the given already-initialized value.
+ pub fn new_completed(tgt: Tgt) -> Self {
+ let lazy = Lazy {
+ src: Cell::new(None),
+ tgt: OnceCell::new(),
+ };
+ let _ = lazy.tgt.set(tgt);
+ lazy
+ }
+}
+
+impl<Src, Tgt> Deref for Lazy<Src, Tgt>
+where
+ Src: Eval<Tgt>,
+{
+ type Target = Tgt;
+ fn deref(&self) -> &Self::Target {
+ self.tgt.get_or_init(|| {
+ let src = self.src.take().unwrap();
+ src.eval()
+ })
+ }
+}
+
+impl<Src, Tgt> Debug for Lazy<Src, Tgt>
+where
+ Tgt: Debug,
+{
+ fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+ if let Some(tgt) = self.tgt.get() {
+ fmt.debug_tuple("Lazy@Init").field(tgt).finish()
+ } else {
+ fmt.debug_tuple("Lazy@Uninit").finish()
+ }
+ }
+}
diff --git a/dhall/src/semantics/nze/mod.rs b/dhall/src/semantics/nze/mod.rs
new file mode 100644
index 0000000..2c8d907
--- /dev/null
+++ b/dhall/src/semantics/nze/mod.rs
@@ -0,0 +1,9 @@
+pub mod env;
+pub mod lazy;
+pub mod normalize;
+pub mod value;
+pub mod var;
+pub(crate) use env::*;
+pub(crate) use normalize::*;
+pub(crate) use value::*;
+pub(crate) use var::*;
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
new file mode 100644
index 0000000..e9d140b
--- /dev/null
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -0,0 +1,421 @@
+use std::collections::HashMap;
+
+use crate::semantics::NzEnv;
+use crate::semantics::{
+ Binder, BuiltinClosure, Closure, TextLit, TyExpr, TyExprKind, Value,
+ ValueKind,
+};
+use crate::syntax::{
+ BinOp, Builtin, Const, ExprKind, InterpolatedTextContents,
+};
+use crate::Normalized;
+
+pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind {
+ match f.kind() {
+ ValueKind::LamClosure { closure, .. } => {
+ closure.apply(a).to_whnf_check_type(ty)
+ }
+ ValueKind::AppliedBuiltin(closure) => {
+ closure.apply(a, f.get_type().unwrap(), ty)
+ }
+ ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit(
+ l.clone(),
+ a,
+ kts.clone(),
+ uniont.clone(),
+ f.get_type().unwrap(),
+ ),
+ _ => ValueKind::PartialExpr(ExprKind::App(f, a)),
+ }
+}
+
+pub(crate) fn squash_textlit(
+ elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
+) -> Vec<InterpolatedTextContents<Value>> {
+ use std::mem::replace;
+ use InterpolatedTextContents::{Expr, Text};
+
+ fn inner(
+ elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
+ crnt_str: &mut String,
+ ret: &mut Vec<InterpolatedTextContents<Value>>,
+ ) {
+ for contents in elts {
+ match contents {
+ Text(s) => crnt_str.push_str(&s),
+ Expr(e) => match e.kind() {
+ ValueKind::TextLit(elts2) => {
+ inner(elts2.iter().cloned(), crnt_str, ret)
+ }
+ _ => {
+ if !crnt_str.is_empty() {
+ ret.push(Text(replace(crnt_str, String::new())))
+ }
+ ret.push(Expr(e.clone()))
+ }
+ },
+ }
+ }
+ }
+
+ let mut crnt_str = String::new();
+ let mut ret = Vec::new();
+ inner(elts, &mut crnt_str, &mut ret);
+ if !crnt_str.is_empty() {
+ ret.push(Text(replace(&mut crnt_str, String::new())))
+ }
+ ret
+}
+
+pub(crate) fn merge_maps<K, V, F, Err>(
+ map1: &HashMap<K, V>,
+ map2: &HashMap<K, V>,
+ mut f: F,
+) -> Result<HashMap<K, V>, Err>
+where
+ F: FnMut(&K, &V, &V) -> Result<V, Err>,
+ K: std::hash::Hash + Eq + Clone,
+ V: Clone,
+{
+ let mut kvs = HashMap::new();
+ for (x, v2) in map2 {
+ let newv = if let Some(v1) = map1.get(x) {
+ f(x, v1, v2)?
+ } else {
+ v2.clone()
+ };
+ kvs.insert(x.clone(), newv);
+ }
+ for (x, v1) in map1 {
+ // Insert only if key not already present
+ kvs.entry(x.clone()).or_insert_with(|| v1.clone());
+ }
+ Ok(kvs)
+}
+
+// Small helper enum to avoid repetition
+enum Ret<'a> {
+ ValueKind(ValueKind),
+ Value(Value),
+ ValueRef(&'a Value),
+ Expr(ExprKind<Value, Normalized>),
+}
+
+fn apply_binop<'a>(
+ o: BinOp,
+ x: &'a Value,
+ y: &'a Value,
+ ty: &Value,
+) -> Option<Ret<'a>> {
+ use BinOp::{
+ BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
+ NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
+ RightBiasedRecordMerge, TextAppend,
+ };
+ use ValueKind::{
+ BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
+ };
+ Some(match (o, x.kind(), y.kind()) {
+ (BoolAnd, BoolLit(true), _) => Ret::ValueRef(y),
+ (BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x),
+ (BoolAnd, BoolLit(false), _) => Ret::ValueKind(BoolLit(false)),
+ (BoolAnd, _, BoolLit(false)) => Ret::ValueKind(BoolLit(false)),
+ (BoolAnd, _, _) if x == y => Ret::ValueRef(x),
+ (BoolOr, BoolLit(true), _) => Ret::ValueKind(BoolLit(true)),
+ (BoolOr, _, BoolLit(true)) => Ret::ValueKind(BoolLit(true)),
+ (BoolOr, BoolLit(false), _) => Ret::ValueRef(y),
+ (BoolOr, _, BoolLit(false)) => Ret::ValueRef(x),
+ (BoolOr, _, _) if x == y => Ret::ValueRef(x),
+ (BoolEQ, BoolLit(true), _) => Ret::ValueRef(y),
+ (BoolEQ, _, BoolLit(true)) => Ret::ValueRef(x),
+ (BoolEQ, BoolLit(x), BoolLit(y)) => Ret::ValueKind(BoolLit(x == y)),
+ (BoolEQ, _, _) if x == y => Ret::ValueKind(BoolLit(true)),
+ (BoolNE, BoolLit(false), _) => Ret::ValueRef(y),
+ (BoolNE, _, BoolLit(false)) => Ret::ValueRef(x),
+ (BoolNE, BoolLit(x), BoolLit(y)) => Ret::ValueKind(BoolLit(x != y)),
+ (BoolNE, _, _) if x == y => Ret::ValueKind(BoolLit(false)),
+
+ (NaturalPlus, NaturalLit(0), _) => Ret::ValueRef(y),
+ (NaturalPlus, _, NaturalLit(0)) => Ret::ValueRef(x),
+ (NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
+ Ret::ValueKind(NaturalLit(x + y))
+ }
+ (NaturalTimes, NaturalLit(0), _) => Ret::ValueKind(NaturalLit(0)),
+ (NaturalTimes, _, NaturalLit(0)) => Ret::ValueKind(NaturalLit(0)),
+ (NaturalTimes, NaturalLit(1), _) => Ret::ValueRef(y),
+ (NaturalTimes, _, NaturalLit(1)) => Ret::ValueRef(x),
+ (NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
+ Ret::ValueKind(NaturalLit(x * y))
+ }
+
+ (ListAppend, EmptyListLit(_), _) => Ret::ValueRef(y),
+ (ListAppend, _, EmptyListLit(_)) => Ret::ValueRef(x),
+ (ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::ValueKind(
+ NEListLit(xs.iter().chain(ys.iter()).cloned().collect()),
+ ),
+
+ (TextAppend, ValueKind::TextLit(x), _) if x.is_empty() => {
+ Ret::ValueRef(y)
+ }
+ (TextAppend, _, ValueKind::TextLit(y)) if y.is_empty() => {
+ Ret::ValueRef(x)
+ }
+ (TextAppend, ValueKind::TextLit(x), ValueKind::TextLit(y)) => {
+ Ret::ValueKind(ValueKind::TextLit(x.concat(y)))
+ }
+ (TextAppend, ValueKind::TextLit(x), _) => Ret::ValueKind(
+ ValueKind::TextLit(x.concat(&TextLit::interpolate(y.clone()))),
+ ),
+ (TextAppend, _, ValueKind::TextLit(y)) => Ret::ValueKind(
+ ValueKind::TextLit(TextLit::interpolate(x.clone()).concat(y)),
+ ),
+
+ (RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
+ Ret::ValueRef(x)
+ }
+ (RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
+ Ret::ValueRef(y)
+ }
+ (RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
+ let mut kvs = kvs2.clone();
+ for (x, v) in kvs1 {
+ // Insert only if key not already present
+ kvs.entry(x.clone()).or_insert_with(|| v.clone());
+ }
+ Ret::ValueKind(RecordLit(kvs))
+ }
+
+ (RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
+ Ret::ValueRef(x)
+ }
+ (RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
+ Ret::ValueRef(y)
+ }
+ (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
+ let kts = match ty.kind() {
+ RecordType(kts) => kts,
+ _ => unreachable!("Internal type error"),
+ };
+ let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| {
+ Ok(Value::from_partial_expr(
+ ExprKind::BinOp(
+ RecursiveRecordMerge,
+ v1.clone(),
+ v2.clone(),
+ ),
+ kts.get(k).expect("Internal type error").clone(),
+ ))
+ })?;
+ Ret::ValueKind(RecordLit(kvs))
+ }
+
+ (RecursiveRecordTypeMerge, RecordType(kts_x), RecordType(kts_y)) => {
+ let kts = merge_maps::<_, _, _, !>(
+ kts_x,
+ kts_y,
+ // If the Label exists for both records, then we hit the recursive case.
+ |_, l: &Value, r: &Value| {
+ Ok(Value::from_partial_expr(
+ ExprKind::BinOp(
+ RecursiveRecordTypeMerge,
+ l.clone(),
+ r.clone(),
+ ),
+ ty.clone(),
+ ))
+ },
+ )?;
+ Ret::ValueKind(RecordType(kts))
+ }
+
+ (Equivalence, _, _) => {
+ Ret::ValueKind(ValueKind::Equivalence(x.clone(), y.clone()))
+ }
+
+ _ => return None,
+ })
+}
+
+pub(crate) fn normalize_one_layer(
+ expr: ExprKind<Value, Normalized>,
+ ty: &Value,
+ env: &NzEnv,
+) -> ValueKind {
+ use ValueKind::{
+ BoolLit, DoubleLit, EmptyOptionalLit, IntegerLit, NEListLit,
+ NEOptionalLit, NaturalLit, RecordLit, RecordType, UnionConstructor,
+ UnionLit, UnionType,
+ };
+
+ let ret = match expr {
+ ExprKind::Import(_) => unreachable!(
+ "There should remain no imports in a resolved expression"
+ ),
+ // Those cases have already been completely handled in the typechecking phase (using
+ // `RetWhole`), so they won't appear here.
+ ExprKind::Lam(..)
+ | ExprKind::Pi(..)
+ | ExprKind::Let(..)
+ | ExprKind::Embed(_)
+ | ExprKind::Var(_) => {
+ unreachable!("This case should have been handled in typecheck")
+ }
+ ExprKind::Annot(x, _) => Ret::Value(x),
+ ExprKind::Const(c) => Ret::Value(Value::from_const(c)),
+ ExprKind::Builtin(b) => Ret::Value(Value::from_builtin_env(b, env)),
+ ExprKind::Assert(_) => Ret::Expr(expr),
+ ExprKind::App(v, a) => Ret::Value(v.app(a)),
+ ExprKind::BoolLit(b) => Ret::ValueKind(BoolLit(b)),
+ ExprKind::NaturalLit(n) => Ret::ValueKind(NaturalLit(n)),
+ ExprKind::IntegerLit(n) => Ret::ValueKind(IntegerLit(n)),
+ ExprKind::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)),
+ ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)),
+ ExprKind::EmptyListLit(t) => {
+ let arg = match &*t.kind() {
+ ValueKind::AppliedBuiltin(BuiltinClosure {
+ b: Builtin::List,
+ args,
+ ..
+ }) if args.len() == 1 => args[0].clone(),
+ _ => panic!("internal type error"),
+ };
+ Ret::ValueKind(ValueKind::EmptyListLit(arg))
+ }
+ ExprKind::NEListLit(elts) => {
+ Ret::ValueKind(NEListLit(elts.into_iter().collect()))
+ }
+ ExprKind::RecordLit(kvs) => {
+ Ret::ValueKind(RecordLit(kvs.into_iter().collect()))
+ }
+ ExprKind::RecordType(kvs) => {
+ Ret::ValueKind(RecordType(kvs.into_iter().collect()))
+ }
+ ExprKind::UnionType(kvs) => {
+ Ret::ValueKind(UnionType(kvs.into_iter().collect()))
+ }
+ ExprKind::TextLit(elts) => {
+ let tlit = TextLit::new(elts.into_iter());
+ // Simplify bare interpolation
+ if let Some(v) = tlit.as_single_expr() {
+ Ret::Value(v.clone())
+ } else {
+ Ret::ValueKind(ValueKind::TextLit(tlit))
+ }
+ }
+ ExprKind::BoolIf(ref b, ref e1, ref e2) => {
+ match b.kind() {
+ BoolLit(true) => Ret::ValueRef(e1),
+ BoolLit(false) => Ret::ValueRef(e2),
+ _ => {
+ match (e1.kind(), e2.kind()) {
+ // Simplify `if b then True else False`
+ (BoolLit(true), BoolLit(false)) => Ret::ValueRef(b),
+ _ if e1 == e2 => Ret::ValueRef(e1),
+ _ => Ret::Expr(expr),
+ }
+ }
+ }
+ }
+ ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) {
+ Some(ret) => ret,
+ None => Ret::Expr(expr),
+ },
+
+ ExprKind::Projection(_, ref ls) if ls.is_empty() => {
+ Ret::ValueKind(RecordLit(HashMap::new()))
+ }
+ ExprKind::Projection(ref v, ref ls) => match v.kind() {
+ RecordLit(kvs) => Ret::ValueKind(RecordLit(
+ ls.iter()
+ .filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone())))
+ .collect(),
+ )),
+ _ => Ret::Expr(expr),
+ },
+ ExprKind::Field(ref v, ref l) => match v.kind() {
+ RecordLit(kvs) => match kvs.get(l) {
+ Some(r) => Ret::Value(r.clone()),
+ None => Ret::Expr(expr),
+ },
+ UnionType(kts) => Ret::ValueKind(UnionConstructor(
+ l.clone(),
+ kts.clone(),
+ v.get_type().unwrap(),
+ )),
+ _ => Ret::Expr(expr),
+ },
+ ExprKind::ProjectionByExpr(_, _) => {
+ unimplemented!("selection by expression")
+ }
+ ExprKind::Completion(_, _) => unimplemented!("record completion"),
+
+ ExprKind::Merge(ref handlers, ref variant, _) => {
+ match handlers.kind() {
+ RecordLit(kvs) => match variant.kind() {
+ UnionConstructor(l, _, _) => match kvs.get(l) {
+ Some(h) => Ret::Value(h.clone()),
+ None => Ret::Expr(expr),
+ },
+ UnionLit(l, v, _, _, _) => match kvs.get(l) {
+ Some(h) => Ret::Value(h.app(v.clone())),
+ None => Ret::Expr(expr),
+ },
+ EmptyOptionalLit(_) => match kvs.get(&"None".into()) {
+ Some(h) => Ret::Value(h.clone()),
+ None => Ret::Expr(expr),
+ },
+ NEOptionalLit(v) => match kvs.get(&"Some".into()) {
+ Some(h) => Ret::Value(h.app(v.clone())),
+ None => Ret::Expr(expr),
+ },
+ _ => Ret::Expr(expr),
+ },
+ _ => Ret::Expr(expr),
+ }
+ }
+ ExprKind::ToMap(_, _) => unimplemented!("toMap"),
+ };
+
+ match ret {
+ Ret::ValueKind(v) => v,
+ Ret::Value(v) => v.to_whnf_check_type(ty),
+ Ret::ValueRef(v) => v.to_whnf_check_type(ty),
+ Ret::Expr(expr) => ValueKind::PartialExpr(expr),
+ }
+}
+
+/// Normalize a TyExpr into WHNF
+pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind {
+ match tye.kind() {
+ TyExprKind::Var(var) => env.lookup_val(var),
+ TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => {
+ let annot = annot.eval(env);
+ ValueKind::LamClosure {
+ binder: Binder::new(binder.clone()),
+ annot: annot.clone(),
+ closure: Closure::new(annot, env, body.clone()),
+ }
+ }
+ TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => {
+ let annot = annot.eval(env);
+ let closure = Closure::new(annot.clone(), env, body.clone());
+ ValueKind::PiClosure {
+ binder: Binder::new(binder.clone()),
+ annot,
+ closure,
+ }
+ }
+ TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => {
+ let val = val.eval(env);
+ body.eval(&env.insert_value(val)).kind().clone()
+ }
+ TyExprKind::Expr(e) => {
+ let ty = match tye.get_type() {
+ Ok(ty) => ty,
+ Err(_) => return ValueKind::Const(Const::Sort),
+ };
+ let e = e.map_ref(|tye| tye.eval(env));
+ normalize_one_layer(e, &ty, env)
+ }
+ }
+}
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
new file mode 100644
index 0000000..ae06942
--- /dev/null
+++ b/dhall/src/semantics/nze/value.rs
@@ -0,0 +1,656 @@
+use std::collections::HashMap;
+use std::rc::Rc;
+
+use crate::error::{TypeError, TypeMessage};
+use crate::semantics::nze::lazy;
+use crate::semantics::Binder;
+use crate::semantics::{
+ apply_any, normalize_one_layer, normalize_tyexpr_whnf, squash_textlit,
+};
+use crate::semantics::{type_of_builtin, typecheck, TyExpr, TyExprKind};
+use crate::semantics::{BuiltinClosure, NzEnv, NzVar, VarEnv};
+use crate::syntax::{
+ BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
+ NaiveDouble, Natural, Span,
+};
+use crate::{Normalized, NormalizedExpr, ToExprOptions};
+
+/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation
+/// automatically. Uses a Rc<RefCell> to share computation.
+/// If you compare for equality two `Value`s, then equality will be up to alpha-equivalence
+/// (renaming of bound variables) and beta-equivalence (normalization). It will recursively
+/// normalize as needed.
+#[derive(Clone)]
+pub(crate) struct Value(Rc<ValueInternal>);
+
+#[derive(Debug)]
+struct ValueInternal {
+ kind: lazy::Lazy<Thunk, ValueKind>,
+ /// This is None if and only if `form` is `Sort` (which doesn't have a type)
+ ty: Option<Value>,
+ span: Span,
+}
+
+/// An unevaluated subexpression
+#[derive(Debug, Clone)]
+pub(crate) enum Thunk {
+ /// A completely unnormalized expression.
+ Thunk { env: NzEnv, body: TyExpr },
+ /// A partially normalized expression that may need to go through `normalize_one_layer`.
+ PartialExpr {
+ env: NzEnv,
+ expr: ExprKind<Value, Normalized>,
+ ty: Value,
+ },
+}
+
+/// An unevaluated subexpression that takes an argument.
+#[derive(Debug, Clone)]
+pub(crate) enum Closure {
+ /// Normal closure
+ Closure {
+ arg_ty: Value,
+ env: NzEnv,
+ body: TyExpr,
+ },
+ /// Closure that ignores the argument passed
+ ConstantClosure { body: Value },
+}
+
+/// A text literal with interpolations.
+// Invariant: this must not contain interpolations that are themselves TextLits, and contiguous
+// text values must be merged.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) struct TextLit(Vec<InterpolatedTextContents<Value>>);
+
+/// This represents a value in Weak Head Normal Form (WHNF). This means that the value is
+/// normalized up to the first constructor, but subexpressions may not be fully normalized.
+/// When all the Values in a ValueKind are in WHNF, and recursively so, then the ValueKind is in
+/// Normal Form (NF). This is because WHNF ensures that we have the first constructor of the NF; so
+/// if we have the first constructor of the NF at all levels, we actually have the NF.
+/// In particular, this means that once we get a `ValueKind`, it can be considered immutable, and
+/// we only need to recursively normalize its sub-`Value`s to get to the NF.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub(crate) enum ValueKind {
+ /// Closures
+ LamClosure {
+ binder: Binder,
+ annot: Value,
+ closure: Closure,
+ },
+ PiClosure {
+ binder: Binder,
+ annot: Value,
+ closure: Closure,
+ },
+ AppliedBuiltin(BuiltinClosure<Value>),
+
+ Var(NzVar),
+ Const(Const),
+ BoolLit(bool),
+ NaturalLit(Natural),
+ IntegerLit(Integer),
+ DoubleLit(NaiveDouble),
+ EmptyOptionalLit(Value),
+ NEOptionalLit(Value),
+ // EmptyListLit(t) means `[] : List t`, not `[] : t`
+ EmptyListLit(Value),
+ NEListLit(Vec<Value>),
+ RecordType(HashMap<Label, Value>),
+ RecordLit(HashMap<Label, Value>),
+ UnionType(HashMap<Label, Option<Value>>),
+ // Also keep the type of the uniontype around
+ UnionConstructor(Label, HashMap<Label, Option<Value>>, Value),
+ // Also keep the type of the uniontype and the constructor around
+ UnionLit(Label, Value, HashMap<Label, Option<Value>>, Value, Value),
+ TextLit(TextLit),
+ Equivalence(Value, Value),
+ /// Invariant: evaluation must not be able to progress with `normalize_one_layer`?
+ PartialExpr(ExprKind<Value, Normalized>),
+}
+
+impl Value {
+ pub(crate) fn const_sort() -> Value {
+ ValueInternal::from_whnf(
+ ValueKind::Const(Const::Sort),
+ None,
+ Span::Artificial,
+ )
+ .into_value()
+ }
+ /// Construct a Value from a completely unnormalized expression.
+ pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value {
+ ValueInternal::from_thunk(
+ Thunk::new(env, tye.clone()),
+ tye.get_type().ok(),
+ tye.span().clone(),
+ )
+ .into_value()
+ }
+ /// Construct a Value from a partially normalized expression that's not in WHNF.
+ pub(crate) fn from_partial_expr(
+ e: ExprKind<Value, Normalized>,
+ ty: Value,
+ ) -> Value {
+ // TODO: env
+ let env = NzEnv::new();
+ ValueInternal::from_thunk(
+ Thunk::from_partial_expr(env, e, ty.clone()),
+ Some(ty),
+ Span::Artificial,
+ )
+ .into_value()
+ }
+ /// Make a Value from a ValueKind
+ pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value {
+ ValueInternal::from_whnf(v, Some(t), Span::Artificial).into_value()
+ }
+ pub(crate) fn from_const(c: Const) -> Self {
+ let v = ValueKind::Const(c);
+ match c {
+ Const::Type => {
+ Value::from_kind_and_type(v, Value::from_const(Const::Kind))
+ }
+ Const::Kind => {
+ Value::from_kind_and_type(v, Value::from_const(Const::Sort))
+ }
+ Const::Sort => Value::const_sort(),
+ }
+ }
+ pub(crate) fn from_builtin(b: Builtin) -> Self {
+ Self::from_builtin_env(b, &NzEnv::new())
+ }
+ pub(crate) fn from_builtin_env(b: Builtin, env: &NzEnv) -> Self {
+ Value::from_kind_and_type(
+ ValueKind::from_builtin_env(b, env.clone()),
+ typecheck(&type_of_builtin(b)).unwrap().eval_closed_expr(),
+ )
+ }
+
+ pub(crate) fn as_const(&self) -> Option<Const> {
+ match &*self.kind() {
+ ValueKind::Const(c) => Some(*c),
+ _ => None,
+ }
+ }
+ pub(crate) fn span(&self) -> Span {
+ self.0.span.clone()
+ }
+
+ /// This is what you want if you want to pattern-match on the value.
+ /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut
+ /// panics.
+ pub(crate) fn kind(&self) -> &ValueKind {
+ self.0.kind()
+ }
+
+ /// Converts a value back to the corresponding AST expression.
+ pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
+ if opts.normalize {
+ self.normalize();
+ }
+
+ self.to_tyexpr_noenv().to_expr(opts)
+ }
+ pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind {
+ self.kind().clone()
+ }
+ /// Before discarding type information, check that it matches the expected return type.
+ pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueKind {
+ self.check_type(ty);
+ self.to_whnf_ignore_type()
+ }
+
+ /// Normalizes contents to normal form; faster than `normalize` if
+ /// no one else shares this.
+ pub(crate) fn normalize_mut(&mut self) {
+ match Rc::get_mut(&mut self.0) {
+ // Mutate directly if sole owner
+ Some(vint) => vint.normalize_mut(),
+ // Otherwise mutate through the refcell
+ None => self.normalize(),
+ }
+ }
+ pub(crate) fn normalize(&self) {
+ self.0.normalize()
+ }
+
+ pub(crate) fn app(&self, v: Value) -> Value {
+ let body_t = match &*self.get_type_not_sort().kind() {
+ ValueKind::PiClosure { annot, closure, .. } => {
+ v.check_type(annot);
+ closure.apply(v.clone())
+ }
+ _ => unreachable!("Internal type error"),
+ };
+ Value::from_kind_and_type(apply_any(self.clone(), v, &body_t), body_t)
+ }
+
+ /// In debug mode, panic if the provided type doesn't match the value's type.
+ /// Otherwise does nothing.
+ pub(crate) fn check_type(&self, _ty: &Value) {
+ // TODO: reenable
+ // debug_assert_eq!(
+ // Some(ty),
+ // self.get_type().ok().as_ref(),
+ // "Internal type error"
+ // );
+ }
+ pub(crate) fn get_type(&self) -> Result<Value, TypeError> {
+ Ok(self.0.get_type()?.clone())
+ }
+ /// When we know the value isn't `Sort`, this gets the type directly
+ pub(crate) fn get_type_not_sort(&self) -> Value {
+ self.get_type()
+ .expect("Internal type error: value is `Sort` but shouldn't be")
+ }
+
+ pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr {
+ let map_uniontype = |kts: &HashMap<Label, Option<Value>>| {
+ ExprKind::UnionType(
+ kts.iter()
+ .map(|(k, v)| {
+ (k.clone(), v.as_ref().map(|v| v.to_tyexpr(venv)))
+ })
+ .collect(),
+ )
+ };
+
+ let tye = match &*self.kind() {
+ ValueKind::Var(v) => TyExprKind::Var(venv.lookup(v)),
+ ValueKind::AppliedBuiltin(closure) => closure.to_tyexprkind(venv),
+ self_kind => TyExprKind::Expr(match self_kind {
+ ValueKind::Var(..) | ValueKind::AppliedBuiltin(..) => {
+ unreachable!()
+ }
+ ValueKind::LamClosure {
+ binder,
+ annot,
+ closure,
+ } => ExprKind::Lam(
+ binder.to_label(),
+ annot.to_tyexpr(venv),
+ closure.to_tyexpr(venv),
+ ),
+ ValueKind::PiClosure {
+ binder,
+ annot,
+ closure,
+ } => ExprKind::Pi(
+ binder.to_label(),
+ annot.to_tyexpr(venv),
+ closure.to_tyexpr(venv),
+ ),
+ 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(
+ Value::from_builtin(Builtin::OptionalNone).to_tyexpr(venv),
+ n.to_tyexpr(venv),
+ ),
+ ValueKind::NEOptionalLit(n) => {
+ ExprKind::SomeLit(n.to_tyexpr(venv))
+ }
+ ValueKind::EmptyListLit(n) => {
+ ExprKind::EmptyListLit(TyExpr::new(
+ TyExprKind::Expr(ExprKind::App(
+ Value::from_builtin(Builtin::List).to_tyexpr(venv),
+ n.to_tyexpr(venv),
+ )),
+ Some(Value::from_const(Const::Type)),
+ Span::Artificial,
+ ))
+ }
+ ValueKind::NEListLit(elts) => ExprKind::NEListLit(
+ elts.iter().map(|v| v.to_tyexpr(venv)).collect(),
+ ),
+ ValueKind::TextLit(elts) => ExprKind::TextLit(
+ elts.iter()
+ .map(|t| t.map_ref(|v| v.to_tyexpr(venv)))
+ .collect(),
+ ),
+ ValueKind::RecordLit(kvs) => ExprKind::RecordLit(
+ kvs.iter()
+ .map(|(k, v)| (k.clone(), v.to_tyexpr(venv)))
+ .collect(),
+ ),
+ ValueKind::RecordType(kts) => ExprKind::RecordType(
+ kts.iter()
+ .map(|(k, v)| (k.clone(), v.to_tyexpr(venv)))
+ .collect(),
+ ),
+ ValueKind::UnionType(kts) => map_uniontype(kts),
+ ValueKind::UnionConstructor(l, kts, t) => ExprKind::Field(
+ TyExpr::new(
+ TyExprKind::Expr(map_uniontype(kts)),
+ Some(t.clone()),
+ Span::Artificial,
+ ),
+ l.clone(),
+ ),
+ ValueKind::UnionLit(l, v, kts, uniont, ctort) => ExprKind::App(
+ TyExpr::new(
+ TyExprKind::Expr(ExprKind::Field(
+ TyExpr::new(
+ TyExprKind::Expr(map_uniontype(kts)),
+ Some(uniont.clone()),
+ Span::Artificial,
+ ),
+ l.clone(),
+ )),
+ Some(ctort.clone()),
+ Span::Artificial,
+ ),
+ v.to_tyexpr(venv),
+ ),
+ ValueKind::Equivalence(x, y) => ExprKind::BinOp(
+ BinOp::Equivalence,
+ x.to_tyexpr(venv),
+ y.to_tyexpr(venv),
+ ),
+ ValueKind::PartialExpr(e) => e.map_ref(|v| v.to_tyexpr(venv)),
+ }),
+ };
+
+ TyExpr::new(tye, self.0.ty.clone(), self.0.span.clone())
+ }
+ pub fn to_tyexpr_noenv(&self) -> TyExpr {
+ self.to_tyexpr(VarEnv::new())
+ }
+}
+
+impl ValueInternal {
+ fn from_whnf(k: ValueKind, ty: Option<Value>, span: Span) -> Self {
+ ValueInternal {
+ kind: lazy::Lazy::new_completed(k),
+ ty,
+ span,
+ }
+ }
+ fn from_thunk(th: Thunk, ty: Option<Value>, span: Span) -> Self {
+ ValueInternal {
+ kind: lazy::Lazy::new(th),
+ ty,
+ span,
+ }
+ }
+ fn into_value(self) -> Value {
+ Value(Rc::new(self))
+ }
+
+ fn kind(&self) -> &ValueKind {
+ &self.kind
+ }
+ fn normalize(&self) {
+ self.kind().normalize();
+ }
+ // TODO: deprecated
+ fn normalize_mut(&mut self) {
+ self.normalize();
+ }
+
+ fn get_type(&self) -> Result<&Value, TypeError> {
+ match &self.ty {
+ Some(t) => Ok(t),
+ None => Err(TypeError::new(TypeMessage::Sort)),
+ }
+ }
+}
+
+impl ValueKind {
+ pub(crate) fn into_value_with_type(self, t: Value) -> Value {
+ Value::from_kind_and_type(self, t)
+ }
+
+ pub(crate) fn normalize(&self) {
+ match self {
+ ValueKind::Var(..)
+ | ValueKind::Const(_)
+ | ValueKind::BoolLit(_)
+ | ValueKind::NaturalLit(_)
+ | ValueKind::IntegerLit(_)
+ | ValueKind::DoubleLit(_) => {}
+
+ ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => {
+ tth.normalize();
+ }
+
+ ValueKind::NEOptionalLit(th) => {
+ th.normalize();
+ }
+ ValueKind::LamClosure { annot, closure, .. }
+ | ValueKind::PiClosure { annot, closure, .. } => {
+ annot.normalize();
+ closure.normalize();
+ }
+ ValueKind::AppliedBuiltin(closure) => closure.normalize(),
+ ValueKind::NEListLit(elts) => {
+ for x in elts.iter() {
+ x.normalize();
+ }
+ }
+ ValueKind::RecordLit(kvs) => {
+ for x in kvs.values() {
+ x.normalize();
+ }
+ }
+ ValueKind::RecordType(kvs) => {
+ for x in kvs.values() {
+ x.normalize();
+ }
+ }
+ ValueKind::UnionType(kts)
+ | ValueKind::UnionConstructor(_, kts, _) => {
+ for x in kts.values().flat_map(|opt| opt) {
+ x.normalize();
+ }
+ }
+ ValueKind::UnionLit(_, v, kts, _, _) => {
+ v.normalize();
+ for x in kts.values().flat_map(|opt| opt) {
+ x.normalize();
+ }
+ }
+ ValueKind::TextLit(tlit) => tlit.normalize(),
+ ValueKind::Equivalence(x, y) => {
+ x.normalize();
+ y.normalize();
+ }
+ ValueKind::PartialExpr(e) => {
+ e.map_ref(Value::normalize);
+ }
+ }
+ }
+
+ pub(crate) fn from_builtin(b: Builtin) -> ValueKind {
+ ValueKind::from_builtin_env(b, NzEnv::new())
+ }
+ pub(crate) fn from_builtin_env(b: Builtin, env: NzEnv) -> ValueKind {
+ ValueKind::AppliedBuiltin(BuiltinClosure::new(b, env))
+ }
+}
+
+impl Thunk {
+ pub fn new(env: &NzEnv, body: TyExpr) -> Self {
+ Thunk::Thunk {
+ env: env.clone(),
+ body,
+ }
+ }
+ pub fn from_partial_expr(
+ env: NzEnv,
+ expr: ExprKind<Value, Normalized>,
+ ty: Value,
+ ) -> Self {
+ Thunk::PartialExpr { env, expr, ty }
+ }
+ pub fn eval(self) -> ValueKind {
+ match self {
+ Thunk::Thunk { env, body } => normalize_tyexpr_whnf(&body, &env),
+ Thunk::PartialExpr { env, expr, ty } => {
+ normalize_one_layer(expr, &ty, &env)
+ }
+ }
+ }
+}
+
+impl Closure {
+ pub fn new(arg_ty: Value, env: &NzEnv, body: TyExpr) -> Self {
+ Closure::Closure {
+ arg_ty,
+ env: env.clone(),
+ body,
+ }
+ }
+ /// New closure that ignores its argument
+ pub fn new_constant(body: Value) -> Self {
+ Closure::ConstantClosure { body }
+ }
+
+ pub fn apply(&self, val: Value) -> Value {
+ match self {
+ Closure::Closure { env, body, .. } => {
+ body.eval(&env.insert_value(val))
+ }
+ Closure::ConstantClosure { body, .. } => body.clone(),
+ }
+ }
+ fn apply_var(&self, var: NzVar) -> Value {
+ match self {
+ Closure::Closure { arg_ty, .. } => {
+ let val = Value::from_kind_and_type(
+ ValueKind::Var(var),
+ arg_ty.clone(),
+ );
+ self.apply(val)
+ }
+ Closure::ConstantClosure { body, .. } => body.clone(),
+ }
+ }
+
+ // TODO: somehow normalize the body. Might require to pass an env.
+ pub fn normalize(&self) {}
+ /// Convert this closure to a TyExpr
+ pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr {
+ self.apply_var(NzVar::new(venv.size()))
+ .to_tyexpr(venv.insert())
+ }
+ /// If the closure variable is free in the closure, return Err. Otherwise, return the value
+ /// with that free variable remove.
+ pub fn remove_binder(&self) -> Result<Value, ()> {
+ match self {
+ Closure::Closure { .. } => {
+ let v = NzVar::fresh();
+ // TODO: handle case where variable is used in closure
+ // TODO: return information about where the variable is used
+ Ok(self.apply_var(v))
+ }
+ Closure::ConstantClosure { body, .. } => Ok(body.clone()),
+ }
+ }
+}
+
+impl TextLit {
+ pub fn new(
+ elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
+ ) -> Self {
+ TextLit(squash_textlit(elts))
+ }
+ pub fn interpolate(v: Value) -> TextLit {
+ TextLit(vec![InterpolatedTextContents::Expr(v)])
+ }
+ pub fn from_text(s: String) -> TextLit {
+ TextLit(vec![InterpolatedTextContents::Text(s)])
+ }
+
+ pub fn concat(&self, other: &TextLit) -> TextLit {
+ TextLit::new(self.iter().chain(other.iter()).cloned())
+ }
+ pub fn is_empty(&self) -> bool {
+ self.0.is_empty()
+ }
+ /// If the literal consists of only one interpolation and not text, return the interpolated
+ /// value.
+ pub fn as_single_expr(&self) -> Option<&Value> {
+ use InterpolatedTextContents::Expr;
+ if let [Expr(v)] = self.0.as_slice() {
+ Some(v)
+ } else {
+ None
+ }
+ }
+ /// If there are no interpolations, return the corresponding text value.
+ pub fn as_text(&self) -> Option<String> {
+ use InterpolatedTextContents::Text;
+ if self.is_empty() {
+ Some(String::new())
+ } else if let [Text(s)] = self.0.as_slice() {
+ Some(s.clone())
+ } else {
+ None
+ }
+ }
+ pub fn iter(
+ &self,
+ ) -> impl Iterator<Item = &InterpolatedTextContents<Value>> {
+ self.0.iter()
+ }
+ /// Normalize the contained values. This does not break the invariant because we have already
+ /// ensured that no contained values normalize to a TextLit.
+ pub fn normalize(&self) {
+ for x in self.0.iter() {
+ x.map_ref(Value::normalize);
+ }
+ }
+}
+
+impl lazy::Eval<ValueKind> for Thunk {
+ fn eval(self) -> ValueKind {
+ self.eval()
+ }
+}
+
+/// Compare two values for equality modulo alpha/beta-equivalence.
+impl std::cmp::PartialEq for Value {
+ fn eq(&self, other: &Self) -> bool {
+ Rc::ptr_eq(&self.0, &other.0) || self.kind() == other.kind()
+ }
+}
+impl std::cmp::Eq for Value {}
+
+impl std::cmp::PartialEq for Thunk {
+ fn eq(&self, _other: &Self) -> bool {
+ unreachable!(
+ "Trying to compare thunks but we should only compare WHNFs"
+ )
+ }
+}
+impl std::cmp::Eq for Thunk {}
+
+impl std::cmp::PartialEq for Closure {
+ fn eq(&self, other: &Self) -> bool {
+ let v = NzVar::fresh();
+ self.apply_var(v) == other.apply_var(v)
+ }
+}
+impl std::cmp::Eq for Closure {}
+
+impl std::fmt::Debug for Value {
+ fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+ let vint: &ValueInternal = &self.0;
+ let kind = vint.kind();
+ if let ValueKind::Const(c) = kind {
+ return write!(fmt, "{:?}", c);
+ }
+ let mut x = fmt.debug_struct(&format!("Value@WHNF"));
+ x.field("kind", kind);
+ if let Some(ty) = vint.ty.as_ref() {
+ x.field("type", &ty);
+ } else {
+ x.field("type", &None::<()>);
+ }
+ x.finish()
+ }
+}
diff --git a/dhall/src/semantics/nze/var.rs b/dhall/src/semantics/nze/var.rs
new file mode 100644
index 0000000..264b81d
--- /dev/null
+++ b/dhall/src/semantics/nze/var.rs
@@ -0,0 +1,36 @@
+use crate::syntax::Label;
+
+// Exactly like a Label, but equality returns always true.
+// This is so that ValueKind equality is exactly alpha-equivalence.
+#[derive(Clone, Eq)]
+pub struct Binder {
+ name: Label,
+}
+
+impl Binder {
+ pub(crate) fn new(name: Label) -> Self {
+ Binder { name }
+ }
+ pub(crate) fn to_label(&self) -> Label {
+ self.clone().into()
+ }
+}
+
+/// Equality up to alpha-equivalence
+impl std::cmp::PartialEq for Binder {
+ fn eq(&self, _other: &Self) -> bool {
+ true
+ }
+}
+
+impl std::fmt::Debug for Binder {
+ fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+ write!(f, "Binder({})", &self.name)
+ }
+}
+
+impl From<Binder> for Label {
+ fn from(x: Binder) -> Label {
+ x.name
+ }
+}
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-19 04:55:01 +0000