| 2011-06-21 |
Adam Megacz | add crude support for flattening with LetRec and Case... |
tree | commitdiff |
| 2011-06-19 |
Adam Megacz | remove magic flatten/unflatten identifiers |
tree | commitdiff |
| 2011-06-19 |
Adam Megacz | use CoreM monad to acquire known-to-compiler identifiers |
tree | commitdiff |
| 2011-06-02 |
Adam Megacz | add support for flattening recursive-let |
tree | commitdiff |
| 2011-05-31 |
Adam Megacz | update for new GHC coercion representation |
tree | commitdiff |
| 2011-05-31 |
Adam Megacz | remove RLet and RWhere |
tree | commitdiff |
| 2011-05-31 |
Adam Megacz | let RCut take a left environment as well |
tree | commitdiff |
| 2011-05-31 |
Adam Megacz | remove RJoin rule |
tree | commitdiff |
| 2011-05-31 |
Adam Megacz | better error reporting in coreTypeToWeakType; dont... |
tree | commitdiff |
| 2011-05-30 |
Adam Megacz | add -fflatten and -funsafe-skolemize flags |
tree | commitdiff |
| 2011-05-29 |
Adam Megacz | add RCut, RLeft, RRight rules |
tree | commitdiff |
| 2011-05-28 |
Adam Megacz | rename constructors of Arrange to start with A instead... |
tree | commitdiff |
| 2011-05-28 |
Adam Megacz | move more arrange routines into NaturalDeductionContext |
tree | commitdiff |
| 2011-05-28 |
Adam Megacz | move Arrange into NaturalDeductionContext |
tree | commitdiff |
| 2011-05-28 |
Adam Megacz | migrate HaskStrong away from using LeveledHaskType |
tree | commitdiff |
| 2011-05-27 |
Adam Megacz | HaskProof: make the succedent level part of the judgment |
tree | commitdiff |
| 2011-05-27 |
Adam Megacz | add commented-out/incomplete implementation of simplify... |
tree | commitdiff |
| 2011-05-27 |
Adam Megacz | General.v: add boolean and/or functions |
tree | commitdiff |
| 2011-05-27 |
Adam Megacz | rename variables to avoid Coq pickiness during extraction |
tree | commitdiff |
| 2011-05-27 |
Adam Megacz | partial support for LetRec in flattener |
tree | commitdiff |
| 2011-05-26 |
Adam Megacz | add new Where rule, eliminate unnecessary ga_swaps... |
tree | commitdiff |
| 2011-05-26 |
Adam Megacz | note to self in HaskWeak |
tree | commitdiff |
| 2011-05-23 |
Adam Megacz | NaturalDeduction: add nd_exch |
tree | commitdiff |
| 2011-05-16 |
Adam Megacz | HaskFlattener: support escapifying multi-leaf contexts |
tree | commitdiff |
| 2011-05-15 |
Adam Megacz | more efficient encoding of function types |
tree | commitdiff |
| 2011-05-15 |
Adam Megacz | add an identity production for Arrange |
tree | commitdiff |
| 2011-05-15 |
Adam Megacz | fix bug in flattener, make extensionality axiom explicit |
tree | commitdiff |
| 2011-05-14 |
Adam Megacz | integrate skolemization pass with flattening |
tree | commitdiff |
| 2011-05-14 |
Adam Megacz | improve detection of type function kinds, mainly their... |
tree | commitdiff |
| 2011-05-14 |
Adam Megacz | add split_list to General.v |
tree | commitdiff |
| 2011-05-14 |
Adam Megacz | add ToString instance for lists |
tree | commitdiff |
| 2011-05-13 |
Adam Megacz | first draft of skolemization pass |
tree | commitdiff |
| 2011-05-13 |
Adam Megacz | add EqDecidable instances for option and Tree |
tree | commitdiff |
| 2011-05-12 |
Adam Megacz | swap order of hypotheses in RApp to match RLet |
tree | commitdiff |
| 2011-05-12 |
Adam Megacz | rewrite {take,drop}_arg_types to avoid use of equality... |
tree | commitdiff |
| 2011-05-12 |
Adam Megacz | HaskFlattener: represent first-order abstraction using... |
tree | commitdiff |
| 2011-05-12 |
Adam Megacz | HaskFlattener: use ga_mk_raw |
tree | commitdiff |
| 2011-05-12 |
Adam Megacz | update PCF.v for new ECKind |
tree | commitdiff |
| 2011-05-12 |
Adam Megacz | HaskFlattener: simplify the flattener |
tree | commitdiff |
| 2011-05-12 |
Adam Megacz | HaskStrongTypes: add {take,drop}_arg_types |
tree | commitdiff |
| 2011-05-11 |
Adam Megacz | HaskFLattener: formatting fixes and refactoring |
tree | commitdiff |
| 2011-05-10 |
Adam Megacz | start using type-family-based GArrow classes |
tree | commitdiff |
| 2011-05-10 |
Adam Megacz | add support for flattening non-recursive Let bindings |
tree | commitdiff |
| 2011-05-09 |
Adam Megacz | move general-purpose routines from HaskFlattener to... |
tree | commitdiff |
| 2011-05-09 |
Adam Megacz | split HaskLiteralsAndTyCons into two files |
tree | commitdiff |
| 2011-05-09 |
Adam Megacz | add support for hetmet_unflatten |
tree | commitdiff |
| 2011-05-09 |
Adam Megacz | add support for hetmet_flatten casting variable |
tree | commitdiff |
| 2011-05-09 |
Adam Megacz | allow -fcoqpass to change the type of top-level bindings |
tree | commitdiff |
| 2011-05-09 |
Adam Megacz | use the "debug" version of Outputable for ToString... |
tree | commitdiff |
| 2011-05-09 |
Adam Megacz | change ECKind to *=>*=>* |
tree | commitdiff |
| 2011-05-09 |
Adam Megacz | abstract out the kind of environment classifiers (ECKind) |
tree | commitdiff |
| 2011-05-09 |
Adam Megacz | major improvements to flattener; almost finished now |
tree | commitdiff |
| 2011-05-09 |
Adam Megacz | allow rank-1 polymorphic types for globals |
tree | commitdiff |
| 2011-05-09 |
Adam Megacz | add PairTyCon and UnitTyCon |
tree | commitdiff |
| 2011-05-09 |
Adam Megacz | minor cleanups to Extraction-prefix.hs to eliminate... |
tree | commitdiff |
| 2011-05-05 |
Adam Megacz | further improvements to flattener |
tree | commitdiff |
| 2011-05-03 |
Adam Megacz | separate HaskProofStratified into PCF.v, HaskProgrammin... |
tree | commitdiff |
| 2011-04-30 |
Adam Megacz | reorganize HaskProof files |
tree | commitdiff |
| 2011-04-30 |
Adam Megacz | clean up hints for NaturalDeduction, split ProgrammingL... |
tree | commitdiff |
| 2011-04-29 |
Adam Megacz | remove many [[admit]]s from HaskProofFlattener.v |
tree | commitdiff |
| 2011-04-27 |
Adam Megacz | Merge branch 'master' of git.megacz.com/coq-hetmet |
tree | commitdiff |
| 2011-04-27 |
Adam Megacz | prove all [admit]ted lemmas in HaskStrongToProof (not... |
tree | commitdiff |
| 2011-04-25 |
Adam Megacz | add -fno-warn-unused-{binds,patterns} to Coq extraction |
tree | commitdiff |
| 2011-04-25 |
Adam Megacz | remove ClosedSIND (use "SIND []" instead) |
tree | commitdiff |
| 2011-04-24 |
Adam Megacz | remove all admits from ProgrammingLanguage.v |
tree | commitdiff |
| 2011-04-24 |
Adam Megacz | NaturalDeduction: add nd_swap, nd_prod_split, and some... |
tree | commitdiff |
| 2011-04-18 |
Adam Megacz | speed up builds by removing some dependencies from... |
tree | commitdiff |
| 2011-04-16 |
Adam Megacz | fix erroneous conclusion to penultimate lemma |
tree | commitdiff |
| 2011-04-11 |
Adam Megacz | unbreak lots more stuff |
tree | commitdiff |
| 2011-04-11 |
Adam Megacz | uncomment some code in ProgrammingLanguage.v |
tree | commitdiff |
| 2011-04-10 |
Adam Megacz | remove the very last admit (missing proof) from General... |
tree | commitdiff |
| 2011-04-10 |
Adam Megacz | fix bug in GeneralizedArrowFromReification |
tree | commitdiff |
| 2011-04-10 |
Adam Megacz | All.v: uncomment things |
tree | commitdiff |
| 2011-04-10 |
Adam Megacz | bugfix in ReificationsIsomorphicToGeneralizedArrows |
tree | commitdiff |
| 2011-04-10 |
Adam Megacz | add commented-out definitions for analytic proofs and... |
tree | commitdiff |
| 2011-04-10 |
Adam Megacz | fill in lots of missing proofs |
tree | commitdiff |
| 2011-04-10 |
Adam Megacz | update to new coq-categories, base ND_Relation on inert... |
tree | commitdiff |
| 2011-04-09 |
Adam Megacz | remove notations from Preamble that come from coq-categ... |
tree | commitdiff |
| 2011-04-04 |
Adam Megacz | update to account for coq-categories changes |
tree | commitdiff |
| 2011-04-02 |
Adam Megacz | update submodule pointer, account for changes upstream |
tree | commitdiff |
| 2011-04-02 |
Adam Megacz | ExtractionMain: better pdflatex code output |
tree | commitdiff |
| 2011-04-02 |
Adam Megacz | re-arrange ProgrammingLanguage |
tree | commitdiff |
| 2011-04-02 |
Adam Megacz | split HaskProofCategory into two files |
tree | commitdiff |
| 2011-04-01 |
Adam Megacz | remove unproven step1_lemma (it has a proof now) |
tree | commitdiff |
| 2011-03-29 |
Adam Megacz | formatting fixes |
tree | commitdiff |
| 2011-03-29 |
Adam Megacz | remove stale import from ExtractionMain |
tree | commitdiff |
| 2011-03-29 |
Adam Megacz | lots of cleanup |
tree | commitdiff |
| 2011-03-29 |
Adam Megacz | reorganize flattening code |
tree | commitdiff |
| 2011-03-29 |
Adam Megacz | HaskProofCategory: more work |
tree | commitdiff |
| 2011-03-29 |
Adam Megacz | swap the order of the hypotheses of RLet |
tree | commitdiff |
| 2011-03-29 |
Adam Megacz | NaturalDeduction: remove unnecessary scnd_leaf, add... |
tree | commitdiff |
| 2011-03-28 |
Adam Megacz | replace UJudg with Arrange |
tree | commitdiff |
| 2011-03-28 |
Adam Megacz | checkpoint |
tree | commitdiff |
| 2011-03-28 |
Adam Megacz | checkpoint |
tree | commitdiff |
| 2011-03-28 |
Adam Megacz | fix typo |
tree | commitdiff |
| 2011-03-28 |
Adam Megacz | ProgrammingLanguage: more implementation |
tree | commitdiff |
| 2011-03-28 |
Adam Megacz | HaskProofCategory: implement more |
tree | commitdiff |
| 2011-03-28 |
Adam Megacz | remove old code from WeakFunctorCategory |
tree | commitdiff |
| 2011-03-28 |
Adam Megacz | ReificationsIsomorphicToGeneralizedArrows: use EqDep |
tree | commitdiff |
| 2011-03-28 |
Adam Megacz | NaturalDeduction: allow multi-rule implementations... |
tree | commitdiff |
| next |
projects / coq-hetmet.git / history