Code

Refinement typing#1961

Code

Draft

catvayor wants to merge 43 commits intomasterdiku-dk/futhark:masterfrom refinement-typingdiku-dk/futhark:refinement-typingCopy head branch name to clipboard

+7,562-65

Commits

Commits on Jun 9, 2023

• Refinement in typeExp

  catvayor

  committed
  3c62dfb

Commits on Jun 12, 2023

• Predicate checking

  catvayor

  committed
  4c67e64

• Type check the refinement predicate

  catvayor

  committed
  b4406e1

• parsing of refinement

  catvayor

  committed
  63df742

• Types now have refinement

  catvayor

  committed
  c51ed5a

• Refinement are given to types

  catvayor

  committed
  ce21543

Commits on Jun 13, 2023

• argument are now substituted in predicates

  catvayor

  committed
  2677d93

• Merge branch 'master' into refinement-typing

  catvayor

  committed
  5ee4b58

• correct merge

  catvayor

  committed
  922e4fd

• Initial merge of the sum-of-products functionality.

  zfnmxt

  committed
  4fdaeda

• Add tests and do some renaming.

  zfnmxt

  committed
  8d309ea

• Use VNameSource.

  zfnmxt

  committed
  65a64c6

• Provide a class so SoP functionality can be tacked on more easily.

  zfnmxt

  committed
  48492fa

• Get things in place to experiment in internalization.

  zfnmxt

  committed
  ba69e74

• Early experimentation.

  zfnmxt

  committed
  fd66c21

• Use MonadSoP class instead of SoPM.

  zfnmxt

  committed
  0090d7d

• Beginnings of the refinement pass.

  zfnmxt

  committed
  23fa8ca

• correct errors in unittest typing

  catvayor

  committed
  f7afab4

• array shapes go through refinement

  catvayor

  committed
  9003024

• futhark dev: add --refinement-check.

  athas

  committed
  7212caa

• style typing

  catvayor

  committed
  59cbac9

• some "not implemented" error removal

  catvayor

  committed
  9e8b157

• some working to make things type

  catvayor

  committed
  78f00f5

• Also look in expression.

  athas

  committed
  e23c4d1

Commits on Jun 14, 2023

• Oops, restore this.

  zfnmxt

  committed
  6fe09cc

• Generalize SoP system to be able to work on different expression

  Show description for 088201e
  zfnmxt

  committed
  088201e

• slicing through refinement

  catvayor

  committed
  b9c1626

Commits on Jun 15, 2023

• avoid the insertion of bad refinement

  catvayor

  committed
  11ea8cd

Commits on Jun 16, 2023

• prettier pretty for refinement

  catvayor

  committed
  6d7394b

• use pipe for refinements

  catvayor

  committed
  ae4ee36

• Remove back conversion from SoPs and fix to conversion.

  zfnmxt

  committed
  dfd3b6d

• Everything should be done in SoP land.

  zfnmxt

  committed
  8874bcb

• Merge branch 'master' into refinement-typing

  athas

  committed
  78d47bb

Commits on Jun 18, 2023

• Revert "futhark dev: add --refinement-check."

  Show description for 8361492
  zfnmxt

  committed
  8361492

• Add futhark refinement.

  zfnmxt

  committed
  a7ffac3

• Add a Constraint type.

  zfnmxt

  committed
  8580cc8

• Merge remote-tracking branch 'origin/master' into refinement-typing

  zfnmxt

  committed
  e2b12f8

• Ormolu isn't playing nice with :&&:.

  zfnmxt

  committed
  137320f

Commits on Jun 19, 2023

• Things are broken.

  zfnmxt

  committed
  5ff0982

• Merge branch 'master' into refinement-typing

  athas

  committed
  d5e4664

Commits on Jun 22, 2023

• A bit of progress.

  zfnmxt

  committed
  5f232b1

Commits on Dec 30, 2023

• Proof goes through now.

  zfnmxt

  committed
  b33f54e

• Add old rules for reference.

  zfnmxt

  committed
  01841a5