| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | Simplify type error type | Nadrieril | 2020-01-21 | 1 | -9/+4 |
| | | |||||
| * | Reimplement basic tck/nze with proper environments | Nadrieril | 2020-01-20 | 1 | -0/+5 |
| | | | | | Inspired from dhall_haskell | ||||
| * | s/TypecheckContext/TyCtx/ | Nadrieril | 2020-01-17 | 1 | -6/+3 |
| | | |||||
| * | Extend merge to work on Optionals | Nadrieril | 2019-12-24 | 1 | -1/+1 |
| | | |||||
| * | Add debug output to unhandled type error message | Nadrieril | 2019-12-24 | 1 | -1/+1 |
| | | |||||
| * | Update dhall-lang submodule | Nadrieril | 2019-12-22 | 1 | -0/+1 |
| | | |||||
| * | Move error module to root of crate | Nadrieril | 2019-12-20 | 1 | -0/+178 |
| | | |||||
| * | Move contents of dhall under a semantics submodule | Nadrieril | 2019-12-15 | 1 | -179/+0 |
| | | |||||
| * | Reexport dhall_syntax as a module in dhall | Nadrieril | 2019-12-15 | 1 | -1/+1 |
| | | |||||
| * | Add more detail to TypeMismatch error | Nadrieril | 2019-11-11 | 1 | -3/+14 |
| | | |||||
| * | Remove unused error texts | Nadrieril | 2019-11-11 | 34 | -1765/+0 |
| | | | | | | Those were copied from dhall-haskell back before I (Nadrieril) forked dhall-rust from Nanotech. They have never been used. | ||||
| * | Add a few more pretty errors | Nadrieril | 2019-11-11 | 1 | -8/+8 |
| | | |||||
| * | Move "Type error" error prefix | Nadrieril | 2019-11-11 | 1 | -7/+11 |
| | | |||||
| * | Display first pretty type error | Nadrieril | 2019-11-11 | 1 | -4/+4 |
| | | |||||
| * | Implement basicest Display for TypeError | Nadrieril | 2019-11-11 | 1 | -43/+18 |
| | | |||||
| * | Rename SubExpr to Expr, and Expr to RawExpr | Nadrieril | 2019-08-28 | 1 | -4/+4 |
| | | | | | For clarity, and consistency with Value | ||||
| * | Enforce type information almost everywhere | Nadrieril | 2019-08-25 | 1 | -1/+0 |
| | | |||||
| * | Standardize records of mixed kinds | Nadrieril | 2019-08-20 | 1 | -2/+0 |
| | | |||||
| * | Reuse work to avoid complicated recursion in record merging | Nadrieril | 2019-08-20 | 1 | -1/+0 |
| | | |||||
| * | Merge TypedValue and Value | Nadrieril | 2019-08-19 | 1 | -27/+27 |
| | | |||||
| * | Use TypedValue instead of Typed in normalize and typecheck | Nadrieril | 2019-08-19 | 1 | -27/+28 |
| | | | | | | 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 | 1 | -10/+10 |
| | | |||||
| * | Implement inline headers parsing | Nadrieril | 2019-08-13 | 1 | -4/+4 |
| | | |||||
| * | Add new error type for serde_dhall | Nadrieril | 2019-08-13 | 1 | -12/+0 |
| | | |||||
| * | Move api into its own crate | Nadrieril | 2019-08-13 | 1 | -0/+10 |
| | | |||||
| * | Add support for dependent types | Nadrieril | 2019-08-08 | 1 | -2/+4 |
| | | |||||
| * | Add some new tests and implement import alternatives | Nadrieril | 2019-08-06 | 1 | -1/+1 |
| | | |||||
| * | Merge remote-tracking branch 'origin/master' into fintan/typecheck-combine-types | FintanH | 2019-08-03 | 1 | -1/+1 |
| |\ | |||||
| | * | Merge remote-tracking branch 'origin/master' into fintan/typecheck-combine | FintanH | 2019-08-03 | 1 | -1/+1 |
| | |\ | |||||
| | * | | Add the typechecking of RecursiveRecordMerge. | FintanH | 2019-08-01 | 1 | -0/+3 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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. | ||||
| * | | | Merge remote-tracking branch 'origin/master' into fintan/typecheck-combine-types | FintanH | 2019-08-03 | 1 | -0/+2 |
| |\ \ \ | | |/ | |/| | |||||
| | * | | Add case for RightBasedRecordMerge in the typechecking phase. | Fintan Halpenny | 2019-07-31 | 1 | -0/+2 |
| | |/ | | | | | | | | | | | | | | | | | | | | | | | 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. | ||||
| * / | Add typechecking for RecursiveRecordTypeMerge. | FintanH | 2019-08-01 | 1 | -0/+3 |
| |/ | | | | | | | | | | 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. | ||||
| * | Implement binary encoding | Nadrieril | 2019-05-12 | 1 | -0/+12 |
| | | | | | Closes #39 | ||||
| * | Make shift fallible and improve shift ergonomics | Nadrieril | 2019-05-09 | 1 | -0/+1 |
| | | |||||
| * | Detect duplicate record fields in typecheck | Nadrieril | 2019-05-09 | 1 | -0/+2 |
| | | |||||
| * | Typecheck record projection | Nadrieril | 2019-05-08 | 1 | -0/+2 |
| | | |||||
| * | Typecheck merge | Nadrieril | 2019-05-08 | 1 | -0/+7 |
| | | |||||
| * | Unify typecheck and normalization contexts | Nadrieril | 2019-05-07 | 1 | -6/+0 |
| | | |||||
| * | Move main datatypes into their own modules | Nadrieril | 2019-05-06 | 1 | -1/+1 |
| | | |||||
| * | Consolidate errors in the error module | Nadrieril | 2019-05-06 | 35 | -0/+1934 |
 |
index : dhall_rust | |
| working copy forked from https://github.com/Nadrieril/dhall-rust |
| summaryrefslogtreecommitdiff |