compiler: fix case on Bool type

[skip bamboo]

compiler: rework parts of Dargent's typehecking

[skip bamboo]

compiler: partly revert 64c25e67f49

... as it breaks recursive types.
Now cogent-c type corres table needs to be reworked for Dargent.

compiler: add support for ghc-8.8+

compiler: fix desugar bug due to c68ff1

[skip lemma]

TODO: fix other potential bugs in field non-reordering

compiler: fix mismatched ordering causing proof failures

compiler: fix merge breakge

[skip lemma]

compiler: Fix various recursive types bugs, fix common library, fix anti C

compiler: building after dargent merge

compiler: fix small issues

Added banged recpars

compiler: recursive types inference in core language

compiler: further integrate recursive parameters into the core/surface language, begin work on typechecking

compiler.dargent: add layout synonym support

[skip lemma]

compiler.dargent: modify desugar to support layout polyphorism

[skip lemma]

compiler.dargent: WIP - typecheck for layout polymorphism

- have typecheck working for some basic cases
- change core lang to allow layout args
- introduce TLApp to surface syntax

[skip lemma]

compiler.dargent: WIP - progress on typechecking

- also modify travis config, it should be able to build binary now

[skip lemma]

compiler.dargent: WIP - more changes on core lang & misc

[skip lemma]

compiler.dargent: WIP - change core lang; fix typevar check

[skip lemma]

compiler.dargent: add syntax for layout polymorphism

[skip lemma]

compiler: fix merge breakage

[skip lemma]

compiler.array: fix an SMT solver mistake

[skip ci][skip lemma]

dargent: add array layout support

[skip lemma]

compiler.array: [wip] get many types right

compiler.array: use LExpr for predicates in types

[skip lemma]

compiler: [wip] kill tons of type errors. still infinitely many left.

[skip lemma]

compiler,array: some progress on array take

thanks to Vivian and Vincent for helping me debug the parser
Post is currently broken.

[skip lemma]

compiler,array: [wip] take/put with a single hole

[skip lemma]

compiler: post and desugar array put

[skip lemma][skip ci]

compiler: try out a general way to track array takes/puts

[skip lemma][skip ci]

compiler: keep track of takens array elems in core

[skip lemma][skip ci]

compiler: eliminate trailing spaces

[skip lemma][skip ci]

compiler: relax array indexing op

[skip lemma][skip ci]

compiler: array fix parser and pp

[skip lemma][skip ci]

compiler: array core-tc, normal, mono, surface-tc gen

[skip ci][skip lemma]

compiler: a little bit of desugar

[skip lemma][skip ci]

compiler: compiles with tarray ast

[skip lemma][skip ci]

dargent-merge: add in quasi quoter + tests

dargent-merge: fix desugar

compiler: rename modules to Dargent

[skip lemma]

Implemented layout generation in desugaring phase.

* Changed INSTALL.md to reflect need for GNU sed for some tests
* Modified Core language `Type t` `Sigils` so that `TCon` sigils are of type `Sigil ()` and `TRecord` sigils are of type `Sigil (DataLayout BitRange)`. This is because in the core language, `TCon` is only used for abstract types, and abstract types have no layout. `TRecords` must always have a layout if they are boxed.
* Added layout generation in the desugaring phase for types whose layout wasn't provided.
* Changed a few test cases to WIP because they involve records containing boxed abstract types, which we will probably be removing from the language, and the initial dargent implementation doesn't support.

Setup for implementing separated typechecking and desugaring.

Not sure why `make test-tc` has `fail_wf-take-nonexisting-field.cogent` broken.

Updated project to use new DataLayout structures, instead of Repr structures.

compiler: fix (partially) #306.

the compiler should work but the formal verification hasn't been
established for unboxed variables.

[skip lemma]

compiler: fix #307

[skip lemma]

compiler: keep function typevar context when making lambda toplevel

Isabelle embedding now avoids the use of keywords

compiler: fix tuple->record field order problem

Some parts of desugar were not treating the tuple order correctly.
Unboxed records are required to be ordered by their field name.

Co-authored-by: Zilin Chen <Zilin.Chen@data61.csiro.au>

compiler: add a nice error for FFI constants

cogent-repl: preload almost works

[skip lemma][skip ci]

problems:
* it loops :(
* int literals can be used as Bool for some reason

cogent: [wip] add a repl for cogent

lots of annoying problems are present...
[skip ci][skip lemma]

compiler: individuate the types of function names in core (#273)

compiler: fix an obsolate presense of Char

[skip lemma]

compiler: implement MultiWayIf syntax

[skip lemma]

compiler: migrate from lens to microlens

[skip lemma]

compiler: deps := deps - {tuple}

[skip lemma]

compiler: experimental arrays are now behind a cabal flag

[skip lemma]

compiler: deps := deps - {flippers}

[skip lemma]

compiler: move Data out of Cogent

compiler: break out existentials

compiler: break out nats

compiler: break out propositional equality

compiler: move data to Cogent.Data

compiler: [major] refactor C-gen code

compiler: minor fixes to haskell gen

[skip lemma][skip ci]

compiler: fix haskell gen breakage

[skip lemma]

compiler: trim comments so that they don't clash with Haddock syntax

[skip ci][skip lemma]

compiler: TPtr -> Sigil layout

[skip lemma]

compiler: [wip] clean up Deep.hs + small fixes

I just managed to fixed the most obvious problems. For the rest,
we'll fix them as we test the proofs.

compiler: push repr to the syntax of the core lang.

compiler: fix array indices eval and core pp

[skip ci]

compiler: implement function composition

compiler: largely improve coherence btw parser and pp

compiler: initial ptr backend impln

[skip lemma]

compiler: fix important flaw re. arrays

[skip lemma][skip ci]

compiler: up to core tc.

very coarse. [skip lemma][skip ci]

compiler: wip - arrays (parser, ds).

also fix a lot of code to make it work with ghc-8.4

[skip ci][skip lemma]

compiler: some initial array implementation

[skip lemma][skip ci]

compiler: implement abs type dependency [WIP]

but it doesn't seems to solve the ordering problem
WordArray and WordArrayView introduced.

[skip ci]

compiler: fix a bug in desugaring BindingAlts

[skip ci]

compiler: finish early exit feature

compiler: wip - closures

compiler: simple lambda-expressions done

[skip ci]

compiler: basic lambda expressions

[skip ci]

compiler: lambda-lifting wip

hit a ghc bug!
[skip ci]

compiler: insert Promote nodes

[skip ci]

compiler: wip removing debug mode

run into some GHC panic!

compiler: kill some warnings

compiler: cleanup; copyright blocks

compiler: codegen roughly done

compiler: ds,core-tc

- tested with testsuites, bilbyfs, ext2
- looks complete (modulo bugs), but may be unsound(?)
- need later phases to confirm

compiler/tc: wip - desugar/core

not quite right. maybe need a dedicated phase for adding
promote nodes

resolve breakage introduced by a huge rebase

[skip ci]

compiler: trivial fixes in desugarer and core-tc

[skip ci]

compiler: rework AST to add location to patterns

This solves #36.

FIXME:
* Lots of locations are still not accurate, esp. in desugarer;
* Pattern context might not be good enough (or not added properly);

warn: add warnings for unused binders (WIP)

compiler: implement type holes

compiler: fix build issues when rebasing.

When rebasing to the current master, there were a bunch of patches missing
when I replayed the commits from the `tc-new` branch. This patch adds all
those missing pieces.

compiler: kind of fix desugarer properly.

if and case still not correct. not promoted.

Proper variant subtyping as per Cogent 2.1 Proposal.

compiler: rename Sugarfree to Core

compiler: all DS errors now occur in guards

compiler: fix desugarType to deal with multi-param variant alts

copmiler: change to right way of desugaring Put

compiler: better pp with more internal structure info

--fdisambiguate-pp flag

compiler: some cleanup and better debugging funcs

normaliseT doesn't normalise enough

compiler: a few more desugar fixed

Add “widen” and “upcast” keywords; update tests.

Now the typechecker passes all pass_ tests.

compiler: simply use old typeWHNF and helper functions.

Kinda works. some don't (internal) typechecker, may due to new
subtyping rules (cast, promote)

compiler: use todo instead of undefined

Rudimentary pretty printing; make the thing build through liberal use of undefined; fixed some solver bugs

compiler: fix warnings.

all remaining warnings are due to WARNINGS pragma

compiler: [trivial] disambiguate `take'.

for some reason suddenly picked up by ghc-7.10.3

compiler: alpha version of ffi-generator

* users can specify customised type generation via --cust-ty-gen flag
* add examples pass_ffi-gen-1
* bump to 2.0.8.0

* todo: put pass_ffi-gen-1 into testsuite

[compiler] GHC 8.0 support and other fixes.

This patch contains the following changes:
* Drop `monoid-subclasses` as a dependency because it is really broken in 8.0
and has lots of orphans.
* Made a number of Fin types more accurate.
* Remove GHC < 8.0 conditional error branches that allegedly aren't needed in
8.0.
* Fixed some good number of Ticked Constructor warnings
* Trimmed trailing whitespace noise.

[compiler] Support for C-style includes.

This patch adds support for C-style includes to the Cogent compiler/parser.

* include <> : Search for the included file in the default path(can be
over-ridden by `COGENT_GUM_INC_DIR` enviroment variable.
* include "" : Search for the included file in relation to the current
working directory.

Code reorganisation.

* A rejig of the the Cogent compiler's directory structure.
* Support for building Cogent compiler with both `cabal` and `stack`.
(`stack` support is EXPERIMENTAL)
* Use Makefiles for build and install.
* Remove trailing white-spaces.
* Generate `dummy headers` in `tests/include` for testing C code.
* Remove unused `gen_types.sh` script
* Bump version to `2.0.6`

TODO:
* Remove duplicated files in `libgum`