Code

TC solver 2#529

Code

Merged

gares merged 65 commits intomasterLPCIC/coq-elpi:masterfrom master-tcLPCIC/coq-elpi:master-tcCopy head branch name to clipboardNov 7, 2023

+7,231-19

Commits

Commits on Nov 7, 2023

• version1 tc

  

  FissoreD

  authored and

  gares

  committed
  ca6a78b

• version2 tc: first test passes

  

  FissoreD

  authored and

  gares

  committed
  b52a0b8

• version3: add tests

  

  FissoreD

  authored and

  gares

  committed
  2e8449e

• Delete apps/tc/README.md

  gares

  committed
  69061fb

• Apply suggestions from code review

  gares

  committed
  6746b35

• Update apps/tc/Makefile.coq.local

  gares

  committed
  f8c975b

• wip

  gares

  committed
  c29b9a3

• skeleton observer

  gares

  committed
  6fe9f93

• inst&classes auto inserted in db of elpi

  

  FissoreD

  authored and

  gares

  committed
  da1328e

• move comment

  

  FissoreD

  authored and

  gares

  committed
  fb3d944

• Update get_instances order

  

  FissoreD

  authored and

  gares

  committed
  8b5672b

• Persistent register

  

  FissoreD

  authored and

  gares

  committed
  ffb669a

• rm generated file

  gares

  committed
  5af5df1

• pass a term

  gares

  committed
  ff4758f

• ignore generated file

  gares

  committed
  7c7e5c1

• Refactor instance/class observer

  

  FissoreD

  authored and

  gares

  committed
  825c084

• Ok all tests + correct instance insertion order

  

  FissoreD

  authored and

  gares

  committed
  e3953ff

• WIP: tc-for2 returns tc-instnce

  

  FissoreD

  authored and

  gares

  committed
  8a36c1b

• fun to get prio of an inst

  

  FissoreD

  authored and

  gares

  committed
  14bc7a9

• function rename

  

  FissoreD

  authored and

  gares

  committed
  9973e59

• Small correction for no-argument classes

  

  FissoreD

  authored and

  gares

  committed
  fb49b26

• uniform API

  gares

  committed
  5e74cdc

• fix paths for vscoq

  gares

  committed
  bcdecdc

• wip section ending

  gares

  committed
  e5be2a6

• OK for Instances recompilation on section end

  

  FissoreD

  authored and

  gares

  committed
  d78cc02

• small test for locality in #[...] style

  

  FissoreD

  authored and

  gares

  committed
  ec852b4

• Correct behavior of #{export]

  

  FissoreD

  authored and

  gares

  committed
  c94d7d8

• auto_compiler in tc.v

  

  FissoreD

  authored and

  gares

  committed
  aabcbc1

• Add licences in TC sources

  

  FissoreD

  authored and

  gares

  committed
  6d988b3

• remove :index(X) from tc.v

  

  FissoreD

  authored and

  gares

  committed
  d8491c3

• comment

  

  FissoreD

  authored and

  gares

  committed
  1c2f489

• Add path for plugin in CoqProject

  

  FissoreD

  authored and

  gares

  committed
  02a064a

• Mv function for takeover in separate file

  

  FissoreD

  authored and

  gares

  committed
  292326b

• Update test wrt to previous commit

  

  FissoreD

  authored and

  gares

  committed
  81a8dee

• Modify commad addHook to add custom hooks

  

  FissoreD

  authored and

  gares

  committed
  2570e8c

• Mv rew_forward and alias to wip

  

  FissoreD

  authored and

  gares

  committed
  9bcc96b

• option in namespace + separated db for them

  

  FissoreD

  authored and

  gares

  committed
  1b25399

• vscode hide .melin file

  

  FissoreD

  authored and

  gares

  committed
  73e453a

• no elpi folder in coercion

  

  FissoreD

  authored and

  gares

  committed
  f9a5b9a

• clean Makefile.coq.local for tc

  

  FissoreD

  authored and

  gares

  committed
  e8fe51e

• clean code

  

  FissoreD

  authored and

  gares

  committed
  03776cf

• smal refactor

  

  FissoreD

  authored and

  gares

  committed
  0552fbc

• rename cammand to register compiler

  

  FissoreD

  authored and

  gares

  committed
  74b7fdc

• coq option to activate compiler w/pattern fragment

  

  FissoreD

  authored and

  gares

  committed
  c928bee

• move addAllInstances-Classes ... in dedicated file

  

  FissoreD

  authored and

  gares

  committed
  55cb5ed

• start readme

  

  FissoreD

  authored and

  gares

  committed
  3c50554

• remove tests/mode_no_repetition.v

  

  FissoreD

  authored and

  gares

  committed
  ffb3838

• command get_class_info

  

  FissoreD

  authored and

  gares

  committed
  2eea646

• update solver

  

  FissoreD

  authored and

  gares

  committed
  14eae87

• Update readme

  

  FissoreD

  authored and

  gares

  committed
  f85e7a1

• update instance printer

  

  FissoreD

  authored and

  gares

  committed
  2107837

• readme udpate

  

  FissoreD

  authored and

  gares

  committed
  656fc15

• Update readme

  

  FissoreD

  authored and

  gares

  committed
  3e17855

• Update readme

  

  FissoreD

  authored and

  gares

  committed
  06b111d

• update readme + tutorial.v

  

  FissoreD

  authored and

  gares

  committed
  670cad5

• Update apps/tc/tests/WIP/premisesSort/sort1.v

  gares

  committed
  165fc08

• Update apps/tc/README.md

  gares

  committed
  43b91cd

• fix _CoqProject

  gares

  committed
  8b81fd5

• more tests

  gares

  committed
  80e7705

• wip TC.declare to give attributes on the fly

  gares

  committed
  8e0e87c

• Inst/Class event listener can be (de-)activated

  

  FissoreD

  authored and

  gares

  committed
  d88f683

• Add toposort

  

  FissoreD

  authored and

  gares

  committed
  8d9db9e

• Rename AddXXX commands

  

  FissoreD

  authored and

  gares

  committed
  db249c3

• Rename command with prefix

  

  FissoreD

  authored and

  gares

  committed
  440453e

• Update readme

  

  FissoreD

  authored and

  gares

  committed
  f0a4439