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

PHI 11 - Type Constructors #13

Open
wants to merge 181 commits into
base: master
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
181 commits
Select commit Hold shift + click to select a range
d5c4db2
Initial draft
bkase Mar 21, 2021
8b3f0dd
Adds note about type holes
bkase Mar 21, 2021
aaa112a
Delta supports htyp/varctx or kind/tyvarctx
bkase Mar 22, 2021
696d9d9
Adds kind assignment, fixes a few bugs
bkase Mar 24, 2021
41f5187
Updated for kind-assignment and sane delta
bkase Mar 24, 2021
f57dd56
Uses cdot for both empty sets
bkase Mar 24, 2021
b14fc0c
Attempts to add Ana uvar rule
bkase Mar 24, 2021
ecdcd5b
Judgements and changes for singleton kinds
bkase Apr 11, 2021
0d0dcb9
Requested changes
bkase Apr 12, 2021
1506086
Fixes issues in PHI, adds theorems for reasoning
bkase Apr 17, 2021
2759c7e
Unrecognition tweak
bkase Apr 17, 2021
c43241e
Fixes for broken handling of tyvars
bkase Apr 20, 2021
b2ea0f1
Made suggested changes
bkase Apr 20, 2021
ed6b5e1
Latest changes
bkase Apr 24, 2021
ce7d4fe
Moves to bidirectional kind assignment
bkase Apr 28, 2021
3f6986b
Tweaks to design docs
bkase Apr 30, 2021
f1f1ed1
Removes the extra recursive param in lines
bkase May 1, 2021
99db512
Remove kind ascription on type equivalence
bkase May 17, 2021
4410cd5
Synthesize self for tvars
bkase May 20, 2021
8f53339
htau should be dtau in judgment box
hejohns Jun 15, 2021
4201af8
KSVar bug?
hejohns Jun 19, 2021
bb3b828
let's backup before any possible hard drive failures!
hejohns Jul 13, 2021
247cd79
ditto
hejohns Jul 13, 2021
bb3088e
good place to stop
hejohns Jul 13, 2021
6d376f8
forgot some stuff
hejohns Jul 13, 2021
3f093b3
small fixes before reading
hejohns Jul 13, 2021
7bccc52
circularity mostly worked out?
hejohns Jul 14, 2021
d9c0c83
progress. I think
hejohns Jul 14, 2021
cd20c07
::>, :: better, but equivalence at superkinds still broken
hejohns Jul 15, 2021
ebc1cfd
is this necessary for consistentsubkinding+labeled singletons?
hejohns Jul 15, 2021
644f71e
I think the solid rules are finally right.......
hejohns Jul 15, 2021
43f2f9f
change ordering
hejohns Jul 15, 2021
f9491db
KindWellFormed
hejohns Jul 15, 2021
a3afbe4
auto number rules
hejohns Jul 16, 2021
ea84685
mucking around
hejohns Jul 16, 2021
5a39d2f
probably should've named the branch 11-parameterized-types
hejohns Jul 16, 2021
7e80c00
rename things
hejohns Jul 16, 2021
838ac8d
does 21 make sense??
hejohns Jul 20, 2021
9f6442b
a bunch of well formedness stuff
hejohns Jul 20, 2021
9e1dfe0
sad. needs "redundant" premiss to be provable
hejohns Jul 20, 2021
cc97e96
slow progess
hejohns Jul 21, 2021
9e68518
please don't let weaking be sim. inductive as well :(
hejohns Jul 21, 2021
30576fe
remove redundant premisses
hejohns Jul 21, 2021
b6dbc6e
?! looks strange. But might actually work
hejohns Jul 23, 2021
2fb1e60
are holes handled correctly now??
hejohns Jul 24, 2021
aa481af
title
hejohns Jul 24, 2021
5942690
equality of types and KHole strangeness
hejohns Jul 26, 2021
c9d7b2a
type equality fixed?(take 2)
hejohns Jul 27, 2021
aefe5c8
actually need this rule after all
hejohns Jul 27, 2021
311380e
yeah ok we do need refl,symm,trans for type equality
hejohns Jul 27, 2021
2e1a28c
naming rules
hejohns Jul 28, 2021
7bea7b2
about to regex so let's backup
hejohns Jul 28, 2021
178ee30
eh
hejohns Jul 28, 2021
6aa25fb
all rules named
hejohns Jul 28, 2021
123f6af
weakening
hejohns Jul 28, 2021
efb1075
idk why I insisted on typing it all out last time
hejohns Jul 28, 2021
8152963
fix exchange
hejohns Jul 29, 2021
ffbd8c4
I screwed up the layout of these lemmas
hejohns Jul 29, 2021
9325d5c
huge waste of a day. but at least it worked out in the end?
hejohns Jul 29, 2021
92f4950
fix context marking
hejohns Jul 29, 2021
cb0ab62
:(
hejohns Jul 29, 2021
a1c4806
dodged a KOMA-Script bullet
hejohns Jul 29, 2021
86dd78e
:(
hejohns Jul 29, 2021
66ec9c9
:-()
hejohns Jul 30, 2021
047ff3c
I sure hope the trees swapped w/o error
hejohns Jul 30, 2021
3332c80
I hate myself for not reversing the inferrule args earlier
hejohns Jul 30, 2021
d6f78f0
got vim macro'd to hell. We'll fix the spacing another time
hejohns Jul 30, 2021
6603660
we've gone back/forth 100 times but COK does need subderivation
hejohns Jul 30, 2021
2928d32
ended up just fixing weakening manually. had to fix an error
hejohns Jul 30, 2021
642e010
this error
hejohns Jul 30, 2021
21e7cd4
weaking looks good!
hejohns Jul 30, 2021
d981a97
finally figured out how to use typearea
hejohns Jul 31, 2021
5277d18
I think we need induction on type size for K-subst
hejohns Jul 31, 2021
8be7879
lemma -> theorem, OK-PK
hejohns Aug 12, 2021
3a06278
must've changed DIV on accident
hejohns Aug 12, 2021
af7d58f
meant THIS one
hejohns Aug 12, 2021
0fed84e
sending it out to cyrus-
hejohns Aug 17, 2021
f969eb0
might as well add the pptx
hejohns Aug 17, 2021
1b1edeb
fell asleep; saving
hejohns Sep 2, 2021
9651a66
singleton reduction/normalization rules?
hejohns Sep 3, 2021
f3d4356
named singleton reduction rules
hejohns Sep 26, 2021
5e42ccf
mostly sketch PK-Unicity
hejohns Sep 27, 2021
90e2dc6
singleton normalization unicity took too many steps
hejohns Oct 3, 2021
b399dc1
tiny bit of notes to myself
hejohns Oct 7, 2021
cbd6fe8
syntastic
hejohns Feb 4, 2022
a7e06fb
we actually do need this rule
hejohns Feb 4, 2022
80ddf74
put code scratch here
hejohns Feb 7, 2022
440c06c
HUnit instead
hejohns Feb 7, 2022
caac5f0
The most trivial cases
hejohns Feb 13, 2022
d209b78
what a waste of time fiddling w/ (.)/flip...
hejohns Feb 15, 2022
6973fce
finish αRename
hejohns Mar 1, 2022
7f50d1e
canonical form stuff
hejohns Mar 1, 2022
3a19195
just to save what's in Algo so far
hejohns Mar 1, 2022
da687e0
hindent/various cosmetics
hejohns Mar 1, 2022
1dfe911
too tired, just add everything
hejohns Mar 1, 2022
5613974
wrap up last commit sorta-- canon isn't totally broken
hejohns Mar 3, 2022
d633581
move canon to Algo
hejohns Mar 3, 2022
b5c6d41
Need pk wfak csk now
hejohns Mar 3, 2022
a161847
need to do csk, then we can test some stuff
hejohns Mar 3, 2022
57b6d99
hs-perl5 actually works.......
hejohns Mar 3, 2022
8f9a0bc
regoranize tests to make running only some tests easier
hejohns Mar 4, 2022
94b3867
what a fun way to implement fresh
hejohns Mar 4, 2022
ca43b99
focusing on getting tests working
hejohns Mar 4, 2022
5590356
working on very basic test. Still not sure how to handle the mutually…
hejohns Mar 4, 2022
2bd58d9
some self-induced pain because I didn't want to use de bruijn indeces
hejohns Mar 4, 2022
2762e9a
≡_α for Typ s (although idk where we need it) as part of Rewrite class
hejohns Mar 4, 2022
40aa431
Good canonKnd test
hejohns Mar 4, 2022
41e63cc
debugging trace calls
hejohns Mar 4, 2022
c65c55c
current tests pass now; can keep moving forward
hejohns Mar 4, 2022
ef2dc25
check ≡_α in csk
hejohns Mar 4, 2022
7b7d5ce
use kequiv instead of just ≡_α where appropriate
hejohns Mar 4, 2022
8aaeb79
some basic tests pass
hejohns Mar 5, 2022
eb3753d
some documentation for myself (I think I'll Reason this soon)
hejohns Mar 5, 2022
66edc62
need to run; doesn't build; need to handle base types like `list`
hejohns Mar 5, 2022
455b31c
partial revert (working on η rules)
hejohns Mar 7, 2022
f092459
apparently hindent really doesn't like deriving via
hejohns Mar 7, 2022
e81f20a
forgot haskell has type families. doesn't build-- lots of changes
hejohns Mar 7, 2022
540a87c
I didn't think this through-- need to revert last couple commits
hejohns Mar 7, 2022
a73675f
revert most of last couple commits (see last commit)
hejohns Mar 7, 2022
c85c950
clean the crumbs from last revert-- make it build
hejohns Mar 7, 2022
bfb5e56
need to run, but our current plan is to have two Aps for irriducible/…
hejohns Mar 7, 2022
458f3c1
leaving this here, but we're gonna branch and move a lot
hejohns Mar 12, 2022
bcb806e
idk what's what anymore-- adding and then creating new files
hejohns Mar 20, 2022
e24cb49
reorganizing everything
hejohns Mar 20, 2022
0557640
lots of changes. Reorganized everything to ex/internal language
hejohns Mar 21, 2022
3a1900d
tooling paaaiiinn
hejohns Mar 27, 2022
ba49549
elab
hejohns Mar 27, 2022
c3b6103
a little wh/normal + hindent
hejohns Mar 27, 2022
3da60be
path normalization reduces in the kind-- need to work out
hejohns Mar 29, 2022
fbfa586
tests pass again. But I'm not really sure what I've done
hejohns Apr 3, 2022
3f164da
mpk
hejohns Apr 3, 2022
6577ca0
used wrong ctx function
hejohns Apr 3, 2022
b966106
test exception call stack
hejohns Apr 3, 2022
f6e5222
hmmm not fun
hejohns Apr 3, 2022
ffacd61
simple test
hejohns Apr 3, 2022
b2a7b05
forgot recursive type_normal for HO singletons
hejohns Apr 4, 2022
fd92ad6
parser for writing tests: SEE LONG MESSAGE
hejohns Apr 4, 2022
dc74221
some tests from before
hejohns Apr 4, 2022
9f74d92
well the test fails... but due to perl eval...
hejohns Apr 4, 2022
9772124
I cannot l;we;nasdk
hejohns Apr 4, 2022
1c2d0a8
adsf
hejohns Apr 4, 2022
39e4cf4
epic fail. I mean seriously. ~5 hours wasted
hejohns Apr 4, 2022
4711719
external expression langauge
hejohns Apr 10, 2022
ed846f8
Bidirectional typechecker basics
hejohns Apr 18, 2022
021ba1a
syn tests
hejohns Apr 21, 2022
8c2c03f
Didn't realize I didn't add BiDirectional.hs ... rip git history
hejohns Apr 25, 2022
ec2df08
writing up algorithmic rules
hejohns May 2, 2022
23a220e
type normal
hejohns May 2, 2022
35da088
did that perl filter actually work
hejohns May 8, 2022
500f790
AlgTypeNormal
hejohns May 8, 2022
b19d8fb
AlgWHNormal
hejohns May 8, 2022
fd7bb16
make sure binop types normalize correctly
hejohns May 8, 2022
291c09d
AlgNatKind
hejohns May 8, 2022
0d20a8e
typo in path normal (caught during latexing). TODO: test should ve ex…
hejohns May 8, 2022
810b293
AlgPathNormal
hejohns May 9, 2022
76219f8
ElimCtx not EvalCtx
hejohns May 11, 2022
b085914
number alg rules for now
hejohns May 11, 2022
d459cec
start gradualizing type equality
hejohns May 11, 2022
de980ae
some perl pie action: |- to ⊢
hejohns May 11, 2022
eb3b80f
typo
hejohns May 11, 2022
a03263d
term_normal at KHole?
hejohns May 12, 2022
fb54ccc
initial gradualization and csk and kequiv
hejohns May 12, 2022
37eef7b
I think caught up gradual
hejohns May 12, 2022
39b68e2
as discussed in OH minus TODO s
hejohns May 12, 2022
4756f0d
part way through tidying up for PR
hejohns Jul 9, 2022
8c8bbc4
make isPath a judgment
hejohns Jul 10, 2022
a1432d2
partial revert: we did need this whreduc rule
hejohns Jul 10, 2022
cdd9fff
minor fixes
hejohns Jul 10, 2022
757b419
clarify normalize at kind and fill in TODO
hejohns Jul 10, 2022
690c4a6
clean up notes
hejohns Jul 10, 2022
d549b0c
rename md tex source to reduce confusion
hejohns Aug 22, 2022
0832702
rename j.....dunfield.sty by getting upstream version
hejohns Aug 22, 2022
3242dd8
add information to jdunfield.sty header
hejohns Aug 22, 2022
5531f4d
comment out \newcommand{\mathcolor}{..} for now and build
hejohns Aug 22, 2022
12eabe1
fix \today substitution
hejohns Aug 24, 2022
5a40fcf
update hejohns-colors
hejohns Aug 24, 2022
c319f0a
fixup latex, incorporating recent hejohns-stub changes and comment ou…
hejohns Aug 24, 2022
ec4973b
need to write md
hejohns Aug 24, 2022
892a2ec
bump to newer ghc by removing unused Language.Perl dependency
hejohns Sep 26, 2022
4e1ef53
untrack tex to generate md-- just don't accidentally rm it locally...
hejohns Sep 26, 2022
962e2ac
...and we're going back to older ghc since hls doesn't work for some …
hejohns Sep 26, 2022
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
adsf
  • Loading branch information
hejohns committed Apr 4, 2022
commit 1c2d0a8e6f45b09b0ded7ff7f3757ac98b67ec9b
8 changes: 7 additions & 1 deletion 11-type-constructors/algo/src/Normalize.hs
Original file line number Diff line number Diff line change
@@ -186,7 +186,13 @@ term_normal iΓ δ τ =
S _ _ -> error "type_normal failure?\n"
Π t ωτ1 ωτ2 ->
let t' = fresh t
in Tλ t' ωτ1 (term_normal (iΓ ⌢ (t', ωτ1)) (TAp δ (TVar t')) ωτ2)
in Tλ
t'
ωτ1
(term_normal
(iΓ ⌢ (t', ωτ1))
(TAp δ (TVar t'))
(αRename t' t ωτ2))

path_normal :: Ctx -> Term -> (Term, Typ)
path_normal _ Bse = (Bse, Type)