Commit message (Collapse) | Author | Files | Lines | ||
---|---|---|---|---|---|
2019-12-19 | Rename ValueF to ValueKind | Nadrieril | 1 | -108/+108 | |
2019-12-15 | Refer to semantics module properly | Nadrieril | 1 | -4/+4 | |
2019-12-15 | Avoid mention of `crate::` outside of top-level imports | Nadrieril | 1 | -9/+9 | |
2019-12-15 | Move contents of dhall under a semantics submodule | Nadrieril | 1 | -0/+0 | |
2019-12-15 | Reexport dhall_syntax as a module in dhall | Nadrieril | 1 | -5/+5 | |
2019-11-11 | rustfmt | Nadrieril | 1 | -1/+3 | |
2019-11-11 | Parse projection by expression | Nadrieril | 1 | -0/+1 | |
2019-09-03 | Upgrade rust toolchain | Nadrieril | 1 | -3/+4 | |
2019-08-31 | Implement parsing of `toMap` keyword | Nadrieril | 1 | -0/+1 | |
2019-08-25 | Remove now unnecessary VoVF enum | Nadrieril | 1 | -22/+24 | |
2019-08-25 | Rework apply_builtin to enforce preservation of type information | Nadrieril | 1 | -183/+156 | |
2019-08-25 | Enforce type information almost everywhere | Nadrieril | 1 | -16/+9 | |
2019-08-25 | Check consistency of type information | Nadrieril | 1 | -2/+2 | |
2019-08-25 | Keep type information through normalization | Nadrieril | 1 | -69/+131 | |
2019-08-23 | Clarify which syntax elements are completely handled in the tck phase | Nadrieril | 1 | -22/+18 | |
2019-08-23 | Keep type information after RecursiveRecordTypeMerge | Nadrieril | 1 | -62/+13 | |
2019-08-20 | Use Ret in apply_builtin | Nadrieril | 1 | -90/+101 | |
2019-08-20 | Propagate type information in Value::app() | Nadrieril | 1 | -19/+16 | |
2019-08-20 | Track evaluation status alongside ValueF in VoVF | Nadrieril | 1 | -32/+40 | |
2019-08-20 | Introduce a new enum to store either a Value or a ValueF | Nadrieril | 1 | -60/+81 | |
2019-08-20 | Naming tweaks | Nadrieril | 1 | -29/+23 | |
2019-08-20 | Add Value::from_builtin | Nadrieril | 1 | -25/+19 | |
2019-08-20 | Cleanup | Nadrieril | 1 | -32/+55 | |
2019-08-20 | Reuse work to avoid complicated recursion in record merging | Nadrieril | 1 | -54/+0 | |
2019-08-19 | Merge TypedValue and Value | Nadrieril | 1 | -62/+28 | |
2019-08-19 | Reduce untyped construction of Values | Nadrieril | 1 | -26/+46 | |
2019-08-19 | Use TypedValue instead of Typed in normalize and typecheck | Nadrieril | 1 | -3/+3 | |
Now Typed is only used in dhall::phase, similarly to Parsed/Resolved/Normalized | |||||
2019-08-19 | s/to_valuef/to_whnf/ and avoid cloning ValueFs when possible | Nadrieril | 1 | -48/+46 | |
2019-08-18 | Rework ValueInternal and clarify invariants around ValueF | Nadrieril | 1 | -8/+21 | |
2019-08-17 | s/Thunk/Value/ | Nadrieril | 1 | -103/+105 | |
2019-08-16 | s/Value/ValueF/ | Nadrieril | 1 | -124/+126 | |
2019-08-16 | Try to minimize untyped TypedThunks | Nadrieril | 1 | -23/+31 | |
2019-08-16 | Remove dead code | Nadrieril | 1 | -21/+1 | |
2019-08-16 | Reduce api surface of dhall crate | Nadrieril | 1 | -7/+7 | |
Helps detect unused code | |||||
2019-08-15 | Disable some unused unstable features | Nadrieril | 1 | -1/+1 | |
2019-08-15 | Remove special closures from Value | Nadrieril | 1 | -42/+55 | |
Instead construct their values directly | |||||
2019-08-13 | Store Imports in their own node instead of in Embed | Nadrieril | 1 | -0/+3 | |
2019-08-13 | Considerably simplify Embed handling | Nadrieril | 1 | -1/+0 | |
2019-08-13 | Stop tracking the absence of Embed values at the type level | Nadrieril | 1 | -10/+11 | |
2019-08-13 | s/TypeThunk/TypedThunk/g | Nadrieril | 1 | -17/+17 | |
2019-08-08 | Update dhall-lang submodule | Nadrieril | 1 | -0/+1 | |
2019-08-08 | Add support for dependent types | Nadrieril | 1 | -3/+9 | |
2019-08-07 | Add truncated Natural subtraction | Nadrieril | 1 | -0/+10 | |
2019-08-07 | Remove union literals from the language | Nadrieril | 1 | -7/+0 | |
2019-08-06 | Prepare for https://github.com/dhall-lang/dhall-lang/pull/630 | Nadrieril | 1 | -5/+17 | |
2019-08-06 | rustfmt | Nadrieril | 1 | -1/+2 | |
2019-08-06 | Add some tests | Nadrieril | 1 | -0/+10 | |
2019-08-06 | Remove old-style optional literals | Nadrieril | 1 | -7/+3 | |
2019-08-03 | rustfmt | Nadrieril | 1 | -1/+3 | |
2019-08-01 | Add typechecking for RecursiveRecordTypeMerge. | FintanH | 1 | -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. |