summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/phase
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics/phase')
-rw-r--r--dhall/src/semantics/phase/normalize.rs155
-rw-r--r--dhall/src/semantics/phase/typecheck.rs30
2 files changed, 103 insertions, 82 deletions
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index d81a910..459eaf1 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -1,4 +1,5 @@
use std::collections::HashMap;
+use std::convert::TryInto;
use crate::semantics::core::value::Value;
use crate::semantics::core::value::ValueKind;
@@ -141,6 +142,16 @@ pub(crate) fn apply_builtin(
}
_ => Ret::DoneAsIs,
},
+ (IntegerNegate, [n]) => match &*n.as_whnf() {
+ IntegerLit(n) => Ret::ValueKind(IntegerLit(-n)),
+ _ => Ret::DoneAsIs,
+ },
+ (IntegerClamp, [n]) => match &*n.as_whnf() {
+ IntegerLit(n) => {
+ Ret::ValueKind(NaturalLit((*n).try_into().unwrap_or(0)))
+ }
+ _ => Ret::DoneAsIs,
+ },
(DoubleShow, [n]) => {
match &*n.as_whnf() {
DoubleLit(n) => Ret::ValueKind(TextLit(vec![
@@ -259,37 +270,23 @@ pub(crate) fn apply_builtin(
_ => Ret::DoneAsIs,
}
}
- (ListBuild, [t, f]) => match &*f.as_whnf() {
- // fold/build fusion
- ValueKind::AppliedBuiltin(ListFold, args) => {
- if args.len() >= 2 {
- Ret::Value(args[1].clone())
- } else {
- // Do we really need to handle this case ?
- unimplemented!()
- }
- }
- _ => {
- let list_t = Value::from_builtin(List).app(t.clone());
- Ret::Value(
- f.app(list_t.clone())
- .app({
- // Move `t` under new variables
- let t1 = t.under_binder(Label::from("x"));
- let t2 = t1.under_binder(Label::from("xs"));
- make_closure!(
- λ(x : #t) ->
- λ(xs : List #t1) ->
- [ var(x, 1, #t2) ] # var(xs, 0, List #t2)
- )
- })
- .app(
- EmptyListLit(t.clone())
- .into_value_with_type(list_t),
- ),
- )
- }
- },
+ (ListBuild, [t, f]) => {
+ let list_t = Value::from_builtin(List).app(t.clone());
+ Ret::Value(
+ f.app(list_t.clone())
+ .app({
+ // Move `t` under new variables
+ let t1 = t.under_binder(Label::from("x"));
+ let t2 = t1.under_binder(Label::from("xs"));
+ make_closure!(
+ λ(x : #t) ->
+ λ(xs : List #t1) ->
+ [ var(x, 1, #t2) ] # var(xs, 0, List #t2)
+ )
+ })
+ .app(EmptyListLit(t.clone()).into_value_with_type(list_t)),
+ )
+ }
(ListFold, [_, l, _, cons, nil, r @ ..]) => match &*l.as_whnf() {
EmptyListLit(_) => Ret::ValueWithRemainingArgs(r, nil.clone()),
NEListLit(xs) => {
@@ -301,31 +298,20 @@ pub(crate) fn apply_builtin(
}
_ => Ret::DoneAsIs,
},
- (OptionalBuild, [t, f]) => match &*f.as_whnf() {
- // fold/build fusion
- ValueKind::AppliedBuiltin(OptionalFold, args) => {
- if args.len() >= 2 {
- Ret::Value(args[1].clone())
- } else {
- // Do we really need to handle this case ?
- unimplemented!()
- }
- }
- _ => {
- let optional_t = Value::from_builtin(Optional).app(t.clone());
- Ret::Value(
- f.app(optional_t.clone())
- .app({
- let t1 = t.under_binder(Label::from("x"));
- make_closure!(λ(x: #t) -> Some(var(x, 0, #t1)))
- })
- .app(
- EmptyOptionalLit(t.clone())
- .into_value_with_type(optional_t),
- ),
- )
- }
- },
+ (OptionalBuild, [t, f]) => {
+ let optional_t = Value::from_builtin(Optional).app(t.clone());
+ Ret::Value(
+ f.app(optional_t.clone())
+ .app({
+ let t1 = t.under_binder(Label::from("x"));
+ make_closure!(λ(x: #t) -> Some(var(x, 0, #t1)))
+ })
+ .app(
+ EmptyOptionalLit(t.clone())
+ .into_value_with_type(optional_t),
+ ),
+ )
+ }
(OptionalFold, [_, v, _, just, nothing, r @ ..]) => match &*v.as_whnf()
{
EmptyOptionalLit(_) => {
@@ -336,27 +322,17 @@ pub(crate) fn apply_builtin(
}
_ => Ret::DoneAsIs,
},
- (NaturalBuild, [f]) => match &*f.as_whnf() {
- // fold/build fusion
- ValueKind::AppliedBuiltin(NaturalFold, args) => {
- if !args.is_empty() {
- Ret::Value(args[0].clone())
- } else {
- // Do we really need to handle this case ?
- unimplemented!()
- }
- }
- _ => Ret::Value(
- f.app(Value::from_builtin(Natural))
- .app(make_closure!(
- λ(x : Natural) -> 1 + var(x, 0, Natural)
- ))
- .app(
- NaturalLit(0)
- .into_value_with_type(Value::from_builtin(Natural)),
- ),
- ),
- },
+ (NaturalBuild, [f]) => Ret::Value(
+ f.app(Value::from_builtin(Natural))
+ .app(make_closure!(
+ λ(x : Natural) -> 1 + var(x, 0, Natural)
+ ))
+ .app(
+ NaturalLit(0)
+ .into_value_with_type(Value::from_builtin(Natural)),
+ ),
+ ),
+
(NaturalFold, [n, t, succ, zero, r @ ..]) => match &*n.as_whnf() {
NaturalLit(0) => Ret::ValueWithRemainingArgs(r, zero.clone()),
NaturalLit(n) => {
@@ -614,8 +590,8 @@ pub(crate) fn normalize_one_layer(
ty: &Value,
) -> ValueKind {
use ValueKind::{
- AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit,
- NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit,
+ AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, EmptyOptionalLit,
+ IntegerLit, NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit,
UnionConstructor, UnionLit, UnionType,
};
@@ -741,6 +717,7 @@ pub(crate) fn normalize_one_layer(
ExprKind::ProjectionByExpr(_, _) => {
unimplemented!("selection by expression")
}
+ ExprKind::Completion(_, _) => unimplemented!("record completion"),
ExprKind::Merge(ref handlers, ref variant, _) => {
let handlers_borrow = handlers.as_whnf();
@@ -762,6 +739,26 @@ pub(crate) fn normalize_one_layer(
Ret::Expr(expr)
}
},
+ (RecordLit(kvs), EmptyOptionalLit(_)) => {
+ match kvs.get(&"None".into()) {
+ Some(h) => Ret::Value(h.clone()),
+ None => {
+ drop(handlers_borrow);
+ drop(variant_borrow);
+ Ret::Expr(expr)
+ }
+ }
+ }
+ (RecordLit(kvs), NEOptionalLit(v)) => {
+ match kvs.get(&"Some".into()) {
+ Some(h) => Ret::Value(h.app(v.clone())),
+ None => {
+ drop(handlers_borrow);
+ drop(variant_borrow);
+ Ret::Expr(expr)
+ }
+ }
+ }
_ => {
drop(handlers_borrow);
drop(variant_borrow);
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index c439f74..97502d4 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -1,3 +1,4 @@
+use std::borrow::Cow;
use std::cmp::max;
use std::collections::HashMap;
@@ -235,6 +236,9 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
IntegerToDouble => make_type!(Integer -> Double),
IntegerShow => make_type!(Integer -> Text),
+ IntegerNegate => make_type!(Integer -> Integer),
+ IntegerClamp => make_type!(Integer -> Natural),
+
DoubleShow => make_type!(Double -> Text),
TextShow => make_type!(Text -> Text),
@@ -692,8 +696,19 @@ fn type_last_layer(
let union_type = union.get_type()?;
let union_borrow = union_type.as_whnf();
let variants = match &*union_borrow {
- ValueKind::UnionType(kts) => kts,
- _ => return mkerr(Merge2ArgMustBeUnion(union.clone())),
+ ValueKind::UnionType(kts) => Cow::Borrowed(kts),
+ ValueKind::AppliedBuiltin(syntax::Builtin::Optional, args)
+ if args.len() == 1 =>
+ {
+ let ty = &args[0];
+ let mut kts = HashMap::new();
+ kts.insert("None".into(), None);
+ kts.insert("Some".into(), Some(ty.clone()));
+ Cow::Owned(kts)
+ }
+ _ => {
+ return mkerr(Merge2ArgMustBeUnionOrOptional(union.clone()))
+ }
};
let mut inferred_type = None;
@@ -774,7 +789,15 @@ fn type_last_layer(
for l in labels {
match kts.get(l) {
None => return mkerr(ProjectionMissingEntry),
- Some(t) => new_kts.insert(l.clone(), t.clone()),
+ Some(t) => {
+ use std::collections::hash_map::Entry;
+ match new_kts.entry(l.clone()) {
+ Entry::Occupied(_) => {
+ return mkerr(ProjectionDuplicateField)
+ }
+ Entry::Vacant(e) => e.insert(t.clone()),
+ }
+ }
};
}
@@ -784,6 +807,7 @@ fn type_last_layer(
))
}
ProjectionByExpr(_, _) => unimplemented!("selection by expression"),
+ Completion(_, _) => unimplemented!("record completion"),
};
Ok(match ret {
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 11:37:06 +0000