summaryrefslogtreecommitdiff
path: root/dhall/src/error (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Move error module to root of crateNadrieril2019-12-201-0/+178
|
* Move contents of dhall under a semantics submoduleNadrieril2019-12-151-179/+0
|
* Reexport dhall_syntax as a module in dhallNadrieril2019-12-151-1/+1
|
* Add more detail to TypeMismatch errorNadrieril2019-11-111-3/+14
|
* Remove unused error textsNadrieril2019-11-1134-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 errorsNadrieril2019-11-111-8/+8
|
* Move "Type error" error prefixNadrieril2019-11-111-7/+11
|
* Display first pretty type errorNadrieril2019-11-111-4/+4
|
* Implement basicest Display for TypeErrorNadrieril2019-11-111-43/+18
|
* Rename SubExpr to Expr, and Expr to RawExprNadrieril2019-08-281-4/+4
| | | | For clarity, and consistency with Value
* Enforce type information almost everywhereNadrieril2019-08-251-1/+0
|
* Standardize records of mixed kindsNadrieril2019-08-201-2/+0
|
* Reuse work to avoid complicated recursion in record mergingNadrieril2019-08-201-1/+0
|
* Merge TypedValue and ValueNadrieril2019-08-191-27/+27
|
* Use TypedValue instead of Typed in normalize and typecheckNadrieril2019-08-191-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 possibleNadrieril2019-08-191-10/+10
|
* Implement inline headers parsingNadrieril2019-08-131-4/+4
|
* Add new error type for serde_dhallNadrieril2019-08-131-12/+0
|
* Move api into its own crateNadrieril2019-08-131-0/+10
|
* Add support for dependent typesNadrieril2019-08-081-2/+4
|
* Add some new tests and implement import alternativesNadrieril2019-08-061-1/+1
|
* Merge remote-tracking branch 'origin/master' into fintan/typecheck-combine-typesFintanH2019-08-031-1/+1
|\
| * Merge remote-tracking branch 'origin/master' into fintan/typecheck-combineFintanH2019-08-031-1/+1
| |\
| * | Add the typechecking of RecursiveRecordMerge.FintanH2019-08-011-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-typesFintanH2019-08-031-0/+2
|\ \ \ | | |/ | |/|
| * | Add case for RightBasedRecordMerge in the typechecking phase.Fintan Halpenny2019-07-311-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.FintanH2019-08-011-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 encodingNadrieril2019-05-121-0/+12
| | | | Closes #39
* Make shift fallible and improve shift ergonomicsNadrieril2019-05-091-0/+1
|
* Detect duplicate record fields in typecheckNadrieril2019-05-091-0/+2
|
* Typecheck record projectionNadrieril2019-05-081-0/+2
|
* Typecheck mergeNadrieril2019-05-081-0/+7
|
* Unify typecheck and normalization contextsNadrieril2019-05-071-6/+0
|
* Move main datatypes into their own modulesNadrieril2019-05-061-1/+1
|
* Consolidate errors in the error moduleNadrieril2019-05-0635-0/+1934