Commit message (Collapse) | Author | Files | Lines | ||
---|---|---|---|---|---|
2019-08-27 | clippy | Nadrieril | 1 | -1/+1 | |
2019-08-25 | Enforce type information almost everywhere | Nadrieril | 1 | -13/+8 | |
2019-08-25 | Keep type information through normalization | Nadrieril | 1 | -10/+11 | |
2019-08-23 | Clarify which syntax elements are completely handled in the tck phase | Nadrieril | 1 | -3/+6 | |
2019-08-23 | Keep type information after RecursiveRecordTypeMerge | Nadrieril | 1 | -27/+10 | |
2019-08-20 | Propagate type information in Value::app() | Nadrieril | 1 | -8/+2 | |
2019-08-20 | No need for Cow in return type of get_type | Nadrieril | 1 | -20/+19 | |
2019-08-20 | Introduce a new enum to store either a Value or a ValueF | Nadrieril | 1 | -8/+9 | |
2019-08-20 | Naming tweaks | Nadrieril | 1 | -3/+2 | |
2019-08-20 | Clarify conversion of Const/Builtin to Value | Nadrieril | 1 | -16/+27 | |
2019-08-20 | Cleanup | Nadrieril | 1 | -3/+3 | |
2019-08-20 | Standardize records of mixed kinds | Nadrieril | 1 | -51/+17 | |
2019-08-20 | Reuse work to avoid complicated recursion in record merging | Nadrieril | 1 | -96/+25 | |
2019-08-20 | Tweak Ok/Err handling in typecheck | Nadrieril | 1 | -157/+128 | |
2019-08-19 | Merge TypedValue and Value | Nadrieril | 1 | -96/+81 | |
2019-08-19 | Reduce untyped construction of Values | Nadrieril | 1 | -17/+16 | |
2019-08-19 | Use TypedValue instead of Typed in normalize and typecheck | Nadrieril | 1 | -218/+174 | |
Now Typed is only used in dhall::phase, similarly to Parsed/Resolved/Normalized | |||||
2019-08-19 | s/to_valuef/to_whnf/ and avoid cloning ValueFs when possible | Nadrieril | 1 | -104/+94 | |
2019-08-17 | s/Thunk/Value/ | Nadrieril | 1 | -34/+34 | |
2019-08-16 | s/Value/ValueF/ | Nadrieril | 1 | -54/+56 | |
2019-08-16 | Remove dead code | Nadrieril | 1 | -5/+5 | |
2019-08-16 | Typecheck before normalizing in tests | Nadrieril | 1 | -4/+1 | |
2019-08-16 | Avoid capture when typechecking union constructor | Nadrieril | 1 | -2/+1 | |
2019-08-16 | Reduce api surface of dhall crate | Nadrieril | 1 | -6/+6 | |
Helps detect unused code | |||||
2019-08-15 | Disable some unused unstable features | Nadrieril | 1 | -1/+1 | |
2019-08-13 | Store Imports in their own node instead of in Embed | Nadrieril | 1 | -0/+3 | |
2019-08-13 | Considerably simplify Embed handling | Nadrieril | 1 | -2/+1 | |
2019-08-13 | Stop tracking the absence of Embed values at the type level | Nadrieril | 1 | -7/+4 | |
2019-08-13 | No need to track the absence of `Span`s at the type level | Nadrieril | 1 | -8/+8 | |
2019-08-13 | s/TypeThunk/TypedThunk/g | Nadrieril | 1 | -16/+24 | |
2019-08-12 | Remove ensure_... macros in typecheck | Nadrieril | 1 | -115/+89 | |
They weren't worth it | |||||
2019-08-10 | Remove dhall::expr!() macro | Nadrieril | 1 | -26/+81 | |
It's a lot of hassle for not a lot of benefit | |||||
2019-08-08 | Add support for dependent types | Nadrieril | 1 | -20/+40 | |
2019-08-07 | Add truncated Natural subtraction | Nadrieril | 1 | -0/+1 | |
2019-08-07 | Remove union literals from the language | Nadrieril | 1 | -9/+0 | |
2019-08-06 | Prepare for https://github.com/dhall-lang/dhall-lang/pull/630 | Nadrieril | 1 | -35/+40 | |
2019-08-06 | Auto-generate typechecking tests list | Nadrieril | 1 | -395/+0 | |
2019-08-06 | Change some tests | Nadrieril | 1 | -0/+5 | |
2019-08-06 | Add some new tests and implement import alternatives | Nadrieril | 1 | -1/+1 | |
2019-08-06 | Remove old-style optional literals | Nadrieril | 1 | -23/+4 | |
2019-08-06 | Inline headers | Nadrieril | 1 | -0/+1 | |
2019-08-03 | rustfmt | Nadrieril | 1 | -25/+61 | |
2019-08-03 | Update dhall-lang submodule | Nadrieril | 1 | -2/+2 | |
2019-08-03 | Simplify Const checking logic | FintanH | 1 | -11/+7 | |
2019-08-01 | Add typechecking for RecursiveRecordTypeMerge. | FintanH | 1 | -7/+85 | |
The implementation brings with it intersection_with_key over HashMaps to help with the type checking of records of records. The implementation first checks that the Const values line up with the LHS and RHS. Then checks that combining the records does not result in a FieldCollision. It will finally return the shared Const type of the arguments. | |||||
2019-08-01 | Mark RecursiveRecordMerge as unreachable | FintanH | 1 | -0/+1 | |
2019-08-01 | Add the typechecking of RecursiveRecordMerge. | FintanH | 1 | -8/+73 | |
This introduces an external function for HashMaps to perform an outer join so that you can do a unionWith but with more power by having a new tagert type. Using outer_join and recursively looking through records of records we have an implementation for combining records. | |||||
2019-07-31 | Add unreachable call for RightBasedRecordMerge case | FintanH | 1 | -0/+1 | |
2019-07-31 | Reuse the merge_maps function to implement the right-biased union | FintanH | 1 | -6/+6 | |
2019-07-31 | Add case for RightBasedRecordMerge in the typechecking phase. | Fintan Halpenny | 1 | -5/+46 | |
The implementation checks the types and kinds of the LHS and RHS. In the happy path it unions the HashMap prefering keys on the RHS over the LHS, and the result is the type of the resulting HashMap. The error cases are: - If the kinds of the records differ it results in a RecordMismatch error. - If either the LHS or RHS are not records it results in a MustCombineRecord error. |