WIP: canonical structures compilation - #1045

Draft

FissoreD wants to merge 62 commits into

LPCIC:masterfrom

Commits on Jul 20, 2026

fix bug in term decompilation
FissoreD
committed
1b585bc
class mode attribute
FissoreD
committed
9dd46c2
class mode attribute
FissoreD
committed
7b903cb
add comment to ho_compile
FissoreD
committed
8eebf5e
fix bench.py
FissoreD
committed
d3c7645
bench all
FissoreD
committed
8016d0e
bench
FissoreD
committed
08597ba
plot elpi stats
FissoreD
committed
b46f202
fix rebase
FissoreD
committed
d247bac
links for cs
FissoreD
committed
87db2fe
more on projections
FissoreD
committed
5b3abcf
add comment to code
FissoreD
committed
44ee00c
externalize get-vars
FissoreD
committed
badd8b5
some fixes
FissoreD
committed
990359d
fix variable scoping in compiled rule
FissoreD
committed
db26cdc
do notcle link-proj opaque constants + coq.env.const-body instead of coq.reduction.cbv.norm
FissoreD
committed
eb1eda1
refactor code
FissoreD
committed
decf030
fix proj number (with get-proj-nb)
FissoreD
committed
956130b
proj-reducer for names
FissoreD
committed
e846e61
wip cs.elpi
FissoreD
committed
cf9f7c2
fix tests
FissoreD
committed
5255269
remove empty line
FissoreD
committed
05c67b8
remove empty line
FissoreD
committed
70ba27c
add main to cs
FissoreD
committed
8f657f0
imporve cs comment
FissoreD
committed
c916803
extract common code in ho_precompile for reusability
FissoreD
committed
75e62c5
add solve_cs tactic
FissoreD
committed
618753e
remove range-arity since unused
FissoreD
committed
06f93ff
rename and comment max-arity-aux
FissoreD
committed
a6399e7
clean get-max-arity-aux
FissoreD
committed
74d2718
add comment to get-max-arity
FissoreD
committed
b9bfc4b
align comment
FissoreD
committed
561756a
collapse namespace in ho_compile
FissoreD
committed
374940b
curry decompile-term-aux
FissoreD
committed
cd54eb5
clean sig of fold-map2
FissoreD
committed
461b22b
externalize decomp-term from fold-map
FissoreD
committed
508ec64
ho_compile share common code
FissoreD
committed
5115749
add doc precompile-aux of instances
FissoreD
committed
ac6672f
move fold-map2 in base.elpi
FissoreD
committed
a6bf2fe
complete pattern matching for precompile-aux in instances
FissoreD
committed
870d3ba
namespace in ho_link
FissoreD
committed
e46bedd
rework constr maybe-proj + first integration of tc with cs using ad-hoc predicates
FissoreD
committed
1d6723d
remove main in solver.elpi
FissoreD
committed
b282d71
use coq.CS.canonical-projection? to check if the constant refers to a canonical projection
FissoreD
committed
88186a1
remove call to solver main in bench_inj.v
FissoreD
committed
6a24165
cs compile only canonical projection predicates
FissoreD
committed
8c22eff
cs input mode in predicate declaration
FissoreD
committed
57ad4f8
cs main error message on wrong input
FissoreD
committed
651d73b
rm map-filter2 (already in stdlib)
FissoreD
committed
b5de436
forall-ocan to iter over a list of option constant
FissoreD
committed
3981447
tc.link.proj for all projection
FissoreD
committed
a0e5343
check-pname
FissoreD
committed
17fa7d9
simpl decompile of proj link
FissoreD
committed
723720f
cs start plug with tc
FissoreD
committed
0bc4e80
remove prod-range
FissoreD
committed
3198110
fix lex error
FissoreD
committed
daddcf5
kill cs default + clean tc.maybe-llam
FissoreD
committed
8ab0a77
add tc prems to cs
FissoreD
committed
a10fff7
record constructor compiler for cs
FissoreD
committed
3d31cb4
add tests in test_proj
FissoreD
committed
399a415
link.proj is a func (not pred) + add build-proj-app
FissoreD
committed
334a0e7
add solve to cs
FissoreD
committed
a32364a