coq-hetmet.git
8 years agoadd "sanity" target to Makefile
Adam Megacz [Mon, 30 May 2011 01:44:52 +0000 (18:44 -0700)]
add "sanity" target to Makefile

8 years agoadd -fflatten and -funsafe-skolemize flags
Adam Megacz [Mon, 30 May 2011 00:01:32 +0000 (17:01 -0700)]
add -fflatten and -funsafe-skolemize flags

8 years agoadd RCut, RLeft, RRight rules
Adam Megacz [Sun, 29 May 2011 22:48:51 +0000 (15:48 -0700)]
add RCut, RLeft, RRight rules

8 years agorename constructors of Arrange to start with A instead of R
Adam Megacz [Sat, 28 May 2011 20:54:31 +0000 (13:54 -0700)]
rename constructors of Arrange to start with A instead of R

8 years agomove more arrange routines into NaturalDeductionContext
Adam Megacz [Sat, 28 May 2011 04:39:45 +0000 (21:39 -0700)]
move more arrange routines into NaturalDeductionContext

8 years agomove Arrange into NaturalDeductionContext
Adam Megacz [Sat, 28 May 2011 03:43:15 +0000 (20:43 -0700)]
move Arrange into NaturalDeductionContext

8 years agomigrate HaskStrong away from using LeveledHaskType
Adam Megacz [Sat, 28 May 2011 02:50:34 +0000 (19:50 -0700)]
migrate HaskStrong away from using LeveledHaskType

8 years agoHaskProof: make the succedent level part of the judgment
Adam Megacz [Fri, 27 May 2011 21:30:24 +0000 (14:30 -0700)]
HaskProof: make the succedent level part of the judgment

8 years agoupdate Demo.hs
Adam Megacz [Fri, 27 May 2011 05:47:16 +0000 (22:47 -0700)]
update Demo.hs

8 years agoadd commented-out/incomplete implementation of simplifyWeakExpr
Adam Megacz [Fri, 27 May 2011 05:47:08 +0000 (22:47 -0700)]
add commented-out/incomplete implementation of simplifyWeakExpr

8 years agoGeneral.v: add boolean and/or functions
Adam Megacz [Fri, 27 May 2011 05:46:43 +0000 (22:46 -0700)]
General.v: add boolean and/or functions

8 years agorename variables to avoid Coq pickiness during extraction
Adam Megacz [Fri, 27 May 2011 02:39:58 +0000 (19:39 -0700)]
rename variables to avoid Coq pickiness during extraction

8 years agopartial support for LetRec in flattener
Adam Megacz [Fri, 27 May 2011 02:39:42 +0000 (19:39 -0700)]
partial support for LetRec in flattener

8 years agofix types of GAS_loop{l,r}
Adam Megacz [Thu, 26 May 2011 22:26:54 +0000 (15:26 -0700)]
fix types of GAS_loop{l,r}

8 years agoadd new Where rule, eliminate unnecessary ga_swaps in the Skolemizer
Adam Megacz [Thu, 26 May 2011 03:55:29 +0000 (20:55 -0700)]
add new Where rule, eliminate unnecessary ga_swaps in the Skolemizer

8 years agonote to self in HaskWeak
Adam Megacz [Thu, 26 May 2011 03:52:54 +0000 (20:52 -0700)]
note to self in HaskWeak

8 years agoNaturalDeduction: add nd_exch
Adam Megacz [Mon, 23 May 2011 06:55:56 +0000 (23:55 -0700)]
NaturalDeduction: add nd_exch

8 years agoHaskFlattener: support escapifying multi-leaf contexts
Adam Megacz [Mon, 16 May 2011 07:44:50 +0000 (00:44 -0700)]
HaskFlattener: support escapifying multi-leaf contexts

8 years agocomplete rewrite of GArrowTikZ, update examples
Adam Megacz [Mon, 16 May 2011 07:44:32 +0000 (00:44 -0700)]
complete rewrite of GArrowTikZ, update examples

8 years agoGArrowSkeleton: add some more optimization cases
Adam Megacz [Mon, 16 May 2011 07:44:05 +0000 (00:44 -0700)]
GArrowSkeleton: add some more optimization cases

8 years agoGArrowPortShape: add detectShape
Adam Megacz [Mon, 16 May 2011 07:43:48 +0000 (00:43 -0700)]
GArrowPortShape: add detectShape

8 years agoUnify.hs: commenting fix
Adam Megacz [Mon, 16 May 2011 07:43:22 +0000 (00:43 -0700)]
Unify.hs: commenting fix

8 years agoadd begin/end{preview} to tex output
Adam Megacz [Sun, 15 May 2011 21:31:23 +0000 (14:31 -0700)]
add begin/end{preview} to tex output

8 years agoGArrowTikZ: improve pdf page cropping
Adam Megacz [Sun, 15 May 2011 19:13:35 +0000 (12:13 -0700)]
GArrowTikZ: improve pdf page cropping

8 years agoupdate demo for new more-efficient encoding of functions
Adam Megacz [Sun, 15 May 2011 08:28:17 +0000 (01:28 -0700)]
update demo for new more-efficient encoding of functions

8 years agomore efficient encoding of function types
Adam Megacz [Sun, 15 May 2011 07:55:34 +0000 (00:55 -0700)]
more efficient encoding of function types

8 years agoadd an identity production for Arrange
Adam Megacz [Sun, 15 May 2011 07:55:19 +0000 (00:55 -0700)]
add an identity production for Arrange

8 years agoupdate demo
Adam Megacz [Sun, 15 May 2011 07:00:10 +0000 (00:00 -0700)]
update demo

8 years agoadd GArrowPortShape
Adam Megacz [Sun, 15 May 2011 06:59:59 +0000 (23:59 -0700)]
add GArrowPortShape

8 years agoadd GArrowSkeleton
Adam Megacz [Sun, 15 May 2011 06:59:51 +0000 (23:59 -0700)]
add GArrowSkeleton

8 years agofix bug in flattener, make extensionality axiom explicit
Adam Megacz [Sun, 15 May 2011 06:53:57 +0000 (23:53 -0700)]
fix bug in flattener, make extensionality axiom explicit

8 years agoupdate examples
Adam Megacz [Sat, 14 May 2011 03:33:10 +0000 (20:33 -0700)]
update examples

8 years agointegrate skolemization pass with flattening
Adam Megacz [Sat, 14 May 2011 03:33:00 +0000 (20:33 -0700)]
integrate skolemization pass with flattening

8 years agoimprove detection of type function kinds, mainly their saturation needs
Adam Megacz [Sat, 14 May 2011 03:31:50 +0000 (20:31 -0700)]
improve detection of type function kinds, mainly their saturation needs

8 years agoadd split_list to General.v
Adam Megacz [Sat, 14 May 2011 03:30:01 +0000 (20:30 -0700)]
add split_list to General.v

8 years agoadd ToString instance for lists
Adam Megacz [Sat, 14 May 2011 03:28:54 +0000 (20:28 -0700)]
add ToString instance for lists

8 years agofirst draft of skolemization pass
Adam Megacz [Fri, 13 May 2011 07:36:09 +0000 (00:36 -0700)]
first draft of skolemization pass

8 years agoadd EqDecidable instances for option and Tree
Adam Megacz [Fri, 13 May 2011 07:35:52 +0000 (00:35 -0700)]
add EqDecidable instances for option and Tree

8 years agoswap order of hypotheses in RApp to match RLet
Adam Megacz [Thu, 12 May 2011 22:28:14 +0000 (15:28 -0700)]
swap order of hypotheses in RApp to match RLet

8 years agorewrite {take,drop}_arg_types to avoid use of equality proofs
Adam Megacz [Thu, 12 May 2011 05:04:51 +0000 (22:04 -0700)]
rewrite {take,drop}_arg_types to avoid use of equality proofs

8 years agoHaskFlattener: represent first-order abstraction using GArrows
Adam Megacz [Thu, 12 May 2011 02:32:34 +0000 (19:32 -0700)]
HaskFlattener: represent first-order abstraction using GArrows

8 years agoHaskFlattener: use ga_mk_raw
Adam Megacz [Thu, 12 May 2011 02:28:45 +0000 (19:28 -0700)]
HaskFlattener: use ga_mk_raw

8 years agoupdate PCF.v for new ECKind
Adam Megacz [Thu, 12 May 2011 02:15:58 +0000 (19:15 -0700)]
update PCF.v for new ECKind

8 years agoHaskFlattener: simplify the flattener
Adam Megacz [Thu, 12 May 2011 01:55:34 +0000 (18:55 -0700)]
HaskFlattener: simplify the flattener

8 years agoHaskStrongTypes: add {take,drop}_arg_types
Adam Megacz [Thu, 12 May 2011 01:55:13 +0000 (18:55 -0700)]
HaskStrongTypes: add {take,drop}_arg_types

8 years agoHaskFLattener: formatting fixes and refactoring
Adam Megacz [Wed, 11 May 2011 23:08:41 +0000 (16:08 -0700)]
HaskFLattener: formatting fixes and refactoring

8 years agostart using type-family-based GArrow classes
Adam Megacz [Tue, 10 May 2011 04:57:53 +0000 (21:57 -0700)]
start using type-family-based GArrow classes

8 years agohave Makefile check for coq 8.3pl2-tracer
Adam Megacz [Tue, 10 May 2011 02:57:08 +0000 (19:57 -0700)]
have Makefile check for coq 8.3pl2-tracer

8 years agoadd examples/.build to gitignore
Adam Megacz [Tue, 10 May 2011 02:56:44 +0000 (19:56 -0700)]
add examples/.build to gitignore

8 years agoadd support for flattening non-recursive Let bindings
Adam Megacz [Tue, 10 May 2011 00:38:37 +0000 (17:38 -0700)]
add support for flattening non-recursive Let bindings

8 years agomove general-purpose routines from HaskFlattener to HaskProof/General
Adam Megacz [Mon, 9 May 2011 23:38:49 +0000 (16:38 -0700)]
move general-purpose routines from HaskFlattener to HaskProof/General

8 years agosplit HaskLiteralsAndTyCons into two files
Adam Megacz [Mon, 9 May 2011 23:26:46 +0000 (16:26 -0700)]
split HaskLiteralsAndTyCons into two files

8 years agoadd support for hetmet_unflatten
Adam Megacz [Mon, 9 May 2011 21:10:56 +0000 (14:10 -0700)]
add support for hetmet_unflatten

8 years agoadd Demo.hs
Adam Megacz [Mon, 9 May 2011 21:10:38 +0000 (14:10 -0700)]
add Demo.hs

8 years agomake GArrowTikZ into a module rather than a standalone program
Adam Megacz [Mon, 9 May 2011 21:10:29 +0000 (14:10 -0700)]
make GArrowTikZ into a module rather than a standalone program

8 years agoadd support for hetmet_flatten casting variable
Adam Megacz [Mon, 9 May 2011 08:18:46 +0000 (01:18 -0700)]
add support for hetmet_flatten casting variable

8 years agoallow -fcoqpass to change the type of top-level bindings
Adam Megacz [Mon, 9 May 2011 06:29:31 +0000 (23:29 -0700)]
allow -fcoqpass to change the type of top-level bindings

8 years agouse the "debug" version of Outputable for ToString in Coq code
Adam Megacz [Mon, 9 May 2011 06:28:57 +0000 (23:28 -0700)]
use the "debug" version of Outputable for ToString in Coq code

8 years agochange ECKind to *=>*=>*
Adam Megacz [Mon, 9 May 2011 04:36:07 +0000 (21:36 -0700)]
change ECKind to *=>*=>*

8 years agoabstract out the kind of environment classifiers (ECKind)
Adam Megacz [Mon, 9 May 2011 04:35:56 +0000 (21:35 -0700)]
abstract out the kind of environment classifiers (ECKind)

8 years agomajor improvements to flattener; almost finished now
Adam Megacz [Mon, 9 May 2011 04:21:59 +0000 (21:21 -0700)]
major improvements to flattener; almost finished now

8 years agoallow rank-1 polymorphic types for globals
Adam Megacz [Mon, 9 May 2011 04:21:45 +0000 (21:21 -0700)]
allow rank-1 polymorphic types for globals

8 years agoadd PairTyCon and UnitTyCon
Adam Megacz [Mon, 9 May 2011 04:21:15 +0000 (21:21 -0700)]
add PairTyCon and UnitTyCon

8 years agominor cleanups to Extraction-prefix.hs to eliminate warnings
Adam Megacz [Mon, 9 May 2011 04:20:06 +0000 (21:20 -0700)]
minor cleanups to Extraction-prefix.hs to eliminate warnings

8 years agofurther improvements to flattener
Adam Megacz [Thu, 5 May 2011 05:08:20 +0000 (22:08 -0700)]
further improvements to flattener

8 years agoseparate HaskProofStratified into PCF.v, HaskProgrammingLanguage.v, and HaskFlattener...
Adam Megacz [Tue, 3 May 2011 07:01:21 +0000 (00:01 -0700)]
separate HaskProofStratified into PCF.v, HaskProgrammingLanguage.v, and HaskFlattener.v, major improvements to flattening algorithm

8 years agoreorganize HaskProof files
Adam Megacz [Sat, 30 Apr 2011 23:26:17 +0000 (16:26 -0700)]
reorganize HaskProof files

8 years agoclean up hints for NaturalDeduction, split ProgrammingLanguage into multiple files
Adam Megacz [Sat, 30 Apr 2011 04:47:25 +0000 (21:47 -0700)]
clean up hints for NaturalDeduction, split ProgrammingLanguage into multiple files

8 years agoremove many [[admit]]s from HaskProofFlattener.v
Adam Megacz [Fri, 29 Apr 2011 22:09:11 +0000 (15:09 -0700)]
remove many [[admit]]s from HaskProofFlattener.v

8 years agoMerge branch 'master' of http://git.megacz.com/coq-hetmet
Adam Megacz [Wed, 27 Apr 2011 01:26:49 +0000 (18:26 -0700)]
Merge branch 'master' of git.megacz.com/coq-hetmet

8 years agoprove all [admit]ted lemmas in HaskStrongToProof (not necessarily elegantly!)
Adam Megacz [Wed, 27 Apr 2011 01:26:42 +0000 (18:26 -0700)]
prove all [admit]ted lemmas in HaskStrongToProof (not necessarily elegantly!)

8 years agoadd Makefile target for tikz demo
Adam Megacz [Tue, 26 Apr 2011 23:30:27 +0000 (16:30 -0700)]
add Makefile target for tikz demo

8 years agoadd examples/Makefile
Adam Megacz [Tue, 26 Apr 2011 17:54:37 +0000 (10:54 -0700)]
add examples/Makefile

8 years agoadd -fno-warn-unused-{binds,patterns} to Coq extraction
Adam Megacz [Mon, 25 Apr 2011 06:45:15 +0000 (23:45 -0700)]
add -fno-warn-unused-{binds,patterns} to Coq extraction

8 years agoupdate GArrowTikZ.hs; still not finished, though
Adam Megacz [Mon, 25 Apr 2011 05:54:13 +0000 (22:54 -0700)]
update GArrowTikZ.hs; still not finished, though

8 years agoremove ClosedSIND (use "SIND []" instead)
Adam Megacz [Mon, 25 Apr 2011 05:52:09 +0000 (22:52 -0700)]
remove ClosedSIND (use "SIND []" instead)

8 years agoremove all admits from ProgrammingLanguage.v
Adam Megacz [Sun, 24 Apr 2011 09:03:40 +0000 (02:03 -0700)]
remove all admits from ProgrammingLanguage.v

8 years agoNaturalDeduction: add nd_swap, nd_prod_split, and some tactics
Adam Megacz [Sun, 24 Apr 2011 07:04:13 +0000 (00:04 -0700)]
NaturalDeduction: add nd_swap, nd_prod_split, and some tactics

8 years agoadd examples targets to Makefile
Adam Megacz [Sun, 24 Apr 2011 07:03:22 +0000 (00:03 -0700)]
add examples targets to Makefile

8 years agoadd Unify.hs to examples
Adam Megacz [Sun, 24 Apr 2011 02:39:52 +0000 (19:39 -0700)]
add Unify.hs to examples

8 years agospeed up builds by removing some dependencies from ExtractionMain
Adam Megacz [Mon, 18 Apr 2011 23:59:00 +0000 (16:59 -0700)]
speed up builds by removing some dependencies from ExtractionMain

8 years agofix erroneous conclusion to penultimate lemma
Adam Megacz [Sat, 16 Apr 2011 22:14:58 +0000 (15:14 -0700)]
fix erroneous conclusion to penultimate lemma

8 years agouse the $(MAKE) variable so -j2 works
Adam Megacz [Mon, 11 Apr 2011 21:46:23 +0000 (14:46 -0700)]
use the $(MAKE) variable so -j2 works

8 years agoMerge branches 'master' and 'master' of http://git.megacz.com/coq-hetmet
Adam Megacz [Mon, 11 Apr 2011 21:45:49 +0000 (14:45 -0700)]
Merge branches 'master' and 'master' of git.megacz.com/coq-hetmet

8 years agounbreak lots more stuff
Adam Megacz [Mon, 11 Apr 2011 07:24:23 +0000 (07:24 +0000)]
unbreak lots more stuff

8 years agouncomment some code in ProgrammingLanguage.v
Adam Megacz [Mon, 11 Apr 2011 00:09:26 +0000 (00:09 +0000)]
uncomment some code in ProgrammingLanguage.v

8 years agoremove the very last admit (missing proof) from GeneralizedArrowFromReification
Adam Megacz [Sun, 10 Apr 2011 23:34:48 +0000 (23:34 +0000)]
remove the very last admit (missing proof) from GeneralizedArrowFromReification

8 years agoadd skeleton of GArrowTikZ
Adam Megacz [Sun, 10 Apr 2011 19:59:38 +0000 (19:59 +0000)]
add skeleton of GArrowTikZ

8 years agoseparate CoqPass.hs from All.v in Makefile
Adam Megacz [Sun, 10 Apr 2011 19:53:11 +0000 (19:53 +0000)]
separate CoqPass.hs from All.v in Makefile

8 years agofix bug in GeneralizedArrowFromReification
Adam Megacz [Sun, 10 Apr 2011 19:51:27 +0000 (19:51 +0000)]
fix bug in GeneralizedArrowFromReification

8 years agoAll.v: uncomment things
Adam Megacz [Sun, 10 Apr 2011 19:37:59 +0000 (19:37 +0000)]
All.v: uncomment things

8 years agobugfix in ReificationsIsomorphicToGeneralizedArrows
Adam Megacz [Sun, 10 Apr 2011 19:37:53 +0000 (19:37 +0000)]
bugfix in ReificationsIsomorphicToGeneralizedArrows

8 years agoadd commented-out definitions for analytic proofs and cut elimination
Adam Megacz [Sun, 10 Apr 2011 19:37:36 +0000 (19:37 +0000)]
add commented-out definitions for analytic proofs and cut elimination

8 years agofill in lots of missing proofs
Adam Megacz [Sun, 10 Apr 2011 11:22:43 +0000 (11:22 +0000)]
fill in lots of missing proofs

8 years agoupdate to new coq-categories, base ND_Relation on inert sequences
Adam Megacz [Sun, 10 Apr 2011 04:04:51 +0000 (04:04 +0000)]
update to new coq-categories, base ND_Relation on inert sequences

8 years agoremove notations from Preamble that come from coq-categories
Adam Megacz [Sat, 9 Apr 2011 08:54:24 +0000 (08:54 +0000)]
remove notations from Preamble that come from coq-categories

8 years agoupdate to account for coq-categories changes
Adam Megacz [Mon, 4 Apr 2011 02:53:27 +0000 (02:53 +0000)]
update to account for coq-categories changes

8 years agofix Makefile bug
Adam Megacz [Sat, 2 Apr 2011 22:53:42 +0000 (22:53 +0000)]
fix Makefile bug

8 years agoupdate submodule pointer, account for changes upstream
Adam Megacz [Sat, 2 Apr 2011 22:49:20 +0000 (15:49 -0700)]
update submodule pointer, account for changes upstream

8 years agoExtractionMain: better pdflatex code output
Adam Megacz [Sat, 2 Apr 2011 22:48:01 +0000 (15:48 -0700)]
ExtractionMain: better pdflatex code output