coq-hetmet.git
8 years agoupdate baked in CoqPass.hs coq-extraction-baked-in
gentzen [Tue, 30 Aug 2011 13:59:54 +0000 (06:59 -0700)]
update baked in CoqPass.hs

8 years agoMerge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet
Adam Megacz [Tue, 30 Aug 2011 13:59:54 +0000 (06:59 -0700)]
Merge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet

8 years agoNaturalDeductionContext: more permutation proofs
Adam Megacz [Mon, 29 Aug 2011 23:19:37 +0000 (16:19 -0700)]
NaturalDeductionContext: more permutation proofs

8 years agoGeneral: add ilist_ins
Adam Megacz [Mon, 11 Jul 2011 05:04:16 +0000 (22:04 -0700)]
General: add ilist_ins

8 years agoNaturalDeductionContext: add arrangePullback
Adam Megacz [Sun, 10 Jul 2011 01:24:08 +0000 (18:24 -0700)]
NaturalDeductionContext: add arrangePullback

8 years agoHaskStrongTypes: add TBool and TInt for convenience
Adam Megacz [Wed, 6 Jul 2011 01:39:02 +0000 (18:39 -0700)]
HaskStrongTypes: add TBool and TInt for convenience

8 years agoHaskTyCons: add Int and Bool
Adam Megacz [Mon, 4 Jul 2011 07:33:28 +0000 (00:33 -0700)]
HaskTyCons: add Int and Bool

8 years agoaddErrorMessage: put blank lines between messages
Adam Megacz [Mon, 4 Jul 2011 07:33:11 +0000 (00:33 -0700)]
addErrorMessage: put blank lines between messages

8 years agoallow quantification over any tyvar in the environment, not just the first
Adam Megacz [Fri, 24 Jun 2011 11:29:27 +0000 (04:29 -0700)]
allow quantification over any tyvar in the environment, not just the first

8 years agoHaskFlattener: use pga_kappa a bit more, but not everywhere yet
Adam Megacz [Fri, 24 Jun 2011 11:29:06 +0000 (04:29 -0700)]
HaskFlattener: use pga_kappa a bit more, but not everywhere yet

8 years agoGeneral.v: add list_{ins,del,take,drop}
Adam Megacz [Fri, 24 Jun 2011 11:24:47 +0000 (04:24 -0700)]
General.v: add list_{ins,del,take,drop}

8 years agoAdd "atomic" component during optimization
Adam Megacz [Wed, 22 Jun 2011 22:16:55 +0000 (15:16 -0700)]
Add "atomic" component during optimization

8 years agoGArrowTikZ: add ability to omit rendering of assoc/first/second
Adam Megacz [Tue, 21 Jun 2011 03:47:11 +0000 (20:47 -0700)]
GArrowTikZ: add ability to omit rendering of assoc/first/second

8 years agoGArrowSkeleton: improve optimizations
Adam Megacz [Tue, 21 Jun 2011 03:46:32 +0000 (20:46 -0700)]
GArrowSkeleton: improve optimizations

8 years agoupdate Demo.hs
Adam Megacz [Tue, 21 Jun 2011 03:02:38 +0000 (20:02 -0700)]
update Demo.hs

8 years agoadd crude support for flattening with LetRec and Case at level zero
Adam Megacz [Tue, 21 Jun 2011 03:02:25 +0000 (20:02 -0700)]
add crude support for flattening with LetRec and Case at level zero

8 years agoupdate for GHC.HetMet package renaming
Adam Megacz [Mon, 20 Jun 2011 02:07:07 +0000 (19:07 -0700)]
update for GHC.HetMet package renaming

8 years agoupdate baked in CoqPass.hs
gentzen [Sun, 19 Jun 2011 13:55:22 +0000 (06:55 -0700)]
update baked in CoqPass.hs

8 years agoMerge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet
Adam Megacz [Sun, 19 Jun 2011 13:55:22 +0000 (06:55 -0700)]
Merge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet

8 years agoremove magic flatten/unflatten identifiers
Adam Megacz [Sun, 19 Jun 2011 00:44:23 +0000 (17:44 -0700)]
remove magic flatten/unflatten identifiers

8 years agouse CoreM monad to acquire known-to-compiler identifiers
Adam Megacz [Sun, 19 Jun 2011 00:33:30 +0000 (17:33 -0700)]
use CoreM monad to acquire known-to-compiler identifiers

8 years agoMakefile: use -f when doing git pull for baked-in branch
Adam Megacz [Wed, 15 Jun 2011 19:32:23 +0000 (12:32 -0700)]
Makefile: use -f when doing git pull for baked-in branch

8 years agomove to new normalization-based optimizer, add GArrowSkeleton.beautify
Adam Megacz [Wed, 15 Jun 2011 07:01:22 +0000 (00:01 -0700)]
move to new normalization-based optimizer, add GArrowSkeleton.beautify

8 years agopull baked-in branch automatically if correct coq version not found
Adam Megacz [Wed, 15 Jun 2011 00:27:12 +0000 (17:27 -0700)]
pull baked-in branch automatically if correct coq version not found

8 years agoclean up demo code
Adam Megacz [Wed, 15 Jun 2011 00:14:06 +0000 (17:14 -0700)]
clean up demo code

8 years agoGArrowTikZ: support ga_loopl
Adam Megacz [Tue, 14 Jun 2011 03:53:33 +0000 (20:53 -0700)]
GArrowTikZ: support ga_loopl

8 years agoGArrowTikZ: draw input wires before first box, output wires after last
Adam Megacz [Tue, 14 Jun 2011 03:52:48 +0000 (20:52 -0700)]
GArrowTikZ: draw input wires before first box, output wires after last

8 years agoGArrowTikZ: render more of the structural stuff in gray!50
Adam Megacz [Tue, 14 Jun 2011 03:50:31 +0000 (20:50 -0700)]
GArrowTikZ: render more of the structural stuff in gray!50

8 years agoupdate baked in CoqPass.hs
gentzen [Mon, 6 Jun 2011 14:16:30 +0000 (07:16 -0700)]
update baked in CoqPass.hs

8 years agomerge
Adam Megacz [Sun, 5 Jun 2011 21:03:47 +0000 (14:03 -0700)]
merge

8 years agoUnify.hs: propagate errors through the unifier
Adam Megacz [Sat, 4 Jun 2011 01:22:02 +0000 (18:22 -0700)]
Unify.hs: propagate errors through the unifier

8 years agoGArrowPortShape: add Show instance, use new Unify.hs
Adam Megacz [Sat, 4 Jun 2011 01:16:52 +0000 (18:16 -0700)]
GArrowPortShape: add Show instance, use new Unify.hs

8 years agofix bugs in Unify.hs, store unifiers in fully-resolved form
Adam Megacz [Sat, 4 Jun 2011 01:16:48 +0000 (18:16 -0700)]
fix bugs in Unify.hs, store unifiers in fully-resolved form

8 years agovery rudimentary support for feedback in GArrowTikZ
Adam Megacz [Thu, 2 Jun 2011 02:15:25 +0000 (19:15 -0700)]
very rudimentary support for feedback in GArrowTikZ

8 years agoadd support for flattening recursive-let
Adam Megacz [Thu, 2 Jun 2011 02:02:59 +0000 (19:02 -0700)]
add support for flattening recursive-let

8 years agofix bugs in BiGArrow
Adam Megacz [Tue, 31 May 2011 05:57:45 +0000 (22:57 -0700)]
fix bugs in BiGArrow

8 years agoupdate for new GHC coercion representation
Adam Megacz [Tue, 31 May 2011 05:48:14 +0000 (22:48 -0700)]
update for new GHC coercion representation

8 years agoremove RLet and RWhere
Adam Megacz [Tue, 31 May 2011 01:58:37 +0000 (18:58 -0700)]
remove RLet and RWhere

8 years agolet RCut take a left environment as well
Adam Megacz [Tue, 31 May 2011 01:30:46 +0000 (18:30 -0700)]
let RCut take a left environment as well

8 years agouse -fsimpleopt-before-flatten in sanity checks
Adam Megacz [Tue, 31 May 2011 00:41:07 +0000 (17:41 -0700)]
use -fsimpleopt-before-flatten in sanity checks

8 years agoremove RJoin rule
Adam Megacz [Mon, 30 May 2011 23:22:42 +0000 (16:22 -0700)]
remove RJoin rule

8 years agobetter error reporting in coreTypeToWeakType; dont use Prelude_error
Adam Megacz [Mon, 30 May 2011 22:22:17 +0000 (15:22 -0700)]
better error reporting in coreTypeToWeakType; dont use Prelude_error

8 years agoMakefile: use a for-loop to compile sanity checks
Adam Megacz [Mon, 30 May 2011 22:21:49 +0000 (15:21 -0700)]
Makefile: use a for-loop to compile sanity checks

8 years agoupdate baked in CoqPass.hs
gentzen [Tue, 31 May 2011 14:14:25 +0000 (07:14 -0700)]
update baked in CoqPass.hs

8 years agoMerge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet
Adam Megacz [Tue, 31 May 2011 14:14:25 +0000 (07:14 -0700)]
Merge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet

8 years agofix bugs in BiGArrow
Adam Megacz [Tue, 31 May 2011 05:57:45 +0000 (22:57 -0700)]
fix bugs in BiGArrow

8 years agoupdate for new GHC coercion representation
Adam Megacz [Tue, 31 May 2011 05:48:14 +0000 (22:48 -0700)]
update for new GHC coercion representation

8 years agoremove RLet and RWhere
Adam Megacz [Tue, 31 May 2011 01:58:37 +0000 (18:58 -0700)]
remove RLet and RWhere

8 years agolet RCut take a left environment as well
Adam Megacz [Tue, 31 May 2011 01:30:46 +0000 (18:30 -0700)]
let RCut take a left environment as well

8 years agouse -fsimpleopt-before-flatten in sanity checks
Adam Megacz [Tue, 31 May 2011 00:41:07 +0000 (17:41 -0700)]
use -fsimpleopt-before-flatten in sanity checks

8 years agoremove RJoin rule
Adam Megacz [Mon, 30 May 2011 23:22:42 +0000 (16:22 -0700)]
remove RJoin rule

8 years agobetter error reporting in coreTypeToWeakType; dont use Prelude_error
Adam Megacz [Mon, 30 May 2011 22:22:17 +0000 (15:22 -0700)]
better error reporting in coreTypeToWeakType; dont use Prelude_error

8 years agoMakefile: use a for-loop to compile sanity checks
Adam Megacz [Mon, 30 May 2011 22:21:49 +0000 (15:21 -0700)]
Makefile: use a for-loop to compile sanity checks

8 years agoupdate baked in CoqPass.hs
gentzen [Mon, 30 May 2011 14:11:57 +0000 (07:11 -0700)]
update baked in CoqPass.hs

8 years agoMerge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet
Adam Megacz [Mon, 30 May 2011 14:11:57 +0000 (07:11 -0700)]
Merge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet

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 agoupdate baked in CoqPass.hs
gentzen [Sat, 28 May 2011 14:16:00 +0000 (07:16 -0700)]
update baked in CoqPass.hs

8 years agoMerge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet
Adam Megacz [Sat, 28 May 2011 14:15:59 +0000 (07:15 -0700)]
Merge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet

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 agoupdate baked in CoqPass.hs
gentzen [Thu, 26 May 2011 13:50:42 +0000 (06:50 -0700)]
update baked in CoqPass.hs

8 years agoMerge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet
Adam Megacz [Thu, 26 May 2011 13:50:42 +0000 (06:50 -0700)]
Merge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet

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 agoupdate baked in CoqPass.hs
gentzen [Mon, 16 May 2011 13:49:40 +0000 (06:49 -0700)]
update baked in CoqPass.hs

8 years agoMerge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet
Adam Megacz [Mon, 16 May 2011 13:49:39 +0000 (06:49 -0700)]
Merge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet

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 baked in CoqPass.hs
gentzen [Sun, 15 May 2011 06:38:45 +0000 (23:38 -0700)]
update baked in CoqPass.hs

8 years agoMerge branch 'coq-extraction-baked-in' of /afs/megacz.com/pub/software/coq-hetmet
Adam Megacz [Sun, 15 May 2011 06:36:47 +0000 (23:36 -0700)]
Merge branch 'coq-extraction-baked-in' of /afs/megacz.com/pub/software/coq-hetmet

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