summaryrefslogtreecommitdiff
path: root/dhall/src/semantics
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics')
-rw-r--r--dhall/src/semantics/builtins.rs15
-rw-r--r--dhall/src/semantics/nze/normalize.rs139
-rw-r--r--dhall/src/semantics/nze/value.rs6
-rw-r--r--dhall/src/semantics/tck/typecheck.rs183
4 files changed, 300 insertions, 43 deletions
diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
index c20fb77..907d449 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/semantics/builtins.rs
@@ -1,5 +1,5 @@
use crate::semantics::{
- self, typecheck, NzEnv, TyExpr, TyExprKind, Value, ValueKind, VarEnv,
+ typecheck, NzEnv, TyExpr, TyExprKind, Value, ValueKind, VarEnv,
};
use crate::syntax::map::DupTreeMap;
use crate::syntax::Const::Type;
@@ -301,9 +301,7 @@ fn apply_builtin(
_ => Ret::DoneAsIs,
},
(NaturalShow, [n]) => match &*n.kind() {
- NaturalLit(n) => Ret::ValueKind(TextLit(
- semantics::TextLit::from_text(n.to_string()),
- )),
+ NaturalLit(n) => Ret::Value(Value::from_text(n)),
_ => Ret::DoneAsIs,
},
(NaturalSubtract, [a, b]) => match (&*a.kind(), &*b.kind()) {
@@ -322,7 +320,7 @@ fn apply_builtin(
} else {
format!("+{}", n)
};
- Ret::ValueKind(TextLit(semantics::TextLit::from_text(s)))
+ Ret::Value(Value::from_text(s))
}
_ => Ret::DoneAsIs,
},
@@ -343,9 +341,7 @@ fn apply_builtin(
_ => Ret::DoneAsIs,
},
(DoubleShow, [n]) => match &*n.kind() {
- DoubleLit(n) => Ret::ValueKind(TextLit(
- semantics::TextLit::from_text(n.to_string()),
- )),
+ DoubleLit(n) => Ret::Value(Value::from_text(n)),
_ => Ret::DoneAsIs,
},
(TextShow, [v]) => match &*v.kind() {
@@ -355,8 +351,7 @@ fn apply_builtin(
let txt: InterpolatedText<Normalized> =
std::iter::once(InterpolatedTextContents::Text(s))
.collect();
- let s = txt.to_string();
- Ret::ValueKind(TextLit(semantics::TextLit::from_text(s)))
+ Ret::Value(Value::from_text(txt))
} else {
Ret::DoneAsIs
}
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index e9d140b..a00b7ff 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -1,3 +1,4 @@
+use itertools::Itertools;
use std::collections::HashMap;
use crate::semantics::NzEnv;
@@ -184,6 +185,7 @@ fn apply_binop<'a>(
}
Ret::ValueKind(RecordLit(kvs))
}
+ (RightBiasedRecordMerge, _, _) if x == y => Ret::ValueRef(y),
(RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
Ret::ValueRef(x)
@@ -242,9 +244,9 @@ pub(crate) fn normalize_one_layer(
env: &NzEnv,
) -> ValueKind {
use ValueKind::{
- BoolLit, DoubleLit, EmptyOptionalLit, IntegerLit, NEListLit,
- NEOptionalLit, NaturalLit, RecordLit, RecordType, UnionConstructor,
- UnionLit, UnionType,
+ BoolLit, DoubleLit, EmptyListLit, EmptyOptionalLit, IntegerLit,
+ NEListLit, NEOptionalLit, NaturalLit, PartialExpr, RecordLit,
+ RecordType, UnionConstructor, UnionLit, UnionType,
};
let ret = match expr {
@@ -271,7 +273,7 @@ pub(crate) fn normalize_one_layer(
ExprKind::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)),
ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)),
ExprKind::EmptyListLit(t) => {
- let arg = match &*t.kind() {
+ let arg = match t.kind() {
ValueKind::AppliedBuiltin(BuiltinClosure {
b: Builtin::List,
args,
@@ -330,6 +332,13 @@ pub(crate) fn normalize_one_layer(
.filter_map(|l| kvs.get(l).map(|x| (l.clone(), x.clone())))
.collect(),
)),
+ PartialExpr(ExprKind::Projection(v2, _)) => {
+ return normalize_one_layer(
+ ExprKind::Projection(v2.clone(), ls.clone()),
+ ty,
+ env,
+ )
+ }
_ => Ret::Expr(expr),
},
ExprKind::Field(ref v, ref l) => match v.kind() {
@@ -342,6 +351,88 @@ pub(crate) fn normalize_one_layer(
kts.clone(),
v.get_type().unwrap(),
)),
+ PartialExpr(ExprKind::BinOp(
+ BinOp::RightBiasedRecordMerge,
+ x,
+ y,
+ )) => match (x.kind(), y.kind()) {
+ (_, RecordLit(kvs)) => match kvs.get(l) {
+ Some(r) => Ret::Value(r.clone()),
+ None => {
+ return normalize_one_layer(
+ ExprKind::Field(x.clone(), l.clone()),
+ ty,
+ env,
+ )
+ }
+ },
+ (RecordLit(kvs), _) => match kvs.get(l) {
+ Some(r) => Ret::Expr(ExprKind::Field(
+ Value::from_kind_and_type(
+ PartialExpr(ExprKind::BinOp(
+ BinOp::RightBiasedRecordMerge,
+ Value::from_kind_and_type(
+ RecordLit({
+ let mut kvs = HashMap::new();
+ kvs.insert(l.clone(), r.clone());
+ kvs
+ }),
+ Value::from_kind_and_type(
+ RecordType({
+ let mut kvs = HashMap::new();
+ kvs.insert(
+ l.clone(),
+ r.get_type_not_sort(),
+ );
+ kvs
+ }),
+ r.get_type_not_sort()
+ .get_type_not_sort(),
+ ),
+ ),
+ y.clone(),
+ )),
+ v.get_type_not_sort(),
+ ),
+ l.clone(),
+ )),
+ None => {
+ return normalize_one_layer(
+ ExprKind::Field(y.clone(), l.clone()),
+ ty,
+ env,
+ )
+ }
+ },
+ _ => Ret::Expr(expr),
+ },
+ PartialExpr(ExprKind::BinOp(
+ BinOp::RecursiveRecordTypeMerge,
+ x,
+ y,
+ )) => match (x.kind(), y.kind()) {
+ (RecordLit(kvs), _) => match kvs.get(l) {
+ Some(_) => Ret::Expr(expr),
+ None => {
+ return normalize_one_layer(
+ ExprKind::Field(y.clone(), l.clone()),
+ ty,
+ env,
+ )
+ }
+ },
+ (_, RecordLit(kvs)) => match kvs.get(l) {
+ Some(_) => Ret::Expr(expr),
+ None => {
+ return normalize_one_layer(
+ ExprKind::Field(x.clone(), l.clone()),
+ ty,
+ env,
+ )
+ }
+ },
+ _ => Ret::Expr(expr),
+ },
_ => Ret::Expr(expr),
},
ExprKind::ProjectionByExpr(_, _) => {
@@ -373,7 +464,45 @@ pub(crate) fn normalize_one_layer(
_ => Ret::Expr(expr),
}
}
- ExprKind::ToMap(_, _) => unimplemented!("toMap"),
+ ExprKind::ToMap(ref v, ref annot) => match v.kind() {
+ RecordLit(kvs) if kvs.is_empty() => {
+ match annot.as_ref().map(|v| v.kind()) {
+ Some(ValueKind::AppliedBuiltin(BuiltinClosure {
+ b: Builtin::List,
+ args,
+ ..
+ })) if args.len() == 1 => {
+ Ret::ValueKind(EmptyListLit(args[0].clone()))
+ }
+ _ => Ret::Expr(expr),
+ }
+ }
+ RecordLit(kvs) => Ret::ValueKind(NEListLit(
+ kvs.iter()
+ .sorted_by_key(|(k, _)| k.clone())
+ .map(|(k, v)| {
+ let mut rec = HashMap::new();
+ let mut rec_ty = HashMap::new();
+ rec.insert("mapKey".into(), Value::from_text(k));
+ rec.insert("mapValue".into(), v.clone());
+ rec_ty.insert(
+ "mapKey".into(),
+ Value::from_builtin(Builtin::Text),
+ );
+ rec_ty.insert("mapValue".into(), v.get_type_not_sort());
+
+ Value::from_kind_and_type(
+ ValueKind::RecordLit(rec),
+ Value::from_kind_and_type(
+ ValueKind::RecordType(rec_ty),
+ Value::from_const(Const::Type),
+ ),
+ )
+ })
+ .collect(),
+ )),
+ _ => Ret::Expr(expr),
+ },
};
match ret {
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 1143781..607aa0d 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -167,6 +167,12 @@ impl Value {
typecheck(&type_of_builtin(b)).unwrap().eval_closed_expr(),
)
}
+ pub(crate) fn from_text(txt: impl ToString) -> Self {
+ Value::from_kind_and_type(
+ ValueKind::TextLit(TextLit::from_text(txt.to_string())),
+ Value::from_builtin(Builtin::Text),
+ )
+ }
pub(crate) fn as_const(&self) -> Option<Const> {
match &*self.kind() {
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index c3c589b..6817712 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -51,9 +51,9 @@ fn mkerr<T, S: ToString>(x: S) -> Result<T, TypeError> {
/// layer.
fn type_one_layer(
env: &TyEnv,
- kind: &ExprKind<TyExpr, Normalized>,
+ ekind: ExprKind<TyExpr, Normalized>,
span: Span,
-) -> Result<Type, TypeError> {
+) -> Result<TyExpr, TypeError> {
let span_err = |msg: &str| {
mkerr(
ErrorBuilder::new(msg.to_string())
@@ -62,7 +62,7 @@ fn type_one_layer(
)
};
- Ok(match kind {
+ let ty = match &ekind {
ExprKind::Import(..) => unreachable!(
"There should remain no imports in a resolved expression"
),
@@ -74,13 +74,8 @@ fn type_one_layer(
let body_ty = body.get_type()?;
let body_ty = body_ty.to_tyexpr(env.as_varenv().insert());
let pi_ekind = ExprKind::Pi(binder.clone(), annot.clone(), body_ty);
- let pi_ty = type_one_layer(env, &pi_ekind, Span::Artificial)?;
- let ty = TyExpr::new(
- TyExprKind::Expr(pi_ekind),
- Some(pi_ty),
- Span::Artificial,
- );
- ty.eval(env.as_nzenv())
+ type_one_layer(env, pi_ekind, Span::Artificial)?
+ .eval(env.as_nzenv())
}
ExprKind::Pi(_, annot, body) => {
let ks = match annot.get_type()?.as_const() {
@@ -187,7 +182,7 @@ fn type_one_layer(
}
let ty = type_of_recordtype(
- span,
+ span.clone(),
kts.iter()
.map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_varenv()))),
)?;
@@ -206,7 +201,10 @@ fn type_one_layer(
};
}
- type_of_recordtype(span, kts.iter().map(|(_, t)| Cow::Borrowed(t)))?
+ type_of_recordtype(
+ span.clone(),
+ kts.iter().map(|(_, t)| Cow::Borrowed(t)),
+ )?
}
ExprKind::UnionType(kts) => {
use std::collections::hash_map::Entry;
@@ -389,7 +387,7 @@ fn type_one_layer(
// Construct the final record type
let ty = type_of_recordtype(
- span,
+ span.clone(),
kts.iter()
.map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_varenv()))),
)?;
@@ -401,9 +399,7 @@ fn type_one_layer(
x.get_type()?.to_tyexpr(env.as_varenv()),
y.get_type()?.to_tyexpr(env.as_varenv()),
);
- let ty = type_one_layer(env, &ekind, Span::Artificial)?;
- TyExpr::new(TyExprKind::Expr(ekind), Some(ty), Span::Artificial)
- .eval(env.as_nzenv())
+ type_one_layer(env, ekind, Span::Artificial)?.eval(env.as_nzenv())
}
ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
let x_val = x.eval(env.as_nzenv());
@@ -420,7 +416,7 @@ fn type_one_layer(
if let Some(ty) = kts_y.get(k) {
type_one_layer(
env,
- &ExprKind::BinOp(
+ ExprKind::BinOp(
BinOp::RecursiveRecordTypeMerge,
tx.to_tyexpr(env.as_varenv()),
ty.to_tyexpr(env.as_varenv()),
@@ -547,9 +543,14 @@ fn type_one_layer(
);
}
- closure.remove_binder().or_else(|()| {
- span_err("MergeReturnTypeIsDependent")
- })?
+ match closure.remove_binder() {
+ Ok(v) => v,
+ Err(()) => {
+ return span_err(
+ "MergeReturnTypeIsDependent",
+ )
+ }
+ }
}
_ => {
return mkerr(
@@ -619,7 +620,85 @@ fn type_one_layer(
(None, None) => return span_err("MergeEmptyNeedsAnnotation"),
}
}
- ExprKind::ToMap(_, _) => unimplemented!("toMap"),
+ ExprKind::ToMap(record, annot) => {
+ let record_t = record.get_type()?;
+ let kts = match record_t.kind() {
+ ValueKind::RecordType(kts) => kts,
+ _ => {
+ return span_err("The argument to `toMap` must be a record")
+ }
+ };
+
+ if kts.is_empty() {
+ let annot = if let Some(annot) = annot {
+ annot
+ } else {
+ return span_err(
+ "`toMap` applied to an empty record requires a type \
+ annotation",
+ );
+ };
+ let annot_val = annot.eval(env.as_nzenv());
+
+ let err_msg = "The type of `toMap x` must be of the form \
+ `List { mapKey : Text, mapValue : T }`";
+ let arg = match annot_val.kind() {
+ ValueKind::AppliedBuiltin(BuiltinClosure {
+ b: Builtin::List,
+ args,
+ ..
+ }) if args.len() == 1 => &args[0],
+ _ => return span_err(err_msg),
+ };
+ let kts = match arg.kind() {
+ ValueKind::RecordType(kts) => kts,
+ _ => return span_err(err_msg),
+ };
+ if kts.len() != 2 {
+ return span_err(err_msg);
+ }
+ match kts.get(&"mapKey".into()) {
+ Some(t) if *t == Value::from_builtin(Builtin::Text) => {}
+ _ => return span_err(err_msg),
+ }
+ match kts.get(&"mapValue".into()) {
+ Some(_) => {}
+ None => return span_err(err_msg),
+ }
+ annot_val
+ } else {
+ let entry_type = kts.iter().next().unwrap().1.clone();
+ if entry_type.get_type()?.as_const() != Some(Const::Type) {
+ return span_err(
+ "`toMap` only accepts records of type `Type`",
+ );
+ }
+ for (_, t) in kts.iter() {
+ if *t != entry_type {
+ return span_err(
+ "Every field of the record must have the same type",
+ );
+ }
+ }
+
+ let mut kts = HashMap::new();
+ kts.insert("mapKey".into(), Value::from_builtin(Builtin::Text));
+ kts.insert("mapValue".into(), entry_type);
+ let output_type = Value::from_builtin(Builtin::List).app(
+ Value::from_kind_and_type(
+ ValueKind::RecordType(kts),
+ Value::from_const(Const::Type),
+ ),
+ );
+ if let Some(annot) = annot {
+ let annot_val = annot.eval(env.as_nzenv());
+ if output_type != annot_val {
+ return span_err("Annotation mismatch");
+ }
+ }
+ output_type
+ }
+ }
ExprKind::Projection(record, labels) => {
let record_type = record.get_type()?;
let kts = match record_type.kind() {
@@ -648,11 +727,61 @@ fn type_one_layer(
record_type.get_type()?,
)
}
- ExprKind::ProjectionByExpr(_, _) => {
- unimplemented!("selection by expression")
+ ExprKind::ProjectionByExpr(record, selection) => {
+ let record_type = record.get_type()?;
+ let rec_kts = match record_type.kind() {
+ ValueKind::RecordType(kts) => kts,
+ _ => return span_err("ProjectionMustBeRecord"),
+ };
+
+ let selection_val = selection.eval(env.as_nzenv());
+ let sel_kts = match selection_val.kind() {
+ ValueKind::RecordType(kts) => kts,
+ _ => return span_err("ProjectionByExprTakesRecordType"),
+ };
+
+ for (l, sel_ty) in sel_kts {
+ match rec_kts.get(l) {
+ Some(rec_ty) => {
+ if rec_ty != sel_ty {
+ return span_err("ProjectionWrongType");
+ }
+ }
+ None => return span_err("ProjectionMissingEntry"),
+ }
+ }
+
+ selection_val
+ }
+ ExprKind::Completion(ty, compl) => {
+ let ty_field_default = type_one_layer(
+ env,
+ ExprKind::Field(ty.clone(), "default".into()),
+ span.clone(),
+ )?;
+ let ty_field_type = type_one_layer(
+ env,
+ ExprKind::Field(ty.clone(), "Type".into()),
+ span.clone(),
+ )?;
+ let merge = type_one_layer(
+ env,
+ ExprKind::BinOp(
+ BinOp::RightBiasedRecordMerge,
+ ty_field_default,
+ compl.clone(),
+ ),
+ span.clone(),
+ )?;
+ return type_one_layer(
+ env,
+ ExprKind::Annot(merge, ty_field_type),
+ span.clone(),
+ );
}
- ExprKind::Completion(_, _) => unimplemented!("record completion"),
- })
+ };
+
+ Ok(TyExpr::new(TyExprKind::Expr(ekind), Some(ty), span))
}
/// `type_with` typechecks an expressio in the provided environment.
@@ -708,9 +837,7 @@ pub(crate) fn type_with(
}
_ => ekind.traverse_ref(|e| type_with(env, e))?,
};
-
- let ty = type_one_layer(env, &ekind, expr.span())?;
- (TyExprKind::Expr(ekind), Some(ty))
+ return type_one_layer(env, ekind, expr.span());
}
};
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-06 15:15:25 +0000