change import order in HaskCoreToWeak

add n-ary form of nd_weak

add ndr_void_proofs_irrelevant

move ModalBoxTyCon, ArrowTyCon to HaskLiteralsAndTyCons

add kindToLatex in HaskKinds

add ToLatex class, move machinery to General.v

add machinery to create merged Coq script GArrow.v

update categories submodule pointer

proofs that Types/Judgments form an enrichment

update tutorial for new GArrow classes

add distinctT, InT to General

add HaskXXXXCategory, generalized arrows, and reifications

add coq-categories as a submodule

comment out portions of the tutorial which do not yet work due to GHC.Prim.Any

Makefile update

make StrongAlt a parameter rather than field in StrongCaseBranch and ProofCaseBranch

remove vec2list_injective

get rid of a bunch of admits in HaskStrongToProof

require all branches of LetRec be at the same level in HaskProof

add mapOptionTree_extensional, leaves_unleaves, mapleaves

add distinct_decidable, in_decidable to General.v

checkpoint

improve HaskProofToStrong, although its messier now

add tracing support to Extraction-prefix.hs

add mapleaves to General.v

change LetRec rule to allow only a single expression in the body

add ToString instance for HaskStrong

add closedNDtoNormalND to NaturalDeduction

add UniqMonad

add itmap and itree_to_tree

add treeToString method to General

move Prelude_error to General.v

expand tutorial.hs, include justification for scoping changes

check for Case that uses its binder, which we do not support

Makefile fixes: ignore emacs droppings

fix broken sortAlts implementation

major overhaul of WeakToStrong/StrongToWeak; it can now handle the whole tutorial

better variable names in HaskWeakToCore

restrict RNote to one hypothesis, major additions to ProofToStrong

add EGlobal/RGlobal for CoreVars whose binder we cannot see

add crude Monad type class

final batch of fixups before enabling -fcoqpass

fix spellings in Extraction-prefix.hs, minor tweaks

formatting

change names of Kind constructors to be more informative

reshuffle definitions in an attempt to iron out inter-file dependenceies

add support for CSP in HaskCore+HaskWeak

remove dead code from HaskWeak

eliminate ext_tree_{left,right} keywords

more formatting fixes

formatting fixes

minor cleanups, deleted dead code, eliminated use of (==) on CoreType

fix sortAlts so it actually does something

add tutorial.coqpass to gitignore

add tutorial to the repository

rename weakTypeToType'' to weakTypeToTypeOfKind

revise tyFunKind to use splitKind

add splitKind to HaskKind

fix ToString instance for Kind

minor cleanups in HaskStrongToWeak

include URL for trfrac.sty and mathpartir in LaTeX output

first pass at proper handling of coercions in HaskWeak

better error reporting in HaskWeakToStrong

better error reporting in Extraction.v

close numerous holes in HaskStrongToProof

major revision of HaskWeakToStrong, put phi/psi on the error monad

fix spelling error in HaskWeakToCore

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

detect (->) TyCon and substitute FunTy in WeakToCore

fix bugs in LaTeX output

ToString instance for HaskCore

General.addErrorMessage, orErrorBindWithMessage

move eol:string to General.v

restore HaskWeakToStrong functionality that I broke over the weekend

Remove unnecessary coreVar_eq_refl axiom

Rename Extraction.fail to Extraction.Prelude_error

Eliminate the need for WeakVar decidable equality axiom

update push-url in Makefile

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.

more Makefile updates

Makefile updates

make latex output use the preview package to set the page size

add HaskProofToStrong skeleton implementation

add HaskStrongToWeak

add HaskStrongToProof

add HaskWeakToStrong

give HaskWeak its own type representation, fix numerous bugs

better names for the auxiliary CaseBranch records

separate type/coer/expr variables in HaskWeak case branches

store variables in ELetRecBindings rather than its indexing tree

add HaskWeakToCore

add proper proofs of the fact that every rule has exactly one conclusion

Changed WEBrak/WEEsc to store a CoreType

Added WeakVar, a separate variable representation for HaskWeak

added "publish" target to regenerate tex/pdf code

added HaskCoreToWeak

cleaned up lots of FIXMEs in ProofToLatex

Initial checkin of Coq-in-GHC code