Code

Tactic metaprogramming#1776

Code

Merged

mergify[bot] merged 57 commits intohaskell:masterhaskell/haskell-language-server:masterfrom

isovector:metaprogramming2isovector/haskell-language-server:metaprogramming2Copy head branch name to clipboard

May 16, 2021

Commits

Commits on Apr 26, 2021

• Metaprogramming parser

  isovector

  committed
  2cc54a4

  Copy full SHA for 2cc54a4

• Enable quasiquotes by default in ghcide

  isovector

  committed
  352dbb0

  Copy full SHA for 352dbb0

• Install the Wingman tactic syntax in ghcide

  isovector

  committed
  a32d563

  Copy full SHA for a32d563

• Underscores are allowed in identifiers too

  isovector

  committed
  643fb88

  Copy full SHA for 643fb88

• Test showing we can expand out tactics

  isovector

  committed
  22a509f

  Copy full SHA for 22a509f

• Use a more concrete type for mkWingmanMetaprogram

  isovector

  committed
  762f43c

  Copy full SHA for 762f43c

• Cleanup lexer

  isovector

  committed
  7ddb88d

  Copy full SHA for 7ddb88d

• Use operator parsing for multiple tactics

  isovector

  committed
  0cd6a0e

  Copy full SHA for 0cd6a0e

• Tidy the parser

  isovector

  committed
  10105a9

  Copy full SHA for 10105a9

• Add 'obvious' tactic

  isovector

  committed
  65ff472

  Copy full SHA for 65ff472

• Add intros', which lets you bind the names you want

  isovector

  committed
  f24c7b7

  Copy full SHA for f24c7b7

• Add intro to the parser

  isovector

  committed
  6162a81

  Copy full SHA for 6162a81

• Add a modifyDynFlags field to plugins; push it into the parsed module

  isovector

  committed
  dd548ba

  Copy full SHA for dd548ba

• Modify dflags when typechecking too

  isovector

  committed
  fe4f84a

  Copy full SHA for fe4f84a

Commits on Apr 27, 2021

• Use the dynflags modifier to remove wingman specific code from ghcide

  isovector

  committed
  7961245

  Copy full SHA for 7961245

• Move the staticplugin out of ghcide

  isovector

  committed
  3383f64

  Copy full SHA for 3383f64

• Add application, add split, rename split to ctor

  isovector

  committed
  b586b85

  Copy full SHA for b586b85

• Tidy parser

  isovector

  committed
  74d4e64

  Copy full SHA for 74d4e64

• Track remaining subgoals for interactive proofstate

  isovector

  committed
  f488be8

  Copy full SHA for f488be8

• Add a pretty printer of the proofstate

  isovector

  committed
  735a28d

  Copy full SHA for 735a28d

• Add sorry

  isovector

  committed
  d18cbf5

  Copy full SHA for d18cbf5

• Attach proof state as a hover action

  isovector

  committed
  da1bec0

  Copy full SHA for da1bec0

Commits on Apr 28, 2021

• Much prettier proof state

  isovector

  committed
  ce85e9f

  Copy full SHA for ce85e9f

• Tidy and tag hover as markdown

  isovector

  committed
  f8abb95

  Copy full SHA for f8abb95

• Be smarter about where we run the dflags endo

  isovector

  committed
  3e3bff5

  Copy full SHA for 3e3bff5

• Undo changes

  isovector

  committed
  5a57078

  Copy full SHA for 5a57078

• Make Plugin accumulators robust to changing defs

  isovector

  committed
  9e74afc

  Copy full SHA for 9e74afc

• Remove unused exts from Session

  isovector

  committed
  5adc279

  Copy full SHA for 5adc279

• Reannotate the AST with tactic blocks

  isovector

  committed
  92e95c5

  Copy full SHA for 92e95c5

• Tidy parser

  isovector

  committed
  2c98fec

  Copy full SHA for 2c98fec

• MetaprogramSyntax and exact combinator

  isovector

  committed
  e3d2e8d

  Copy full SHA for e3d2e8d

• Add introduce metaprogram code action

  isovector

  committed
  cf6fc2e

  Copy full SHA for cf6fc2e

Commits on May 4, 2021

• Merge branch 'master' into metaprogramming2

  isovector

  committed
  3c015e4

  Copy full SHA for 3c015e4

• Use noExtField

  isovector

  committed
  89b7e63

  Copy full SHA for 89b7e63

• Appease Hlint

  isovector

  committed
  c032f7b

  Copy full SHA for c032f7b

• Compat for mkFunTys

  isovector

  committed
  69d3296

  Copy full SHA for 69d3296

Commits on May 6, 2021

• Guard the static plugin

  isovector

  committed
  5657286

  Copy full SHA for 5657286

• Static plugin doesn't even need to be here!

  isovector

  committed
  86e58b9

  Copy full SHA for 86e58b9

• textSpaces doesn't exist in old versions of prettyprinter

  isovector

  committed
  994662d

  Copy full SHA for 994662d

• Use a record for the result of judgmentForHole

  isovector

  committed
  8ad359e

  Copy full SHA for 8ad359e

• Return the hole's occName

  isovector

  committed
  9f43fca

  Copy full SHA for 9f43fca

• Add HoleSort; filter code actions by their holesort

  isovector

  committed
  0fae78c

  Copy full SHA for 0fae78c

• Minor tidying

  isovector

  committed
  4100b2d

  Copy full SHA for 4100b2d

• Better name for metaprogram holes

  isovector

  committed
  1b9cafa

  Copy full SHA for 1b9cafa

• Merge branch 'master' into metaprogramming2

  isovector

  committed
  7966c15

  Copy full SHA for 7966c15

• Use a record for DynFlags modifications

  isovector

  committed
  e078635

  Copy full SHA for e078635

• More hlint

  isovector

  committed
  4cf4a79

  Copy full SHA for 4cf4a79

Commits on May 8, 2021

• Use modified dynflags for parser with comments

  isovector

  committed
  64350dd

  Copy full SHA for 64350dd

• Allow running custom code blocks

  isovector

  committed
  5ee9c1f

  Copy full SHA for 5ee9c1f

• Don't assume tactic providers use occnames

  isovector

  committed
  1dce53e

  Copy full SHA for 1dce53e

Commits on May 12, 2021

• Revert changes to ghcide

  isovector

  committed
  37ac02b

  Copy full SHA for 37ac02b

• Merge branch 'master' into metaprogramming2

  isovector

  committed
  a8306f3

  Copy full SHA for a8306f3

Commits on May 13, 2021

• Add tests

  isovector

  committed
  0399ce4

  Copy full SHA for 0399ce4

• Feature gate

  isovector

  committed
  6424855

  Copy full SHA for 6424855

Commits on May 14, 2021

• Restrict metaprograms to >=8.8

  isovector

  committed
  6da17ee

  Copy full SHA for 6da17ee

Commits on May 15, 2021

• Merge branch 'master' into metaprogramming2

  mergify[bot]

  authored
  38780c1

  Copy full SHA for 38780c1

• Merge branch 'master' into metaprogramming2

  mergify[bot]

  authored
  c986c3f

  Copy full SHA for c986c3f