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
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
ed9f309306
add type alias for HashMapSubst
2025-06-01 16:23:17 +02:00
08a9bad0ad
add Substitution trait
2025-06-01 16:21:39 +02:00
fab6818fe9
Merge branch 'topic-subtype-satisfaction' into dev
2025-06-01 15:33:56 +02:00
63eb4798ac
work on subtype satisfaction
...
- correctly propagate error
- in case of subtype between two ladders, check that the matching sub-ladders end at the same bottom rung (to exclude trait-types from sub-types)
- rewrite subtype satisfaction of ladders to work from bottom up
- add more tests
2025-06-01 14:36:23 +02:00
a2fc025eea
add (failing) tests for subtype-satisfaction
...
- these tests fail and uncover a bug in the subtype unification algorithm where a trait-relationship is treated as subtype relationship which is not wanted
- add test with variable substitution
2025-06-01 14:36:12 +02:00
229c6193c4
subtype satisfaction: move rhs-variable assignment up in match-priority
2025-06-01 14:25:24 +02:00
82a6a20a31
unification: allow subtype and equality constraints
...
in one problem, solve both at the same time
2025-06-01 14:25:18 +02:00
deb097acd3
term: add get_interface_type() to get the top rung of a ladder
2025-06-01 00:42:32 +02:00
aa67520184
term: add strip() to flatten ladders
2025-06-01 00:39:43 +02:00
c4a26d11da
term: add check if term is empty
2025-06-01 00:35:41 +02:00
9db57488dd
Merge branch 'topic-dict' into dev
2025-06-01 00:33:02 +02:00
e15db9d1f3
type dict: get_typename_create
2025-05-31 22:49:53 +02:00
fb2b54059d
add Send+Sync trait bound to TypeDict
2025-05-31 21:52:32 +02:00
25649084ab
make TypeDict a trait & BimapTypeDict an impl
...
- add TypeDict trait
- impl TypeDict for BimapTypeDict
- add Debug for Bimap & BimapTypeDict
- adapt tests
2025-05-31 21:46:08 +02:00
9906972009
Merge branch 'topic-pretty' into dev
2025-05-31 21:38:49 +02:00
af595bffde
pretty format: use different colors for variables
2025-05-31 21:01:17 +02:00
099ba9b0df
pretty: output escape character for \0 and \n
2025-05-31 21:01:17 +02:00
1b8768894e
fix unification test
2025-05-31 21:00:51 +02:00
d861bba741
Merge branch 'topic-unification' into dev
2025-05-31 20:49:29 +02:00
b502b62479
unification: reject non-identity loops & add test cases
2025-02-15 18:35:38 +01:00
f05ef07589
subtype unification
2025-02-15 18:32:34 +01:00
e17a1a9462
add subtype unification
2025-02-09 16:58:58 +01:00
e53edd23b9
unification: remove unreachable pattern
2025-02-09 13:13:56 +01:00
3c5d7111bc
Merge branch 'fix-pnf' into dev
2025-02-09 12:42:40 +01:00
a9a35aed1b
rewrite param_normalize()
2025-02-09 12:42:24 +01:00
4a6a35a897
pnf: add test for collapsing first application argument
2025-02-09 12:42:23 +01:00
4aa62d4813
Merge branch 'topic-sugar' into dev
2025-02-09 12:40:11 +01:00
c6bad6046a
add sugared terms & pretty printing
2025-02-09 12:38:07 +01:00
