summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/builtins.rs
diff options
context:
space:
mode:
authorNadrieril2020-02-09 22:07:03 +0000
committerNadrieril2020-02-09 22:07:03 +0000
commitad085a20bc257d03a52708d920cfc65f0e9051e6 (patch)
treefe5767a11a0a2001e115323c6e34fa1fd20ef8cd /dhall/src/semantics/builtins.rs
parent21db63d3e614554f258526182c7ed89a2c244b65 (diff)
Remove all types from Value
Diffstat (limited to 'dhall/src/semantics/builtins.rs')
-rw-r--r--dhall/src/semantics/builtins.rs14
1 files changed, 3 insertions, 11 deletions
diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
index b1d12aa..9d4f8a2 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/semantics/builtins.rs
@@ -370,17 +370,9 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
}
_ => Ret::DoneAsIs,
},
- (ListIndexed, [_, l]) => {
- let l_whnf = l.kind();
- match &*l_whnf {
+ (ListIndexed, [t, l]) => {
+ match l.kind() {
EmptyListLit(_) | NEListLit(_) => {
- // Extract the type of the list elements
- let t = match &*l_whnf {
- EmptyListLit(t) => t.clone(),
- NEListLit(xs) => xs[0].get_type_not_sort(),
- _ => unreachable!(),
- };
-
// Construct the returned record type: { index: Natural, value: t }
let mut kts = HashMap::new();
kts.insert("index".into(), Value::from_builtin(Natural));
@@ -388,7 +380,7 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
let t = Value::from_kind(RecordType(kts));
// Construct the new list, with added indices
- let list = match &*l_whnf {
+ let list = match l.kind() {
EmptyListLit(_) => EmptyListLit(t),
NEListLit(xs) => NEListLit(
xs.iter()