summaryrefslogtreecommitdiff
path: root/dhall (unfollow)
Commit message (Expand)AuthorFilesLines
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
2019-04-23Avoid duplicating work when matching on Pi typesNadrieril5-40/+118
2019-04-23Pass TypedImproved directly to type_last_layerNadrieril1-40/+55
2019-04-22Temporarily simplify functions depending on TypeInternalNadrieril3-41/+35
2019-04-22Pass through new TypedImproved typeNadrieril1-25/+92
2019-04-22Store context in TypedNadrieril3-33/+39
2019-04-22Avoid shift_subst in typecheckNadrieril2-32/+40
2019-04-21Prepare for interop between two contextsNadrieril3-25/+91
2019-04-21Factor out context handlingNadrieril2-19/+34
2019-04-21Embrace TypeInternal as a semantic valueNadrieril4-9/+25
2019-04-20Move TypeInternal to typecheckNadrieril2-23/+31
2019-04-20CleanupNadrieril1-3/+0
2019-04-20Improve test failure ergonomicsNadrieril2-10/+6
2019-04-20An empty optional value is purely semanticNadrieril3-16/+7
2019-04-20Implement more normalization simplificationsNadrieril1-9/+16
2019-04-20shift by mutable ref to avoid reallocationsNadrieril1-80/+71
2019-04-20TweaksNadrieril1-5/+6
2019-04-20AppliedBuiltin does not need a contextNadrieril1-25/+23
2019-04-20Avoid a lot of unnecessary cloning in apply_builtinNadrieril2-126/+184
2019-04-20CleanupNadrieril1-166/+144
2019-04-20Swap importNadrieril1-62/+54
2019-04-20Remove last remnant of expr buildingNadrieril1-12/+29
2019-04-20Introduce special closures to avoid constructing exprsNadrieril1-34/+67
2019-04-20Avoid a lot of slow Expr costructionNadrieril1-73/+52
2019-04-20FormattingNadrieril1-153/+152
2019-04-20Remove WHNF/Closure distinctionNadrieril1-132/+113
2019-04-20Refcount contexts to avoid clonesNadrieril1-40/+40
2019-04-20Rewrite apply_builtin to work on WHNFsNadrieril1-152/+160
2019-04-20More cleanupNadrieril1-125/+51
2019-04-20Cleanup leftover normalization codeNadrieril1-58/+10