syntaxAlchemist/lib-laddertypes
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

add Id as case for MorphismInstance

Browse source
This commit is contained in:
Michael Sippel 2025-05-28 17:32:30 +02:00
parent c05dc688b5
commit 3240c472ca
Signed by: senvas
GPG key ID: F96CF119C34B64A6
2 changed files with 16 additions and 1 deletions

13
src/morphism.rs
View file

@ -186,6 +186,7 @@ pub trait Morphism : Sized {
#[derive(Clone, PartialEq, Debug)]
pub enum MorphismInstance<M: Morphism + Clone> {
Id { ψ: TypeTerm },
Primitive{
ψ: TypeTerm,
σ: HashMap<TypeID, TypeTerm>,
@ -220,6 +221,12 @@ impl<M: Morphism + Clone> MorphismInstance<M> {
pub fn get_type(&self) -> MorphismType {
match self {
MorphismInstance::Id { ψ } => {
MorphismType {
src_type: ψ.clone(),
dst_type: ψ.clone()
}
}
MorphismInstance::Primitive { ψ, σ, morph } => {
MorphismType {
src_type:
@ -311,6 +318,9 @@ impl<M: Morphism + Clone> MorphismInstance<M> {
pub fn get_subst(&self) -> std::collections::HashMap< TypeID, TypeTerm > {
match self {
MorphismInstance::Id { ψ } => {
std::collections::HashMap::new()
}
MorphismInstance::Primitive { ψ, σ, morph } => σ.clone(),
MorphismInstance::Chain { path } => {
path.iter().fold(
@ -341,6 +351,9 @@ impl<M: Morphism + Clone> MorphismInstance<M> {
pub fn apply_subst(&mut self, γ: &std::collections::HashMap< TypeID, TypeTerm >) {
let ty = self.get_type();
match self {
MorphismInstance::Id { ψ } => {
ψ.apply_subst( γ );
}
MorphismInstance::Primitive { ψ, σ, morph } => {
ψ.apply_subst(γ);
for (n,t) in σ.iter_mut() {

4
src/morphism_base.rs
View file

@ -28,7 +28,9 @@ impl<M: Morphism + Clone> MorphismBase<M> {
pub fn get_morphism_instance(&self, ty: &MorphismType) -> Option<MorphismInstance<M>> {
if let Some(path) = ShortestPathProblem::new(self, ty.clone()).solve() {
if path.len() == 1 {
if path.len() == 0 {
Some(MorphismInstance::Id{ ψ: ty.src_type.clone() })
} else if path.len() == 1 {
Some(path[0].clone())
} else {
Some(MorphismInstance::Chain { path })