summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/operations/normalization.rs181
-rw-r--r--dhall/src/operations/typecheck.rs63
-rw-r--r--dhall/src/semantics/nze/lazy.rs32
-rw-r--r--dhall/src/semantics/nze/nir.rs58
-rw-r--r--dhall/src/semantics/nze/normalize.rs4
-rw-r--r--dhall/src/semantics/tck/tir.rs3
-rw-r--r--dhall/src/semantics/tck/typecheck.rs4
7 files changed, 152 insertions, 193 deletions
diff --git a/dhall/src/operations/normalization.rs b/dhall/src/operations/normalization.rs
index dbd58f9..28375b2 100644
--- a/dhall/src/operations/normalization.rs
+++ b/dhall/src/operations/normalization.rs
@@ -8,52 +8,52 @@ use crate::semantics::{
};
use crate::syntax::{ExprKind, Label, NumKind};
-fn normalize_binop(o: BinOp, x: &Nir, y: &Nir) -> Ret {
+fn normalize_binop(o: BinOp, x: Nir, y: Nir) -> Ret {
use BinOp::*;
use NirKind::{EmptyListLit, NEListLit, Num, RecordLit, RecordType};
use NumKind::{Bool, Natural};
match (o, x.kind(), y.kind()) {
- (BoolAnd, Num(Bool(true)), _) => ret_ref(y),
- (BoolAnd, _, Num(Bool(true))) => ret_ref(x),
+ (BoolAnd, Num(Bool(true)), _) => ret_nir(y),
+ (BoolAnd, _, Num(Bool(true))) => ret_nir(x),
(BoolAnd, Num(Bool(false)), _) => ret_kind(Num(Bool(false))),
(BoolAnd, _, Num(Bool(false))) => ret_kind(Num(Bool(false))),
- (BoolAnd, _, _) if x == y => ret_ref(x),
+ (BoolAnd, _, _) if x == y => ret_nir(x),
(BoolOr, Num(Bool(true)), _) => ret_kind(Num(Bool(true))),
(BoolOr, _, Num(Bool(true))) => ret_kind(Num(Bool(true))),
- (BoolOr, Num(Bool(false)), _) => ret_ref(y),
- (BoolOr, _, Num(Bool(false))) => ret_ref(x),
- (BoolOr, _, _) if x == y => ret_ref(x),
- (BoolEQ, Num(Bool(true)), _) => ret_ref(y),
- (BoolEQ, _, Num(Bool(true))) => ret_ref(x),
+ (BoolOr, Num(Bool(false)), _) => ret_nir(y),
+ (BoolOr, _, Num(Bool(false))) => ret_nir(x),
+ (BoolOr, _, _) if x == y => ret_nir(x),
+ (BoolEQ, Num(Bool(true)), _) => ret_nir(y),
+ (BoolEQ, _, Num(Bool(true))) => ret_nir(x),
(BoolEQ, Num(Bool(x)), Num(Bool(y))) => ret_kind(Num(Bool(x == y))),
(BoolEQ, _, _) if x == y => ret_kind(Num(Bool(true))),
- (BoolNE, Num(Bool(false)), _) => ret_ref(y),
- (BoolNE, _, Num(Bool(false))) => ret_ref(x),
+ (BoolNE, Num(Bool(false)), _) => ret_nir(y),
+ (BoolNE, _, Num(Bool(false))) => ret_nir(x),
(BoolNE, Num(Bool(x)), Num(Bool(y))) => ret_kind(Num(Bool(x != y))),
(BoolNE, _, _) if x == y => ret_kind(Num(Bool(false))),
- (NaturalPlus, Num(Natural(0)), _) => ret_ref(y),
- (NaturalPlus, _, Num(Natural(0))) => ret_ref(x),
+ (NaturalPlus, Num(Natural(0)), _) => ret_nir(y),
+ (NaturalPlus, _, Num(Natural(0))) => ret_nir(x),
(NaturalPlus, Num(Natural(x)), Num(Natural(y))) => {
ret_kind(Num(Natural(x + y)))
}
(NaturalTimes, Num(Natural(0)), _) => ret_kind(Num(Natural(0))),
(NaturalTimes, _, Num(Natural(0))) => ret_kind(Num(Natural(0))),
- (NaturalTimes, Num(Natural(1)), _) => ret_ref(y),
- (NaturalTimes, _, Num(Natural(1))) => ret_ref(x),
+ (NaturalTimes, Num(Natural(1)), _) => ret_nir(y),
+ (NaturalTimes, _, Num(Natural(1))) => ret_nir(x),
(NaturalTimes, Num(Natural(x)), Num(Natural(y))) => {
ret_kind(Num(Natural(x * y)))
}
- (ListAppend, EmptyListLit(_), _) => ret_ref(y),
- (ListAppend, _, EmptyListLit(_)) => ret_ref(x),
+ (ListAppend, EmptyListLit(_), _) => ret_nir(y),
+ (ListAppend, _, EmptyListLit(_)) => ret_nir(x),
(ListAppend, NEListLit(xs), NEListLit(ys)) => {
ret_kind(NEListLit(xs.iter().chain(ys.iter()).cloned().collect()))
}
- (TextAppend, NirKind::TextLit(x), _) if x.is_empty() => ret_ref(y),
- (TextAppend, _, NirKind::TextLit(y)) if y.is_empty() => ret_ref(x),
+ (TextAppend, NirKind::TextLit(x), _) if x.is_empty() => ret_nir(y),
+ (TextAppend, _, NirKind::TextLit(y)) if y.is_empty() => ret_nir(x),
(TextAppend, NirKind::TextLit(x), NirKind::TextLit(y)) => {
ret_kind(NirKind::TextLit(x.concat(y)))
}
@@ -65,10 +65,10 @@ fn normalize_binop(o: BinOp, x: &Nir, y: &Nir) -> Ret {
)),
(RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
- ret_ref(x)
+ ret_nir(x)
}
(RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
- ret_ref(y)
+ ret_nir(y)
}
(RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
let mut kvs = kvs2.clone();
@@ -78,13 +78,13 @@ fn normalize_binop(o: BinOp, x: &Nir, y: &Nir) -> Ret {
}
ret_kind(RecordLit(kvs))
}
- (RightBiasedRecordMerge, _, _) if x == y => ret_ref(y),
+ (RightBiasedRecordMerge, _, _) if x == y => ret_nir(y),
(RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
- ret_ref(x)
+ ret_nir(x)
}
(RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
- ret_ref(y)
+ ret_nir(y)
}
(RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
let kvs = merge_maps(kvs1, kvs2, |_, v1, v2| {
@@ -113,11 +113,9 @@ fn normalize_binop(o: BinOp, x: &Nir, y: &Nir) -> Ret {
ret_kind(RecordType(kts))
}
- (Equivalence, _, _) => {
- ret_kind(NirKind::Equivalence(x.clone(), y.clone()))
- }
+ (Equivalence, _, _) => ret_kind(NirKind::Equivalence(x, y)),
- _ => ret_op(OpKind::BinOp(o, x.clone(), y.clone())),
+ _ => ret_op(OpKind::BinOp(o, x, y)),
}
}
@@ -189,7 +187,7 @@ fn normalize_field(v: &Nir, field: &Label) -> Ret {
}
}
-pub fn normalize_operation(opkind: &OpKind<Nir>) -> Ret {
+pub fn normalize_operation(opkind: OpKind<Nir>) -> Ret {
use self::BinOp::RightBiasedRecordMerge;
use NirKind::{
EmptyListLit, EmptyOptionalLit, NEListLit, NEOptionalLit, Num, Op,
@@ -197,46 +195,45 @@ pub fn normalize_operation(opkind: &OpKind<Nir>) -> Ret {
};
use NumKind::Bool;
use OpKind::*;
- let nothing_to_do = || ret_op(opkind.clone());
match opkind {
- App(v, a) => ret_kind(v.app_to_kind(a.clone())),
- BinOp(o, x, y) => normalize_binop(*o, x, y),
+ App(v, a) => ret_kind(v.app_to_kind(a)),
+ BinOp(o, x, y) => normalize_binop(o, x, y),
BoolIf(b, e1, e2) => {
match b.kind() {
- Num(Bool(true)) => ret_ref(e1),
- Num(Bool(false)) => ret_ref(e2),
+ Num(Bool(true)) => ret_nir(e1),
+ Num(Bool(false)) => ret_nir(e2),
_ => {
match (e1.kind(), e2.kind()) {
// Simplify `if b then True else False`
- (Num(Bool(true)), Num(Bool(false))) => ret_ref(b),
- _ if e1 == e2 => ret_ref(e1),
- _ => nothing_to_do(),
+ (Num(Bool(true)), Num(Bool(false))) => ret_nir(b),
+ _ if e1 == e2 => ret_nir(e1),
+ _ => ret_op(BoolIf(b, e1, e2)),
}
}
}
}
- Merge(handlers, variant, _) => match handlers.kind() {
+ Merge(handlers, variant, ty) => match handlers.kind() {
RecordLit(kvs) => match variant.kind() {
UnionConstructor(l, _) => match kvs.get(l) {
Some(h) => ret_ref(h),
- None => nothing_to_do(),
+ None => ret_op(Merge(handlers, variant, ty)),
},
UnionLit(l, v, _) => match kvs.get(l) {
Some(h) => ret_kind(h.app_to_kind(v.clone())),
- None => nothing_to_do(),
+ None => ret_op(Merge(handlers, variant, ty)),
},
EmptyOptionalLit(_) => match kvs.get("None") {
Some(h) => ret_ref(h),
- None => nothing_to_do(),
+ None => ret_op(Merge(handlers, variant, ty)),
},
NEOptionalLit(v) => match kvs.get("Some") {
Some(h) => ret_kind(h.app_to_kind(v.clone())),
- None => nothing_to_do(),
+ None => ret_op(Merge(handlers, variant, ty)),
},
- _ => nothing_to_do(),
+ _ => ret_op(Merge(handlers, variant, ty)),
},
- _ => nothing_to_do(),
+ _ => ret_op(Merge(handlers, variant, ty)),
},
ToMap(v, annot) => match v.kind() {
RecordLit(kvs) if kvs.is_empty() => {
@@ -244,7 +241,7 @@ pub fn normalize_operation(opkind: &OpKind<Nir>) -> Ret {
Some(NirKind::ListType(t)) => {
ret_kind(EmptyListLit(t.clone()))
}
- _ => nothing_to_do(),
+ _ => ret_op(ToMap(v, annot)),
}
}
RecordLit(kvs) => ret_kind(NEListLit(
@@ -258,9 +255,9 @@ pub fn normalize_operation(opkind: &OpKind<Nir>) -> Ret {
})
.collect(),
)),
- _ => nothing_to_do(),
+ _ => ret_op(ToMap(v, annot)),
},
- Field(v, field) => normalize_field(v, field),
+ Field(v, field) => normalize_field(&v, &field),
Projection(_, ls) if ls.is_empty() => {
ret_kind(RecordLit(HashMap::new()))
}
@@ -271,12 +268,12 @@ pub fn normalize_operation(opkind: &OpKind<Nir>) -> Ret {
.collect(),
)),
Op(Projection(v2, _)) => {
- normalize_operation(&Projection(v2.clone(), ls.clone()))
+ normalize_operation(Projection(v2.clone(), ls))
}
Op(BinOp(RightBiasedRecordMerge, l, r)) => match r.kind() {
RecordLit(kvs) => {
let r_keys = kvs.keys().cloned().collect();
- normalize_operation(&BinOp(
+ normalize_operation(BinOp(
RightBiasedRecordMerge,
Nir::from_partial_expr(ExprKind::Op(Projection(
l.clone(),
@@ -288,73 +285,45 @@ pub fn normalize_operation(opkind: &OpKind<Nir>) -> Ret {
))),
))
}
- _ => nothing_to_do(),
+ _ => ret_op(Projection(v, ls)),
},
- _ => nothing_to_do(),
+ _ => ret_op(Projection(v, ls)),
},
ProjectionByExpr(v, t) => match t.kind() {
- RecordType(kts) => normalize_operation(&Projection(
- v.clone(),
+ RecordType(kts) => normalize_operation(Projection(
+ v,
kts.keys().cloned().collect(),
)),
- _ => nothing_to_do(),
+ _ => ret_op(ProjectionByExpr(v, t)),
},
- With(record, labels, expr) => {
- let mut current_nir: Option<Nir> = Some(record.clone());
- let mut visited: Vec<(&Label, HashMap<Label, Nir>)> = Vec::new();
- let mut to_create = Vec::new();
-
- // To be used when an abstract entry is reached
- let mut abstract_nir = None;
-
- for label in labels {
- match current_nir {
- None => to_create.push(label.clone()),
- Some(nir) => match nir.kind() {
- RecordLit(kvs) => {
- current_nir = kvs.get(label).cloned();
- visited.push((label, kvs.clone()));
- }
- // Handle partially abstract case
- _ => {
- abstract_nir = Some(nir);
- to_create.push(label.clone());
- current_nir = None;
- }
- },
+ With(mut record, labels, expr) => {
+ let mut labels = labels.into_iter();
+ let mut current = &mut record;
+ // We dig through the current record with the provided labels.
+ while let RecordLit(kvs) = current.kind_mut() {
+ if let Some(label) = labels.next() {
+ // Get existing entry or insert empty record into it.
+ let nir = kvs.entry(label).or_insert_with(|| {
+ Nir::from_kind(RecordLit(HashMap::new()))
+ });
+ // Disgusting, but the normal assignment works with -Zpolonius, so this
+ // is safe. See https://github.com/rust-lang/rust/issues/70255 .
+ current = unsafe { &mut *(nir as *mut _) };
+ } else {
+ break;
}
}
- // Create Nir for record bottom up
- let mut nir = expr.clone();
-
- match abstract_nir {
- // No abstract nir, creating singleton records
- None => {
- while let Some(label) = to_create.pop() {
- let rec =
- RecordLit(once((label.clone(), nir)).collect());
- nir = Nir::from_kind(rec);
- }
- }
- // Abstract nir, creating with op
- Some(abstract_nir) => {
- nir = Nir::from_kind(Op(OpKind::With(
- abstract_nir,
- to_create,
- nir,
- )));
- }
- }
-
- // Update visited records
- while let Some((label, mut kvs)) = visited.pop() {
- kvs.insert(label.clone(), nir);
- let rec = RecordLit(kvs);
- nir = Nir::from_kind(rec);
- }
+ // If there are still some fields to dig through, we need to create a `with` expression
+ // with the remaining fields.
+ let labels: Vec<_> = labels.collect();
+ *current = if labels.is_empty() {
+ expr
+ } else {
+ Nir::from_kind(Op(OpKind::With(current.clone(), labels, expr)))
+ };
- ret_nir(nir)
+ ret_nir(record)
}
Completion(..) => {
unreachable!("This case should have been handled in resolution")
diff --git a/dhall/src/operations/typecheck.rs b/dhall/src/operations/typecheck.rs
index 9329aff..3016fea 100644
--- a/dhall/src/operations/typecheck.rs
+++ b/dhall/src/operations/typecheck.rs
@@ -48,8 +48,8 @@ fn typecheck_binop(
env: &TyEnv,
span: Span,
op: BinOp,
- l: &Tir<'_>,
- r: &Tir<'_>,
+ l: Tir<'_>,
+ r: Tir<'_>,
) -> Result<Type, TypeError> {
let span_err = |msg: &str| mk_span_err(span.clone(), msg);
use BinOp::*;
@@ -290,7 +290,7 @@ fn typecheck_merge(
pub fn typecheck_operation(
env: &TyEnv,
span: Span,
- opkind: &OpKind<Tir<'_>>,
+ opkind: OpKind<Tir<'_>>,
) -> Result<Type, TypeError> {
let span_err = |msg: &str| mk_span_err(span.clone(), msg);
use NirKind::{ListType, PiClosure, RecordType, UnionType};
@@ -345,7 +345,7 @@ pub fn typecheck_operation(
),
}
}
- BinOp(o, l, r) => typecheck_binop(env, span, *o, l, r)?,
+ BinOp(o, l, r) => typecheck_binop(env, span, o, l, r)?,
BoolIf(x, y, z) => {
if *x.ty().kind() != NirKind::from_builtin(Builtin::Bool) {
return span_err("InvalidPredicate");
@@ -360,7 +360,7 @@ pub fn typecheck_operation(
y.ty().clone()
}
Merge(record, scrut, type_annot) => {
- typecheck_merge(env, span, record, scrut, type_annot.as_ref())?
+ typecheck_merge(env, span, &record, &scrut, type_annot.as_ref())?
}
ToMap(record, annot) => {
if record.ty().ty().as_const() != Some(Const::Type) {
@@ -434,14 +434,14 @@ pub fn typecheck_operation(
}
Field(scrut, x) => {
match scrut.ty().kind() {
- RecordType(kts) => match kts.get(x) {
+ RecordType(kts) => match kts.get(&x) {
Some(val) => Type::new_infer_universe(env, val.clone())?,
None => return span_err("MissingRecordField"),
},
NirKind::Const(_) => {
let scrut = scrut.eval_to_type(env)?;
match scrut.kind() {
- UnionType(kts) => match kts.get(x) {
+ UnionType(kts) => match kts.get(&x) {
// Constructor has type T -> < x: T, ... >
Some(Some(ty)) => Nir::from_kind(PiClosure {
binder: Binder::new(x.clone()),
@@ -467,7 +467,7 @@ pub fn typecheck_operation(
let mut new_kts = HashMap::new();
for l in labels {
- match kts.get(l) {
+ match kts.get(&l) {
None => return span_err("ProjectionMissingEntry"),
Some(t) => {
new_kts.insert(l.clone(), t.clone());
@@ -504,45 +504,22 @@ pub fn typecheck_operation(
selection_val
}
With(record, labels, expr) => {
- use crate::syntax::Label;
- use std::iter::once;
-
- let mut current_nir: Option<Nir> =
- Some(record.ty().as_nir().clone());
- let mut visited: Vec<(&Label, HashMap<Label, Nir>)> = Vec::new();
- let mut to_create = Vec::new();
-
+ let mut record_ty = record.into_ty().into_nir();
+ let mut current = &mut record_ty;
+ // We dig through the current record type with the provided labels.
for label in labels {
- match current_nir {
- None => to_create.push(label),
- Some(nir) => {
- let kts = (match nir.kind() {
- NirKind::RecordType(kts) => Ok(kts.clone()),
- _ => mk_span_err(span.clone(), "WithMustBeRecord"), // TODO better error
- })?;
-
- current_nir = kts.get(label).cloned();
- visited.push((label, kts));
- }
+ if let RecordType(kts) = current.kind_mut() {
+ // Get existing entry or insert empty record type into it.
+ current = kts.entry(label).or_insert_with(|| {
+ Nir::from_kind(RecordType(HashMap::new()))
+ });
+ } else {
+ return mk_span_err(span.clone(), "WithMustBeRecord");
}
}
+ *current = expr.into_ty().into_nir();
- // Create Nir for record type bottom up
- let mut nir = expr.ty().as_nir().clone();
-
- while let Some(label) = to_create.pop() {
- let rec = RecordType(once((label.clone(), nir)).collect());
- nir = Nir::from_kind(rec);
- }
-
- // Update visited records
- while let Some((label, mut kts)) = visited.pop() {
- kts.insert(label.clone(), nir);
- let rec = RecordType(kts);
- nir = Nir::from_kind(rec);
- }
-
- Type::new_infer_universe(env, nir)?
+ Type::new_infer_universe(env, record_ty)?
}
Completion(..) => {
unreachable!("This case should have been handled in resolution")
diff --git a/dhall/src/semantics/nze/lazy.rs b/dhall/src/semantics/nze/lazy.rs
index d361313..d3b5c8d 100644
--- a/dhall/src/semantics/nze/lazy.rs
+++ b/dhall/src/semantics/nze/lazy.rs
@@ -35,6 +35,22 @@ where
let _ = lazy.tgt.set(tgt);
lazy
}
+
+ pub fn force(&self) -> &Tgt {
+ self.tgt.get_or_init(|| {
+ let src = self.src.take().unwrap();
+ src.eval()
+ })
+ }
+
+ pub fn get_mut(&mut self) -> &mut Tgt {
+ self.force();
+ self.tgt.get_mut().unwrap()
+ }
+ pub fn into_inner(self) -> Tgt {
+ self.force();
+ self.tgt.into_inner().unwrap()
+ }
}
impl<Src, Tgt> Deref for Lazy<Src, Tgt>
@@ -43,10 +59,18 @@ where
{
type Target = Tgt;
fn deref(&self) -> &Self::Target {
- self.tgt.get_or_init(|| {
- let src = self.src.take().unwrap();
- src.eval()
- })
+ self.force()
+ }
+}
+
+/// This implementation evaluates before cloning, because we can't clone the contents of a `Cell`.
+impl<Src, Tgt> Clone for Lazy<Src, Tgt>
+where
+ Src: Eval<Tgt>,
+ Tgt: Clone,
+{
+ fn clone(&self) -> Self {
+ Self::new_completed(self.force().clone())
}
}
diff --git a/dhall/src/semantics/nze/nir.rs b/dhall/src/semantics/nze/nir.rs
index 12f1b14..7bda836 100644
--- a/dhall/src/semantics/nze/nir.rs
+++ b/dhall/src/semantics/nze/nir.rs
@@ -14,18 +14,13 @@ use crate::syntax::{
use crate::ToExprOptions;
/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation
-/// automatically. Uses a Rc<RefCell> to share computation.
+/// automatically. Uses a Rc<OnceCell> to share computation.
/// If you compare for equality two `Nir`s, then equality will be up to alpha-equivalence
/// (renaming of bound variables) and beta-equivalence (normalization). It will recursively
/// normalize as needed.
-/// Stands for "Normalized intermediate representation"
+/// Stands for "Normalized Intermediate Representation"
#[derive(Clone)]
-pub struct Nir(Rc<NirInternal>);
-
-#[derive(Debug)]
-struct NirInternal {
- kind: lazy::Lazy<Thunk, NirKind>,
-}
+pub struct Nir(Rc<lazy::Lazy<Thunk, NirKind>>);
/// An unevaluated subexpression
#[derive(Debug, Clone)]
@@ -101,17 +96,17 @@ pub enum NirKind {
impl Nir {
/// Construct a Nir from a completely unnormalized expression.
pub fn new_thunk(env: NzEnv, hir: Hir) -> Nir {
- NirInternal::from_thunk(Thunk::new(env, hir)).into_nir()
+ Nir(Rc::new(lazy::Lazy::new(Thunk::new(env, hir))))
}
/// Construct a Nir from a partially normalized expression that's not in WHNF.
pub fn from_partial_expr(e: ExprKind<Nir>) -> Nir {
// TODO: env
let env = NzEnv::new();
- NirInternal::from_thunk(Thunk::from_partial_expr(env, e)).into_nir()
+ Nir(Rc::new(lazy::Lazy::new(Thunk::from_partial_expr(env, e))))
}
/// Make a Nir from a NirKind
pub fn from_kind(v: NirKind) -> Nir {
- NirInternal::from_whnf(v).into_nir()
+ Nir(Rc::new(lazy::Lazy::new_completed(v)))
}
pub fn from_const(c: Const) -> Self {
Self::from_kind(NirKind::Const(c))
@@ -135,7 +130,20 @@ impl Nir {
/// This is what you want if you want to pattern-match on the value.
pub fn kind(&self) -> &NirKind {
- self.0.kind()
+ &*self.0
+ }
+
+ /// The contents of a `Nir` are immutable and shared. If however we happen to be the sole
+ /// owners, we can mutate it directly. Otherwise, this clones the internal value first.
+ pub fn kind_mut(&mut self) -> &mut NirKind {
+ Rc::make_mut(&mut self.0).get_mut()
+ }
+ /// If we are the sole owner of this Nir, we can avoid a clone.
+ pub fn into_kind(self) -> NirKind {
+ match Rc::try_unwrap(self.0) {
+ Ok(lazy) => lazy.into_inner(),
+ Err(rc) => (**rc).clone(),
+ }
}
pub fn to_type(&self, u: impl Into<Universe>) -> Type {
@@ -273,26 +281,6 @@ impl Nir {
}
}
-impl NirInternal {
- fn from_whnf(k: NirKind) -> Self {
- NirInternal {
- kind: lazy::Lazy::new_completed(k),
- }
- }
- fn from_thunk(th: Thunk) -> Self {
- NirInternal {
- kind: lazy::Lazy::new(th),
- }
- }
- fn into_nir(self) -> Nir {
- Nir(Rc::new(self))
- }
-
- fn kind(&self) -> &NirKind {
- &self.kind
- }
-}
-
impl NirKind {
pub fn into_nir(self) -> Nir {
Nir::from_kind(self)
@@ -448,13 +436,11 @@ impl std::cmp::Eq for Closure {}
impl std::fmt::Debug for Nir {
fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
- let vint: &NirInternal = &self.0;
- let kind = vint.kind();
- if let NirKind::Const(c) = kind {
+ if let NirKind::Const(c) = self.kind() {
return write!(fmt, "{:?}", c);
}
let mut x = fmt.debug_struct("Nir");
- x.field("kind", kind);
+ x.field("kind", self.kind());
x.finish()
}
}
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index d042f3f..62efc5f 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -84,7 +84,7 @@ where
pub type Ret = NirKind;
pub fn ret_nir(x: Nir) -> Ret {
- ret_ref(&x)
+ x.into_kind()
}
pub fn ret_kind(x: NirKind) -> Ret {
x
@@ -144,7 +144,7 @@ pub fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
ExprKind::UnionType(kvs) => {
ret_kind(UnionType(kvs.into_iter().collect()))
}
- ExprKind::Op(ref op) => normalize_operation(op),
+ ExprKind::Op(op) => normalize_operation(op),
ExprKind::Annot(x, _) => ret_nir(x),
ExprKind::Assert(x) => ret_kind(Assert(x)),
ExprKind::Import(..) => {
diff --git a/dhall/src/semantics/tck/tir.rs b/dhall/src/semantics/tck/tir.rs
index ec15a1f..f34802c 100644
--- a/dhall/src/semantics/tck/tir.rs
+++ b/dhall/src/semantics/tck/tir.rs
@@ -117,6 +117,9 @@ impl<'hir> Tir<'hir> {
pub fn ty(&self) -> &Type {
&self.ty
}
+ pub fn into_ty(self) -> Type {
+ self.ty
+ }
pub fn to_hir(&self) -> Hir {
self.as_hir().clone()
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index d21c7ce..498bd76 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -35,7 +35,7 @@ fn type_one_layer(
) -> Result<Type, TypeError> {
let span_err = |msg: &str| mk_span_err(span.clone(), msg);
- Ok(match &ekind {
+ Ok(match ekind {
ExprKind::Import(..) => {
unreachable!("This case should have been handled in resolution")
}
@@ -57,7 +57,7 @@ fn type_one_layer(
NumKind::Double(_) => Builtin::Double,
}),
ExprKind::Builtin(b) => {
- let t_hir = type_of_builtin(*b);
+ let t_hir = type_of_builtin(b);
typecheck(&t_hir)?.eval_to_type(env)?
}
ExprKind::TextLit(interpolated) => {
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 22:48:49 +0000