Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Simple refinement types #638

Merged
merged 83 commits into from
Oct 10, 2019
Merged

Simple refinement types #638

merged 83 commits into from
Oct 10, 2019

Commits on Sep 15, 2019

  1. Added simple refinement types

    For design, see PistonDevelopers#636
    
    - Added “typechk/refinement.dyon”
    - Added “typechk/refinement_2.dyon”
    bvssvni committed Sep 15, 2019
    Configuration menu
    Copy the full SHA
    1d1ab19 View commit details
    Browse the repository at this point in the history

Commits on Sep 16, 2019

  1. Configuration menu
    Copy the full SHA
    288f055 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    15eafdc View commit details
    Browse the repository at this point in the history
  3. Make refinement propagate across item declarations

    - Added “typechk/refinement_3.dyon”
    bvssvni committed Sep 16, 2019
    Configuration menu
    Copy the full SHA
    fa9ac22 View commit details
    Browse the repository at this point in the history
  4. Remove condition for refinement

    - Added “typechk/refinement_4.dyon”
    bvssvni committed Sep 16, 2019
    Configuration menu
    Copy the full SHA
    30c0eb1 View commit details
    Browse the repository at this point in the history
  5. Handle ambiguity

    - Removed `Type::is_concrete`
    - Added “typechk/refinement_5.dyon”
    bvssvni committed Sep 16, 2019
    Configuration menu
    Copy the full SHA
    fb282ed View commit details
    Browse the repository at this point in the history

Commits on Sep 17, 2019

  1. Delay premature error

    - Fixed bug `a.goes_with(b)` => `b.goes_with(a)`
    - Added “typechk/refinement_6.dyon”
    - Added “typechk/refinement_7.dyon”
    bvssvni committed Sep 17, 2019
    Configuration menu
    Copy the full SHA
    7470d32 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    17091b6 View commit details
    Browse the repository at this point in the history
  3. Make f64 ambiguous with any

    - Swap order of `Type::ambiguous`
    - Added “typechk/refinement_8.dyon”
    - Added “typechk/refinement_9.dyon”
    bvssvni committed Sep 17, 2019
    Configuration menu
    Copy the full SHA
    6019448 View commit details
    Browse the repository at this point in the history
  4. Make bool ambiguous with any

    - Added “typechk/refinement_10.dyon”
    - Added “typechk/refinement_11.dyon”
    bvssvni committed Sep 17, 2019
    Configuration menu
    Copy the full SHA
    10ac60e View commit details
    Browse the repository at this point in the history
  5. Make str ambiguous with any

    - Added “typechk/refinement_12.dyon”
    - Added “typechk/refinement_13.dyon”
    bvssvni committed Sep 17, 2019
    Configuration menu
    Copy the full SHA
    afac0dc View commit details
    Browse the repository at this point in the history
  6. Make mat4 ambiguous with any

    - Added “typechk/refinement_14.dyon”
    - Added “typechk/refinement_15.dyon”
    bvssvni committed Sep 17, 2019
    Configuration menu
    Copy the full SHA
    9647ecb View commit details
    Browse the repository at this point in the history
  7. Make vec4 ambiguous with any

    - Added “typechk/refinement_16.dyon”
    - Added “typechk/refinement_17.dyon”
    bvssvni committed Sep 17, 2019
    Configuration menu
    Copy the full SHA
    79de1d3 View commit details
    Browse the repository at this point in the history
  8. Make link ambiguous with any

    - Added “typechk/refinement_18.dyon”
    - Added “typechk/refinement_19.dyon”
    bvssvni committed Sep 17, 2019
    Configuration menu
    Copy the full SHA
    abb26ec View commit details
    Browse the repository at this point in the history
  9. Added ambiguity check for opt

    - Added “typechk/refinement_20.dyon”
    - Added “typechk/refinement_21.dyon”
    bvssvni committed Sep 17, 2019
    Configuration menu
    Copy the full SHA
    e7bcd06 View commit details
    Browse the repository at this point in the history
  10. Added ambiguity check for res

    - Added “typechk/refinement_22.dyon”
    - Added “typechk/refinement_23.dyon”
    bvssvni committed Sep 17, 2019
    Configuration menu
    Copy the full SHA
    ff0233d View commit details
    Browse the repository at this point in the history
  11. Do not allow "sec" as ad-hoc type

    - Added “syntax/secret_fail.dyon”
    bvssvni committed Sep 17, 2019
    Configuration menu
    Copy the full SHA
    91bc454 View commit details
    Browse the repository at this point in the history
  12. Report error if function has extra type information without returning…

    … something
    
    - Added “typechk/void_refinement.dyon”
    bvssvni committed Sep 17, 2019
    Configuration menu
    Copy the full SHA
    9b367e0 View commit details
    Browse the repository at this point in the history
  13. Report error on wrong number of arguments in extra type information

    - Added “typechk/args_refinement.dyon”
    bvssvni committed Sep 17, 2019
    Configuration menu
    Copy the full SHA
    f59e01e View commit details
    Browse the repository at this point in the history
  14. Check that extra type information arguments work with function arguments

    - Added “typechk/refine_type_fail.dyon”
    bvssvni committed Sep 17, 2019
    Configuration menu
    Copy the full SHA
    069874c View commit details
    Browse the repository at this point in the history
  15. Added "norm" to "lib.dyon"

    bvssvni committed Sep 17, 2019
    Configuration menu
    Copy the full SHA
    1688e3c View commit details
    Browse the repository at this point in the history
  16. Added ambiguity check for thr

    - Added “typechk/refinement_24.dyon”
    - Added “typechk/refinement_25.dyon”
    bvssvni committed Sep 17, 2019
    Configuration menu
    Copy the full SHA
    47953c4 View commit details
    Browse the repository at this point in the history
  17. Added ambiguity check for in

    - Added ambiguity check for wrapper types
    - Fixed doc comment on `Type::ambiguous`
    - Added “typechk/refinement_26.dyon”
    - Added “typechk/refinement_27.dyon”
    bvssvni committed Sep 17, 2019
    Configuration menu
    Copy the full SHA
    d981874 View commit details
    Browse the repository at this point in the history
  18. Check return type of extra type information

    - Added “typechk/refine_type_fail_2.dyon”
    bvssvni committed Sep 17, 2019
    Configuration menu
    Copy the full SHA
    f089477 View commit details
    Browse the repository at this point in the history
  19. Make closure calls work with ad-hoc types

    - Added “typechk/closure_ad_hoc.dyon”
    bvssvni committed Sep 17, 2019
    Configuration menu
    Copy the full SHA
    bebd9d1 View commit details
    Browse the repository at this point in the history

Commits on Sep 18, 2019

  1. Configuration menu
    Copy the full SHA
    566c842 View commit details
    Browse the repository at this point in the history
  2. Convert !a into not(a)

    - Added `UnOpEpression::into_expression`
    bvssvni committed Sep 18, 2019
    Configuration menu
    Copy the full SHA
    6a53ce2 View commit details
    Browse the repository at this point in the history
  3. Write not(a) as !a

    bvssvni committed Sep 18, 2019
    Configuration menu
    Copy the full SHA
    801ca83 View commit details
    Browse the repository at this point in the history
  4. Rewrite !a as not(a) in type checker

    - Added `Kind::Not`
    bvssvni committed Sep 18, 2019
    Configuration menu
    Copy the full SHA
    0610573 View commit details
    Browse the repository at this point in the history
  5. Added not to "lib.dyon"

    bvssvni committed Sep 18, 2019
    Configuration menu
    Copy the full SHA
    1021361 View commit details
    Browse the repository at this point in the history
  6. Configuration menu
    Copy the full SHA
    6911237 View commit details
    Browse the repository at this point in the history
  7. Added neg to "lib.dyon"

    bvssvni committed Sep 18, 2019
    Configuration menu
    Copy the full SHA
    3f36cdf View commit details
    Browse the repository at this point in the history
  8. Use -a as neg(a)

    - Removed `Expression::UnOp`
    - Added `Node::rewrite_unop`
    - Added `Kind::Neg`
    - Removed `Kind::UnOp`
    - Removed `Runtime::unop`
    bvssvni committed Sep 18, 2019
    Configuration menu
    Copy the full SHA
    4cdd6ab View commit details
    Browse the repository at this point in the history
  9. Report error if refinement failed without ambiguity

    Closes PistonDevelopers#644
    
    - Added “typechk/refine_closed_fail_1.dyon”
    - Added “typechk/refine_closed_fail_2.dyon”
    - Added “typechk/refine_closed_pass_1.dyon”
    bvssvni committed Sep 18, 2019
    Configuration menu
    Copy the full SHA
    0baf934 View commit details
    Browse the repository at this point in the history
  10. Added Dfn::ext

    bvssvni committed Sep 18, 2019
    Configuration menu
    Copy the full SHA
    0428c23 View commit details
    Browse the repository at this point in the history
  11. Configuration menu
    Copy the full SHA
    80e9cc0 View commit details
    Browse the repository at this point in the history
  12. Configuration menu
    Copy the full SHA
    de9ddc2 View commit details
    Browse the repository at this point in the history
  13. Configuration menu
    Copy the full SHA
    a869534 View commit details
    Browse the repository at this point in the history
  14. Configuration menu
    Copy the full SHA
    8abd609 View commit details
    Browse the repository at this point in the history
  15. Removed UnOp

    bvssvni committed Sep 18, 2019
    Configuration menu
    Copy the full SHA
    af99af9 View commit details
    Browse the repository at this point in the history
  16. Configuration menu
    Copy the full SHA
    498ad2a View commit details
    Browse the repository at this point in the history

Commits on Sep 19, 2019

  1. Rewrite multiple binary operators into nested ones

    - Added efficient normalizing algorithm based on Group Theory
    bvssvni committed Sep 19, 2019
    Configuration menu
    Copy the full SHA
    21c8f1c View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    ad82d86 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    8fd5242 View commit details
    Browse the repository at this point in the history

Commits on Sep 20, 2019

  1. Rewrite dot in type checker

    bvssvni committed Sep 20, 2019
    Configuration menu
    Copy the full SHA
    bd1ed87 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    ec96e00 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    1204046 View commit details
    Browse the repository at this point in the history

Commits on Sep 21, 2019

  1. Added support for ad-hoc variables in refinement types

    See PistonDevelopers#645
    
    Use the semantics that none ad-hoc type is quantified over by `all`.
    
    - Added `Type::all_ext`
    - Added `Type::bind_ty_vars`
    - Added `Type::insert_var`
    - Added `Type::insert_none_var`
    - Added `T` lazy static string
    - Added some refine quantifier tests
    - Updated `add` in “lib.dyon”
    - Updated `add` extra type information
    - Added support for type quantifier in syntax
    - Push type variable names to “ty” node
    bvssvni committed Sep 21, 2019
    Configuration menu
    Copy the full SHA
    54ab7db View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    eea3463 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    758bffd View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    abfee35 View commit details
    Browse the repository at this point in the history
  5. Configuration menu
    Copy the full SHA
    f2b5aea View commit details
    Browse the repository at this point in the history
  6. Configuration menu
    Copy the full SHA
    a46afd4 View commit details
    Browse the repository at this point in the history

Commits on Sep 22, 2019

  1. Added support for lazy invariants

    See PistonDevelopers#640
    
    - Use fake grab expressions to precompute lazy invariant values
    - Added lazy invariant fake grap expressions
    - Added lazy invariant `ok(_)` pattern
    - Added lazy invariant `err(_)` pattern
    - Added lazy invariant `some(_)` pattern
    - Added test for lazy invariant
    - Removed `Expression::BinOp`
    - Added `ast::Lazy`
    - Added `ast::Arg::lazy`
    - Added `FnIndex::ExternalLazy`
    - Removed `BinOpExpression::resolve_locals`
    - Made `and_also` standard external function
    - Made `or_else` standard external function
    - Changed external function signature to return
    `Result<Option<Variable>, String>`
    - Returns value directly from external functions whenever possible
    - Made `unwrap_or` lazy
    - Use static pointers for external lazy invariants
    - Added `LAZY_UNWRAP_OR`
    - Added `LAZY_AND`
    - Added `LAZY_OR`
    - Added `LAZY_NO`
    - Rewrite binary operators in type checker
    - Delay errors in type checker for external functions
    - Treat `Kind::Add`, `Kind::Mul`, `Kind::Pow` as expressions in type
    checker
    - Updated `dyon_fn!` macro to return value directly when possible
    - Removed `Runtime::binop`
    - Added ambiguity check for `sec[_] vs any`
    - Added `standard_binop` to “write.rs”
    bvssvni committed Sep 22, 2019
    Configuration menu
    Copy the full SHA
    704e879 View commit details
    Browse the repository at this point in the history
  2. Removed Type::add, Type::mul and Type::pow

    - Fixed two warnings
    bvssvni committed Sep 22, 2019
    Configuration menu
    Copy the full SHA
    a1d07de View commit details
    Browse the repository at this point in the history

Commits on Sep 23, 2019

  1. Configuration menu
    Copy the full SHA
    453eab9 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    4f073a6 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    63d4f76 View commit details
    Browse the repository at this point in the history
  4. Configuration menu
    Copy the full SHA
    05f9ba3 View commit details
    Browse the repository at this point in the history
  5. Configuration menu
    Copy the full SHA
    f69bccc View commit details
    Browse the repository at this point in the history
  6. Configuration menu
    Copy the full SHA
    332a0a0 View commit details
    Browse the repository at this point in the history
  7. Configuration menu
    Copy the full SHA
    cfa11bc View commit details
    Browse the repository at this point in the history
  8. Configuration menu
    Copy the full SHA
    7b42297 View commit details
    Browse the repository at this point in the history
  9. Configuration menu
    Copy the full SHA
    453aecd View commit details
    Browse the repository at this point in the history
  10. Configuration menu
    Copy the full SHA
    2aa0813 View commit details
    Browse the repository at this point in the history
  11. Use todo list for type check

    bvssvni committed Sep 23, 2019
    Configuration menu
    Copy the full SHA
    dbb0888 View commit details
    Browse the repository at this point in the history
  12. Reduce work in type checker

    bvssvni committed Sep 23, 2019
    Configuration menu
    Copy the full SHA
    ba19536 View commit details
    Browse the repository at this point in the history
  13. Check Kind::N

    - Added “typechk/arr_fail_2.dyon”
    bvssvni committed Sep 23, 2019
    Configuration menu
    Copy the full SHA
    da655f5 View commit details
    Browse the repository at this point in the history

Commits on Sep 24, 2019

  1. Removed unnecessary check of arguments

    This case is covered by the type checker.
    bvssvni committed Sep 24, 2019
    Configuration menu
    Copy the full SHA
    9886f89 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    aec0bac View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    8e8f962 View commit details
    Browse the repository at this point in the history

Commits on Sep 25, 2019

  1. Split calls

    bvssvni committed Sep 25, 2019
    Configuration menu
    Copy the full SHA
    4a8f706 View commit details
    Browse the repository at this point in the history

Commits on Sep 27, 2019

  1. Configuration menu
    Copy the full SHA
    61f7bd3 View commit details
    Browse the repository at this point in the history

Commits on Sep 28, 2019

  1. Added check__in_string_imports

    - Added `_` as printable character of objects
    bvssvni committed Sep 28, 2019
    Configuration menu
    Copy the full SHA
    b60b15c View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    c91e290 View commit details
    Browse the repository at this point in the history
  3. Move CompareOp into BinOp

    bvssvni committed Sep 28, 2019
    Configuration menu
    Copy the full SHA
    c272930 View commit details
    Browse the repository at this point in the history
  4. Removed ast::Add

    bvssvni committed Sep 28, 2019
    Configuration menu
    Copy the full SHA
    d9edb8e View commit details
    Browse the repository at this point in the history
  5. Removed ast::Pow

    bvssvni committed Sep 28, 2019
    Configuration menu
    Copy the full SHA
    90a7a46 View commit details
    Browse the repository at this point in the history
  6. Configuration menu
    Copy the full SHA
    6517726 View commit details
    Browse the repository at this point in the history
  7. Removed unneeded Send impl

    bvssvni committed Sep 28, 2019
    Configuration menu
    Copy the full SHA
    fe7f6e4 View commit details
    Browse the repository at this point in the history

Commits on Oct 2, 2019

  1. Use Ok(...) directly

    bvssvni committed Oct 2, 2019
    Configuration menu
    Copy the full SHA
    1094d73 View commit details
    Browse the repository at this point in the history
  2. Fixed bug in div

    bvssvni committed Oct 2, 2019
    Configuration menu
    Copy the full SHA
    39868f7 View commit details
    Browse the repository at this point in the history

Commits on Oct 3, 2019

  1. Cleaned up import code

    bvssvni committed Oct 3, 2019
    Configuration menu
    Copy the full SHA
    cc88f06 View commit details
    Browse the repository at this point in the history