Code

PHI 11 - Type Constructors#13

Code

Open

hejohns wants to merge 181 commits intomasterhazelgrove/phi:masterfrom 11-type-constructorshazelgrove/phi:11-type-constructorsCopy head branch name to clipboard

+4,747

Commits

Commits on Mar 21, 2021

• Initial draft

  Show description for d5c4db2
  bkase

  committed
  d5c4db2

• Adds note about type holes

  bkase

  committed
  8b3f0dd

Commits on Mar 22, 2021

• Delta supports htyp/varctx or kind/tyvarctx

  bkase

  committed
  aaa112a

Commits on Mar 24, 2021

• Adds kind assignment, fixes a few bugs

  bkase

  committed
  696d9d9

• Updated for kind-assignment and sane delta

  bkase

  committed
  41f5187

• Uses cdot for both empty sets

  bkase

  committed
  f57dd56

• Attempts to add Ana uvar rule

  bkase

  committed
  b14fc0c

Commits on Apr 11, 2021

• Judgements and changes for singleton kinds

  bkase

  committed
  ecdcd5b

Commits on Apr 12, 2021

• Requested changes

  bkase

  committed
  0d0dcb9

Commits on Apr 17, 2021

• Fixes issues in PHI, adds theorems for reasoning

  bkase

  committed
  1506086

• Unrecognition tweak

  bkase

  committed
  2759c7e

Commits on Apr 20, 2021

• Fixes for broken handling of tyvars

  bkase

  committed
  c43241e

• Made suggested changes

  bkase

  committed
  b2ea0f1

Commits on Apr 24, 2021

• Latest changes

  bkase

  committed
  ed6b5e1

Commits on Apr 28, 2021

• Moves to bidirectional kind assignment

  bkase

  committed
  ce7d4fe

Commits on Apr 30, 2021

• Tweaks to design docs

  bkase

  committed
  3f6986b

Commits on May 1, 2021

• Removes the extra recursive param in lines

  bkase

  committed
  f1f1ed1

Commits on May 17, 2021

• Remove kind ascription on type equivalence

  bkase

  committed
  99db512

Commits on May 20, 2021

• Synthesize self for tvars

  bkase

  committed
  4410cd5

Commits on Jun 15, 2021

• htau should be dtau in judgment box

  hejohns

  committed
  8f53339

Commits on Jun 19, 2021

• KSVar bug?

  hejohns

  committed
  4201af8

Commits on Jul 13, 2021

• let's backup before any possible hard drive failures!

  hejohns

  committed
  bb3b828

• ditto

  hejohns

  committed
  247cd79

• good place to stop

  Show description for bb3088e
  hejohns

  committed
  bb3088e

• forgot some stuff

  hejohns

  committed
  6d376f8

• small fixes before reading

  hejohns

  committed
  3f093b3

Commits on Jul 14, 2021

• circularity mostly worked out?

  Show description for 7bccc52
  hejohns

  committed
  7bccc52

• progress. I think

  hejohns

  committed
  d9c0c83

Commits on Jul 15, 2021

• ::>, :: better, but equivalence at superkinds still broken

  hejohns

  committed
  cd20c07

• is this necessary for consistentsubkinding+labeled singletons?

  hejohns

  committed
  ebc1cfd

• I think the solid rules are finally right.......

  hejohns

  committed
  644f71e

• change ordering

  hejohns

  committed
  43f2f9f

• KindWellFormed

  hejohns

  committed
  f9491db

Commits on Jul 16, 2021

• auto number rules

  hejohns

  committed
  a3afbe4

• mucking around

  hejohns

  committed
  ea84685

• probably should've named the branch 11-parameterized-types

  hejohns

  committed
  5a39d2f

• rename things

  hejohns

  committed
  7e80c00

Commits on Jul 20, 2021

• does 21 make sense??

  hejohns

  committed
  838ac8d

• a bunch of well formedness stuff

  hejohns

  committed
  9f6442b

• sad. needs "redundant" premiss to be provable

  hejohns

  committed
  9e1dfe0

Commits on Jul 21, 2021

• slow progess

  hejohns

  committed
  cc97e96

• please don't let weaking be sim. inductive as well :(

  hejohns

  committed
  9e68518

• remove redundant premisses

  Show description for 30576fe
  hejohns

  committed
  30576fe

Commits on Jul 23, 2021

• ?! looks strange. But might actually work

  hejohns

  committed
  b6dbc6e

Commits on Jul 24, 2021

• are holes handled correctly now??

  hejohns

  committed
  2fb1e60

• title

  hejohns

  committed
  aa481af

Commits on Jul 26, 2021

• equality of types and KHole strangeness

  hejohns

  committed
  5942690

Commits on Jul 27, 2021

• type equality fixed?(take 2)

  hejohns

  committed
  c9d7b2a

• actually need this rule after all

  Show description for aefe5c8
  hejohns

  committed
  aefe5c8

• yeah ok we do need refl,symm,trans for type equality

  Show description for 311380e
  hejohns

  committed
  311380e

Commits on Jul 28, 2021

• naming rules

  hejohns

  committed
  2e1a28c

• about to regex so let's backup

  hejohns

  committed
  7bea7b2

• eh

  hejohns

  committed
  178ee30

• all rules named

  hejohns

  committed
  6aa25fb

• weakening

  hejohns

  committed
  123f6af

• idk why I insisted on typing it all out last time

  hejohns

  committed
  efb1075

Commits on Jul 29, 2021

• fix exchange

  hejohns

  committed
  8152963

• I screwed up the layout of these lemmas

  hejohns

  committed
  ffbd8c4

• huge waste of a day. but at least it worked out in the end?

  hejohns

  committed
  9325d5c

• fix context marking

  hejohns

  committed
  92f4950

• :(

  hejohns

  committed
  cb0ab62

• dodged a KOMA-Script bullet

  hejohns

  committed
  a1c4806

• :(

  hejohns

  committed
  86dd78e

Commits on Jul 30, 2021

• :-()

  hejohns

  committed
  66ec9c9

• I sure hope the trees swapped w/o error

  hejohns

  committed
  047ff3c

• I hate myself for not reversing the inferrule args earlier

  Show description for 3332c80
  hejohns

  committed
  3332c80

• got vim macro'd to hell. We'll fix the spacing another time

  hejohns

  committed
  d6f78f0

• we've gone back/forth 100 times but COK does need subderivation

  hejohns

  committed
  6603660

• ended up just fixing weakening manually. had to fix an error

  hejohns

  committed
  2928d32

• this error

  hejohns

  committed
  642e010

• weaking looks good!

  hejohns

  committed
  21e7cd4

Commits on Jul 31, 2021

• finally figured out how to use typearea

  hejohns

  committed
  d981a97

• I think we need induction on type size for K-subst

  hejohns

  committed
  5277d18

Commits on Aug 12, 2021

• lemma -> theorem, OK-PK

  hejohns

  committed
  8be7879

• must've changed DIV on accident

  hejohns

  committed
  3a06278

• meant THIS one

  hejohns

  committed
  af7d58f

Commits on Aug 17, 2021

• sending it out to cyrus-

  hejohns

  committed
  0fed84e

• might as well add the pptx

  hejohns

  committed
  f969eb0

Commits on Sep 2, 2021

• fell asleep; saving

  hejohns

  committed
  1b1edeb

Commits on Sep 3, 2021

• singleton reduction/normalization rules?

  Show description for 9651a66
  hejohns

  committed
  9651a66

Commits on Sep 26, 2021

• named singleton reduction rules

  Show description for f3d4356
  hejohns

  committed
  f3d4356

Commits on Sep 27, 2021

• mostly sketch PK-Unicity

  Show description for 5e42ccf
  hejohns

  committed
  5e42ccf

Commits on Oct 3, 2021

• singleton normalization unicity took too many steps

  hejohns

  committed
  90e2dc6

Commits on Oct 7, 2021

• tiny bit of notes to myself

  hejohns

  committed
  b399dc1

Commits on Feb 4, 2022

• syntastic

  hejohns

  committed
  cbd6fe8

• we actually do need this rule

  Show description for a7e06fb
  hejohns

  committed
  a7e06fb

Commits on Feb 7, 2022

• put code scratch here

  hejohns

  committed
  80ddf74

• HUnit instead

  hejohns

  committed
  440c06c

Commits on Feb 13, 2022

• The most trivial cases

  Show description for caac5f0
  hejohns

  committed
  caac5f0

Commits on Feb 15, 2022

• what a waste of time fiddling w/ (.)/flip...

  hejohns

  committed
  d209b78

Commits on Mar 1, 2022

• finish αRename

  Show description for 6973fce
  hejohns

  committed
  6973fce

• canonical form stuff

  hejohns

  committed
  7f50d1e

• just to save what's in Algo so far

  hejohns

  committed
  3a19195

• hindent/various cosmetics

  hejohns

  committed
  da687e0

• too tired, just add everything

  hejohns

  committed
  1dfe911

Commits on Mar 3, 2022

• wrap up last commit sorta-- canon isn't totally broken

  hejohns

  committed
  5613974

• move canon to Algo

  Show description for d633581
  hejohns

  committed
  d633581

• Need pk wfak csk now

  hejohns

  committed
  b5c6d41

• need to do csk, then we can test some stuff

  hejohns

  committed
  a161847

• hs-perl5 actually works.......

  hejohns

  committed
  57b6d99

Commits on Mar 4, 2022

• regoranize tests to make running only some tests easier

  Show description for 8f9a0bc
  hejohns

  committed
  8f9a0bc

• what a fun way to implement fresh

  hejohns

  committed
  94b3867

• focusing on getting tests working

  hejohns

  committed
  ca43b99

• working on very basic test. Still not sure how to handle the mutually recursive judgments

  hejohns

  committed
  5590356

• some self-induced pain because I didn't want to use de bruijn indeces

  hejohns

  committed
  2bd58d9

• ≡_α for Typ s (although idk where we need it) as part of Rewrite class

  hejohns

  committed
  2762e9a

• Good canonKnd test

  hejohns

  committed
  40aa431

• debugging trace calls

  Show description for 41e63cc
  hejohns

  committed
  41e63cc

• current tests pass now; can keep moving forward

  hejohns

  committed
  c65c55c

• check ≡_α in csk

  hejohns

  committed
  ef2dc25

• use kequiv instead of just ≡_α where appropriate

  hejohns

  committed
  7b7d5ce

Commits on Mar 5, 2022

• some basic tests pass

  hejohns

  committed
  8aaeb79

• some documentation for myself (I think I'll Reason this soon)

  hejohns

  committed
  eb3753d

• need to run; doesn't build; need to handle base types like list

  hejohns

  committed
  66edc62

Commits on Mar 7, 2022

• partial revert (working on η rules)

  hejohns

  committed
  455b31c

• apparently hindent really doesn't like deriving via

  hejohns

  committed
  f092459

• forgot haskell has type families. doesn't build-- lots of changes

  hejohns

  committed
  e81f20a

• I didn't think this through-- need to revert last couple commits

  Show description for 540a87c
  hejohns

  committed
  540a87c

• revert most of last couple commits (see last commit)

  Show description for a73675f
  hejohns

  committed
  a73675f

• clean the crumbs from last revert-- make it build

  hejohns

  committed
  c85c950

• need to run, but our current plan is to have two Aps for irriducible/reducible

  hejohns

  committed
  bfb5e56

Commits on Mar 12, 2022

• leaving this here, but we're gonna branch and move a lot

  hejohns

  committed
  458f3c1

Commits on Mar 20, 2022

• idk what's what anymore-- adding and then creating new files

  hejohns

  committed
  bcb806e

• reorganizing everything

  hejohns

  committed
  e24cb49

Commits on Mar 21, 2022

• lots of changes. Reorganized everything to ex/internal language

  Show description for 0557640
  hejohns

  committed
  0557640

Commits on Mar 27, 2022

• tooling paaaiiinn

  Show description for 3a1900d
  hejohns

  committed
  3a1900d

• elab

  hejohns

  committed
  ba49549

• a little wh/normal + hindent

  hejohns

  committed
  c3b6103

Commits on Mar 29, 2022

• path normalization reduces in the kind-- need to work out

  hejohns

  committed
  3da60be

Commits on Apr 3, 2022

• tests pass again. But I'm not really sure what I've done

  hejohns

  committed
  fbfa586

• mpk

  hejohns

  committed
  3f164da

• used wrong ctx function

  hejohns

  committed
  6577ca0

• test exception call stack

  hejohns

  committed
  b966106

• hmmm not fun

  hejohns

  committed
  f6e5222

• simple test

  hejohns

  committed
  ffacd61

Commits on Apr 4, 2022

• forgot recursive type_normal for HO singletons

  hejohns

  committed
  b2a7b05

• parser for writing tests: SEE LONG MESSAGE

  Show description for fd92ad6
  hejohns

  committed
  fd92ad6

• some tests from before

  hejohns

  committed
  dc74221

• well the test fails... but due to perl eval...

  hejohns

  committed
  9f74d92

• I cannot l;we;nasdk

  hejohns

  committed
  9772124

• adsf

  hejohns

  committed
  1c2d0a8

• epic fail. I mean seriously. ~5 hours wasted

  Show description for 39e4cf4
  hejohns

  committed
  39e4cf4

Commits on Apr 10, 2022

• external expression langauge

  hejohns

  committed
  4711719

Commits on Apr 18, 2022

• Bidirectional typechecker basics

  Show description for ed846f8
  hejohns

  committed
  ed846f8

Commits on Apr 21, 2022

• syn tests

  hejohns

  committed
  021ba1a

Commits on Apr 25, 2022

• Didn't realize I didn't add BiDirectional.hs ... rip git history

  Show description for 8c2c03f
  hejohns

  committed
  8c2c03f

Commits on May 2, 2022

• writing up algorithmic rules

  Show description for ec2df08
  hejohns

  committed
  ec2df08

• type normal

  Show description for 23a220e
  hejohns

  committed
  23a220e

Commits on May 8, 2022

• did that perl filter actually work

  hejohns

  committed
  35da088

• AlgTypeNormal

  hejohns

  committed
  500f790

• AlgWHNormal

  hejohns

  committed
  b19d8fb

• make sure binop types normalize correctly

  hejohns

  committed
  fd7bb16

• AlgNatKind

  hejohns

  committed
  291c09d

• typo in path normal (caught during latexing). TODO: test should ve exposed

  hejohns

  committed
  0d20a8e

Commits on May 9, 2022

• AlgPathNormal

  hejohns

  committed
  810b293

Commits on May 11, 2022

• ElimCtx not EvalCtx

  hejohns

  committed
  76219f8

• number alg rules for now

  Show description for b085914
  hejohns

  committed
  b085914

• start gradualizing type equality

  hejohns

  committed
  d459cec

• some perl pie action: |- to ⊢

  hejohns

  committed
  de980ae

• typo

  hejohns

  committed
  eb3b80f

Commits on May 12, 2022

• term_normal at KHole?

  hejohns

  committed
  a03263d

• initial gradualization and csk and kequiv

  hejohns

  committed
  fb54ccc

• I think caught up gradual

  Show description for 37eef7b
  hejohns

  committed
  37eef7b

• as discussed in OH minus TODO s

  hejohns

  committed
  39b68e2

Commits on Jul 9, 2022

• part way through tidying up for PR

  Show description for 4756f0d
  hejohns

  committed
  4756f0d

Commits on Jul 10, 2022

• make isPath a judgment

  hejohns

  committed
  8c8bbc4

• partial revert: we did need this whreduc rule

  hejohns

  committed
  a1432d2

• minor fixes

  hejohns

  committed
  cdd9fff

• clarify normalize at kind and fill in TODO

  hejohns

  committed
  757b419

• clean up notes

  hejohns

  committed
  690c4a6

Commits on Aug 22, 2022

• rename md tex source to reduce confusion

  hejohns

  committed
  d549b0c

• rename j.....dunfield.sty by getting upstream version

  Show description for 0832702
  hejohns

  committed
  0832702

• add information to jdunfield.sty header

  hejohns

  committed
  3242dd8

• comment out \newcommand{\mathcolor}{..} for now and build

  hejohns

  committed
  5531f4d

Commits on Aug 24, 2022

• fix \today substitution

  Show description for 12eabe1
  hejohns

  committed
  12eabe1

• update hejohns-colors

  hejohns

  committed
  5a40fcf

• fixup latex, incorporating recent hejohns-stub changes and comment out unwanted

  hejohns

  committed
  c319f0a

• need to write md

  hejohns

  committed
  ec4973b

Commits on Sep 26, 2022

• bump to newer ghc by removing unused Language.Perl dependency

  hejohns

  committed
  892a2ec

• untrack tex to generate md-- just don't accidentally rm it locally...

  hejohns

  committed
  4e1ef53

• ...and we're going back to older ghc since hls doesn't work for some reason

  Show description for 962e2ac
  hejohns

  committed
  962e2ac