Skip to content

Latest commit

 

History

History
197 lines (143 loc) · 4.65 KB

CHANGELOG.md

File metadata and controls

197 lines (143 loc) · 4.65 KB

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

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