coq-hetmet.git
8 years agoupdate push-url in Makefile
Adam Megacz [Sat, 12 Mar 2011 13:49:02 +0000 (05:49 -0800)]
update push-url in Makefile

8 years agoMake the HaskStrong type representation Kind-indexed, and many supporting changes...
Adam Megacz [Sat, 12 Mar 2011 12:44:18 +0000 (04:44 -0800)]
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.

8 years agomore Makefile updates
Adam Megacz [Mon, 7 Mar 2011 20:26:33 +0000 (12:26 -0800)]
more Makefile updates

8 years agoMakefile updates
Adam Megacz [Mon, 7 Mar 2011 20:21:30 +0000 (12:21 -0800)]
Makefile updates

8 years agomake latex output use the preview package to set the page size
Adam Megacz [Mon, 7 Mar 2011 13:42:04 +0000 (05:42 -0800)]
make latex output use the preview package to set the page size

8 years agoadd HaskProofToStrong skeleton implementation
Adam Megacz [Mon, 7 Mar 2011 13:41:56 +0000 (05:41 -0800)]
add HaskProofToStrong skeleton implementation

8 years agoadd HaskStrongToWeak
Adam Megacz [Mon, 7 Mar 2011 13:41:54 +0000 (05:41 -0800)]
add HaskStrongToWeak

8 years agoadd HaskStrongToProof
Adam Megacz [Mon, 7 Mar 2011 13:41:51 +0000 (05:41 -0800)]
add HaskStrongToProof

8 years agoadd HaskWeakToStrong
Adam Megacz [Mon, 7 Mar 2011 13:41:48 +0000 (05:41 -0800)]
add HaskWeakToStrong

8 years agogive HaskWeak its own type representation, fix numerous bugs
Adam Megacz [Mon, 7 Mar 2011 13:41:46 +0000 (05:41 -0800)]
give HaskWeak its own type representation, fix numerous bugs

8 years agobetter names for the auxiliary CaseBranch records
Adam Megacz [Mon, 7 Mar 2011 13:41:43 +0000 (05:41 -0800)]
better names for the auxiliary CaseBranch records

8 years agoseparate type/coer/expr variables in HaskWeak case branches
Adam Megacz [Mon, 7 Mar 2011 13:41:40 +0000 (05:41 -0800)]
separate type/coer/expr variables in HaskWeak case branches

8 years agostore variables in ELetRecBindings rather than its indexing tree
Adam Megacz [Mon, 7 Mar 2011 13:41:37 +0000 (05:41 -0800)]
store variables in ELetRecBindings rather than its indexing tree

8 years agoadd HaskWeakToCore
Adam Megacz [Mon, 7 Mar 2011 13:41:35 +0000 (05:41 -0800)]
add HaskWeakToCore

8 years agoadd proper proofs of the fact that every rule has exactly one conclusion
Adam Megacz [Mon, 7 Mar 2011 13:41:33 +0000 (05:41 -0800)]
add proper proofs of the fact that every rule has exactly one conclusion

8 years agoChanged WEBrak/WEEsc to store a CoreType
Adam Megacz [Mon, 7 Mar 2011 13:41:30 +0000 (05:41 -0800)]
Changed WEBrak/WEEsc to store a CoreType

8 years agoAdded WeakVar, a separate variable representation for HaskWeak
Adam Megacz [Mon, 7 Mar 2011 13:41:27 +0000 (05:41 -0800)]
Added WeakVar, a separate variable representation for HaskWeak

8 years agoadded "publish" target to regenerate tex/pdf code
Adam Megacz [Mon, 7 Mar 2011 13:41:24 +0000 (05:41 -0800)]
added "publish" target to regenerate tex/pdf code

8 years agoadded HaskCoreToWeak
Adam Megacz [Mon, 7 Mar 2011 13:41:17 +0000 (05:41 -0800)]
added HaskCoreToWeak

8 years agocleaned up lots of FIXMEs in ProofToLatex
Adam Megacz [Mon, 7 Mar 2011 13:40:58 +0000 (05:40 -0800)]
cleaned up lots of FIXMEs in ProofToLatex

8 years agoInitial checkin of Coq-in-GHC code
Adam Megacz [Wed, 2 Mar 2011 22:25:04 +0000 (14:25 -0800)]
Initial checkin of Coq-in-GHC code