partial implementation of KappaAbs/KappaApp in Coq code
rename constructors of Arrange to start with A instead of R
add commented-out/incomplete implementation of simplifyWeakExpr
note to self in HaskWeak
split HaskLiteralsAndTyCons into two files
reshuffle definitions in an attempt to iron out inter-file dependenceies
add support for CSP in HaskCore+HaskWeak
remove dead code from HaskWeak
remove weakTypeOfWeakExpr and replaceWeakTypeVar, no longer required
store the scrutinee CoreVar in WeakExpr Case to simplify WeakExprToCoreExpr
store the magic CoreVar for hetmet brak/esc in WeakExpr Esc/Brak
restore HaskWeakToStrong functionality that I broke over the weekend
Eliminate the need for WeakVar decidable equality axiom
Make the HaskStrong type representation Kind-indexed, and many supporting changes (see long comment). This patch makes a whole lot of interlocking changes, with the ultimate (accomplished) goal of changing the HaskStrong type representation ("HaskType") so that it is indexed by the Haskell Kind of the type. As a result, the auxiliary well-kindedness judgment \vdash_{ty} is no longer necessary. Other changes in this patch: - Added Coq ToString class (similar to Haskell's Show class) - Massive reduction in volume of code extracted for string literals - Decidable equality on HaskStrong's - Much more reliable HaskWeakToStrong, although it has regressed a bit in terms of number of cases handled; this will be remediated shortly.
give HaskWeak its own type representation, fix numerous bugs
separate type/coer/expr variables in HaskWeak case branches
Changed WEBrak/WEEsc to store a CoreType
Added WeakVar, a separate variable representation for HaskWeak
Initial checkin of Coq-in-GHC code