Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Development #2

Open
wants to merge 87 commits into
base: master
Choose a base branch
from
Open

Development #2

wants to merge 87 commits into from

Conversation

ajrouvoet
Copy link
Contributor

@ajrouvoet ajrouvoet commented Aug 15, 2018 •
edited by casperbp
Loading

This branch contains:

  • Updated MJ semantics to use do-notation and abstract monad
  • Categorical development of the monotone predicate state monad using categories library
  • Update to 2.5.4

Blocked by:

  • Updating examples
  • Concrete monad implementation for MJ semantics

@ajrouvoet
Basic Delay monotone predicate definition
ec99a80
@ajrouvoet
The partiality monad is also monad in the category of MPs
ef121bd 
By naturality of eta and mu in the category of Sets
@ajrouvoet
Moving with the paper: upcastable references
4387c4b 
Removing coercion
@ajrouvoet
Moving with paper: add concatenation and prepend on paths
99e7d99
@ajrouvoet
Using do-notation in MJ/Semantics/Monadic
daae329
@ajrouvoet
Scratch files for cat development based on copumpkin's categories
8120a2c
@ajrouvoet
Add categories patch
b85f71e
@ajrouvoet
Proven that the product of MPs is an MP
2afefcd
@ajrouvoet
Using copatterns for readability
7f757be
@ajrouvoet
Proven product construction commutative
61aaad7
@ajrouvoet
Universality
07a01aa
@ajrouvoet
Commutativity for Products
faba894
@ajrouvoet
Lowerbounded forall quantification builds monotonicity
464f9e3
@ajrouvoet
Object mapping for monotone-state monad
2c8a7a8
@ajrouvoet
Progress on formulating the monotone-state monad
91d5fb3
@ajrouvoet
Monotone-state functor
de90118
@ajrouvoet
Minor progress
208e10d
@ajrouvoet
Lots of prove readability improvements
0eacdd8
@ajrouvoet
Return is a natural transformation
79b7ac3
@ajrouvoet
Closed one goal
11d42f8
@ajrouvoet
Sometimes you are in luck
ecbe6d7
@ajrouvoet
Another one bites the dust
51c3bcc
@ajrouvoet
Added goals for proving monadic strength
bd4bcb5
@ajrouvoet
Two more proofs down
e8621eb
@ajrouvoet
Left identity
dfd2924
@ajrouvoet
Associative
ea5285a
@ajrouvoet
Transfoooorm
79fb7a6 
WIP making the monad state monad a monad transformer
@ajrouvoet
Prove some lemmas and rename StateT->PredicateT
c0a61b1
@ajrouvoet
Added Delay setoid
85d5de5
@ajrouvoet
Delay is a functor in the category of ISetoids
c593610
@ajrouvoet
Fixed the fixpoint combinator
91287f6
@ajrouvoet
Useful properties
ab26a07
@ajrouvoet
StepIndexed ofes are complete
7674cf7
@ajrouvoet
+ Coproducts on Ofes
7fe1785
@ajrouvoet
Some properties and an example using partiality
a034a8c
@ajrouvoet
Add proof that StepIndexed is a functor from ISetoids to Ofes
55e812c
@ajrouvoet
Rewrote Arith example in terms of eliminator instead of destructor
3bbc472 
+ Generalized some definitions from the Arith example
@ajrouvoet
Some comments
1a274d3
@ajrouvoet
Moved some general properties from Arith
8bb257f
@ajrouvoet
Add BoolNum example demonstrating typed syntax
c8617e3
@ajrouvoet
Added compilation target
78024dd 
+ adapted MJ/Examples/While for extraction (main function)
@ajrouvoet
Cleanup example extraction
a397c2b
@ajrouvoet
Update libs and change MJ binops from Agda function to syntax
676af68
@ajrouvoet
Generalize the MJ semantics over any suitable monad
5f34ade 
+ Pulls in the monotone predicate monad additions of stdlib++
@ajrouvoet
Merge branch 'master' into sugar
78a7bad
@ajrouvoet
Trashing some deprecated code
5b2cb20
@ajrouvoet
Merge branch 'categorical'
09618d8
@ajrouvoet
Fix build and add nix build
7b0f1cc
@ajrouvoet
Update the README: Agda 2.6.0 is required for the syntactic sugar
28e6dbe
@ajrouvoet
Merge branch 'master' into develop
f6769dd
@ajrouvoet
Unphony the libraries for safer builds
d7efc37
@ajrouvoet
Merge branch 'master' into develop
6bbdda9
@ajrouvoet
Abstract the MJ semantics over an arbitrary monad
3b9cc0f
@ajrouvoet
Update to Agda 2.5.4
da382dd
@ajrouvoet
Everything that compiles at 2.5.4
6cf48bf
@ajrouvoet
Fix for 2.5.4
5c2f057
@ajrouvoet
Uncomment imports that are very slow to typecheck in Readme
82bd9c6
@ajrouvoet
Minor updates to stdlib++
aa37b2b
@ajrouvoet
Add instance argument to help Agda 2.5.4.1
05ff9e8 
See agda/agda#3177 (comment)
@ajrouvoet
Remove stale implicit argument
c751dad
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
1 participant
@ajrouvoet