coq-hetmet.git
9 years agomake StrongAlt a parameter rather than field in StrongCaseBranch and ProofCaseBranch
Adam Megacz [Mon, 21 Mar 2011 00:30:30 +0000 (17:30 -0700)]
make StrongAlt a parameter rather than field in StrongCaseBranch and ProofCaseBranch

9 years agoremove vec2list_injective
Adam Megacz [Sun, 20 Mar 2011 10:13:36 +0000 (03:13 -0700)]
remove vec2list_injective

9 years agoget rid of a bunch of admits in HaskStrongToProof
Adam Megacz [Sun, 20 Mar 2011 09:44:20 +0000 (02:44 -0700)]
get rid of a bunch of admits in HaskStrongToProof

9 years agorequire all branches of LetRec be at the same level in HaskProof
Adam Megacz [Sun, 20 Mar 2011 06:10:41 +0000 (23:10 -0700)]
require all branches of LetRec be at the same level in HaskProof

9 years agoadd mapOptionTree_extensional, leaves_unleaves, mapleaves
Adam Megacz [Sun, 20 Mar 2011 06:05:31 +0000 (23:05 -0700)]
add mapOptionTree_extensional, leaves_unleaves, mapleaves

9 years agoadd distinct_decidable, in_decidable to General.v
Adam Megacz [Sun, 20 Mar 2011 06:05:18 +0000 (23:05 -0700)]
add distinct_decidable, in_decidable to General.v

9 years agocheckpoint
Adam Megacz [Sat, 19 Mar 2011 23:23:03 +0000 (16:23 -0700)]
checkpoint

9 years agoimprove HaskProofToStrong, although its messier now
Adam Megacz [Sat, 19 Mar 2011 21:15:34 +0000 (14:15 -0700)]
improve HaskProofToStrong, although its messier now

9 years agoadd tracing support to Extraction-prefix.hs
Adam Megacz [Sat, 19 Mar 2011 21:15:19 +0000 (14:15 -0700)]
add tracing support to Extraction-prefix.hs

9 years agoadd mapleaves to General.v
Adam Megacz [Sat, 19 Mar 2011 21:15:18 +0000 (14:15 -0700)]
add mapleaves to General.v

9 years agochange LetRec rule to allow only a single expression in the body
Adam Megacz [Sat, 19 Mar 2011 21:15:17 +0000 (14:15 -0700)]
change LetRec rule to allow only a single expression in the body

9 years agoadd ToString instance for HaskStrong
Adam Megacz [Sat, 19 Mar 2011 21:15:15 +0000 (14:15 -0700)]
add ToString instance for HaskStrong

9 years agoadd closedNDtoNormalND to NaturalDeduction
Adam Megacz [Sat, 19 Mar 2011 21:15:14 +0000 (14:15 -0700)]
add closedNDtoNormalND to NaturalDeduction

9 years agoadd UniqMonad
Adam Megacz [Sat, 19 Mar 2011 21:15:12 +0000 (14:15 -0700)]
add UniqMonad

9 years agoadd itmap and itree_to_tree
Adam Megacz [Sat, 19 Mar 2011 21:15:11 +0000 (14:15 -0700)]
add itmap and itree_to_tree

9 years agoadd treeToString method to General
Adam Megacz [Sat, 19 Mar 2011 21:15:09 +0000 (14:15 -0700)]
add treeToString method to General

9 years agomove Prelude_error to General.v
Adam Megacz [Sat, 19 Mar 2011 21:15:05 +0000 (14:15 -0700)]
move Prelude_error to General.v

9 years agoexpand tutorial.hs, include justification for scoping changes
Adam Megacz [Wed, 16 Mar 2011 09:45:03 +0000 (02:45 -0700)]
expand tutorial.hs, include justification for scoping changes

9 years agocheck for Case that uses its binder, which we do not support
Adam Megacz [Wed, 16 Mar 2011 09:27:52 +0000 (02:27 -0700)]
check for Case that uses its binder, which we do not support

9 years agoMakefile fixes: ignore emacs droppings
Adam Megacz [Wed, 16 Mar 2011 08:55:22 +0000 (01:55 -0700)]
Makefile fixes: ignore emacs droppings

9 years agofix broken sortAlts implementation
Adam Megacz [Wed, 16 Mar 2011 08:55:07 +0000 (01:55 -0700)]
fix broken sortAlts implementation

9 years agomajor overhaul of WeakToStrong/StrongToWeak; it can now handle the whole tutorial
Adam Megacz [Wed, 16 Mar 2011 08:54:16 +0000 (01:54 -0700)]
major overhaul of WeakToStrong/StrongToWeak; it can now handle the whole tutorial

9 years agobetter variable names in HaskWeakToCore
Adam Megacz [Wed, 16 Mar 2011 08:53:36 +0000 (01:53 -0700)]
better variable names in HaskWeakToCore

9 years agorestrict RNote to one hypothesis, major additions to ProofToStrong
Adam Megacz [Wed, 16 Mar 2011 08:53:16 +0000 (01:53 -0700)]
restrict RNote to one hypothesis, major additions to ProofToStrong

9 years agoadd EGlobal/RGlobal for CoreVars whose binder we cannot see
Adam Megacz [Wed, 16 Mar 2011 08:52:39 +0000 (01:52 -0700)]
add EGlobal/RGlobal for CoreVars whose binder we cannot see

9 years agoadd crude Monad type class
Adam Megacz [Wed, 16 Mar 2011 08:50:06 +0000 (01:50 -0700)]
add crude Monad type class

9 years agofinal batch of fixups before enabling -fcoqpass
Adam Megacz [Tue, 15 Mar 2011 02:09:24 +0000 (19:09 -0700)]
final batch of fixups before enabling -fcoqpass

9 years agofix spellings in Extraction-prefix.hs, minor tweaks
Adam Megacz [Tue, 15 Mar 2011 02:02:30 +0000 (19:02 -0700)]
fix spellings in Extraction-prefix.hs, minor tweaks

9 years agoformatting
Adam Megacz [Tue, 15 Mar 2011 01:50:20 +0000 (18:50 -0700)]
formatting

9 years agochange names of Kind constructors to be more informative
Adam Megacz [Tue, 15 Mar 2011 01:27:32 +0000 (18:27 -0700)]
change names of Kind constructors to be more informative

9 years agoreshuffle definitions in an attempt to iron out inter-file dependenceies
Adam Megacz [Tue, 15 Mar 2011 00:40:24 +0000 (17:40 -0700)]
reshuffle definitions in an attempt to iron out inter-file dependenceies

9 years agoadd support for CSP in HaskCore+HaskWeak
Adam Megacz [Mon, 14 Mar 2011 23:56:06 +0000 (16:56 -0700)]
add support for CSP in HaskCore+HaskWeak

9 years agoremove dead code from HaskWeak
Adam Megacz [Mon, 14 Mar 2011 23:52:55 +0000 (16:52 -0700)]
remove dead code from HaskWeak

9 years agoeliminate ext_tree_{left,right} keywords
Adam Megacz [Mon, 14 Mar 2011 23:50:27 +0000 (16:50 -0700)]
eliminate ext_tree_{left,right} keywords

9 years agomore formatting fixes
Adam Megacz [Mon, 14 Mar 2011 23:46:56 +0000 (16:46 -0700)]
more formatting fixes

9 years agoformatting fixes
Adam Megacz [Mon, 14 Mar 2011 23:41:08 +0000 (16:41 -0700)]
formatting fixes

9 years agominor cleanups, deleted dead code, eliminated use of (==) on CoreType
Adam Megacz [Mon, 14 Mar 2011 23:37:12 +0000 (16:37 -0700)]
minor cleanups, deleted dead code, eliminated use of (==) on CoreType

9 years agofix sortAlts so it actually does something
Adam Megacz [Mon, 14 Mar 2011 23:36:40 +0000 (16:36 -0700)]
fix sortAlts so it actually does something

9 years agoadd tutorial.coqpass to gitignore
Adam Megacz [Mon, 14 Mar 2011 23:24:11 +0000 (16:24 -0700)]
add tutorial.coqpass to gitignore

9 years agoadd tutorial to the repository
Adam Megacz [Mon, 14 Mar 2011 22:15:12 +0000 (15:15 -0700)]
add tutorial to the repository

9 years agorename weakTypeToType'' to weakTypeToTypeOfKind
Adam Megacz [Mon, 14 Mar 2011 22:11:43 +0000 (15:11 -0700)]
rename weakTypeToType'' to weakTypeToTypeOfKind

9 years agorevise tyFunKind to use splitKind
Adam Megacz [Mon, 14 Mar 2011 22:10:33 +0000 (15:10 -0700)]
revise tyFunKind to use splitKind

9 years agoadd splitKind to HaskKind
Adam Megacz [Mon, 14 Mar 2011 22:10:13 +0000 (15:10 -0700)]
add splitKind to HaskKind

9 years agofix ToString instance for Kind
Adam Megacz [Mon, 14 Mar 2011 22:10:01 +0000 (15:10 -0700)]
fix ToString instance for Kind

9 years agominor cleanups in HaskStrongToWeak
Adam Megacz [Mon, 14 Mar 2011 11:43:49 +0000 (04:43 -0700)]
minor cleanups in HaskStrongToWeak

9 years agoinclude URL for trfrac.sty and mathpartir in LaTeX output
Adam Megacz [Mon, 14 Mar 2011 11:07:12 +0000 (04:07 -0700)]
include URL for trfrac.sty and mathpartir in LaTeX output

9 years agofirst pass at proper handling of coercions in HaskWeak
Adam Megacz [Mon, 14 Mar 2011 10:22:31 +0000 (03:22 -0700)]
first pass at proper handling of coercions in HaskWeak

9 years agobetter error reporting in HaskWeakToStrong
Adam Megacz [Mon, 14 Mar 2011 10:20:17 +0000 (03:20 -0700)]
better error reporting in HaskWeakToStrong

9 years agobetter error reporting in Extraction.v
Adam Megacz [Mon, 14 Mar 2011 10:16:48 +0000 (03:16 -0700)]
better error reporting in Extraction.v

9 years agoclose numerous holes in HaskStrongToProof
Adam Megacz [Mon, 14 Mar 2011 10:11:48 +0000 (03:11 -0700)]
close numerous holes in HaskStrongToProof

9 years agomajor revision of HaskWeakToStrong, put phi/psi on the error monad
Adam Megacz [Mon, 14 Mar 2011 10:10:04 +0000 (03:10 -0700)]
major revision of HaskWeakToStrong, put phi/psi on the error monad

9 years agofix spelling error in HaskWeakToCore
Adam Megacz [Mon, 14 Mar 2011 09:58:09 +0000 (02:58 -0700)]
fix spelling error in HaskWeakToCore

9 years agoremove weakTypeOfWeakExpr and replaceWeakTypeVar, no longer required
Adam Megacz [Mon, 14 Mar 2011 09:54:02 +0000 (02:54 -0700)]
remove weakTypeOfWeakExpr and replaceWeakTypeVar, no longer required

9 years agostore the scrutinee CoreVar in WeakExpr Case to simplify WeakExprToCoreExpr
Adam Megacz [Mon, 14 Mar 2011 09:44:09 +0000 (02:44 -0700)]
store the scrutinee CoreVar in WeakExpr Case to simplify WeakExprToCoreExpr

9 years agostore the magic CoreVar for hetmet brak/esc in WeakExpr Esc/Brak
Adam Megacz [Mon, 14 Mar 2011 09:25:55 +0000 (02:25 -0700)]
store the magic CoreVar for hetmet brak/esc in WeakExpr Esc/Brak

9 years agodetect (->) TyCon and substitute FunTy in WeakToCore
Adam Megacz [Mon, 14 Mar 2011 09:08:26 +0000 (02:08 -0700)]
detect (->) TyCon and substitute FunTy in WeakToCore

9 years agofix bugs in LaTeX output
Adam Megacz [Mon, 14 Mar 2011 08:51:16 +0000 (01:51 -0700)]
fix bugs in LaTeX output

9 years agoToString instance for HaskCore
Adam Megacz [Mon, 14 Mar 2011 08:46:43 +0000 (01:46 -0700)]
ToString instance for HaskCore

9 years agoGeneral.addErrorMessage, orErrorBindWithMessage
Adam Megacz [Mon, 14 Mar 2011 08:46:18 +0000 (01:46 -0700)]
General.addErrorMessage, orErrorBindWithMessage

9 years agomove eol:string to General.v
Adam Megacz [Mon, 14 Mar 2011 08:45:36 +0000 (01:45 -0700)]
move eol:string to General.v

9 years agorestore HaskWeakToStrong functionality that I broke over the weekend
Adam Megacz [Sun, 13 Mar 2011 05:54:20 +0000 (21:54 -0800)]
restore HaskWeakToStrong functionality that I broke over the weekend

9 years agoRemove unnecessary coreVar_eq_refl axiom
Adam Megacz [Sun, 13 Mar 2011 00:33:14 +0000 (16:33 -0800)]
Remove unnecessary coreVar_eq_refl axiom

9 years agoRename Extraction.fail to Extraction.Prelude_error
Adam Megacz [Sun, 13 Mar 2011 00:31:37 +0000 (16:31 -0800)]
Rename Extraction.fail to Extraction.Prelude_error

9 years agoEliminate the need for WeakVar decidable equality axiom
Adam Megacz [Sun, 13 Mar 2011 00:30:33 +0000 (16:30 -0800)]
Eliminate the need for WeakVar decidable equality axiom

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

9 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.

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

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

9 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

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

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

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

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

9 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

9 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

9 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

9 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

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

9 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

9 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

9 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

9 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

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

9 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

9 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