2011-03-16 |
Adam Megacz | check for Case that uses its binder, which we do not... |
tree | commitdiff |
2011-03-16 |
Adam Megacz | fix broken sortAlts implementation |
tree | commitdiff |
2011-03-16 |
Adam Megacz | major overhaul of WeakToStrong/StrongToWeak; it can... |
tree | commitdiff |
2011-03-16 |
Adam Megacz | better variable names in HaskWeakToCore |
tree | commitdiff |
2011-03-16 |
Adam Megacz | restrict RNote to one hypothesis, major additions to... |
tree | commitdiff |
2011-03-16 |
Adam Megacz | add EGlobal/RGlobal for CoreVars whose binder we cannot see |
tree | commitdiff |
2011-03-16 |
Adam Megacz | add crude Monad type class |
tree | commitdiff |
2011-03-15 |
Adam Megacz | final batch of fixups before enabling -fcoqpass |
tree | commitdiff |
2011-03-15 |
Adam Megacz | fix spellings in Extraction-prefix.hs, minor tweaks |
tree | commitdiff |
2011-03-15 |
Adam Megacz | formatting |
tree | commitdiff |
2011-03-15 |
Adam Megacz | change names of Kind constructors to be more informative |
tree | commitdiff |
2011-03-15 |
Adam Megacz | reshuffle definitions in an attempt to iron out inter... |
tree | commitdiff |
2011-03-14 |
Adam Megacz | add support for CSP in HaskCore+HaskWeak |
tree | commitdiff |
2011-03-14 |
Adam Megacz | remove dead code from HaskWeak |
tree | commitdiff |
2011-03-14 |
Adam Megacz | eliminate ext_tree_{left,right} keywords |
tree | commitdiff |
2011-03-14 |
Adam Megacz | more formatting fixes |
tree | commitdiff |
2011-03-14 |
Adam Megacz | formatting fixes |
tree | commitdiff |
2011-03-14 |
Adam Megacz | minor cleanups, deleted dead code, eliminated use of... |
tree | commitdiff |
2011-03-14 |
Adam Megacz | fix sortAlts so it actually does something |
tree | commitdiff |
2011-03-14 |
Adam Megacz | rename weakTypeToType'' to weakTypeToTypeOfKind |
tree | commitdiff |
2011-03-14 |
Adam Megacz | revise tyFunKind to use splitKind |
tree | commitdiff |
2011-03-14 |
Adam Megacz | add splitKind to HaskKind |
tree | commitdiff |
2011-03-14 |
Adam Megacz | fix ToString instance for Kind |
tree | commitdiff |
2011-03-14 |
Adam Megacz | minor cleanups in HaskStrongToWeak |
tree | commitdiff |
2011-03-14 |
Adam Megacz | include URL for trfrac.sty and mathpartir in LaTeX... |
tree | commitdiff |
2011-03-14 |
Adam Megacz | first pass at proper handling of coercions in HaskWeak |
tree | commitdiff |
2011-03-14 |
Adam Megacz | better error reporting in HaskWeakToStrong |
tree | commitdiff |
2011-03-14 |
Adam Megacz | better error reporting in Extraction.v |
tree | commitdiff |
2011-03-14 |
Adam Megacz | close numerous holes in HaskStrongToProof |
tree | commitdiff |
2011-03-14 |
Adam Megacz | major revision of HaskWeakToStrong, put phi/psi on... |
tree | commitdiff |
2011-03-14 |
Adam Megacz | fix spelling error in HaskWeakToCore |
tree | commitdiff |
2011-03-14 |
Adam Megacz | remove weakTypeOfWeakExpr and replaceWeakTypeVar, no... |
tree | commitdiff |
2011-03-14 |
Adam Megacz | store the scrutinee CoreVar in WeakExpr Case to simplif... |
tree | commitdiff |
2011-03-14 |
Adam Megacz | store the magic CoreVar for hetmet brak/esc in WeakExpr... |
tree | commitdiff |
2011-03-14 |
Adam Megacz | detect (->) TyCon and substitute FunTy in WeakToCore |
tree | commitdiff |
2011-03-14 |
Adam Megacz | fix bugs in LaTeX output |
tree | commitdiff |
2011-03-14 |
Adam Megacz | ToString instance for HaskCore |
tree | commitdiff |
2011-03-14 |
Adam Megacz | General.addErrorMessage, orErrorBindWithMessage |
tree | commitdiff |
2011-03-14 |
Adam Megacz | move eol:string to General.v |
tree | commitdiff |
2011-03-13 |
Adam Megacz | restore HaskWeakToStrong functionality that I broke... |
tree | commitdiff |
2011-03-13 |
Adam Megacz | Remove unnecessary coreVar_eq_refl axiom |
tree | commitdiff |
2011-03-13 |
Adam Megacz | Rename Extraction.fail to Extraction.Prelude_error |
tree | commitdiff |
2011-03-13 |
Adam Megacz | Eliminate the need for WeakVar decidable equality axiom |
tree | commitdiff |
2011-03-12 |
Adam Megacz | Make the HaskStrong type representation Kind-indexed... |
tree | commitdiff |
2011-03-07 |
Adam Megacz | make latex output use the preview package to set the... |
tree | commitdiff |
2011-03-07 |
Adam Megacz | add HaskProofToStrong skeleton implementation |
tree | commitdiff |
2011-03-07 |
Adam Megacz | add HaskStrongToWeak |
tree | commitdiff |
2011-03-07 |
Adam Megacz | add HaskStrongToProof |
tree | commitdiff |
2011-03-07 |
Adam Megacz | add HaskWeakToStrong |
tree | commitdiff |
2011-03-07 |
Adam Megacz | give HaskWeak its own type representation, fix numerous... |
tree | commitdiff |
2011-03-07 |
Adam Megacz | better names for the auxiliary CaseBranch records |
tree | commitdiff |
2011-03-07 |
Adam Megacz | separate type/coer/expr variables in HaskWeak case... |
tree | commitdiff |
2011-03-07 |
Adam Megacz | store variables in ELetRecBindings rather than its... |
tree | commitdiff |
2011-03-07 |
Adam Megacz | add HaskWeakToCore |
tree | commitdiff |
2011-03-07 |
Adam Megacz | add proper proofs of the fact that every rule has exact... |
tree | commitdiff |
2011-03-07 |
Adam Megacz | Changed WEBrak/WEEsc to store a CoreType |
tree | commitdiff |
2011-03-07 |
Adam Megacz | Added WeakVar, a separate variable representation for... |
tree | commitdiff |
2011-03-07 |
Adam Megacz | added HaskCoreToWeak |
tree | commitdiff |
2011-03-07 |
Adam Megacz | cleaned up lots of FIXMEs in ProofToLatex |
tree | commitdiff |
2011-03-02 |
Adam Megacz | Initial checkin of Coq-in-GHC code |
tree | commitdiff |
|