Code

Derivation trees#1302

Code

Draft

GuoDCZ wants to merge 142 commits intodevhazelgrove/hazel:devfrom derivationhazelgrove/hazel:derivationCopy head branch name to clipboard

+23,241-158

Commits

Commits on May 4, 2024

• init

  GuoDCZ

  committed
  d28642f

  Copy full SHA for d28642f

Commits on May 6, 2024

• abbr trial

  GuoDCZ

  committed
  b851154

  Copy full SHA for b851154

Commits on May 15, 2024

• refactor error msg with concrete type

  GuoDCZ

  committed
  a724ec7

  Copy full SHA for a724ec7

Commits on May 17, 2024

• task(1/7): type ported

  GuoDCZ

  committed
  6976690

  Copy full SHA for 6976690

• task(2/7): prop pattern supported

  GuoDCZ

  committed
  6c8a7b6

  Copy full SHA for 6c8a7b6

• task(2/7): entail pattern supported

  GuoDCZ

  committed
  b1ab19c

  Copy full SHA for b1ab19c

• task(2/7): entail repr refine

  GuoDCZ

  committed
  82e6358

  Copy full SHA for 82e6358

• task(2/7): refine precedence and judgement print

  GuoDCZ

  committed
  37fc71e

  Copy full SHA for 37fc71e

Commits on May 19, 2024

• port everything have done with ml

  GuoDCZ

  committed
  4e14567

  Copy full SHA for 4e14567

• task(3/7): port rule to builtin functions

  GuoDCZ

  committed
  3f066b7

  Copy full SHA for 3f066b7

Commits on May 22, 2024

• task(5/7): cascade derivation

  GuoDCZ

  committed
  dee4bfa

  Copy full SHA for dee4bfa

• task(6/9): new pattern der introduced

  GuoDCZ

  committed
  fae9144

  Copy full SHA for fae9144

Commits on May 27, 2024

• task(7/9): marked conclusion

  GuoDCZ

  committed
  d75a1c8

  Copy full SHA for d75a1c8

• task(8/9): turn derive pattern to close struct

  GuoDCZ

  committed
  fbbee43

  Copy full SHA for fbbee43

Commits on May 28, 2024

• task(8/9): frontend trial

  GuoDCZ

  committed
  dd59d32

  Copy full SHA for dd59d32

Commits on May 29, 2024

• exercise ui change trial

  GuoDCZ

  committed
  2f958a6

  Copy full SHA for 2f958a6

Commits on May 31, 2024

• feat: derivation frame imported to exercise mode

  GuoDCZ

  committed
  4b5f3ab

  Copy full SHA for 4b5f3ab

• rebase tree util

  GuoDCZ

  committed
  47a460b

  Copy full SHA for 47a460b

• exercise mode derivation basic verify

  GuoDCZ

  committed
  5858fff

  Copy full SHA for 5858fff

Commits on Jun 1, 2024

• (unstable): before flatten

  GuoDCZ

  committed
  77831bc

  Copy full SHA for 77831bc

• rebase derivation in exercise.re to pure list

  GuoDCZ

  committed
  e0cd132

  Copy full SHA for e0cd132

• polish util flattree/tree

  GuoDCZ

  committed
  cf47269

  Copy full SHA for cf47269

Commits on Jun 2, 2024

• flattree version, to be rebase

  GuoDCZ

  committed
  23c5655

  Copy full SHA for 23c5655

• manual rule select is ok

  GuoDCZ

  committed
  0ab899b

  Copy full SHA for 0ab899b

Commits on Jun 6, 2024

• Derivaiton UI update

  

  GuoDCZ

  committed
  0b65040

  Copy full SHA for 0b65040

Commits on Jun 17, 2024

• ExerciseMode Partition partial

  

  GuoDCZ

  committed
  eff37c7

  Copy full SHA for eff37c7

• refactor exercise (now normal/proof mode works are happy)

  

  GuoDCZ

  committed
  e00b223

  Copy full SHA for e00b223

• Stopper

  

  GuoDCZ

  committed
  ca0c9f5

  Copy full SHA for ca0c9f5

Commits on Jun 18, 2024

• rebase Proof exercise

  

  GuoDCZ

  committed
  0fe744b

  Copy full SHA for 0fe744b

• lack 22

  

  GuoDCZ

  committed
  b3fe261

  Copy full SHA for b3fe261

Commits on Jun 19, 2024

• frontend update dropdown

  

  GuoDCZ

  committed
  1adf207

  Copy full SHA for 1adf207

Commits on Jun 21, 2024

• feat:ez rule switch

  

  GuoDCZ

  committed
  dde7c1c

  Copy full SHA for dde7c1c

Commits on Jul 1, 2024

• add manual add/del botton

  

  GuoDCZ

  committed
  e0e1c5b

  Copy full SHA for e0e1c5b

Commits on Jul 2, 2024

• Merge branch 'dev' into derivation

  

  GuoDCZ

  committed
  c5950d8

  Copy full SHA for c5950d8

• refine Exercise logic

  

  GuoDCZ

  committed
  8b688af

  Copy full SHA for 8b688af

• modify exercise serialize

  

  GuoDCZ

  committed
  9ac6302

  Copy full SHA for 9ac6302

Commits on Jul 4, 2024

• return builtin

  

  GuoDCZ

  committed
  1606054

  Copy full SHA for 1606054

Commits on Aug 12, 2024

• merge to dev

  

  GuoDCZ

  committed
  2313d37

  Copy full SHA for 2313d37

• modulize exercise

  

  GuoDCZ

  committed
  79d154a

  Copy full SHA for 79d154a

• modulize Proof exercise

  

  GuoDCZ

  committed
  a493a4b

  Copy full SHA for a493a4b

Commits on Aug 13, 2024

• update action handler & exercise clearify module

  

  GuoDCZ

  committed
  0253157

  Copy full SHA for 0253157

• revert changes

  

  GuoDCZ

  committed
  ca31bce

  Copy full SHA for ca31bce

Commits on Aug 15, 2024

• refactor derivation base

  

  GuoDCZ

  committed
  1d77e86

  Copy full SHA for 1d77e86

• refactor derivation error

  

  GuoDCZ

  committed
  05d9863

  Copy full SHA for 05d9863

Commits on Aug 17, 2024

• grade view

  

  GuoDCZ

  committed
  8982e4c

  Copy full SHA for 8982e4c

• derivation abbr scheme

  

  GuoDCZ

  committed
  bb15d17

  Copy full SHA for bb15d17

Commits on Aug 18, 2024

• abbr advance ctrl

  

  GuoDCZ

  committed
  cceb179

  Copy full SHA for cceb179

Commits on Aug 19, 2024

• fix&update UI

  

  GuoDCZ

  committed
  e8afd0b

  Copy full SHA for e8afd0b

Commits on Aug 20, 2024

• Abbr facilitate

  

  GuoDCZ

  committed
  eafa7e1

  Copy full SHA for eafa7e1

Commits on Aug 23, 2024

• update core logic

  

  GuoDCZ

  committed
  0b41ddb

  Copy full SHA for 0b41ddb

• merge to dev

  

  GuoDCZ

  committed
  083dc17

  Copy full SHA for 083dc17

Commits on Aug 24, 2024

• AL basic

  

  GuoDCZ

  committed
  3e1d06b

  Copy full SHA for 3e1d06b

• add builtin derivation ctr

  

  GuoDCZ

  committed
  5000244

  Copy full SHA for 5000244

Commits on Aug 29, 2024

• before removing prop term

  

  GuoDCZ

  committed
  7115bfb

  Copy full SHA for 7115bfb

• remove Prop exp, leaving Typ. Rebase derivation

  

  GuoDCZ

  committed
  efff02b

  Copy full SHA for efff02b

Commits on Aug 31, 2024

• temp cmt/ switch to new device

  

  GuoDCZ

  committed
  0e5004a

  Copy full SHA for 0e5004a

Commits on Sep 1, 2024

• temp: switch device

  

  钟之尧

  authored and

  钟之尧

  committed
  44599fc

  Copy full SHA for 44599fc

• AL complete

  

  GuoDCZ

  committed
  f059c18

  Copy full SHA for f059c18

Commits on Sep 2, 2024

• ALF logic

  

  钟之尧

  authored and

  钟之尧

  committed
  c33e40a

  Copy full SHA for c33e40a

• ALFp logic

  

  钟之尧

  authored and

  钟之尧

  committed
  8e26c59

  Copy full SHA for 8e26c59

• bidirectional type system

  

  钟之尧

  authored and

  钟之尧

  committed
  0257f00

  Copy full SHA for 0257f00

• ALFA logic

  

  ZhiyaoZhong

  committed
  8cba4a3

  Copy full SHA for 8cba4a3

• simplify derivation failure format

  

  ZhiyaoZhong

  committed
  45e2a8d

  Copy full SHA for 45e2a8d

Commits on Sep 3, 2024

• improve unbox GADT

  

  ZhiyaoZhong

  committed
  8027e40

  Copy full SHA for 8027e40

Commits on Sep 4, 2024

• ALFA refine collection/ rule verf.

  

  ZhiyaoZhong

  committed
  d4f3204

  Copy full SHA for d4f3204

• alfa form initial

  

  ZhiyaoZhong

  committed
  4883822

  Copy full SHA for 4883822

Commits on Sep 5, 2024

• use ninja-keys for rules palette

  

  ZhiyaoZhong

  committed
  221368b

  Copy full SHA for 221368b

Commits on Sep 9, 2024

• introduce verfication ghost; fix UI failure

  

  ZhiyaoZhong

  committed
  4c3343c

  Copy full SHA for 4c3343c

• arch frontend progress

  

  ZhiyaoZhong

  committed
  b3490df

  Copy full SHA for b3490df

Commits on Sep 11, 2024

• of drv sort input

  

  ZhiyaoZhong

  committed
  492b549

  Copy full SHA for 492b549

• New Sort proted. fix remolding issue partially.

  

  ZhiyaoZhong

  committed
  0fcad1e

  Copy full SHA for 0fcad1e

Commits on Sep 13, 2024

• for editor view backup

  

  ZhiyaoZhong

  committed
  e6d97f0

  Copy full SHA for e6d97f0

• switch explainthis mode

  

  ZhiyaoZhong

  committed
  5b4ee35

  Copy full SHA for 5b4ee35

Commits on Sep 15, 2024

• good init for sidebar

  

  ZhiyaoZhong

  committed
  1b56ad2

  Copy full SHA for 1b56ad2

• drv frontend upgrade

  

  ZhiyaoZhong

  committed
  20b9986

  Copy full SHA for 20b9986

Commits on Sep 16, 2024

• poor solution to remold issue

  

  ZhiyaoZhong

  committed
  8c2142c

  Copy full SHA for 8c2142c

• temp fix remolding issue: mk jdmt term op

  

  ZhiyaoZhong

  committed
  9951da3

  Copy full SHA for 9951da3

• leave up storing comment

  

  ZhiyaoZhong

  committed
  e6fcd4a

  Copy full SHA for e6fcd4a

• fast trial serialize

  

  ZhiyaoZhong

  committed
  5878da5

  Copy full SHA for 5878da5

• fix reload failure issue

  

  ZhiyaoZhong

  committed
  14cd36a

  Copy full SHA for 14cd36a

• build explainthis

  

  ZhiyaoZhong

  committed
  711d5e1

  Copy full SHA for 711d5e1

Commits on Sep 17, 2024

• refine styling issue drv tree

  

  ZhiyaoZhong

  committed
  452aeb1

  Copy full SHA for 452aeb1

• refine for demo

  

  ZhiyaoZhong

  committed
  4c964f5

  Copy full SHA for 4c964f5

• fix patch exercise issue

  

  ZhiyaoZhong

  committed
  241d59e

  Copy full SHA for 241d59e

• severe bugs fix

  

  ZhiyaoZhong

  committed
  8c6f7d9

  Copy full SHA for 8c6f7d9

Commits on Sep 20, 2024

• prop&exp var binding

  

  ZhiyaoZhong

  committed
  70abfdc

  Copy full SHA for 70abfdc

• Merge branch 'dev' into derivation

  

  ZhiyaoZhong

  committed
  a9e1c83

  Copy full SHA for a9e1c83

• improve ninja-keys search keywords

  

  ZhiyaoZhong

  committed
  b3c68df

  Copy full SHA for b3c68df

• change hasty to typ, check all rules except S/A

  

  ZhiyaoZhong

  committed
  4242234

  Copy full SHA for 4242234

Commits on Sep 30, 2024

• fix tylr parsing

  

  ZhiyaoZhong

  committed
  ba3914a

  Copy full SHA for ba3914a

Commits on Oct 3, 2024

• intro new sort ctxt

  

  ZhiyaoZhong

  committed
  d75978d

  Copy full SHA for d75978d

Commits on Oct 4, 2024

• merge sort

  

  ZhiyaoZhong

  committed
  2be1b1f

  Copy full SHA for 2be1b1f

• update jdmt writing term

  

  ZhiyaoZhong

  committed
  85d8a89

  Copy full SHA for 85d8a89

Commits on Oct 6, 2024

• tv

  

  ZhiyaoZhong

  committed
  1b3957b

  Copy full SHA for 1b3957b

Commits on Oct 7, 2024

• fix typ abbr error

  

  ZhiyaoZhong

  committed
  c77652e

  Copy full SHA for c77652e

• merge to dev

  

  ZhiyaoZhong

  committed
  0c57035

  Copy full SHA for 0c57035

• fix refresh issue, add more example

  

  ZhiyaoZhong

  committed
  1574e73

  Copy full SHA for 1574e73

Commits on Oct 8, 2024

• add demo derivation

  

  ZhiyaoZhong

  committed
  692c784

  Copy full SHA for 692c784

Commits on Oct 15, 2024

• rebase rule spec

  

  ZhiyaoZhong

  committed
  ccf42ad

  Copy full SHA for ccf42ad

• fix rebase minor

  

  ZhiyaoZhong

  committed
  67b3853

  Copy full SHA for 67b3853

• fix test

  

  ZhiyaoZhong

  committed
  1b83caa

  Copy full SHA for 1b83caa

Commits on Oct 25, 2024

• gradual ALFA

  

  ZhiyaoZhong

  committed
  8e741b1

  Copy full SHA for 8e741b1

• version select

  

  ZhiyaoZhong

  committed
  a3931ec

  Copy full SHA for a3931ec

• fix alfa_rul critical issue

  

  ZhiyaoZhong

  committed
  1c94c9d

  Copy full SHA for 1c94c9d

Commits on Oct 30, 2024

• fix cache error

  

  ZhiyaoZhong

  committed
  d026fa7

  Copy full SHA for d026fa7

• fix matched_arrow symbol inconssitent

  

  ZhiyaoZhong

  committed
  4a1df72

  Copy full SHA for 4a1df72

• fix on-load no-parse on treeroot

  

  ZhiyaoZhong

  committed
  bd019e1

  Copy full SHA for bd019e1

• temp fix on weird version select error

  

  ZhiyaoZhong

  committed
  ae15735

  Copy full SHA for ae15735

Commits on Oct 31, 2024

• merge to dev

  

  ZhiyaoZhong

  committed
  9e9ea30

  Copy full SHA for 9e9ea30

Commits on Nov 7, 2024

• fix selected deduction style

  

  ZhiyaoZhong

  committed
  bece313

  Copy full SHA for bece313

Commits on Nov 22, 2024

• accommondate free abbr var:

  

  ZhiyaoZhong

  committed
  92da61d

  Copy full SHA for 92da61d

Commits on Dec 23, 2024

• half merge

  

  ZhiyaoZhong

  committed
  d81eb80

  Copy full SHA for d81eb80

Commits on Jan 10, 2025

• merge to dev

  

  ZhiyaoZhong

  committed
  5110b0f

  Copy full SHA for 5110b0f

Commits on Jan 13, 2025

• fix sidebar backend; recons ex; recons cache

  

  ZhiyaoZhong

  committed
  a51f79c

  Copy full SHA for a51f79c

Commits on Jan 22, 2025

• fix elab/statics/explainview/highlights for derivations

  

  ZhiyaoZhong

  committed
  eb2ceec

  Copy full SHA for eb2ceec

• merge to dev

  

  ZhiyaoZhong

  committed
  8d19b39

  Copy full SHA for 8d19b39

Commits on Jan 26, 2025

• fix a few bugs

  

  ZhiyaoZhong

  committed
  f9523a2

  Copy full SHA for f9523a2

• rewrite maketerm drv logic

  

  ZhiyaoZhong

  committed
  094d7e1

  Copy full SHA for 094d7e1

• code clean up

  

  ZhiyaoZhong

  committed
  d0dedf4

  Copy full SHA for d0dedf4

• merge to dev

  

  ZhiyaoZhong

  committed
  c1e2481

  Copy full SHA for c1e2481

Commits on Jan 27, 2025

• drv complete doc/example; ready for review

  

  ZhiyaoZhong

  committed
  67d0983

  Copy full SHA for 67d0983

Commits on Feb 14, 2025

• merge - dev

  

  ZhiyaoZhong

  committed
  01f3a7f

  Copy full SHA for 01f3a7f

Commits on Feb 20, 2025

• remove drvsymbols (buggy version)

  

  ZhiyaoZhong

  committed
  0e645ec

  Copy full SHA for 0e645ec

• fix mold err; fix drv transistion error

  

  ZhiyaoZhong

  committed
  f3ec13a

  Copy full SHA for f3ec13a

• merge ut dev

  

  ZhiyaoZhong

  committed
  a75b610

  Copy full SHA for a75b610

Commits on Feb 21, 2025

• rebase rule spec

  

  ZhiyaoZhong

  committed
  1362b62

  Copy full SHA for 1362b62

Commits on Mar 1, 2025

• merge to dev; fix drv deco color

  

  ZhiyaoZhong

  committed
  2d715ba

  Copy full SHA for 2d715ba

Commits on Mar 2, 2025

• fix typhole form/maketerm; fix multihole exptoseg

  

  ZhiyaoZhong

  committed
  fec5df9

  Copy full SHA for fec5df9

• fix precedence err

  

  ZhiyaoZhong

  committed
  f33ffe2

  Copy full SHA for f33ffe2

• fix transist function parse err

  

  ZhiyaoZhong

  committed
  7b365db

  Copy full SHA for 7b365db

Commits on Mar 7, 2025

• try fix hole issue

  

  ZhiyaoZhong

  committed
  2409c2d

  Copy full SHA for 2409c2d

• fix re-eval

  

  ZhiyaoZhong

  committed
  8a95813

  Copy full SHA for 8a95813

• refine hole case report; drvgrading exception

  

  ZhiyaoZhong

  committed
  4efe240

  Copy full SHA for 4efe240

• close eval result when setting dynamic is off

  

  ZhiyaoZhong

  committed
  b74681e

  Copy full SHA for b74681e

• write test pp

  

  ZhiyaoZhong

  committed
  7dc51a6

  Copy full SHA for 7dc51a6

• Merge branch 'dev' of github.com:hazelgrove/hazel into derivation

  

  ZhiyaoZhong

  committed
  ae8f838

  Copy full SHA for ae8f838

• fix drv doc (in a way I dont like)

  

  ZhiyaoZhong

  committed
  8191019

  Copy full SHA for 8191019

Commits on Mar 8, 2025

• fix color highlit same id err

  

  ZhiyaoZhong

  committed
  d7635bf

  Copy full SHA for d7635bf

• fix subst/substty sort inconsistency

  

  ZhiyaoZhong

  committed
  91661ba

  Copy full SHA for 91661ba

• fix ignore case cant show

  

  ZhiyaoZhong

  committed
  d678a96

  Copy full SHA for d678a96

• refactor test style

  

  ZhiyaoZhong

  committed
  37d75da

  Copy full SHA for 37d75da

Commits on Mar 9, 2025

• feat ninjakeys only show opts of curr ver

  

  ZhiyaoZhong

  committed
  0c64d6d

  Copy full SHA for 0c64d6d