Prop and Erased #584

mio-19 · 2022-10-16T03:53:25Z

This pr

Added ErasedTerm
generate ErasedTerm on inherit/synthesize whenever sort is Prop
implement illegal erased term check.
add a reduction rule: elim(erased) become erased
corrected prop-related tyck rules for sigma types and struct
updated LittleTyper to support new universe system for type.computeType() use cases

base/src/main/java/org/aya/core/term/ElimTerm.java

base/src/main/java/org/aya/tyck/ExprTycker.java

codecov · 2022-10-17T03:04:47Z

Codecov Report

Merging #584 (4bd6a26) into main (9d88ea7) will increase coverage by 0.05%.
The diff coverage is 68.90%.

@@             Coverage Diff              @@
##               main     #584      +/-   ##
============================================
+ Coverage     80.40%   80.45%   +0.05%     
- Complexity     2759     2791      +32     
============================================
  Files           224      226       +2     
  Lines          8731     8810      +79     
  Branches       1070     1093      +23     
============================================
+ Hits           7020     7088      +68     
- Misses         1125     1131       +6     
- Partials        586      591       +5

Impacted Files	Coverage Δ
base/src/main/java/org/aya/core/term/FormTerm.java	`81.53% <ø> (+5.41%)`	⬆️
...e/src/main/java/org/aya/distill/CoreDistiller.java	`78.74% <0.00%> (-0.39%)`	⬇️
base/src/main/java/org/aya/generic/SortKind.java	`66.66% <ø> (+33.33%)`	⬆️
...c/main/java/org/aya/core/visitor/BetaExpander.java	`68.05% <37.50%> (-4.81%)`	⬇️
base/src/main/java/org/aya/tyck/LittleTyper.java	`72.36% <40.00%> (+6.19%)`	⬆️
base/src/main/java/org/aya/core/serde/SerTerm.java	`80.95% <50.00%> (-0.61%)`	⬇️
base/src/main/java/org/aya/core/term/ElimTerm.java	`73.80% <66.66%> (-3.97%)`	⬇️
base/src/main/java/org/aya/tyck/ExprTycker.java	`83.42% <75.00%> (-0.11%)`	⬇️
base/src/main/java/org/aya/core/term/Term.java	`96.40% <80.00%> (+0.08%)`	⬆️
.../src/main/java/org/aya/tyck/error/ErasedError.java	`80.00% <80.00%> (ø)`
... and 8 more

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

ice1000

Trying to understand

base/src/main/java/org/aya/core/term/ElimTerm.java

ice1000

Trying to understand

base/src/main/java/org/aya/core/visitor/BetaExpander.java

todo: implement not erased check for lambda

base/src/main/java/org/aya/tyck/StmtTycker.java

ice1000 · 2022-10-27T15:28:27Z

TODOs:

Erased pathlam

ice1000 · 2022-10-27T15:29:19Z

bors r+

584: Prop and Erased r=ice1000 a=tsao-chi This pr + Added ErasedTerm + generate ErasedTerm on inherit/synthesize whenever sort is Prop + implement illegal erased term check. + add a reduction rule: `elim(erased)` become `erased` + corrected prop-related tyck rules for sigma types and struct + updated LittleTyper to support new universe system for `type.computeType()` use cases Co-authored-by: ㄗㄠˋ ㄑㄧˊ <tsao-chi@the-lingo.org>

bors · 2022-10-27T15:31:06Z

This PR was included in a batch that successfully built, but then failed to merge into main. It will not be retried.

Additional information:

{"message":"All comments must be resolved.","documentation_url":"https://docs.github.com/articles/about-protected-branches"}

ice1000 · 2022-10-27T22:43:31Z

birs r+

ice1000 · 2022-10-27T22:43:41Z

bors r+

bors · 2022-10-27T22:45:14Z

Build succeeded:

ice1000 reviewed Oct 16, 2022

View reviewed changes

base/src/main/java/org/aya/core/term/ElimTerm.java Show resolved Hide resolved

base/src/main/java/org/aya/core/term/ElimTerm.java Show resolved Hide resolved

ice1000 reviewed Oct 16, 2022

View reviewed changes

base/src/main/java/org/aya/tyck/ExprTycker.java Outdated Show resolved Hide resolved

base/src/main/java/org/aya/tyck/ExprTycker.java Outdated Show resolved Hide resolved

ice1000 reviewed Oct 20, 2022

View reviewed changes

base/src/main/java/org/aya/core/term/ElimTerm.java Outdated Show resolved Hide resolved

base/src/main/java/org/aya/core/term/ElimTerm.java Outdated Show resolved Hide resolved

ice1000 reviewed Oct 20, 2022

View reviewed changes

base/src/main/java/org/aya/core/visitor/BetaExpander.java Outdated Show resolved Hide resolved

mio-19 force-pushed the prop branch from ca349b8 to 28b159c Compare October 23, 2022 16:25

This comment was marked as duplicate.

Sign in to view

mio-19 added 23 commits October 24, 2022 00:36

prop: add test

d5c4ce7

prop: allow Type fields on Prop struct and fixed the test

338d30b

prop: allow Type ctor of Prop data

56d3c3d

prop: add a failing test of Prop

a03c0ab

prop: fix Sig (A : Prop) ** A bug

f8e94ac

prop: add DummyTerm

f18df18

typer: add param of pi to ctx in LittleTyper

4184e40

prop: add ExprTycker.checkDummy()

9cf9779

typer: fix a weird bug

40a78f8

prop: rename Dummy to Erased

270f7be

prop: erase App(Erased) and Proj(Erased) in Normalizer

c9ad587

prop: erase PathApp(Erased)

0e019bf

tyck: yield ErasedTerm for elim(erased)

984c524

tyck: add checkNotErased()

14e328f

prop: add a test

a7092c2

tyck: use ElimTerm.proj

cbc2d25

misc: NotNull

19872f7

prop: also checkNotErased for simpleFn

f301010

prop: address comments

f0224d5

tyck: bring sortPi to LittleTyper and distinguished two ErasedTerm

43cc0b6

todo: implement not erased check for lambda

tyck: implemented new universe for LittleTyper

8a0883f

tyck: fixed not erased check

742e197

prop: make ErasedError readable

4918011

mio-19 added 5 commits October 24, 2022 00:36

prop: check lambda and fix a typo in test

c5c2ab2

misc: fix typo

5183fcd

prop: add comments

7faa437

prop: renames

e416930

refactor: rename methods

227562d

mio-19 force-pushed the prop branch from 0e54e70 to 227562d Compare October 23, 2022 16:37

merge: main into prop

84b9a9b

mio-19 marked this pull request as ready for review October 24, 2022 11:51

mio-19 changed the title ~~Prop WIP~~ Prop and Erased Oct 24, 2022

ice1000 reviewed Oct 24, 2022

View reviewed changes

base/src/main/java/org/aya/tyck/StmtTycker.java Outdated Show resolved Hide resolved

mio-19 added 2 commits October 25, 2022 13:33

merge: main into prop

d53d2e2

tyck: add ExprTycker.check() for inhert+erasure check

b611d70

review: some code review

4bd6a26

ice1000 added this to the v0.23 milestone Oct 27, 2022

ice1000 added the prop Universe of propositions label Oct 27, 2022

ice1000 self-assigned this Oct 27, 2022

bors bot merged commit 0efe1bc into main Oct 27, 2022

bors bot deleted the prop branch October 27, 2022 22:45

ice1000 mentioned this pull request Nov 28, 2022

Aya team logs since 60 days ago plctlab/PLCT-Weekly#532

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Prop and Erased #584

Prop and Erased #584

mio-19 commented Oct 16, 2022 •

edited

codecov bot commented Oct 17, 2022 •

edited

ice1000 left a comment

ice1000 left a comment

This comment was marked as duplicate.

ice1000 commented Oct 27, 2022

ice1000 commented Oct 27, 2022

bors bot commented Oct 27, 2022

ice1000 commented Oct 27, 2022

ice1000 commented Oct 27, 2022

bors bot commented Oct 27, 2022

Prop and Erased #584

Prop and Erased #584

Conversation

mio-19 commented Oct 16, 2022 • edited

codecov bot commented Oct 17, 2022 • edited

Codecov Report

ice1000 left a comment

Choose a reason for hiding this comment

ice1000 left a comment

Choose a reason for hiding this comment

This comment was marked as duplicate.

ice1000 commented Oct 27, 2022

ice1000 commented Oct 27, 2022

bors bot commented Oct 27, 2022

ice1000 commented Oct 27, 2022

ice1000 commented Oct 27, 2022

bors bot commented Oct 27, 2022

mio-19 commented Oct 16, 2022 •

edited

codecov bot commented Oct 17, 2022 •

edited