Encode unknown generic type parameters with `(declare-forall-sort)` - #93

Draft

coeff-aij wants to merge 124 commits into

coord-e:mainfrom

coeff-aij:forall-sort

Commits on Jun 8, 2026

add: ForallSort
coeff-aij
committed
4eae892
change: translate param type using ForallSortIdx
coeff-aij
committed
2e330a3
change: translate Type::Param into chc::Sort::Forall
coeff-aij
committed
f95cfde
change: use forall sort instead of deferred type
coeff-aij
committed
debaa61
add: output (define-forall-sort)
coeff-aij
committed
03d7932
fix: duplication of ForallSortIdx for the same parameter
coeff-aij
committed
0d47cc8
add test cases using unknown type parameters with trait bounds
coeff-aij
committed
4e35b61
change: use DeferredType for generic functions without requires/ensures
coeff-aij
committed
2ef31cb
change: prevent overwriting concrete types with deferred types
coeff-aij
committed
f42debf
change: disable DeferredType completely
coeff-aij
committed
0a2cc17
remove all extern_spec in std.rs temporarily
coeff-aij
committed
dc9b0e9
add: imcomplete support for alias types
coeff-aij
committed
6d82bfb
change: use Type::Param and chc::Sort::Forall for type prameters
coeff-aij
committed
a0df8dc
add: ForallPred represents unresolved user-defined predicates
coeff-aij
committed
85d9e01
change: replace unresolved user-defined predicates with ForallPred
coeff-aij
committed
4d381fc
fix: distinguish different type parameters in subtyping
coeff-aij
committed
14170e7
change: store the def_id of the corresponding function in TypeBuilder
coeff-aij
committed
6ee71de
fix: identify type parameters using the DefId of the owner(e.g. `fn f<T>` for `T` in the body)
coeff-aij
committed
6c8add1
fix: wrong conditionals to insert forall predicates
coeff-aij
committed
af226a4
fix: normalize thrust::Model::Ty
coeff-aij
committed
3888011
fix: propagate the DefId for the owner function of formula_fn and
coeff-aij
committed
968a4a7
fix: use both TypeParamIdx and ForallSortIdx for type parameters
coeff-aij
committed
87969f2
add: insert declarations of universally quantified predicate variables
coeff-aij
committed
2855cc5
add: analyze and output dependencies between predicates
coeff-aij
committed
8127496
add: translate alias type into forall sort
coeff-aij
committed
23187ce
add: tests for unknown type parameters
coeff-aij
committed
01f9f6c
fix: propagate owner_fn_id of type parameters
coeff-aij
committed
743bcda
add: debug print for AliasTy
coeff-aij
committed
d5cdefb
fix: propagate owner_fn_id of type parameters
coeff-aij
committed
0dc245d
add: translate <ParamTy as Model>::Ty into ParamTy
coeff-aij
committed
5d50264
add: register_generic_def() for substitution of generic args from call
coeff-aij
committed
516cbd5
fix: instantiate generic type parameters contained in args of predicate
coeff-aij
committed
6de74be
add: distinguish calls of forall-predicates with different type
coeff-aij
committed
b921e2c
fix: skip expected_ty() for trait methods without MIR body
coeff-aij
committed
59f401c

Commits on Jun 9, 2026

change: try to bypass the instantiation of unknown generic args on
coeff-aij
committed
e4ed770

Commits on Jun 11, 2026

Commits on Jun 12, 2026

Commits on Jun 13, 2026

Commits on Jun 14, 2026

add: opaque type handling for Box and Vec
coeff-aij
committed
c4cb3bc
fix: use try_normalize_erasing_regions to avoid panic
coeff-aij
committed
b6db754
fix: relax &mut restriction to allow any element type
coeff-aij
committed
b1ad064
revert: commenting out most of extern_spec in std.rs
coeff-aij
committed
2077ab7
add: annotations for fold() (WIP)
coeff-aij
committed
92764b7
Merge branch 'main' into forall-sort
coeff-aij
committed
7fc03cd
fix annotations on fold() (WIP)
coeff-aij
committed
312f362
add test codes for reproducing/avoiding annotation errors
coeff-aij
committed
848f511

Commits on Jun 15, 2026

fix: annotations on fold()
coeff-aij
committed
555106e

Commits on Jun 17, 2026

fix: incorrect signature and duplication of ForallPred
coeff-aij
committed
9d1db19
Merge branch 'main' into forall-sort
coeff-aij
committed
7675b06

Commits on Jun 20, 2026

Merge branch 'main' into forall-sort
coeff-aij
committed
20349c1
fix: propagete owner_fn_id to AnnotFnTranslator
coeff-aij
committed
77a562e
fix: runtime error with borrowing RefCell
coeff-aij
committed
9027871
add: translate AliasTy with TemplateTypeBuilder
coeff-aij
committed
164e771
change: use deferred type for generic functions whose annotations and
coeff-aij
committed
3bafc78
fix: wrong abi for closure
coeff-aij
committed
481829f

Commits on Jun 24, 2026

fix: insert ForallPred for the last argument of closure
coeff-aij
committed
45d0bc4
add: positive test cases for traits
coeff-aij
committed
9eac0a5
Merge branch 'main' into forall-sort
coeff-aij
committed
8f6e2fb

Commits on Jun 25, 2026

Commits on Jun 26, 2026

fix: try to normalize alias projections and allocate the same
coeff-aij
committed
7595088
fix: use impl block's DefId for recognition of type parameters in impl<T>
coeff-aij
committed
e27f7ad
change: use GenericDefTy for unannotated generic functions
coeff-aij
committed
2b696ce
remove: instantiation which breaks alias types which are already
coeff-aij
committed
083f312
add: gather closure param type from parent impl block
coeff-aij
committed
d4252d9
fix: unboxing ForallPred
coeff-aij
committed
018444c
fix: replace commas and whitespaces contained in `Map<I, F>` as
coeff-aij
committed
2458b2e

Commits on Jun 27, 2026

Commits on Jun 28, 2026

Commits on Jul 5, 2026

Merge branch 'main' into forall-sort
coeff-aij
committed
57dbc0d

Commits on Aug 16, 2026

Merge branch 'main' into forall-sort
coeff-aij
committed
3db3950
tests: configure extended CoAR solver
coeff-aij
committed
e2a2d43
fix: include caller in generic type cache keys
coeff-aij
committed
5b2d3bf
improve forall sort type formatting
coeff-aij
committed
e18fba1
test: cover forall sort type formatting
coeff-aij
committed
7993e4b
fix: handle singleton refinement values
coeff-aij
committed
ceb4d03
fix: add forall sort default values
coeff-aij
committed
5eef717
fix: handle unresolved trait method calls
coeff-aij
committed
015bda2
test: specify trait update invariant
coeff-aij
committed
6457860
tests: configure solver for remaining polymorphic cases
coeff-aij
committed
1d814ff

Commits on Aug 25, 2026

Merge branch 'main' into forall-sort
coeff-aij
committed
267233d

Commits on Aug 30, 2026

Merge branch 'main' into forall-sort
coeff-aij
committed
9e49de6
Rename ResolvedCallable::Closure to Concrete
coeff-aij
committed
cf01d7b
test: add solver configuration environmental variables
coeff-aij
committed
bb83b7b

Commits on Sep 2, 2026

add: test for impl and generic function using trait
coeff-aij
committed
5094a69

Commits on Sep 4, 2026

Merge branch 'main' into forall-sort
coeff-aij
committed
ce6bcae