summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/lib.rs32
-rw-r--r--dhall/src/semantics/builtins.rs41
-rw-r--r--dhall/src/semantics/nze/normalize.rs124
-rw-r--r--dhall/src/semantics/nze/value.rs84
-rw-r--r--dhall/src/semantics/tck/typecheck.rs42
5 files changed, 86 insertions, 237 deletions
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index d8eeb4a..48d4d96 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -24,7 +24,7 @@ use crate::semantics::resolve;
use crate::semantics::resolve::ImportRoot;
use crate::semantics::{typecheck, typecheck_with, TyExpr, Value, ValueKind};
use crate::syntax::binary;
-use crate::syntax::{Builtin, Const, Expr};
+use crate::syntax::{Builtin, Expr};
pub type ParsedExpr = Expr<Normalized>;
pub type DecodedExpr = Expr<Normalized>;
@@ -148,18 +148,12 @@ impl Normalized {
self.0
}
- pub(crate) fn from_const(c: Const) -> Self {
- Normalized(Value::from_const(c))
- }
- pub(crate) fn from_kind_and_type(v: ValueKind, t: Normalized) -> Self {
- Normalized(Value::from_kind_and_type(v, t.into_value()))
+ pub(crate) fn from_kind(v: ValueKind) -> Self {
+ Normalized(Value::from_kind(v))
}
pub(crate) fn from_value(th: Value) -> Self {
Normalized(th)
}
- pub(crate) fn const_type() -> Self {
- Normalized::from_const(Const::Type)
- }
pub fn make_builtin_type(b: Builtin) -> Self {
Normalized::from_value(Value::from_builtin(b))
@@ -177,23 +171,17 @@ impl Normalized {
pub fn make_record_type(
kts: impl Iterator<Item = (String, Normalized)>,
) -> Self {
- Normalized::from_kind_and_type(
- ValueKind::RecordType(
- kts.map(|(k, t)| (k.into(), t.into_value())).collect(),
- ),
- Normalized::const_type(),
- )
+ Normalized::from_kind(ValueKind::RecordType(
+ kts.map(|(k, t)| (k.into(), t.into_value())).collect(),
+ ))
}
pub fn make_union_type(
kts: impl Iterator<Item = (String, Option<Normalized>)>,
) -> Self {
- Normalized::from_kind_and_type(
- ValueKind::UnionType(
- kts.map(|(k, t)| (k.into(), t.map(|t| t.into_value())))
- .collect(),
- ),
- Normalized::const_type(),
- )
+ Normalized::from_kind(ValueKind::UnionType(
+ kts.map(|(k, t)| (k.into(), t.map(|t| t.into_value())))
+ .collect(),
+ ))
}
}
diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
index 907d449..a513967 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/semantics/builtins.rs
@@ -35,11 +35,11 @@ impl BuiltinClosure<Value> {
}
}
- pub fn apply(&self, a: Value, f_ty: Value, ret_ty: &Value) -> ValueKind {
+ pub fn apply(&self, a: Value, f_ty: Value) -> ValueKind {
use std::iter::once;
let args = self.args.iter().cloned().chain(once(a.clone())).collect();
let types = self.types.iter().cloned().chain(once(f_ty)).collect();
- apply_builtin(self.b, args, ret_ty, types, self.env.clone())
+ apply_builtin(self.b, args, types, self.env.clone())
}
/// This doesn't break the invariant because we already checked that the appropriate arguments
/// did not normalize to something that allows evaluation to proceed.
@@ -267,7 +267,6 @@ macro_rules! make_closure {
fn apply_builtin(
b: Builtin,
args: Vec<Value>,
- ty: &Value,
types: Vec<Value>,
env: NzEnv,
) -> ValueKind {
@@ -399,10 +398,7 @@ fn apply_builtin(
let mut kts = HashMap::new();
kts.insert("index".into(), Value::from_builtin(Natural));
kts.insert("value".into(), t.clone());
- let t = Value::from_kind_and_type(
- RecordType(kts),
- Value::from_const(Type),
- );
+ let t = Value::from_kind(RecordType(kts));
// Construct the new list, with added indices
let list = match &*l_whnf {
@@ -414,18 +410,10 @@ fn apply_builtin(
let mut kvs = HashMap::new();
kvs.insert(
"index".into(),
- Value::from_kind_and_type(
- NaturalLit(i),
- Value::from_builtin(
- Builtin::Natural,
- ),
- ),
+ Value::from_kind(NaturalLit(i)),
);
kvs.insert("value".into(), e.clone());
- Value::from_kind_and_type(
- RecordLit(kvs),
- t.clone(),
- )
+ Value::from_kind(RecordLit(kvs))
})
.collect(),
),
@@ -449,7 +437,7 @@ fn apply_builtin(
))
.app(t.clone()),
)
- .app(EmptyListLit(t.clone()).into_value_with_type(list_t)),
+ .app(EmptyListLit(t.clone()).into_value()),
)
}
(ListFold, [_, l, _, cons, nil]) => match &*l.kind() {
@@ -475,10 +463,7 @@ fn apply_builtin(
))
.app(t.clone()),
)
- .app(
- EmptyOptionalLit(t.clone())
- .into_value_with_type(optional_t),
- ),
+ .app(EmptyOptionalLit(t.clone()).into_value()),
)
}
(OptionalFold, [_, v, _, just, nothing]) => match &*v.kind() {
@@ -492,20 +477,14 @@ fn apply_builtin(
λ(x : Natural) ->
1 + var(x)
)))
- .app(
- NaturalLit(0)
- .into_value_with_type(Value::from_builtin(Natural)),
- ),
+ .app(NaturalLit(0).into_value()),
),
(NaturalFold, [n, t, succ, zero]) => match &*n.kind() {
NaturalLit(0) => Ret::Value(zero.clone()),
NaturalLit(n) => {
let fold = Value::from_builtin(NaturalFold)
- .app(
- NaturalLit(n - 1)
- .into_value_with_type(Value::from_builtin(Natural)),
- )
+ .app(NaturalLit(n - 1).into_value())
.app(t.clone())
.app(succ.clone())
.app(zero.clone());
@@ -517,7 +496,7 @@ fn apply_builtin(
};
match ret {
Ret::ValueKind(v) => v,
- Ret::Value(v) => v.to_whnf_check_type(ty),
+ Ret::Value(v) => v.kind().clone(),
Ret::DoneAsIs => AppliedBuiltin(BuiltinClosure {
b,
args,
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 3a981f4..c660fce 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -6,18 +6,16 @@ use crate::semantics::{
Binder, BuiltinClosure, Closure, TextLit, TyExpr, TyExprKind, Value,
ValueKind,
};
-use crate::syntax::{
- BinOp, Builtin, Const, ExprKind, InterpolatedTextContents,
-};
+use crate::syntax::{BinOp, Builtin, ExprKind, InterpolatedTextContents};
use crate::Normalized;
-pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind {
+pub(crate) fn apply_any(f: Value, a: Value) -> ValueKind {
match f.kind() {
ValueKind::LamClosure { closure, .. } => {
- closure.apply(a).to_whnf_check_type(ty)
+ closure.apply(a).kind().clone()
}
ValueKind::AppliedBuiltin(closure) => {
- closure.apply(a, f.get_type_not_sort(), ty)
+ closure.apply(a, f.get_type_not_sort())
}
ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit(
l.clone(),
@@ -102,12 +100,7 @@ enum Ret<'a> {
Expr(ExprKind<Value, Normalized>),
}
-fn apply_binop<'a>(
- o: BinOp,
- x: &'a Value,
- y: &'a Value,
- ty: &Value,
-) -> Option<Ret<'a>> {
+fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
use BinOp::{
BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
@@ -194,19 +187,12 @@ fn apply_binop<'a>(
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(),
- ))
+ let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |_, v1, v2| {
+ Ok(Value::from_partial_expr(ExprKind::BinOp(
+ RecursiveRecordMerge,
+ v1.clone(),
+ v2.clone(),
+ )))
})?;
Ret::ValueKind(RecordLit(kvs))
}
@@ -217,14 +203,11 @@ fn apply_binop<'a>(
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(),
- ))
+ Ok(Value::from_partial_expr(ExprKind::BinOp(
+ RecursiveRecordTypeMerge,
+ l.clone(),
+ r.clone(),
+ )))
},
)?;
Ret::ValueKind(RecordType(kts))
@@ -240,7 +223,6 @@ fn apply_binop<'a>(
pub(crate) fn normalize_one_layer(
expr: ExprKind<Value, Normalized>,
- ty: &Value,
env: &NzEnv,
) -> ValueKind {
use ValueKind::{
@@ -318,7 +300,7 @@ pub(crate) fn normalize_one_layer(
}
}
}
- ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y, ty) {
+ ExprKind::BinOp(o, ref x, ref y) => match apply_binop(o, x, y) {
Some(ret) => ret,
None => Ret::Expr(expr),
},
@@ -335,7 +317,6 @@ pub(crate) fn normalize_one_layer(
PartialExpr(ExprKind::Projection(v2, _)) => {
return normalize_one_layer(
ExprKind::Projection(v2.clone(), ls.clone()),
- ty,
env,
)
}
@@ -361,45 +342,26 @@ pub(crate) fn normalize_one_layer(
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(),
- ),
+ Value::from_kind(PartialExpr(ExprKind::BinOp(
+ BinOp::RightBiasedRecordMerge,
+ Value::from_kind(RecordLit({
+ let mut kvs = HashMap::new();
+ kvs.insert(l.clone(), r.clone());
+ kvs
+ })),
+ y.clone(),
+ ))),
l.clone(),
)),
None => {
return normalize_one_layer(
ExprKind::Field(y.clone(), l.clone()),
- ty,
env,
)
}
@@ -416,7 +378,6 @@ pub(crate) fn normalize_one_layer(
None => {
return normalize_one_layer(
ExprKind::Field(y.clone(), l.clone()),
- ty,
env,
)
}
@@ -426,7 +387,6 @@ pub(crate) fn normalize_one_layer(
None => {
return normalize_one_layer(
ExprKind::Field(x.clone(), l.clone()),
- ty,
env,
)
}
@@ -482,22 +442,9 @@ pub(crate) fn normalize_one_layer(
.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),
- ),
- )
+ Value::from_kind(ValueKind::RecordLit(rec))
})
.collect(),
)),
@@ -507,8 +454,8 @@ pub(crate) fn normalize_one_layer(
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::Value(v) => v.kind().clone(),
+ Ret::ValueRef(v) => v.kind().clone(),
Ret::Expr(expr) => ValueKind::PartialExpr(expr),
}
}
@@ -521,17 +468,16 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind {
let annot = annot.eval(env);
ValueKind::LamClosure {
binder: Binder::new(binder.clone()),
- annot: annot.clone(),
- closure: Closure::new(annot, env, body.clone()),
+ annot: annot,
+ closure: Closure::new(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,
+ closure: Closure::new(env, body.clone()),
}
}
TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => {
@@ -539,12 +485,8 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind {
body.eval(&env.insert_value_noty(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)
+ normalize_one_layer(e, env)
}
}
}
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 203b479..47c50a4 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_of_builtin, type_with, typecheck, Binder, BuiltinClosure, NzEnv,
- NzVar, TyEnv, TyExpr, TyExprKind, VarEnv,
+ type_with, Binder, BuiltinClosure, NzEnv, NzVar, TyEnv, TyExpr, TyExprKind,
+ VarEnv,
};
use crate::syntax::{
BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
@@ -39,7 +39,6 @@ pub(crate) enum Thunk {
PartialExpr {
env: NzEnv,
expr: ExprKind<Value, Normalized>,
- ty: Value,
},
}
@@ -47,11 +46,7 @@ pub(crate) enum Thunk {
#[derive(Debug, Clone)]
pub(crate) enum Closure {
/// Normal closure
- Closure {
- arg_ty: Value,
- env: NzEnv,
- body: TyExpr,
- },
+ Closure { env: NzEnv, body: TyExpr },
/// Closure that ignores the argument passed
ConstantClosure { body: Value },
}
@@ -130,21 +125,18 @@ impl Value {
.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 {
+ pub(crate) fn from_partial_expr(e: ExprKind<Value, Normalized>) -> Value {
// TODO: env
let env = NzEnv::new();
ValueInternal::from_thunk(
- Thunk::from_partial_expr(env, e, ty.clone()),
+ Thunk::from_partial_expr(env, e),
Some(Value::const_kind()),
Span::Artificial,
)
.into_value()
}
/// Make a Value from a ValueKind
- pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value {
+ pub(crate) fn from_kind(v: ValueKind) -> Value {
ValueInternal::from_whnf(v, Some(Value::const_kind()), Span::Artificial)
.into_value()
}
@@ -170,16 +162,12 @@ impl Value {
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(),
- )
+ Value::from_kind(ValueKind::from_builtin_env(b, env.clone()))
}
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),
- )
+ Value::from_kind(ValueKind::TextLit(TextLit::from_text(
+ txt.to_string(),
+ )))
}
pub(crate) fn as_const(&self) -> Option<Const> {
@@ -210,14 +198,6 @@ impl Value {
pub(crate) fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
self.to_tyexpr(env.as_varenv()).to_expr_tyenv(env)
}
- 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.
@@ -234,33 +214,19 @@ impl Value {
}
pub(crate) fn app(&self, v: Value) -> Value {
- Value::from_kind_and_type(
- apply_any(self.clone(), v, &Value::const_kind()),
- Value::const_kind(),
- )
+ Value::from_kind(apply_any(self.clone(), v))
}
- /// 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, tyenv: &TyEnv) -> Result<Value, TypeError> {
let expr = self.to_tyexpr(tyenv.as_varenv()).to_expr_tyenv(tyenv);
type_with(tyenv, &expr).unwrap().get_type()
}
- pub(crate) fn get_type_noenv(&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_noenv()
+ self.0
+ .get_type()
.expect("Internal type error: value is `Sort` but shouldn't be")
+ .clone()
}
pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr {
@@ -422,8 +388,8 @@ impl ValueInternal {
}
impl ValueKind {
- pub(crate) fn into_value_with_type(self, t: Value) -> Value {
- Value::from_kind_and_type(self, t)
+ pub(crate) fn into_value(self) -> Value {
+ Value::from_kind(self)
}
pub(crate) fn normalize(&self) {
@@ -504,24 +470,20 @@ impl Thunk {
pub fn from_partial_expr(
env: NzEnv,
expr: ExprKind<Value, Normalized>,
- ty: Value,
) -> Self {
- Thunk::PartialExpr { env, expr, ty }
+ Thunk::PartialExpr { env, expr }
}
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)
- }
+ Thunk::PartialExpr { env, expr } => normalize_one_layer(expr, &env),
}
}
}
impl Closure {
- pub fn new(arg_ty: Value, env: &NzEnv, body: TyExpr) -> Self {
+ pub fn new(env: &NzEnv, body: TyExpr) -> Self {
Closure::Closure {
- arg_ty,
env: env.clone(),
body,
}
@@ -541,12 +503,8 @@ impl Closure {
}
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::Closure { .. } => {
+ self.apply(Value::from_kind(ValueKind::Var(var)))
}
Closure::ConstantClosure { body, .. } => body.clone(),
}
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index ceb83de..810e483 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -183,11 +183,11 @@ fn type_one_layer(
};
}
- let ty = type_of_recordtype(
+ type_of_recordtype(
span.clone(),
kts.iter().map(|(_, t)| Cow::Owned(t.to_tyexpr_tyenv(env))),
)?;
- Value::from_kind_and_type(ValueKind::RecordType(kts), ty)
+ Value::from_kind(ValueKind::RecordType(kts))
}
ExprKind::RecordType(kts) => {
use std::collections::hash_map::Entry;
@@ -247,22 +247,11 @@ fn type_one_layer(
ValueKind::UnionType(kts) => match kts.get(x) {
// Constructor has type T -> < x: T, ... >
Some(Some(ty)) => {
- // Can't fail because uniontypes must have type Const(_).
- let kt = scrut.get_type()?.as_const().unwrap();
- // The type of the field must be Const smaller than `kt`, thus the
- // function type has type `kt`.
- let pi_ty = Value::from_const(kt);
-
- Value::from_kind_and_type(
- ValueKind::PiClosure {
- binder: Binder::new(x.clone()),
- annot: ty.clone(),
- closure: Closure::new_constant(
- scrut_nf,
- ),
- },
- pi_ty,
- )
+ Value::from_kind(ValueKind::PiClosure {
+ binder: Binder::new(x.clone()),
+ annot: ty.clone(),
+ closure: Closure::new_constant(scrut_nf),
+ })
}
Some(None) => scrut_nf,
None => return span_err("MissingUnionField"),
@@ -386,11 +375,11 @@ fn type_one_layer(
})?;
// Construct the final record type
- let ty = type_of_recordtype(
+ type_of_recordtype(
span.clone(),
kts.iter().map(|(_, t)| Cow::Owned(t.to_tyexpr_tyenv(env))),
)?;
- Value::from_kind_and_type(ValueKind::RecordType(kts), ty)
+ Value::from_kind(ValueKind::RecordType(kts))
}
ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
let ekind = ExprKind::BinOp(
@@ -685,12 +674,8 @@ fn type_one_layer(
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),
- ),
- );
+ let output_type = Value::from_builtin(Builtin::List)
+ .app(Value::from_kind(ValueKind::RecordType(kts)));
if let Some(annot) = annot {
let annot_val = annot.eval(env.as_nzenv());
if output_type != annot_val {
@@ -723,10 +708,7 @@ fn type_one_layer(
};
}
- Value::from_kind_and_type(
- ValueKind::RecordType(new_kts),
- record_type.get_type(env)?,
- )
+ Value::from_kind(ValueKind::RecordType(new_kts))
}
ExprKind::ProjectionByExpr(record, selection) => {
let record_type = record.get_type()?;
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 17:00:39 +0000