Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[refactor] instance declaration #376

Open
wants to merge 147 commits into
base: master
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
147 commits
Select commit Hold shift + click to select a range
567cee2
[refactor] separate add-mixin and make-mixin-canonical
gares Aug 1, 2023
64525c7
[instance] declare-instance -> declare-mixins-from-factory + declare-…
gares Aug 2, 2023
e0f7895
document exported-op
gares Aug 2, 2023
8c4071c
[instance] test for structure op as subject
gares Aug 2, 2023
6128f44
comment
gares Aug 2, 2023
1f8ca63
add comment
gares Aug 3, 2023
2ce532b
wip-wrapping
gares Aug 3, 2023
f12d772
minor changes
ptorrx Aug 3, 2023
d3273a4
minor changes in instance.elpi
ptorrx Aug 3, 2023
894aff0
introduced derived instance check in instance.elpi (as a hack); still…
ptorrx Aug 3, 2023
1ecb634
fixed bugs in instance.elpi, compiles
ptorrx Aug 4, 2023
cb3d53a
minor changes
ptorrx Aug 4, 2023
2fc6662
added and updated cmon_enriched_cat.v - this file contains three exam…
ptorrx Aug 10, 2023
c002312
fixed bug in cmonoid_enriched_cat.v
ptorrx Aug 24, 2023
46d5932
revised tests/cmonoid_enriched_cat.v
ptorrx Aug 28, 2023
ed74a82
cleanup
gares Sep 25, 2023
3e040b4
eta expand wrapped mixing in context
gares Sep 25, 2023
19fd228
minimal test for parameters
gares Sep 26, 2023
2d94c60
plan for auto wrapping
gares Sep 26, 2023
df1d865
added enriched_cat_case1.v - problematic
ptorrx Oct 3, 2023
ffce0b9
added enriched_cat_case2.v - which works, but wraps without depencies…
ptorrx Oct 3, 2023
f6e4458
added enriched_cat_case4.v
ptorrx Oct 3, 2023
9aebc2b
updated examples
ptorrx Oct 3, 2023
3ef5a1f
updated enriched_cat_case1.v, there are still problems
ptorrx Oct 3, 2023
96a6113
updated enriched_cat_case4.v, not finished but less problematic
ptorrx Oct 3, 2023
1292d1e
fix generation of wrapper-mixin when the mixin has deps
gares Oct 4, 2023
457817c
add more tests
gares Oct 4, 2023
66eb897
cleanup
gares Oct 4, 2023
41da96e
added enriched_cat_case5.v with more cases
ptorrx Oct 4, 2023
30debed
completed enriched_cat_case4.v
ptorrx Oct 4, 2023
7d113d0
note
gares Oct 4, 2023
d3dce62
validate structure declaration and wrap is the wrapper already exists
gares Oct 4, 2023
cad4f20
a bit unsure about this, it looks too smart in some cases
gares Oct 4, 2023
4e80aff
added enriched_cat_case6.v
ptorrx Oct 4, 2023
353b3fd
wip
gares Oct 4, 2023
d343316
fix rebase
gares Oct 5, 2023
063ffc3
fix failsafe structure inference
gares Oct 5, 2023
1d18979
fix test for wrapping
gares Oct 5, 2023
8f2d47d
cleanup
gares Oct 5, 2023
7e41346
cleanup
gares Oct 5, 2023
fb93fbe
option wrapper=off to instance
gares Oct 6, 2023
4c2742c
demo should not break abstractions
gares Oct 4, 2023
bd83789
test
gares Oct 6, 2023
d1c8070
moving category theory to theories
CohenCyril Oct 6, 2023
b73828c
defining pullbacks
CohenCyril Oct 6, 2023
2e25e5c
fix Makefile
gares Oct 6, 2023
cb9cfb0
colors are proofs
gares Oct 6, 2023
feb9249
HB.tag
gares Oct 6, 2023
a180918
remove ELIM hack
gares Oct 6, 2023
450cf7e
cleanup
gares Oct 6, 2023
79aba6c
fix test
gares Oct 6, 2023
8ac8c9d
note
gares Oct 6, 2023
2a39460
fix HB.tag
gares Oct 6, 2023
a2bf6d4
FIX: toposort will always be buggy ;-)
gares Oct 6, 2023
922d6b9
better eta expansion for failsafe structure elab
gares Oct 6, 2023
7005440
CAT: use HB.tag for pb_terminal (the wrapper is not autogen, but coul…
gares Oct 6, 2023
e24e3a1
use subject-lifter instead of structure-op
gares Oct 6, 2023
81fe41f
document toposort bug
gares Oct 6, 2023
da52021
Enter HB.from (from factories)
gares Oct 6, 2023
8d40177
fix rebase
gares Oct 9, 2023
d7007d3
added theories/encat.v (formalization of enriched categories, in prog…
ptorrx Oct 18, 2023
09618b3
updated theories/encat.v
ptorrx Oct 19, 2023
edb0313
updated theories/encat.v; definitions of enriched category and (tenta…
ptorrx Oct 20, 2023
02b0fc5
updated theories/encat.v
ptorrx Oct 22, 2023
75d8bfe
encat.v: fixed the definition of enriched category (reversed dependen…
ptorrx Oct 24, 2023
b415e67
encat.v: basic update of double categories
ptorrx Oct 24, 2023
de22884
encat.v: minor changes in comment
ptorrx Oct 24, 2023
5531d11
encat.v: added Cyril's definition of double categories
ptorrx Oct 24, 2023
b3dd85d
encat.v: revised parametrisation in enriched categories; revised defi…
ptorrx Oct 25, 2023
00c66a9
encat.v: minor changes
ptorrx Oct 25, 2023
31843f2
encat.v: updates to dcat transposition
ptorrx Oct 25, 2023
73a9732
encat.v: minor changes
ptorrx Oct 26, 2023
995fef1
encat.v: fixed unit functor problem (by changing the definition of un…
ptorrx Oct 26, 2023
b1f88ea
encat.v: adding composition - however, it seems more problematic than…
ptorrx Oct 26, 2023
d0014ce
encat.v: adding horizontal cell composition (tough)
ptorrx Oct 27, 2023
5c9bac2
updated encav.v
ptorrx Nov 3, 2023
3fb6dde
updated encav.v; flat version with 4 functors (source, target, horizo…
ptorrx Nov 3, 2023
e2536bc
updated encav.v; still missing: associator; product category to be fixed
ptorrx Nov 6, 2023
9c092de
updated encav.v; nlab-style definition of double categories; still mi…
ptorrx Nov 7, 2023
d158ffc
updated encav.v
ptorrx Nov 7, 2023
5220df5
updated encav.v; improved some definitions
ptorrx Nov 7, 2023
f7a0d99
updated encav.v; version with transpose
ptorrx Nov 8, 2023
6074c78
updated encav.v; improved a definition
ptorrx Nov 8, 2023
0d19f51
updated encav.v; minor changes
ptorrx Nov 8, 2023
64d354c
updated encav.v; added (alternative definitions of) horizontal 2-cell…
ptorrx Nov 9, 2023
1da3981
added encatA.v, older version for experiments on instantiation. minor…
ptorrx Nov 9, 2023
6a942fb
updated encav.v; in progress
ptorrx Nov 9, 2023
429865c
updated encav.v; discharged product precategory assumptions (still to…
ptorrx Nov 10, 2023
7f79278
added encatB.v: complete formalization of double categories, without …
ptorrx Nov 14, 2023
c26463b
encatB.v: cleaned up the definition of strict double category; the de…
ptorrx Nov 15, 2023
5faa745
encatB.v: improving the proofs
ptorrx Nov 16, 2023
a5e0e21
encatB.v: improving the notation
ptorrx Nov 16, 2023
d2e0580
encatB.v: renamed definition to be consistent with slide presentation
ptorrx Nov 19, 2023
6fdcfb5
added encatD.v (starting with internal categories)
ptorrx Nov 24, 2023
5cb88f9
updated encatD.v
ptorrx Nov 27, 2023
7a60a01
updated encatD.v, added definition of internal category based on oper…
ptorrx Nov 28, 2023
45565f9
updated encatD.v, complete definition of internal category based on NLab
ptorrx Nov 29, 2023
0fcd38c
updated encatD.v, minor changes
ptorrx Nov 29, 2023
a2757c4
mono/epi code works now
CohenCyril Nov 20, 2023
d42cc3e
walking span
CohenCyril Nov 23, 2023
dc4548e
rephrasing adjunctions (needs wrapping)
CohenCyril Nov 30, 2023
b00a244
internal categories parametrized with the ambiant one
CohenCyril Nov 30, 2023
4151369
updated encatD.v
ptorrx Dec 7, 2023
fc63ca4
updated encatD.v
ptorrx Dec 8, 2023
f661ea2
updated encatD.v, added encatD1.v; open problems in both
ptorrx Dec 8, 2023
6284697
updated encatD.v
ptorrx Dec 12, 2023
9560c9f
updated encatD.v
ptorrx Dec 13, 2023
b0444ce
added encatI.v, which merges new version of cat.v with internal categ…
Dec 14, 2023
f1325d7
updated encatI.v
Dec 15, 2023
527dd0f
updated encatI.v
Dec 18, 2023
c820234
updated encatI.v
Dec 18, 2023
1e0aa1b
updated encatI.v
Dec 19, 2023
eb7d3eb
updated encatI.v
Dec 19, 2023
9974744
updated encatI.v
Dec 21, 2023
f81757d
updated encatI.v; added encatI0.v as experiment
Dec 22, 2023
ab63881
updated encatI.v
ptorrx Jan 9, 2024
3459991
updated encatI.v
Jan 10, 2024
ca8bffd
updated encatI.v
Jan 11, 2024
82e72d6
updated encatI.v
Jan 11, 2024
f1ab058
updated encatI.v; complete definition of double cat based on internal…
Jan 12, 2024
9ff3448
updated encatI.v; cleaning up
Jan 12, 2024
d9c6869
updated encatI.v; merged in the strict double category direct definit…
Jan 12, 2024
41ad7c1
updated comment in encatI.v
Jan 12, 2024
40f762b
updated comment in encatI.v
Jan 12, 2024
c4724d7
changes in encatI0.v
Jan 16, 2024
6570167
encatI.v and encatI0.v now depend on cat.v
Jan 16, 2024
deb0352
updated encatI.v
Jan 17, 2024
11e40e2
updated encatI.v
Jan 18, 2024
4292494
updated encatI.v
Jan 19, 2024
b21e282
updated encatI.v
Jan 19, 2024
2167b3d
restructuring
ptorrx Jan 18, 2024
a2cc722
restructuring
ptorrx Jan 18, 2024
e84c91f
updated encatI.v
Jan 19, 2024
3564fd6
updated dependencies
Jan 19, 2024
1ce5b11
updated dependencies
Jan 19, 2024
d94c19f
updated encatI.v
Jan 19, 2024
d88dd20
wip
gares Jan 29, 2024
b9cb11f
wip
gares Jan 29, 2024
f2590ab
unsafe(univ) option
gares Jan 31, 2024
e8a680c
wip
gares Jan 31, 2024
18ca7ba
wip
gares Feb 2, 2024
59af016
wip
gares Feb 2, 2024
e19ed85
wip
gares Mar 4, 2024
10b3fb0
wip
gares Mar 4, 2024
af2989f
wip
gares Mar 4, 2024
0cf1c4c
wip
gares Mar 4, 2024
e85441c
wip
gares Mar 4, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
fix failsafe structure inference
gares committed Jan 22, 2024
commit 063ffc3811b2124ed87a0dca1dc3ac393ede0c5f
16 changes: 9 additions & 7 deletions HB/common/utils.elpi
Original file line number Diff line number Diff line change
@@ -317,16 +317,18 @@ re-enable-id-phant T T1 :-

pred failsafe-structure-inference i:term, o:term.
failsafe-structure-inference T T1 :-
(pi OP Args Args1\
(pi OP Args Args1 M Class NP S\
copy (app [global (const OP)|Args]) (app [global (const OP)| Args1]) :-
exported-op _ _ OP, !, eta-structure-record OP Args Args1) =>
exported-op M _ OP, mixin-first-class M Class, factory-nparams Class NP,
std.nth NP Args S,
var S,
!,
eta-structure-record NP Class Args Args1) =>
copy T T1.

pred eta-structure-record i:constant, i:list term, o:list term.
eta-structure-record OP L L1 :-
exported-op M _ OP, mixin-first-class M Class, factory-nparams Class NP,
std.split-at NP L Params [S|Rest],
var S,
pred eta-structure-record i:int, i:classname, i:list term, o:list term.
eta-structure-record NP Class L L1 :-
std.split-at NP L Params [_|Rest],
class-def (class Class Structure _),
get-constructor Structure K,
std.map Params copy Params1,