From f60f8b2ac842781861f648b7e71a09316a5b2dea Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Sun, 1 Sep 2024 23:56:37 +0200 Subject: [PATCH] build repr tree --- lib-nested-core/src/repr_tree/context.rs | 26 ++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/lib-nested-core/src/repr_tree/context.rs b/lib-nested-core/src/repr_tree/context.rs index c39da1e..b592ae0 100644 --- a/lib-nested-core/src/repr_tree/context.rs +++ b/lib-nested-core/src/repr_tree/context.rs @@ -120,6 +120,32 @@ impl Context { } } + pub fn build_repr_tree( + &self, + rt: &Arc>, + root: TypeTerm, + leaves: Vec< TypeTerm > + ) { + let mut st_problem = laddertypes::steiner_tree::PathApproxSteinerTreeSolver::new( + root, + leaves + ); + + if let Some( steiner_tree ) = st_problem.solve( &self.morphisms ) { + for morphism_type in steiner_tree.into_edges() { + eprintln!("--> apply morph to {}", self.type_term_to_str(&morphism_type.dst_type)); + if let Some(( morphism, mut τ, σ )) = + self.morphisms.find_morphism_with_subtyping( &morphism_type ) + { + let mut rt = rt.descend( τ ).expect("descend src repr"); + (morphism.setup_projection)( &mut rt, &σ ); + } + } + } else { + eprintln!("could not find steiner tree to build the requested repr tree"); + } + } + pub fn make_repr(ctx: &Arc>, t: &TypeTerm) -> Arc> { let rt = Arc::new(RwLock::new(ReprTree::new( TypeTerm::unit() ))); ctx.read().unwrap().apply_morphism( &rt, &MorphismType{ src_type: TypeTerm::unit(), dst_type: t.clone() } );