Code

Replace Bindlib by de Bruijn indices#843

Code

Open

fblanqui wants to merge 110 commits intoDeducteam:masterDeducteam/lambdapi:masterfrom fblanqui:dbfblanqui/lambdapi:dbCopy head branch name to clipboard

+1,689-2,102

Commits

Commits on Feb 4, 2022

• add Term.Db constructor

  fblanqui

  committed
  3810bb5

  Copy full SHA for 3810bb5

Commits on Feb 8, 2022

• remove Bindlib from terms (but not rhs)

  fblanqui

  committed
  2dfeb71

  Copy full SHA for 2dfeb71

• change definition of Term.dtree to rule Tree_type.dtree

  fblanqui

  committed
  3434aac

  Copy full SHA for 3434aac

Commits on Feb 14, 2022

• remove Bindlib on rhs

  fblanqui

  committed
  49ec8ab

  Copy full SHA for 49ec8ab

• remove TEnv

  fblanqui

  committed
  7efc5db

  Copy full SHA for 7efc5db

• remove bindlib from dependencies

  fblanqui

  committed
  084ef7a

  Copy full SHA for 084ef7a

• remove mkfree

  fblanqui

  committed
  b522ac7

  Copy full SHA for b522ac7

• remove new_mvar and do not export new_var

  fblanqui

  committed
  23c7397

  Copy full SHA for 23c7397

• remove box type

  fblanqui

  committed
  6730df0

  Copy full SHA for 6730df0

• remove bind_mvar3

  fblanqui

  committed
  170ca77

  Copy full SHA for 170ca77

• Env: rename to_tbox into to_terms

  fblanqui

  committed
  28e2508

  Copy full SHA for 28e2508

• remove fresh_box

  fblanqui

  committed
  02ec00b

  Copy full SHA for 02ec00b

• cli: Term.* -> CLT.*

  fblanqui

  committed
  3a8d502

  Copy full SHA for 3a8d502

• remove bctxt

  fblanqui

  committed
  74aefe9

  Copy full SHA for 74aefe9

• dune-project: use cmdliner <= 1.0.4

  fblanqui

  committed
  d7b6f00

  Copy full SHA for d7b6f00

• lambdapi.opam: use cmdliner <= 1.0.4

  fblanqui

  committed
  b93ccfd

  Copy full SHA for b93ccfd

Commits on Feb 15, 2022

• remove module Bindlib

  fblanqui

  committed
  8ff86cd

  Copy full SHA for 8ff86cd

• renamings: tvar -> var, tbinder -> binder, tmbinder -> mbinder

  fblanqui

  committed
  83b1ec9

  Copy full SHA for 83b1ec9

• call mk_Appl in subst, and reorganize code in term

  fblanqui

  committed
  3376e30

  Copy full SHA for 3376e30

• rename mk_Impl into mk_Arro

  fblanqui

  committed
  2decd3e

  Copy full SHA for 2decd3e

• scope: remove useless call to is_closed

  fblanqui

  committed
  6b5e980

  Copy full SHA for 6b5e980

• fix comment

  fblanqui

  committed
  6fff025

  Copy full SHA for 6fff025

• optimize link/unlink/reset by exposing binder

  fblanqui

  committed
  18e5cd5

  Copy full SHA for 18e5cd5

• remove constraints on bound variable identifiers

  fblanqui

  committed
  4a51e1c

  Copy full SHA for 4a51e1c

Commits on Feb 18, 2022

• fix reset_term

  fblanqui

  committed
  dbecfe9

  Copy full SHA for dbecfe9

• record if a variable is bound

  fblanqui

  committed
  3d6e948

  Copy full SHA for 3d6e948

• details

  fblanqui

  committed
  d46bcab

  Copy full SHA for d46bcab

• details

  fblanqui

  committed
  5f073ca

  Copy full SHA for 5f073ca

• detail

  fblanqui

  committed
  fe9d807

  Copy full SHA for fe9d807

Commits on Feb 22, 2022

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  cfb0ee0

  Copy full SHA for cfb0ee0

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  2b584d3

  Copy full SHA for 2b584d3

Commits on Feb 23, 2022

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  a369ed3

  Copy full SHA for a369ed3

Commits on Feb 24, 2022

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  83e0998

  Copy full SHA for 83e0998

Commits on Mar 17, 2022

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  110eaf7

  Copy full SHA for 110eaf7

Commits on Mar 29, 2022

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  0488ad9

  Copy full SHA for 0488ad9

Commits on May 9, 2022

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  cf4aaef

  Copy full SHA for cf4aaef

Commits on May 12, 2022

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  e4167af

  Copy full SHA for e4167af

Commits on May 18, 2022

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  ead55ce

  Copy full SHA for ead55ce

Commits on May 19, 2022

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  60c75b8

  Copy full SHA for 60c75b8

Commits on Jul 12, 2022

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  eb2c957

  Copy full SHA for eb2c957

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  3bde217

  Copy full SHA for 3bde217

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  e5d646c

  Copy full SHA for e5d646c

Commits on Jul 28, 2022

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  ff0f98e

  Copy full SHA for ff0f98e

Commits on Jul 29, 2022

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  813ae2f

  Copy full SHA for 813ae2f

Commits on Aug 4, 2022

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  d5a25a5

  Copy full SHA for d5a25a5

Commits on Sep 6, 2022

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  6bf38b9

  Copy full SHA for 6bf38b9

Commits on Sep 12, 2022

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  9cc5937

  Copy full SHA for 9cc5937

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  b6eeaa3

  Copy full SHA for b6eeaa3

Commits on Sep 28, 2022

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  65ba575

  Copy full SHA for 65ba575

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  bbc1477

  Copy full SHA for bbc1477

Commits on Dec 28, 2022

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  4085120

  Copy full SHA for 4085120

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  4d8ea21

  Copy full SHA for 4d8ea21

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  d4ef7ad

  Copy full SHA for d4ef7ad

Commits on Dec 30, 2022

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  7eeb49f

  Copy full SHA for 7eeb49f

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  30cd837

  Copy full SHA for 30cd837

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  5329381

  Copy full SHA for 5329381

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  f72ba2f

  Copy full SHA for f72ba2f

Commits on Dec 31, 2022

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  cc114b0

  Copy full SHA for cc114b0

• tests/regressions: update expected output of hrs and xtc

  fblanqui

  committed
  804fc06

  Copy full SHA for 804fc06

• fix dk export

  fblanqui

  committed
  7862dd8

  Copy full SHA for 7862dd8

Commits on Jan 2, 2023

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  7a69b75

  Copy full SHA for 7a69b75

Commits on Jan 11, 2023

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  eb228eb

  Copy full SHA for eb228eb

Commits on Jan 29, 2023

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  7073352

  Copy full SHA for 7073352

Commits on Jan 31, 2023

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  b8980f4

  Copy full SHA for b8980f4

Commits on Feb 27, 2023

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  57d5686

  Copy full SHA for 57d5686

Commits on Mar 12, 2023

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  3807cd1

  Copy full SHA for 3807cd1

Commits on Mar 17, 2023

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  a34cc45

  Copy full SHA for a34cc45

Commits on Mar 30, 2023

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  858f1f3

  Copy full SHA for 858f1f3

Commits on Apr 4, 2023

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  9790ee6

  Copy full SHA for 9790ee6

Commits on Apr 14, 2023

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  4f651f3

  Copy full SHA for 4f651f3

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  7cbc2cd

  Copy full SHA for 7cbc2cd

Commits on Jun 9, 2023

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  a2491c2

  Copy full SHA for a2491c2

• add tests/OK/991.lp

  fblanqui

  committed
  6babc67

  Copy full SHA for 6babc67

Commits on Jun 12, 2023

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  d0b7dde

  Copy full SHA for d0b7dde

Commits on Jul 28, 2023

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  e762e86

  Copy full SHA for e762e86

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  0b16862

  Copy full SHA for 0b16862

Commits on Jul 29, 2023

• update doc

  fblanqui

  committed
  68f62de

  Copy full SHA for 68f62de

Commits on Jul 31, 2023

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  f137ca2

  Copy full SHA for f137ca2

Commits on Aug 1, 2023

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  3a27af9

  Copy full SHA for 3a27af9

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  50a9075

  Copy full SHA for 50a9075

Commits on Sep 15, 2023

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  457a368

  Copy full SHA for 457a368

Commits on Oct 25, 2023

• Merge remote-tracking branch 'lp/master' into db

  fblanqui

  committed
  e7ce853

  Copy full SHA for e7ce853

Commits on Nov 7, 2023

• Merge remote-tracking branch 'dk/master' into db

  fblanqui

  committed
  0db4750

  Copy full SHA for 0db4750

Commits on Nov 11, 2023

• Merge remote-tracking branch 'dk/master' into db

  fblanqui

  committed
  4a3df34

  Copy full SHA for 4a3df34

Commits on Dec 19, 2023

• Merge remote-tracking branch 'dk/master' into db

  fblanqui

  committed
  24a54e8

  Copy full SHA for 24a54e8

Commits on Jan 26, 2024

• enforce locally nameless convention (never deal with terms containing free de Bruijn indices) of Term interface + avoid some unnecessary relocations

  barras

  committed
  c74325b

  Copy full SHA for c74325b

Commits on Feb 22, 2024

• Enforce locally nameless convention (Bruno)

  fblanqui

  authored
  2eb6850

  Copy full SHA for 2eb6850

• spaces

  fblanqui

  committed
  d987930

  Copy full SHA for d987930

• Merge remote-tracking branch 'dk/master' into db

  fblanqui

  committed
  6094505

  Copy full SHA for 6094505

Commits on Feb 28, 2024

• Merge remote-tracking branch 'dk/master' into db

  fblanqui

  committed
  07b05ea

  Copy full SHA for 07b05ea

Commits on Mar 1, 2024

• Merge remote-tracking branch 'dk/master' into db

  fblanqui

  committed
  dad144c

  Copy full SHA for dad144c

• exclude 991 in tests/export_raw_dk.sh

  fblanqui

  committed
  2890ad1

  Copy full SHA for 2890ad1

Commits on Mar 19, 2024

• Merge remote-tracking branch 'dk/master' into db

  fblanqui

  committed
  b00961f

  Copy full SHA for b00961f

Commits on Mar 29, 2024

• remove tests related to identifier restrictions due to bindlib

  fblanqui

  committed
  7dd3baa

  Copy full SHA for 7dd3baa

• Merge remote-tracking branch 'dk/master' into db

  fblanqui

  committed
  641a46c

  Copy full SHA for 641a46c

Commits on Apr 23, 2024

• Merge remote-tracking branch 'dk/master' into db

  fblanqui

  committed
  4f260a9

  Copy full SHA for 4f260a9

Commits on Apr 30, 2024

• Merge remote-tracking branch 'dk/master' into db

  fblanqui

  committed
  fa42a15

  Copy full SHA for fa42a15

Commits on May 3, 2024

• Merge remote-tracking branch 'dk/master' into db

  fblanqui

  committed
  f58c24f

  Copy full SHA for f58c24f

Commits on Jun 24, 2024

• Merge remote-tracking branch 'dk/master' into db

  fblanqui

  committed
  4b4bcf7

  Copy full SHA for 4b4bcf7

• Merge remote-tracking branch 'dk/master' into db

  fblanqui

  committed
  6e123bd

  Copy full SHA for 6e123bd

Commits on Aug 30, 2024

• Merge remote-tracking branch 'dk/master' into db

  fblanqui

  committed
  7757b36

  Copy full SHA for 7757b36

Commits on Oct 30, 2024

• Merge remote-tracking branch 'dk/master' into db

  fblanqui

  committed
  bdba910

  Copy full SHA for bdba910

Commits on Nov 11, 2024

• Merge remote-tracking branch 'dk/master' into db

  fblanqui

  committed
  e9ea382

  Copy full SHA for e9ea382

Commits on Jan 2, 2025

• Merge remote-tracking branch 'dk/master' into db

  fblanqui

  committed
  adcbe71

  Copy full SHA for adcbe71

Commits on Jan 9, 2025

• Merge remote-tracking branch 'dk/master' into db

  fblanqui

  committed
  d130b40

  Copy full SHA for d130b40

• finalize merge

  fblanqui

  committed
  f22cd05

  Copy full SHA for f22cd05

Commits on Jan 24, 2025

• Merge remote-tracking branch 'dk/master' into db

  fblanqui

  committed
  37daab0

  Copy full SHA for 37daab0

Commits on Jan 25, 2025

• Merge remote-tracking branch 'dk/master' into db

  fblanqui

  committed
  b0349f3

  Copy full SHA for b0349f3

Commits on Jan 27, 2025

• Merge remote-tracking branch 'dk/master' into db

  fblanqui

  committed
  565fcbe

  Copy full SHA for 565fcbe

Commits on Jan 28, 2025

• Merge remote-tracking branch 'dk/master' into db

  fblanqui

  committed
  ebcfaed

  Copy full SHA for ebcfaed