summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/phase/typecheck.rs (unfollow)
Commit message (Collapse)AuthorFilesLines
2019-08-23Keep type information after RecursiveRecordTypeMergeNadrieril1-27/+10
2019-08-20Propagate type information in Value::app()Nadrieril1-8/+2
2019-08-20No need for Cow in return type of get_typeNadrieril1-20/+19
2019-08-20Introduce a new enum to store either a Value or a ValueFNadrieril1-8/+9
2019-08-20Naming tweaksNadrieril1-3/+2
2019-08-20Clarify conversion of Const/Builtin to ValueNadrieril1-16/+27
2019-08-20CleanupNadrieril1-3/+3
2019-08-20Standardize records of mixed kindsNadrieril1-51/+17
2019-08-20Reuse work to avoid complicated recursion in record mergingNadrieril1-96/+25
2019-08-20Tweak Ok/Err handling in typecheckNadrieril1-157/+128
2019-08-19Merge TypedValue and ValueNadrieril1-96/+81
2019-08-19Reduce untyped construction of ValuesNadrieril1-17/+16
2019-08-19Use TypedValue instead of Typed in normalize and typecheckNadrieril1-218/+174
Now Typed is only used in dhall::phase, similarly to Parsed/Resolved/Normalized
2019-08-19s/to_valuef/to_whnf/ and avoid cloning ValueFs when possibleNadrieril1-104/+94
2019-08-17s/Thunk/Value/Nadrieril1-34/+34
2019-08-16s/Value/ValueF/Nadrieril1-54/+56
2019-08-16Remove dead codeNadrieril1-5/+5
2019-08-16Typecheck before normalizing in testsNadrieril1-4/+1
2019-08-16Avoid capture when typechecking union constructorNadrieril1-2/+1
2019-08-16Reduce api surface of dhall crateNadrieril1-6/+6
Helps detect unused code
2019-08-15Disable some unused unstable featuresNadrieril1-1/+1
2019-08-13Store Imports in their own node instead of in EmbedNadrieril1-0/+3
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