update baked in CoqPass.hs

Merge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet

NaturalDeductionContext: more permutation proofs

General: add ilist_ins

NaturalDeductionContext: add arrangePullback

HaskStrongTypes: add TBool and TInt for convenience

HaskTyCons: add Int and Bool

addErrorMessage: put blank lines between messages

allow quantification over any tyvar in the environment, not just the first

HaskFlattener: use pga_kappa a bit more, but not everywhere yet

General.v: add list_{ins,del,take,drop}

Add "atomic" component during optimization

GArrowTikZ: add ability to omit rendering of assoc/first/second

GArrowSkeleton: improve optimizations

update Demo.hs

add crude support for flattening with LetRec and Case at level zero

update for GHC.HetMet package renaming

update baked in CoqPass.hs

Merge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet

remove magic flatten/unflatten identifiers

use CoreM monad to acquire known-to-compiler identifiers

Makefile: use -f when doing git pull for baked-in branch

move to new normalization-based optimizer, add GArrowSkeleton.beautify

pull baked-in branch automatically if correct coq version not found

clean up demo code

GArrowTikZ: support ga_loopl

GArrowTikZ: draw input wires before first box, output wires after last

GArrowTikZ: render more of the structural stuff in gray!50

update baked in CoqPass.hs

merge

Unify.hs: propagate errors through the unifier

GArrowPortShape: add Show instance, use new Unify.hs

fix bugs in Unify.hs, store unifiers in fully-resolved form

very rudimentary support for feedback in GArrowTikZ

add support for flattening recursive-let

fix bugs in BiGArrow

update for new GHC coercion representation

remove RLet and RWhere

let RCut take a left environment as well

use -fsimpleopt-before-flatten in sanity checks

remove RJoin rule

better error reporting in coreTypeToWeakType; dont use Prelude_error

Makefile: use a for-loop to compile sanity checks

update baked in CoqPass.hs

Merge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet

fix bugs in BiGArrow

update for new GHC coercion representation

remove RLet and RWhere

let RCut take a left environment as well

use -fsimpleopt-before-flatten in sanity checks

remove RJoin rule

better error reporting in coreTypeToWeakType; dont use Prelude_error

Makefile: use a for-loop to compile sanity checks

update baked in CoqPass.hs

Merge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet

add "sanity" target to Makefile

add -fflatten and -funsafe-skolemize flags

add RCut, RLeft, RRight rules

rename constructors of Arrange to start with A instead of R

update baked in CoqPass.hs

Merge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet

move more arrange routines into NaturalDeductionContext

move Arrange into NaturalDeductionContext

migrate HaskStrong away from using LeveledHaskType

HaskProof: make the succedent level part of the judgment

update Demo.hs

add commented-out/incomplete implementation of simplifyWeakExpr

General.v: add boolean and/or functions

rename variables to avoid Coq pickiness during extraction

partial support for LetRec in flattener

fix types of GAS_loop{l,r}

update baked in CoqPass.hs

Merge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet

add new Where rule, eliminate unnecessary ga_swaps in the Skolemizer

note to self in HaskWeak

NaturalDeduction: add nd_exch

update baked in CoqPass.hs

Merge branch 'coq-extraction-baked-in' of /afs/megacz.com/.pub/software/coq-hetmet

HaskFlattener: support escapifying multi-leaf contexts

complete rewrite of GArrowTikZ, update examples

GArrowSkeleton: add some more optimization cases

GArrowPortShape: add detectShape

Unify.hs: commenting fix

add begin/end{preview} to tex output

GArrowTikZ: improve pdf page cropping

update demo for new more-efficient encoding of functions

more efficient encoding of function types

add an identity production for Arrange

update demo

add GArrowPortShape

add GArrowSkeleton

fix bug in flattener, make extensionality axiom explicit

update baked in CoqPass.hs

Merge branch 'coq-extraction-baked-in' of /afs/megacz.com/pub/software/coq-hetmet

update examples

integrate skolemization pass with flattening

improve detection of type function kinds, mainly their saturation needs

add split_list to General.v

add ToString instance for lists

first draft of skolemization pass