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

Draft

coeff-aij wants to merge 30 commits into

coord-e:mainfrom

coeff-aij:forall-sort

Commits on Jun 3, 2026

add: ForallSort
coeff-aij
committed
change: translate param type using ForallSortIdx
coeff-aij
committed
change: translate Type::Param into chc::Sort::Forall
coeff-aij
committed
change: use forall sort instead of deferred type
coeff-aij
committed
add: output (define-forall-sort)
coeff-aij
committed
fix: duplication of ForallSortIdx for the same parameter
coeff-aij
committed
add test cases using unknown type parameters with trait bounds
coeff-aij
committed
change: use DeferredType for generic functions without requires/ensures
coeff-aij
committed
change: prevent overwriting concrete types with deferred types
coeff-aij
committed
change: disable DeferredType completely
coeff-aij
committed
remove all extern_spec in std.rs temporarily
coeff-aij
committed
add: imcomplete support for alias types
coeff-aij
committed
change: use Type::Param and chc::Sort::Forall for type prameters
coeff-aij
committed
add: ForallPred represents unresolved user-defined predicates
coeff-aij
committed
change: replace unresolved user-defined predicates with ForallPred
coeff-aij
committed
fix: distinguish different type parameters in subtyping
coeff-aij
committed
change: store the def_id of the corresponding function in TypeBuilder
coeff-aij
committed
fix: identify type parameters using the DefId of the owner(e.g. `fn f<T>` for `T` in the body)
coeff-aij
committed
fix: wrong conditionals to insert forall predicates
coeff-aij
committed
fix: normalize thrust::Model::Ty
coeff-aij
committed
fix: propagate the DefId for the owner function of formula_fn and
coeff-aij
committed
fix: use both TypeParamIdx and ForallSortIdx for type parameters
coeff-aij
committed
add: insert declarations of universally quantified predicate variables
coeff-aij
committed
add: analyze and output dependencies between predicates
coeff-aij
committed
add: translate alias type into forall sort
coeff-aij
committed
add: tests for unknown type parameters
coeff-aij
committed
fix: propagate owner_fn_id of type parameters
coeff-aij
committed
add: debug print for AliasTy
coeff-aij
committed
fix: propagate owner_fn_id of type parameters
coeff-aij
committed

Commits on Jun 4, 2026

add: translate <ParamTy as Model>::Ty into ParamTy
coeff-aij
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

Encode unknown generic type parameters with `(declare-forall-sort)`#93
coeff-aij wants to merge 30 commits into
coord-e:mainfrom
coeff-aij:forall-sort

Commits on Jun 3, 2026

add: ForallSort

change: translate param type using ForallSortIdx

change: translate Type::Param into chc::Sort::Forall

change: use forall sort instead of deferred type

add: output (define-forall-sort)

fix: duplication of ForallSortIdx for the same parameter

add test cases using unknown type parameters with trait bounds

change: use DeferredType for generic functions without requires/ensures

change: prevent overwriting concrete types with deferred types

change: disable DeferredType completely

remove all extern_spec in std.rs temporarily

add: imcomplete support for alias types

change: use Type::Param and chc::Sort::Forall for type prameters

add: ForallPred represents unresolved user-defined predicates

change: replace unresolved user-defined predicates with ForallPred

fix: distinguish different type parameters in subtyping

change: store the def_id of the corresponding function in TypeBuilder

fix: identify type parameters using the DefId of the owner(e.g. `fn f<T>` for `T` in the body)

fix: wrong conditionals to insert forall predicates

fix: normalize thrust::Model::Ty

fix: propagate the DefId for the owner function of formula_fn and

fix: use both TypeParamIdx and ForallSortIdx for type parameters

add: insert declarations of universally quantified predicate variables

add: analyze and output dependencies between predicates

add: translate alias type into forall sort

add: tests for unknown type parameters

fix: propagate owner_fn_id of type parameters

add: debug print for AliasTy

fix: propagate owner_fn_id of type parameters

Commits on Jun 4, 2026

add: translate <ParamTy as Model>::Ty into ParamTy