summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/phase/typecheck.rs (unfollow)
Commit message (Collapse)AuthorFilesLines
2019-08-13Considerably simplify Embed handlingNadrieril1-2/+1
2019-08-13Stop tracking the absence of Embed values at the type levelNadrieril1-7/+4
2019-08-13No need to track the absence of `Span`s at the type levelNadrieril1-8/+8
2019-08-13s/TypeThunk/TypedThunk/gNadrieril1-16/+24
2019-08-12Remove ensure_... macros in typecheckNadrieril1-115/+89
They weren't worth it
2019-08-10Remove dhall::expr!() macroNadrieril1-26/+81
It's a lot of hassle for not a lot of benefit
2019-08-08Add support for dependent typesNadrieril1-20/+40
2019-08-07Add truncated Natural subtractionNadrieril1-0/+1
2019-08-07Remove union literals from the languageNadrieril1-9/+0
2019-08-06Prepare for https://github.com/dhall-lang/dhall-lang/pull/630Nadrieril1-35/+40
2019-08-06Auto-generate typechecking tests listNadrieril1-395/+0
2019-08-06Change some testsNadrieril1-0/+5
2019-08-06Add some new tests and implement import alternativesNadrieril1-1/+1
2019-08-06Remove old-style optional literalsNadrieril1-23/+4
2019-08-06Inline headersNadrieril1-0/+1
2019-08-03rustfmtNadrieril1-25/+61
2019-08-03Update dhall-lang submoduleNadrieril1-2/+2
2019-08-03Simplify Const checking logicFintanH1-11/+7
2019-08-01Add typechecking for RecursiveRecordTypeMerge.FintanH1-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-01Mark RecursiveRecordMerge as unreachableFintanH1-0/+1
2019-08-01Add the typechecking of RecursiveRecordMerge.FintanH1-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-31Add unreachable call for RightBasedRecordMerge caseFintanH1-0/+1
2019-07-31Reuse the merge_maps function to implement the right-biased unionFintanH1-6/+6
2019-07-31Add case for RightBasedRecordMerge in the typechecking phase.Fintan Halpenny1-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.
2019-05-12clippyNadrieril1-23/+10
2019-05-12Include success or failure prefix in test filteringNadrieril1-4/+4
2019-05-12Implement binary encodingNadrieril1-1/+1
Closes #39
2019-05-09Merge Type and TypedNadrieril1-49/+40
2019-05-09Make visibilities more consistentNadrieril1-9/+6
2019-05-09Rewrite the StaticType trait and everything around itNadrieril1-1/+1
2019-05-09Reduce the distance between Type and TypedNadrieril1-87/+78
2019-05-09Remove TypeIntermediate in favor of special-purpose functionsNadrieril1-214/+183
2019-05-09Small utility SubExpr::from_builtinNadrieril1-9/+3
2019-05-09ExprF need not be generic in LabelNadrieril1-2/+1
2019-05-09Make shift fallible and improve shift ergonomicsNadrieril1-2/+11
2019-05-09Detect duplicate record fields in typecheckNadrieril1-30/+33
2019-05-09Update dhall-lang submoduleNadrieril1-2/+14
2019-05-08Typecheck record projectionNadrieril1-7/+30
2019-05-08Typecheck mergeNadrieril1-12/+87
2019-05-07Don't discard normalization work done by typecheckingNadrieril1-52/+93
2019-05-07Slight improvement to typecheck ergonomicsNadrieril1-59/+28
2019-05-07Unify typecheck and normalization contextsNadrieril1-2/+2
2019-05-07Promote shift and subst_shift to traitsNadrieril1-0/+1
2019-05-07Clean up some of the SubExpr type-changing methodsNadrieril1-3/+3
2019-05-07Unify Type, TypeInternal and TypedNadrieril1-21/+7
2019-05-06Move main datatypes into their own modulesNadrieril1-208/+137
2019-05-06Consolidate errors in the error moduleNadrieril1-103/+11
2019-05-06Reorganize dhall into a phase structureNadrieril1-137/+20
2019-05-06Merge TypedInternal and TypedNadrieril1-9/+0
2019-05-05s/DoubleVar/AlphaVar/Nadrieril1-8/+8
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 21:13:01 +0000