diff options
author | Nadrieril | 2020-02-09 22:07:03 +0000 |
---|---|---|
committer | Nadrieril | 2020-02-09 22:07:03 +0000 |
commit | ad085a20bc257d03a52708d920cfc65f0e9051e6 (patch) | |
tree | fe5767a11a0a2001e115323c6e34fa1fd20ef8cd /dhall/src/semantics/builtins.rs | |
parent | 21db63d3e614554f258526182c7ed89a2c244b65 (diff) |
Remove all types from Value
Diffstat (limited to '')
-rw-r--r-- | dhall/src/semantics/builtins.rs | 14 |
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() |