summaryrefslogtreecommitdiff
path: root/dhall/src/phase/typecheck.rs (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Inline headersNadrieril2019-08-061-0/+1
|
* rustfmtNadrieril2019-08-031-25/+61
|
* Merge pull request #93 from Nadrieril/catchup-specNadrieril Feneanar2019-08-031-2/+2
|\ | | | | Do some catch up on the spec
| * Update dhall-lang submoduleNadrieril2019-08-031-2/+2
| |
* | Merge remote-tracking branch 'origin/master' into fintan/typecheck-combine-typesFintanH2019-08-031-8/+74
|\|
| * Merge remote-tracking branch 'origin/master' into fintan/typecheck-combineFintanH2019-08-031-5/+47
| |\
| * | Mark RecursiveRecordMerge as unreachableFintanH2019-08-011-0/+1
| | |
| * | Add the typechecking of RecursiveRecordMerge.FintanH2019-08-011-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.
* | | Simplify Const checking logicFintanH2019-08-031-11/+7
| | |
* | | Merge remote-tracking branch 'origin/master' into fintan/typecheck-combine-typesFintanH2019-08-031-5/+47
|\ \ \ | | |/ | |/|
| * | Add unreachable call for RightBasedRecordMerge caseFintanH2019-07-311-0/+1
| | |
| * | Reuse the merge_maps function to implement the right-biased unionFintanH2019-07-311-6/+6
| | |
| * | Add case for RightBasedRecordMerge in the typechecking phase.Fintan Halpenny2019-07-311-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.
* / Add typechecking for RecursiveRecordTypeMerge.FintanH2019-08-011-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.
* clippyNadrieril2019-05-121-23/+10
|
* Include success or failure prefix in test filteringNadrieril2019-05-121-4/+4
|
* Implement binary encodingNadrieril2019-05-121-1/+1
| | | | Closes #39
* Merge Type and TypedNadrieril2019-05-091-49/+40
|
* Make visibilities more consistentNadrieril2019-05-091-9/+6
|
* Rewrite the StaticType trait and everything around itNadrieril2019-05-091-1/+1
|
* Reduce the distance between Type and TypedNadrieril2019-05-091-87/+78
|
* Remove TypeIntermediate in favor of special-purpose functionsNadrieril2019-05-091-214/+183
|
* Small utility SubExpr::from_builtinNadrieril2019-05-091-9/+3
|
* ExprF need not be generic in LabelNadrieril2019-05-091-2/+1
|
* Make shift fallible and improve shift ergonomicsNadrieril2019-05-091-2/+11
|
* Detect duplicate record fields in typecheckNadrieril2019-05-091-30/+33
|
* Update dhall-lang submoduleNadrieril2019-05-091-2/+14
|
* Typecheck record projectionNadrieril2019-05-081-7/+30
|
* Typecheck mergeNadrieril2019-05-081-12/+87
|
* Don't discard normalization work done by typecheckingNadrieril2019-05-071-52/+93
|
* Slight improvement to typecheck ergonomicsNadrieril2019-05-071-59/+28
|
* Unify typecheck and normalization contextsNadrieril2019-05-071-2/+2
|
* Promote shift and subst_shift to traitsNadrieril2019-05-071-0/+1
|
* Clean up some of the SubExpr type-changing methodsNadrieril2019-05-071-3/+3
|
* Unify Type, TypeInternal and TypedNadrieril2019-05-071-21/+7
|
* Move main datatypes into their own modulesNadrieril2019-05-061-208/+137
|
* Consolidate errors in the error moduleNadrieril2019-05-061-103/+11
|
* Reorganize dhall into a phase structureNadrieril2019-05-061-0/+1276
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-09 09:11:56 +0000