Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Update dhall-lang submodule | Nadrieril | 2019-08-03 | 1 | -2/+2 |
| | |||||
* | Merge remote-tracking branch 'origin/master' into fintan/typecheck-combine | FintanH | 2019-08-03 | 2 | -14/+57 |
|\ | |||||
| * | Add unreachable call for RightBasedRecordMerge case | FintanH | 2019-07-31 | 1 | -0/+1 |
| | | |||||
| * | Reuse the merge_maps function to implement the right-biased union | FintanH | 2019-07-31 | 2 | -7/+7 |
| | | |||||
| * | Add case for RightBasedRecordMerge in the typechecking phase. | Fintan Halpenny | 2019-07-31 | 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. | ||||
* | | Mark RecursiveRecordMerge as unreachable | FintanH | 2019-08-01 | 1 | -0/+1 |
| | | |||||
* | | Add the typechecking of RecursiveRecordMerge. | FintanH | 2019-08-01 | 2 | -8/+126 |
|/ | | | | | | | | | 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. | ||||
* | Finish implementing binary encoding | Nadrieril | 2019-05-12 | 1 | -6/+8 |
| | |||||
* | clippy | Nadrieril | 2019-05-12 | 2 | -120/+112 |
| | |||||
* | Include success or failure prefix in test filtering | Nadrieril | 2019-05-12 | 2 | -6/+6 |
| | |||||
* | Implement binary encoding | Nadrieril | 2019-05-12 | 5 | -25/+310 |
| | | | | Closes #39 | ||||
* | Write a custom map type that allows duplicates | Nadrieril | 2019-05-10 | 1 | -29/+38 |
| | |||||
* | Merge Type and Typed | Nadrieril | 2019-05-09 | 2 | -104/+54 |
| | |||||
* | Fix missing methods for tests | Nadrieril | 2019-05-09 | 1 | -0/+8 |
| | |||||
* | Make visibilities more consistent | Nadrieril | 2019-05-09 | 5 | -57/+51 |
| | |||||
* | Rewrite Deserialize trait around new Value and Type | Nadrieril | 2019-05-09 | 1 | -7/+1 |
| | |||||
* | Rewrite the StaticType trait and everything around it | Nadrieril | 2019-05-09 | 2 | -47/+12 |
| | |||||
* | Tweak Typed | Nadrieril | 2019-05-09 | 1 | -15/+16 |
| | |||||
* | Reduce the distance between Type and Typed | Nadrieril | 2019-05-09 | 2 | -109/+97 |
| | |||||
* | Remove TypeIntermediate in favor of special-purpose functions | Nadrieril | 2019-05-09 | 1 | -214/+183 |
| | |||||
* | Small utility SubExpr::from_builtin | Nadrieril | 2019-05-09 | 1 | -9/+3 |
| | |||||
* | ExprF need not be generic in Label | Nadrieril | 2019-05-09 | 2 | -7/+5 |
| | |||||
* | Make shift fallible and improve shift ergonomics | Nadrieril | 2019-05-09 | 2 | -11/+20 |
| | |||||
* | Detect duplicate record fields in typecheck | Nadrieril | 2019-05-09 | 3 | -71/+71 |
| | |||||
* | Generate normalization tests automatically | Nadrieril | 2019-05-09 | 2 | -368/+0 |
| | |||||
* | Correctly shift free variables in normalization | Nadrieril | 2019-05-09 | 1 | -1/+1 |
| | |||||
* | Update dhall-lang submodule | Nadrieril | 2019-05-09 | 2 | -15/+37 |
| | |||||
* | Typecheck record projection | Nadrieril | 2019-05-08 | 1 | -7/+30 |
| | |||||
* | Typecheck merge | Nadrieril | 2019-05-08 | 2 | -12/+90 |
| | |||||
* | Move binop normalization into a separate function | Nadrieril | 2019-05-08 | 1 | -165/+153 |
| | |||||
* | Implement normalization for record merging operators | Nadrieril | 2019-05-08 | 2 | -21/+113 |
| | |||||
* | Rename the record combining operators internally | Nadrieril | 2019-05-08 | 1 | -3/+3 |
| | |||||
* | Implement normalization of missing builtins | Nadrieril | 2019-05-08 | 1 | -21/+68 |
| | |||||
* | Don't discard normalization work done by typechecking | Nadrieril | 2019-05-07 | 1 | -52/+93 |
| | |||||
* | Slight improvement to typecheck ergonomics | Nadrieril | 2019-05-07 | 1 | -59/+28 |
| | |||||
* | Unify typecheck and normalization contexts | Nadrieril | 2019-05-07 | 2 | -5/+2 |
| | |||||
* | Promote shift and subst_shift to traits | Nadrieril | 2019-05-07 | 3 | -29/+42 |
| | |||||
* | Move AlphaVar and AlphaLabel into a new module | Nadrieril | 2019-05-07 | 1 | -1/+2 |
| | |||||
* | Small mistake | Nadrieril | 2019-05-07 | 1 | -1/+3 |
| | |||||
* | Clean up some of the SubExpr type-changing methods | Nadrieril | 2019-05-07 | 2 | -4/+4 |
| | |||||
* | Unify Type, TypeInternal and Typed | Nadrieril | 2019-05-07 | 2 | -116/+43 |
| | |||||
* | Move main datatypes into their own modules | Nadrieril | 2019-05-06 | 3 | -1194/+160 |
| | |||||
* | Consolidate errors in the error module | Nadrieril | 2019-05-06 | 4 | -125/+25 |
| | |||||
* | Reorganize dhall into a phase structure | Nadrieril | 2019-05-06 | 6 | -0/+4093 |