summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/core/var.rs (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Move Value-related stuff under semantics::nzeNadrieril2020-01-301-36/+0
|
* Cleanup variable handlingNadrieril2020-01-291-31/+1
|
* Finally get rid of all of the shift/subst_shift !Nadrieril2020-01-291-10/+0
|
* Fix a bunch of bugs and more tckNadrieril2020-01-271-1/+7
|
* Reimplement basic tck/nze with proper environmentsNadrieril2020-01-201-0/+3
| | | | Inspired from dhall_haskell
* Introduce intermediate representation that stores typed exprNadrieril2020-01-181-17/+1
|
* SimplifyNadrieril2020-01-171-19/+2
|
* Replace all bulk shifting by a single shiftNadrieril2020-01-171-16/+4
|
* Use alpha variables everywhereNadrieril2020-01-171-21/+9
| | | | Don't bother keeping name around, it complicates matters
* Implement bulk shiftingNadrieril2020-01-171-9/+7
|
* Simplify a bitNadrieril2020-01-171-0/+16
|
* Remove Shift/Subst traitsNadrieril2020-01-171-49/+14
|
* Simplify Shift and Subst instancesNadrieril2020-01-171-143/+1
|
* Remove binder idsNadrieril2020-01-171-23/+9
| | | | The underlying purpose of them turned out to be unsound
* Use binder ids to reconstruct variables in expr outputNadrieril2020-01-171-7/+3
|
* Use binder ids for Value equalityNadrieril2020-01-171-0/+6
|
* Store corresponding binder id in AlphaVarNadrieril2020-01-171-10/+14
|
* Assign a unique id to each binderNadrieril2020-01-171-2/+8
|
* Introduce a notion of binderNadrieril2020-01-171-17/+17
|
* Construct T/Build closures in Expr spaceNadrieril2020-01-171-6/+0
|
* s/ExprF/ExprKind/Nadrieril2019-12-201-3/+3
|
* Rename ValueF to ValueKindNadrieril2019-12-191-1/+1
|
* Avoid mention of `crate::` outside of top-level importsNadrieril2019-12-151-5/+5
|
* Move contents of dhall under a semantics submoduleNadrieril2019-12-151-0/+295