595aedf8dc
Merge branch 'topic-parser' into dev
2025-07-13 16:15:12 +02:00
4b898a2a9c
fix pnf: when collapsing seq-repr check if item types overlap, not just if they are equal
2025-07-13 16:13:07 +02:00
8161db46f0
refactor ConstraintPair & TypeTerm::Univ
...
- TypeTerm::Seq: switch from Vec to single, Boxed item type
- parsing of generalized constraints
2025-07-13 16:13:07 +02:00
968db99507
parser: add parsing of sugared func/morph arrows
2025-07-13 16:13:07 +02:00
d14f3310ed
lexer: add arrow tokens
2025-07-13 16:13:07 +02:00
7d8cfa74d1
parser: add parsing of sugared enums
2025-07-13 16:13:07 +02:00
916ac19464
begin extending parser
...
- remove DesugaredTypeTerm
- add lexer tokens for sugared type terms
- parse sugared seq- & struct- types
- parse ∀-types
todo: parse enums, parse function/morph types, how to handle context of bound varaibles in parser?
2025-07-13 16:13:07 +02:00
4d2fa28406
Merge branch 'topic-morphgraph' into dev
2025-07-13 16:12:23 +02:00
042447fbea
restructure contexts & substitutions,
...
still todo: update morphism graph tests
2025-07-13 15:44:26 +02:00
b8f6cab862
morphism graph: cycle detection: exclude trivial loop through Id Step
2025-07-13 15:44:26 +02:00
ef899d28d3
morphism graph: make all structure reprs optional
2025-07-13 15:44:26 +02:00
d256c9cf3b
add shift_variables() and in Morphism trait add ctx()
2025-07-13 15:44:26 +02:00
2c3c526407
pretty: fix dict call to get_varname
2025-07-13 15:44:25 +02:00
2e6cbb65f6
avoid unwrap() due to unspecified struct repr; default to type-id magic for native representation
2025-07-13 15:44:25 +02:00
8474826121
morphism graph: add structure representations
2025-07-13 15:44:25 +02:00
98dfd86f1e
rename morphism modules
2025-07-13 15:44:25 +02:00
a1b4a4e3c5
dictionary: add get_name() & get_varid()
2025-07-13 15:44:25 +02:00
52c120cd57
test
2025-07-13 15:44:25 +02:00
df96e3c8b9
move heuristic into morphism graph module
2025-07-13 15:44:25 +02:00
cead10a62b
rewrite morphism search
2025-07-13 15:44:25 +02:00
e90e9a12ab
add Id as case for MorphismInstance
2025-07-13 15:44:25 +02:00
0cfa228fba
add #[derive(Hash)] to MorphismType
2025-07-13 15:44:24 +02:00
0f0721b6ae
move estimated_cost() to member of MorphismType
2025-07-13 15:43:50 +02:00
3409f7cb1a
initial cost heuristic for morphism types & accelerated graph search (wip)
2025-07-13 15:43:50 +02:00
3f854b3371
submodules for term & morphism_graph
2025-07-13 15:43:26 +02:00
9e0f437f1c
rework variables & substitutions for debruijn indices in layered contexts
2025-07-13 15:43:26 +02:00
58bdcd185b
Merge branch 'topic-constraint-system' into dev
2025-07-13 15:42:37 +02:00
cb9b62b00c
add test with mixed constraints
2025-06-04 23:03:45 +02:00
0cd80c16d5
initial trait type satisfaction
2025-06-03 00:00:32 +02:00
e8615aa42b
initially add bounds to MorphismType
...
.. but this will require scoped variables via debruijn indices first
2025-06-02 22:22:04 +02:00
bf5b2447be
terms: change Morph type to have src/dst instead of Vec
2025-06-02 14:18:16 +02:00
8cb3b1b8ec
move add_upper/lower_bound into subtype module
2025-06-02 00:27:09 +02:00
936ea9a649
split up constraint system unit tests
2025-06-02 00:26:40 +02:00
5a2cdbf009
github workflow: use '--features pretty' option
2025-06-01 20:25:39 +02:00
17ba81c817
split constraint system into files
2025-06-01 18:05:56 +02:00
a1dd6a5121
fix halo type in subtype-constraint
2025-06-01 18:04:38 +02:00
c8b2ffae95
add test to break halo type
2025-06-01 18:04:38 +02:00
10947ce791
rename term&morphism structs to make Sugared* variant the default
...
- SugaredUnification -> ConstraintSystem
- SugaredTypeTerm -> TypeTerm
- SugaredMorphismType -> MorphismType
- etc.
2025-06-01 18:04:38 +02:00
7b25b4472d
MorphismType: add strip_common_rungs()
2025-06-01 18:04:38 +02:00
c75cf43900
terms: rewrite of normalize (PNF, sugared variant)
...
- fixes error in previously added test
2025-06-01 18:04:38 +02:00
c8b3e4f4a2
add failing test (failed to find morphism instance)
2025-06-01 18:04:38 +02:00
646dfcfc2a
rewrite path search & unification for Sugared Terms
...
- deprecates the old term struct
- MorphismType: add apply_subst()
- morphism instance: fix apply subst
- SugaredMorphismType::Struct add src/dst repr
- find_morphism_path(): always advance with direct morph, even if complex decomposition from goal exists
2025-06-01 18:04:38 +02:00
fd1515c0fb
add SugaredStructMember & SugaredVariantEnum
2025-06-01 18:04:38 +02:00
804741cd62
Merge branch 'topic-morphism-base' into dev
2025-06-01 18:02:19 +02:00
de86b3f153
split path search & morphism base into separate files
2025-06-01 16:48:36 +02:00
d56d4089d1
add test for find_morphism_path
2025-06-01 16:48:36 +02:00
59d182135f
rewrite enum_morphisms & find_morphism_path
...
- introduce `MorphismInstantiation` which instantiates a
morphism-template using a type-substitution and a halo type.
- find_morphism_path returns list of `MorphismInstatiation`.
- correctly apply substitutions
- add more path search tests
2025-06-01 16:48:36 +02:00
aa7a39bf17
improvements over initial graph search implementation
...
- turn Morphism into trait and add find_morphism() function
- morphism base: store vec of seq-types
- morphism base: find shortest path instead of just some path
- fix returned halo type in find_morphism_with_subtyping()
- fix find_morphism_path:
* also apply substitution from src-type match
* get this substitution as result from `enum_morphisms_with_subtyping`
2025-06-01 16:48:36 +02:00
0d891e8677
add test for find_morphism_path()
2025-06-01 16:48:36 +02:00
7c4fbf9298
initial implementation of morphism base & graph search
2025-06-01 16:48:03 +02:00
