summaryrefslogtreecommitdiff
path: root/dhall/src/phase/normalize.rs (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Upgrade rust toolchainNadrieril2019-09-031-3/+4
|
* Implement parsing of `toMap` keywordNadrieril2019-08-311-0/+1
|
* Remove now unnecessary VoVF enumNadrieril2019-08-251-22/+24
|
* Rework apply_builtin to enforce preservation of type informationNadrieril2019-08-251-183/+156
|
* Enforce type information almost everywhereNadrieril2019-08-251-16/+9
|
* Check consistency of type informationNadrieril2019-08-251-2/+2
|
* Keep type information through normalizationNadrieril2019-08-251-69/+131
|
* Clarify which syntax elements are completely handled in the tck phaseNadrieril2019-08-231-22/+18
|
* Keep type information after RecursiveRecordTypeMergeNadrieril2019-08-231-62/+13
|
* Use Ret in apply_builtinNadrieril2019-08-201-90/+101
|
* Propagate type information in Value::app()Nadrieril2019-08-201-19/+16
|
* Track evaluation status alongside ValueF in VoVFNadrieril2019-08-201-32/+40
|
* Introduce a new enum to store either a Value or a ValueFNadrieril2019-08-201-60/+81
|
* Naming tweaksNadrieril2019-08-201-29/+23
|
* Add Value::from_builtinNadrieril2019-08-201-25/+19
|
* CleanupNadrieril2019-08-201-32/+55
|
* Reuse work to avoid complicated recursion in record mergingNadrieril2019-08-201-54/+0
|
* Merge TypedValue and ValueNadrieril2019-08-191-62/+28
|
* Reduce untyped construction of ValuesNadrieril2019-08-191-26/+46
|
* Use TypedValue instead of Typed in normalize and typecheckNadrieril2019-08-191-3/+3
| | | | | 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-48/+46
|
* Rework ValueInternal and clarify invariants around ValueFNadrieril2019-08-181-8/+21
|
* s/Thunk/Value/Nadrieril2019-08-171-103/+105
|
* s/Value/ValueF/Nadrieril2019-08-161-124/+126
|
* Try to minimize untyped TypedThunksNadrieril2019-08-161-23/+31
|
* Remove dead codeNadrieril2019-08-161-21/+1
|
* Reduce api surface of dhall crateNadrieril2019-08-161-7/+7
| | | | Helps detect unused code
* Disable some unused unstable featuresNadrieril2019-08-151-1/+1
|
* Remove special closures from ValueNadrieril2019-08-151-42/+55
| | | | Instead construct their values directly
* Store Imports in their own node instead of in EmbedNadrieril2019-08-131-0/+3
|
* Considerably simplify Embed handlingNadrieril2019-08-131-1/+0
|
* Stop tracking the absence of Embed values at the type levelNadrieril2019-08-131-10/+11
|
* s/TypeThunk/TypedThunk/gNadrieril2019-08-131-17/+17
|
* Update dhall-lang submoduleNadrieril2019-08-081-0/+1
|
* Add support for dependent typesNadrieril2019-08-081-3/+9
|
* Add truncated Natural subtractionNadrieril2019-08-071-0/+10
|
* Remove union literals from the languageNadrieril2019-08-071-7/+0
|
* Prepare for https://github.com/dhall-lang/dhall-lang/pull/630Nadrieril2019-08-061-5/+17
|
* rustfmtNadrieril2019-08-061-1/+2
|
* Add some testsNadrieril2019-08-061-0/+10
|
* Remove old-style optional literalsNadrieril2019-08-061-7/+3
|
* rustfmtNadrieril2019-08-031-1/+3
|
* Merge remote-tracking branch 'origin/master' into fintan/typecheck-combine-typesFintanH2019-08-031-0/+54
|\
| * Merge remote-tracking branch 'origin/master' into fintan/typecheck-combineFintanH2019-08-031-9/+10
| |\
| * | Add the typechecking of RecursiveRecordMerge.FintanH2019-08-011-0/+53
| | | | | | | | | | | | | | | | | | | | | | | | | | | 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-1/+1
|\ \ \ | | |/ | |/|
| * | Reuse the merge_maps function to implement the right-biased unionFintanH2019-07-311-1/+1
| |/
* / Add typechecking for RecursiveRecordTypeMerge.FintanH2019-08-011-0/+32
|/ | | | | | | | | | 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-97/+102
|
* Make visibilities more consistentNadrieril2019-05-091-10/+7
|