# Change Log

# 0.2.6

+ Improve CLI implementation
+ Upgrade minitt-util
+ Add `Sub` impl for `DBI`-like types

# 0.2.5

+ Replace AppVeyor + CircleCI with GitHub Actions
+ Support saving & loading command line history

# 0.2.4

+ Add `fall` back
+ Fix the fix to expand-global on neutral terms and a typo

# 0.2.3

+ Inline metas more eagerly (#178)
+ Improve pest utility
+ Unification now unifies extension
+ Fix expand-global on neutral terms and a typo

# 0.2.2

+ Documentation fix
+ Add few more power to the util library

# 0.2.1

+ Mock terms in a smarter way (#174)
+ Make lift actually work (#175)
+ Expand global references in nested neutral terms (#176)

# 0.2.0

+ Update docs
+ Move `Axiom` to `voile-util`

# 0.1.8

+ Move `lisp`, `common.rs` to `voile-util`

# 0.1.7

+ Create a meta variable utility in `voile-util`

# 0.1.6

+ Integrate `minitt-util` for CLI
+ Fix type-checking bug
+ Fix reduction bug

# 0.1.5

+ Create another subcrate `voile-util`,
  move the pest helpers, `vec1`, `UID`-relevant utilities and
 `SyntaxInfo` into it
+ Rename `SyntaxInfo` to `Loc`, `ToSyntaxInfo` to `ToLoc`,
  `syntax_info` to `loc`, etc.

# 0.1.4

+ Implicit argument (#115)
  (https://github.com/owo-lang/voile-rs/compare/0.1.3...b592c09870bf27b8a89cc2b65c2578a231cd1ec4)
+ More unification rules

# 0.1.3

+ Case-split parser (#82), core language elements (#2)
+ Update structopt to 0.3

# 0.1.2

+ Implement record projection (#151, #152, #158)
+ Update `vec1` utility

# 0.1.1

+ Update typing rule for `cons`
+ Support record construction parsing, type-checking, conversion checking,
  reduction and inference (#146, #147)
+ Support empty record and variants (#154)
+ `Closure` is now a variant (#149)
+ More unification rules

# 0.1.0

+ Fix core language `is_type` judgement
+ Update mod rustdoc
+ Evaluation for `RowPoly`

# 0.0.15

+ Error message is now "change my mind" (#126)
+ Introduce `vec1` (#127)
+ New syntax for `Rec` and `Sum`
+ Remove `check_type(e)`, replace with `check(e, TypeOmega)` (#140)
+ Add subtyping back (#132)
+ Add row kinds according to the paper (#83)
+ Row-kinding type-checking (#137)
+ Update KaTeX and crate rustdoc

# 0.0.14

+ Documentation cleanup
+ Report error on redefinitions (#107)
+ Unification (#105, #110)
+ Meta variable solving (#104, #110, #119, #120)
+ Use Rust's newtype pattern to represent different indices (#111, #112)
+ Infer lambda types using metas (#117)
+ Memory optimizations
+ Update dependency versions

# 0.0.9

+ Remove `Bot` in core (#78)
+ Introduce standalone `Axiom` type (#91)
+ Code cleanup, remove `compile` and `Name` (#84)
+ Introduce level lifting operation and level checking (#77)
+ Remove lambda parameter (#89)
+ Rename `Abs::Var` and `Abs::Local` to `Abs::Ref` and `Abs::Var`
  respectively to fit `Val`'s naming convention
+ Redesigned global references (#96) to support mutual recursion
+ Introduce omega level (#99)
+ Support inferring omega level (#101). This does not look like
  something that will be used in the near future.
+ Add `-e` option for `voilec`,
  add `:infer`, `:eval`, and `:level` REPL commands (#90)
+ Use more TeX in `lib.rs` comments

# 0.0.8

+ Rename `ConsType` to `Variant`, `Term` to `Val`
+ Improve lambda compilation (#71, #73)
+ `Variant` related checking, introduce `Sum` in core (#11, #70)
+ Remove features of `clap` to avoid transitive winapi
  0.2.8 dependency
+ Now we're not compiling after tycking, but transform the
  tycked terms (#74, #75)
+ REPL (#56, #76)
+ The message "Type-Check successful." is changed to
  "Checkmate, dram!"
+ Fix wrong desugar of sum expression
+ Fix closure instantiation

# 0.0.7

+ Tuple desugar (#51)
+ Lambda desugar (#59, #62)
+ Upgrade KaTeX to 0.10.2
+ Largely refactor abstract syntax translation logic
+ Abstract/Core pretty-printer
+ Fix evaluator and parameter desugarer (#44, #67, #68)

# 0.0.6

+ Give up implicit parameters (#32)
+ Cleanup (#23, #39, #41)
+ Improve abstract syntax (#21, #24, #43)
+ Add documentation guidelines
+ Improve type-checking state (#15, #39, #40)
+ Fix DBI-based lambda instantiation for real (#47, #48)
+ Implement shadowing (#45)
+ Redesign lambda syntax (#46, #49)

# 0.0.5

+ Introduce core term tests (#17)
+ Fix DBI-based lambda instantiation (#16)
+ Remove captured env in closure (#19)
+ Introduce `RedEx`

# 0.0.4

+ Introduce Type-Checking Monad
+ Introduce the abstract syntax
+ Basic desugar: translate surface syntax to abstract syntax
+ Improve documentation, start writing the tutorial

# 0.0.3

+ Implemented the expression parser
+ Replace `Pi`, `Sigma` with `Dt`
+ Further improve the surface syntax tree for expressions

# 0.0.2

+ Implemented a STLC core language
+ Parser prototype
+ CLI prototype

# 0.0.1

+ Create package on crates.io