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

Fractional permissions for mutable and immutable borrowing #229

Merged
merged 84 commits into from
Nov 22, 2024
Merged

Fractional permissions for mutable and immutable borrowing #229

Changes from 1 commit
Commits
Show all changes
84 commits
Select commit Hold shift + click to select a range
5a76081
prototype that typechecks fractional primitives (no arbitrary fractio…
starsandspirals Jul 10, 2023
1f4e6a8
evaluation for withBorrow, split and join
starsandspirals Jul 10, 2023
4fd3757
toy examples for the fractional paper
starsandspirals Jul 10, 2023
ae8c82b
share and clone allowed at broader range of grades
starsandspirals Jul 13, 2023
0c6be2c
arbitrary fraction support with basic addition and multiplication
starsandspirals Jul 13, 2023
017d409
fix the unification bug so all fractional examples compile
starsandspirals Jul 14, 2023
daaca2c
fix remaining merge conflicts with dev-minor
starsandspirals Oct 11, 2023
9b0defd
note which fractional examples are currently broken
starsandspirals Oct 11, 2023
84573c1
add borrow unification
dorchard Oct 11, 2023
627cf5d
permission representation in smt layer
dorchard Oct 11, 2023
f93b528
rename sPermission to sFraction
starsandspirals Oct 16, 2023
013f98c
add symbolic operations for SFraction
starsandspirals Oct 16, 2023
21fdf4a
compileCoeffect case for fractions
starsandspirals Oct 16, 2023
a20dd8a
working constraint generation for fractions!
starsandspirals Oct 16, 2023
2a21c8a
example from paper
dorchard Oct 26, 2023
c6d00d7
fix array interface and add reference interface
starsandspirals Nov 6, 2023
3a285fb
tweak lengthArray to return unrestricted int (makes loops easier)
starsandspirals Nov 6, 2023
7dc066b
function from float arrays to vec of float refs
starsandspirals Nov 6, 2023
3b1c88e
example function going back from vec of refs to array
starsandspirals Nov 7, 2023
ec898f4
generalise the type of readRef
starsandspirals Nov 9, 2023
c28dbf9
refactor includeOnlyGradeVariables to use requiresSolver
dorchard Dec 13, 2023
c20dd60
let fraction variables be generated by the symbolic layer
dorchard Dec 13, 2023
690a08d
fraction approximation is just equality
dorchard Dec 13, 2023
0097636
flag that permissions require the solver
dorchard Dec 13, 2023
f6b510b
extend unify to star
dorchard Dec 13, 2023
35517a7
improve pretty printing
dorchard Dec 13, 2023
e8bc561
put ids on float arrays
dorchard Dec 13, 2023
615a3f4
add identifiers to references
starsandspirals Dec 13, 2023
d911e88
oopsla wip
starsandspirals Dec 13, 2023
b2a5332
oopsla example typechecks
starsandspirals Dec 13, 2023
2602423
rename identifier kind to Name and some example tidying
starsandspirals Dec 14, 2023
f2fe84f
fix missing id in readFloatArray (unique version)
starsandspirals Dec 14, 2023
cd796dc
star alias for borrow polymorphism (mutable constraint not implemente…
starsandspirals Dec 15, 2023
fb47269
hacky solution for mutable constraint
starsandspirals Dec 18, 2023
26fbbb0
cleanup old version of mutable
starsandspirals Dec 18, 2023
d51a07d
fix type signatures of split and join
starsandspirals Dec 19, 2023
1d67bf4
replace SBV rationals with floats
starsandspirals Dec 19, 2023
ebaa245
more tightly bounded fraction constraint
starsandspirals Dec 19, 2023
e26a289
bug related to unification in specific positions
dorchard Dec 20, 2023
39851b6
make sure primitives use the correct Maybe interface (see #190)
dorchard Oct 26, 2023
74f83cd
fixes #190
dorchard Oct 26, 2023
c11bb42
commented out tracing routine, could be useful in the future, but we …
dorchard Oct 26, 2023
b45eb84
add error message for borrow mismatch rather than crashing
starsandspirals Dec 20, 2023
d30736b
implement references at runtime using Haskell IORefs
starsandspirals Dec 21, 2023
903d270
simple examples used when testing reference runtime
starsandspirals Dec 21, 2023
22b5814
fix bug when pretty-printing reference value
starsandspirals Dec 21, 2023
21b1d26
name implementation and dummy evaluation for new resources
starsandspirals Dec 30, 2023
42958f0
cloneable predicate and generalise rule slightly
starsandspirals Dec 30, 2023
de095ac
better pretty printing for borrows
starsandspirals Dec 30, 2023
7838845
unique name generation
starsandspirals Jan 3, 2024
1ac7fd0
runtime implementation of clone
starsandspirals Jan 3, 2024
48003a7
fix the silly lengthFloatArray bug
starsandspirals Jan 3, 2024
f1cc91e
first bash at type-level renaming function
starsandspirals Jan 3, 2024
ff5eadb
simple clone example that doesn't typecheck, not sure why
starsandspirals Jan 4, 2024
bf53585
equivalent version with uniqueBind
starsandspirals Jan 4, 2024
2c4fa61
more robust renaming with inversion on variables
starsandspirals Jan 4, 2024
436e389
simplify clone examples for easier debugging
starsandspirals Jan 4, 2024
af95c6c
special case for both Rename
starsandspirals Jan 4, 2024
41991b6
fix problem of existentially leaking out of scope due to unification
dorchard Jan 4, 2024
1e01e6f
better diagnostics with holes in synthesis positions
dorchard Jan 4, 2024
e0af2b1
direct type checking of a clone rather than relying on the desugarded…
dorchard Jan 5, 2024
a9d0b6a
be careful when cloning references
starsandspirals Jan 5, 2024
c251824
add nix flake to fractional
starsandspirals Jan 5, 2024
eacc7c2
add 1 <= r constraint for clone
dorchard Jan 5, 2024
f8566b1
checking a clone drops through to synthing a clone (this is needed as…
dorchard Jan 5, 2024
905123d
cloneable constraint and reorder type equality a bit so that normalis…
dorchard Jan 5, 2024
faf4feb
negative test for cloning noncloneable things
dorchard Jan 5, 2024
bb38dad
fix test outputs
dorchard Jan 5, 2024
ba0ab5b
update negative example to identified floatarrays
dorchard Jan 5, 2024
78f3e39
reorder equality for session things otherwise divergenece happens
dorchard Jan 5, 2024
aec6580
Revert "add nix flake to fractional"
raehik Jan 5, 2024
0985b52
put Cabal files in history
raehik Jul 25, 2023
74f346e
add cabal.project for Cabal builds
raehik Jul 25, 2023
b7b059f
add Nix flake with Docker image build
raehik Jul 25, 2023
ee20921
Nix flake: add granule stdlib, grepl wrapper
raehik Jul 26, 2023
92516ed
Nix flake/image: fix locale issue
raehik Jul 26, 2023
6a9247d
regenerate Cabal files
raehik Jan 5, 2024
6be9a50
update output for test
dorchard Jan 5, 2024
4c88421
wip oopsla example
dorchard Jan 5, 2024
c35c265
remove spurious case of equality for star/borrow
dorchard Jan 5, 2024
f5690a8
cleanup
dorchard Jan 6, 2024
66c8c04
more readable hole contexts
dorchard Jan 6, 2024
78b43af
Merge branch 'main' into fractional
dorchard Oct 17, 2024
f861c0d
tweaks
dorchard Nov 21, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
rename sPermission to sFraction
  • Loading branch information
@starsandspirals
starsandspirals committed Oct 16, 2023
commit f93b5288ad49308ce468a96364b7e76da630b3e6
2 changes: 1 addition & 1 deletion frontend/src/Language/Granule/Checker/Constraints/SymbolicGrades.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ solverError msg = liftIO $ throwIO . ErrorCall $ msg
-- Symbolic grades, for coeffects and indices
data SGrade =
SNat SInteger
| SPermission { sPermission :: SRational, sIsUnique :: SBool }
| SFraction { sFraction :: SRational, sIsUnique :: SBool }
| SFloat SFloat
| SLevel SInteger
| SSec SBool -- Hi = True, Lo = False
Expand Down