Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Check correctness of type info in a few more places | Nadrieril | 2019-08-26 | 1 | -17/+43 |
| | |||||
* | Remove now unnecessary VoVF enum | Nadrieril | 2019-08-25 | 2 | -76/+29 |
| | |||||
* | Rework apply_builtin to enforce preservation of type information | Nadrieril | 2019-08-25 | 1 | -17/+15 |
| | |||||
* | Enforce type information almost everywhere | Nadrieril | 2019-08-25 | 2 | -33/+36 |
| | |||||
* | Check consistency of type information | Nadrieril | 2019-08-25 | 1 | -25/+28 |
| | |||||
* | Keep type information through normalization | Nadrieril | 2019-08-25 | 1 | -11/+28 |
| | |||||
* | Don't use take_mut::take lightly since normalize_whnf might panic | Nadrieril | 2019-08-21 | 1 | -9/+18 |
| | |||||
* | Reduce API surface of dhall crate | Nadrieril | 2019-08-20 | 2 | -21/+7 |
| | |||||
* | Use Ret in apply_builtin | Nadrieril | 2019-08-20 | 1 | -6/+0 |
| | |||||
* | Propagate type information in Value::app() | Nadrieril | 2019-08-20 | 1 | -8/+15 |
| | |||||
* | Track evaluation status alongside ValueF in VoVF | Nadrieril | 2019-08-20 | 2 | -36/+40 |
| | |||||
* | No need for Cow in return type of get_type | Nadrieril | 2019-08-20 | 1 | -3/+2 |
| | |||||
* | Introduce a new enum to store either a Value or a ValueF | Nadrieril | 2019-08-20 | 2 | -6/+57 |
| | |||||
* | Naming tweaks | Nadrieril | 2019-08-20 | 2 | -9/+8 |
| | |||||
* | Add Value::from_builtin | Nadrieril | 2019-08-20 | 2 | -12/+5 |
| | |||||
* | Clarify conversion of Const/Builtin to Value | Nadrieril | 2019-08-20 | 1 | -5/+2 |
| | |||||
* | Cleanup | Nadrieril | 2019-08-20 | 2 | -16/+6 |
| | |||||
* | Tweak Value API | Nadrieril | 2019-08-19 | 1 | -28/+19 |
| | |||||
* | Merge TypedValue and Value | Nadrieril | 2019-08-19 | 3 | -161/+88 |
| | |||||
* | Reduce untyped construction of Values | Nadrieril | 2019-08-19 | 3 | -65/+51 |
| | |||||
* | Use TypedValue instead of Typed in normalize and typecheck | Nadrieril | 2019-08-19 | 3 | -44/+39 |
| | | | | | Now Typed is only used in dhall::phase, similarly to Parsed/Resolved/Normalized | ||||
* | s/to_valuef/to_whnf/ and avoid cloning ValueFs when possible | Nadrieril | 2019-08-19 | 2 | -23/+22 |
| | |||||
* | Merge ValueInternal and TypedValueInternal | Nadrieril | 2019-08-18 | 1 | -111/+79 |
| | |||||
* | Rework ValueInternal and clarify invariants around ValueF | Nadrieril | 2019-08-18 | 2 | -70/+63 |
| | |||||
* | s/Thunk/Value/ | Nadrieril | 2019-08-17 | 5 | -775/+775 |
| | |||||
* | Share type alongside the value in a thunk | Nadrieril | 2019-08-16 | 2 | -40/+110 |
| | |||||
* | Use generic Shift/Subst impls | Nadrieril | 2019-08-16 | 3 | -192/+186 |
| | |||||
* | Store type in Thunk | Nadrieril | 2019-08-16 | 2 | -58/+71 |
| | |||||
* | Remove Const-optimization for now | Nadrieril | 2019-08-16 | 1 | -14/+5 |
| | |||||
* | s/Value/ValueF/ | Nadrieril | 2019-08-16 | 4 | -153/+155 |
| | |||||
* | Try to minimize untyped TypedThunks | Nadrieril | 2019-08-16 | 1 | -7/+6 |
| | |||||
* | fixup! No need for generic Context anymore | Nadrieril | 2019-08-16 | 1 | -1/+1 |
| | |||||
* | Free variables don't exist anymore | Nadrieril | 2019-08-16 | 1 | -21/+13 |
| | |||||
* | No need for generic Context anymore | Nadrieril | 2019-08-16 | 1 | -75/+38 |
| | |||||
* | Remove dead code | Nadrieril | 2019-08-16 | 4 | -80/+21 |
| | |||||
* | Reduce api surface of dhall crate | Nadrieril | 2019-08-16 | 4 | -52/+45 |
| | | | | Helps detect unused code | ||||
* | rustfmt | Nadrieril | 2019-08-15 | 1 | -2/+1 |
| | |||||
* | Fix variable substitution | Nadrieril | 2019-08-15 | 1 | -4/+2 |
| | | | | I have no idea how this didn't get caught before | ||||
* | Custom Debug impls to improve debug legibility | Nadrieril | 2019-08-15 | 2 | -3/+37 |
| | |||||
* | Remove special closures from Value | Nadrieril | 2019-08-15 | 2 | -94/+7 |
| | | | | Instead construct their values directly | ||||
* | Fix bug in shifting contexts | Nadrieril | 2019-08-15 | 1 | -1/+10 |
| | |||||
* | Fix typo in normalization | Nadrieril | 2019-08-14 | 1 | -1/+1 |
| | |||||
* | Considerably simplify Embed handling | Nadrieril | 2019-08-13 | 2 | -7/+3 |
| | |||||
* | Stop tracking the absence of Embed values at the type level | Nadrieril | 2019-08-13 | 2 | -11/+11 |
| | |||||
* | Typos | Nadrieril | 2019-08-13 | 1 | -2/+2 |
| | |||||
* | s/TypeThunk/TypedThunk/g | Nadrieril | 2019-08-13 | 2 | -45/+47 |
| | |||||
* | Swap Typed and TypeThunk | Nadrieril | 2019-08-13 | 1 | -21/+104 |
| | |||||
* | Move api into its own crate | Nadrieril | 2019-08-13 | 1 | -4/+4 |
| | |||||
* | Remove dhall::expr!() macro | Nadrieril | 2019-08-10 | 2 | -9/+45 |
| | | | | It's a lot of hassle for not a lot of benefit | ||||
* | Add support for dependent types | Nadrieril | 2019-08-08 | 2 | -1/+22 |
| |