summaryrefslogtreecommitdiff
path: root/dhall (unfollow)
Commit message (Expand)AuthorFilesLines
2019-05-02Remove shift0Nadrieril2-32/+26
2019-05-02Instead of possibly nonexistent Type, treat Sort speciallyNadrieril7-242/+282
2019-05-02Store Thunk in NormalizedNadrieril5-41/+44
2019-05-02TweaksNadrieril3-76/+78
2019-04-30Remove now useless TypedOrType typeNadrieril1-86/+34
2019-04-30Fix NF tracking errorNadrieril1-2/+3
2019-04-30Fix shifting. This completely destroys sharing so performance is dead.Nadrieril1-3/+7
2019-04-30Lazily process unnormalizable expressionNadrieril1-9/+36
2019-04-30Avoid some rewrapping of thunksNadrieril2-36/+51
2019-04-30Mutate thunk contents directly if sole ownerNadrieril1-2/+8
2019-04-30Normalize mutablyNadrieril1-30/+120
2019-04-30Don't borrow from thunk more than necessaryNadrieril2-37/+62
2019-04-30Pass references when possibleNadrieril3-90/+121
2019-04-30Merge Typed and PartiallyNormalizedNadrieril3-124/+94
2019-04-30Store a Thunk in TypedNadrieril4-40/+22
2019-04-30Store thunks in the normalization contextNadrieril1-12/+13
2019-04-30Store thunks behind Rc<RefCell<_>> to ensure minimal computationNadrieril2-81/+160
2019-04-29Remove NF/WHNF distinction at runtimeNadrieril3-100/+79
2019-04-29Make NF and WHNF custom types instead of aliasesNadrieril1-3/+5
2019-04-29Don't shift by mutable refNadrieril1-93/+106
2019-04-29Store thunk in Value::LambdaNadrieril1-19/+17
2019-04-29Allow representing normal form as a semantic valueNadrieril3-249/+368
2019-04-29Don't need to store original expression in TypeErrorNadrieril2-59/+14
2019-04-29Properly substitute when typing AppNadrieril2-57/+218
2019-04-28Use PartiallyNormalized throughout typecheckingNadrieril3-93/+95
2019-04-27Move Pi to WHNFNadrieril2-36/+51
2019-04-27BuiltinsNadrieril2-30/+11
2019-04-27Replace TypeInternal::UnionType with WHNF::UnionTypeNadrieril1-23/+23
2019-04-27Replace TypeInternal::RecordType with WHNF::RecordTypeNadrieril2-32/+68
2019-04-27Rework TypeInternalNadrieril1-83/+72
2019-04-27Store thunks uniformly in WHNFNadrieril1-59/+42
2019-04-27Abstract out thunks in type positionNadrieril1-22/+64
2019-04-27Rename Now to ThunkNadrieril1-45/+44
2019-04-27Define new intermediate expression typeNadrieril2-19/+43
2019-04-27Using only shift0 was not such a great ideaNadrieril1-23/+19
2019-04-26Lists and OptionalsNadrieril1-42/+94
2019-04-26ensure_is_const is not that helpfulNadrieril1-59/+35
2019-04-26Union typesNadrieril1-66/+117
2019-04-25Respect import boundary in normalizationNadrieril1-1/+3
2019-04-25Fix shifting againNadrieril1-13/+9
2019-04-25Now I can use TypeInternal::RecordType fullyNadrieril1-11/+10
2019-04-25Revert "Try property testing against reference implementation"Nadrieril2-134/+0
2019-04-25Try property testing against reference implementationNadrieril2-0/+134
2019-04-25Correctly shift values before inserting into contextNadrieril1-4/+7
2019-04-25normalize_to_type can use the captured contextNadrieril1-14/+14
2019-04-23RecordTypesNadrieril1-62/+108
2019-04-23Fix shifting under PiNadrieril1-13/+29
2019-04-23Silence warningsNadrieril2-0/+5
2019-04-23Avoid duplicating TypeInternal in TypedImprovedNadrieril1-44/+40
2019-04-23Avoid constructing ExprF::Pi while typecheckingNadrieril1-57/+93