Code

v0.9.5.0#239

Code

Merged

dorchard merged 110 commits intomaingranule-project/granule:mainfrom dev-minorgranule-project/granule:dev-minorCopy head branch name to clipboardMar 8, 2024

+1,474-503

Commits

Commits on Jul 25, 2023

• bump version for dev-minor

  dorchard

  committed
  9292c9b

• better localisation of type error for let<>

  dorchard

  committed
  1aa0d43

• slight reorder in primitives for documentation purposes (moving fork to effectful channels section)

  dorchard

  committed
  f0dc679

• improve docs; break long lines and show hidden names information

  dorchard

  committed
  0a0a6e9

• improve docs formatting and pretty printing

  dorchard

  committed
  9f09250

• remove forkLinear' which was used for experimentation

  dorchard

  committed
  7b28782

• fix typo

  dorchard

  committed
  33326bd

Commits on Jul 26, 2023

• pushable alias for hsup constraints; fixes #182

  dorchard

  committed
  a160a82

• make grepl types a bit more clear if there are poly vars around

  dorchard

  committed
  77e9e34

• fix where hsup is used (should be in body)

  dorchard

  committed
  519b5be

• put Set in scope

  dorchard

  committed
  dd146f4

• add hsup constraints to push; Pushable

  dorchard

  committed
  851d377

• tests

  dorchard

  committed
  0a0ec83

• update tests

  dorchard

  committed
  758d593

• handle ty constraints in grepl as well (helps to deal with the example in issue #175)

  dorchard

  committed
  421aeb5

• fix constraint in List module

  dorchard

  committed
  6569e0e

• clear type checker state before synthing expression type in grepl - otherwise pollution occurs

  dorchard

  committed
  5653807

• store derived definitions generated from checking rest of file in repl state

  dorchard

  committed
  fc393d4

• remove duplicate deriving implementations due to modules

  dorchard

  committed
  e54d6be

• Merge pull request #220 from granule-project/derivingImprovements

  Show description for 3582324
  dorchard

  authored
  3582324

• internalise existential binders into predicate

  dorchard

  committed
  790f95b

• Revert "internalise existential binders into predicate"

  Show description for 821f167
  dorchard

  committed
  821f167

• fix bug associated with handled exception effects

  dorchard

  committed
  43d0a89

Commits on Jul 27, 2023

• add a unicode synonym for the existential quantifier

  starsandspirals

  committed
  555e55a

• tweak one example to use unicode exists

  starsandspirals

  committed
  2d4295e

• add exists to ascii/unicode table in README

  starsandspirals

  committed
  1a21959

• add missing throw operation to evaluator

  dorchard

  committed
  e2ce47c

Commits on Aug 7, 2023

• fix formatting bug when splitting lines which don't have forall

  dorchard

  committed
  fd583db

Commits on Aug 10, 2023

• fix flattening for Sec when not in SecurityLevels mode

  dorchard

  committed
  7d9fbac

• add golden output for negative flatten sec test

  dorchard

  committed
  9e9ba91

• dual is involution test reinstanted

  dorchard

  committed
  e463814

Commits on Aug 15, 2023

• Merge pull request #224 from granule-project/fixFlattenSec

  Show description for 5c1b6ca
  jackohughes

  authored
  5c1b6ca

Commits on Sep 19, 2023

• improve kinding with dependent kinds

  dorchard

  committed
  afc45c4

• generic effect operator

  dorchard

  committed
  8a3e258

Commits on Sep 22, 2023

• terms for forall types and corresponding expressions

  dorchard

  committed
  3e1c65d

• key positive test

  dorchard

  committed
  ac482d7

• synth kinds for forall types

  dorchard

  committed
  6b6c936

• checking for tyapp and absty

  dorchard

  committed
  361f35c

• equality on forall types and fixing up type checking

  dorchard

  committed
  c695077

• update test

  dorchard

  committed
  d6432cf

• evaluator for higher rank quantification

  dorchard

  committed
  2bca5c0

• fix name clash check so that it includes primitives

  dorchard

  committed
  1a26e71

Commits on Sep 23, 2023

• extended test with free monad and higher order functions

  dorchard

  committed
  52da14b

• fix freshening bug with new forall rankN

  dorchard

  committed
  c249a0d

• syntactic sugar for type signatures

  dorchard

  committed
  41ebeec

• merge conflix resolution

  dorchard

  committed
  63f5865

• fix freshening bug with exists, and provide an example combining exists and forall

  dorchard

  committed
  ae62bc0

• leverage rankN in generic effect op

  dorchard

  committed
  b7837c5

• wip

  dorchard

  committed
  9d86155

Commits on Sep 25, 2023

• some commenting and commenting out

  dorchard

  committed
  baf1307

• implicit->explicit resolver for rankN

  dorchard

  committed
  53cca3b

• free graded monad eval and handle update

  dorchard

  committed
  99adb90

• embed free monad bind into handler implementation

  dorchard

  committed
  a1cf09f

• tidyup examples

  dorchard

  committed
  5996742

• add tests

  dorchard

  committed
  01515d1

• output for example

  dorchard

  committed
  2bf3df2

• documentation and version number bump

  dorchard

  committed
  5eeef3c

• documentation

  dorchard

  committed
  7c51b6e

• non-determinism example

  dorchard

  committed
  c4f7ab6

• increase power of solver in case we have resolved all cases of Nat \/ Ext Nat on types (seems to happen sometimes due to base guesses)

  dorchard

  committed
  9aa2db0

• typos thanks to @takanuva

  dorchard

  committed
  6eca25d

• Merge, fix typos

  dorchard

  committed
  a5a72ea

• Merge pull request #226 from granule-project/rankN

  Show description for bd702fb
  dorchard

  authored
  bd702fb

• cleanup

  dorchard

  committed
  41f6bf8

• more cleeanup

  dorchard

  committed
  6b976b9

• cleanup

  dorchard

  committed
  4cd8318

Commits on Sep 26, 2023

• graded handle rule

  dorchard

  committed
  b931e76

• make index checking for pi-type conversion more powerful (+ test)

  dorchard

  committed
  57f4079

• Merge branch 'dev-minor' into effectHandlers

  dorchard

  committed
  452138c

• improve solving for sets by checking that the things in the set are in the finite universe given by the set element type

  dorchard

  committed
  8245b4e

• fix error message reporting the wrong variable being unbound in data type checker

  dorchard

  committed
  9aeff0e

• some noodling around how sets are handled to improve solver

  dorchard

  committed
  8e11c6b

• comments

  dorchard

  committed
  d750824

Commits on Sep 27, 2023

• generalise 'call' so that it can reused by handle and gradedHandle, and we get more flexibility

  dorchard

  committed
  7289f98

Commits on Sep 28, 2023

• fmap in handle needs to be nonlinear

  dorchard

  committed
  d42f05d

• fix to kinding for Set (there was a bug)

  dorchard

  committed
  3b29bbc

• generalise call/handle operations to work with arbitrary grading monoids

  dorchard

  committed
  2c6e206

• reused handle for handleGr

  dorchard

  committed
  56e82a4

• fix a test

  dorchard

  committed
  a94a1c0

• add concat operation for vectors

  dorchard

  committed
  25b4e38

• generalising the free graded monad

  dorchard

  committed
  30c16ab

• fixes to implicit binders in pattern match

  dorchard

  committed
  f11954e

• Merge pull request #227 from granule-project/effectHandlers

  Show description for fa2a1d2
  dorchard

  authored
  fa2a1d2

Commits on Oct 26, 2023

• make sure primitives use the correct Maybe interface (see #190)

  dorchard

  committed
  2a2b611

• fixes #190

  dorchard

  committed
  0b7bc1c

• commented out tracing routine, could be useful in the future, but we dont want it always exposed

  dorchard

  committed
  c4a0ba4

Commits on Nov 8, 2023

• Merge pull request #228 from granule-project/fix90

  Show description for 212bcb2
  dorchard

  authored
  212bcb2

Commits on Jan 6, 2024

• unification problem example

  dorchard

  committed
  ac1564e

Commits on Jan 19, 2024

• Add flag --no-print-return-value

  buggymcbugfix

  committed
  a83fada

• Merge pull request #231 from granule-project/buggymcbugfix/--no-print-return-value

  Show description for 568a746
  dorchard

  authored
  568a746

Commits on Mar 7, 2024

• fix drop so that it doesn't run forever with recursive types

  dorchard

  committed
  46f5001

• fixing copyShape; fixes #173

  dorchard

  committed
  82accfe

• fixing copyShape; fixes #173

  dorchard

  committed
  c6a5d7b

• fix pretty printer so that it shows graded base types properly

  dorchard

  committed
  1347734

• update tests

  dorchard

  committed
  6f948b4

• add missing pattern arity check

  dorchard

  committed
  38c1c18

• slightly tweak algebraic effects interface

  dorchard

  committed
  2d180a5

• rename drop on vectors

  dorchard

  committed
  2517787

• make drop and copyShape have primitive placeholders for documentation purposes

  dorchard

  committed
  65c87dc

• fix typing for drop and report errors if ill-kinded uses

  dorchard

  committed
  e329e6c

• kind errors for deriving drop

  dorchard

  committed
  bb5202d

• handle redefinition problems in evaluator around deriving

  dorchard

  committed
  9d89933

• slight naming tweak

  dorchard

  committed
  e3b8898

Commits on Mar 8, 2024

• ignore Premature end of file errors in LSP

  dorchard

  committed
  f804cec

• fix cost example to be more precise

  dorchard

  committed
  77f9d9d

• update some tests

  dorchard

  committed
  5f07f3d

• synth test updates

  dorchard

  committed
  24e2e35

• fix some more tests

  dorchard

  committed
  a407009

• update tests

  dorchard

  committed
  ee6e11c

• changelog

  dorchard

  committed
  577b71a