oxilean_meta/synth_instance/
types.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use crate::basic::{MVarId, MetaContext};
6use crate::def_eq::{MetaDefEq, UnificationResult};
7use crate::discr_tree::DiscrTree;
8use oxilean_kernel::{BinderInfo, Expr, Level, Name};
9use std::collections::{HashMap, HashSet};
10
11use super::functions::{
12    collect_unassigned_mvars, extract_class_name, goals_structurally_similar, InstancePriority,
13    DEFAULT_PRIORITY,
14};
15
16#[allow(dead_code)]
17pub struct SynthInstanceExtDiff1500 {
18    pub added: Vec<String>,
19    pub removed: Vec<String>,
20    pub unchanged: Vec<String>,
21}
22impl SynthInstanceExtDiff1500 {
23    #[allow(dead_code)]
24    pub fn new() -> Self {
25        Self {
26            added: Vec::new(),
27            removed: Vec::new(),
28            unchanged: Vec::new(),
29        }
30    }
31    #[allow(dead_code)]
32    pub fn add(&mut self, s: &str) {
33        self.added.push(s.to_string());
34    }
35    #[allow(dead_code)]
36    pub fn remove(&mut self, s: &str) {
37        self.removed.push(s.to_string());
38    }
39    #[allow(dead_code)]
40    pub fn keep(&mut self, s: &str) {
41        self.unchanged.push(s.to_string());
42    }
43    #[allow(dead_code)]
44    pub fn is_empty(&self) -> bool {
45        self.added.is_empty() && self.removed.is_empty()
46    }
47    #[allow(dead_code)]
48    pub fn total_changes(&self) -> usize {
49        self.added.len() + self.removed.len()
50    }
51    #[allow(dead_code)]
52    pub fn net_additions(&self) -> i64 {
53        self.added.len() as i64 - self.removed.len() as i64
54    }
55    #[allow(dead_code)]
56    pub fn summary(&self) -> String {
57        format!(
58            "+{} -{} =={}",
59            self.added.len(),
60            self.removed.len(),
61            self.unchanged.len()
62        )
63    }
64}
65/// A typed slot for SynthInstance configuration.
66#[allow(dead_code)]
67#[derive(Debug, Clone)]
68pub enum SynthInstanceConfigValue {
69    Bool(bool),
70    Int(i64),
71    Float(f64),
72    Str(String),
73    List(Vec<String>),
74}
75#[allow(dead_code)]
76impl SynthInstanceConfigValue {
77    pub fn as_bool(&self) -> Option<bool> {
78        match self {
79            SynthInstanceConfigValue::Bool(b) => Some(*b),
80            _ => None,
81        }
82    }
83    pub fn as_int(&self) -> Option<i64> {
84        match self {
85            SynthInstanceConfigValue::Int(i) => Some(*i),
86            _ => None,
87        }
88    }
89    pub fn as_float(&self) -> Option<f64> {
90        match self {
91            SynthInstanceConfigValue::Float(f) => Some(*f),
92            _ => None,
93        }
94    }
95    pub fn as_str(&self) -> Option<&str> {
96        match self {
97            SynthInstanceConfigValue::Str(s) => Some(s),
98            _ => None,
99        }
100    }
101    pub fn as_list(&self) -> Option<&[String]> {
102        match self {
103            SynthInstanceConfigValue::List(v) => Some(v),
104            _ => None,
105        }
106    }
107    pub fn type_name(&self) -> &'static str {
108        match self {
109            SynthInstanceConfigValue::Bool(_) => "bool",
110            SynthInstanceConfigValue::Int(_) => "int",
111            SynthInstanceConfigValue::Float(_) => "float",
112            SynthInstanceConfigValue::Str(_) => "str",
113            SynthInstanceConfigValue::List(_) => "list",
114        }
115    }
116}
117/// Choice point for backtracking.
118#[derive(Clone, Debug)]
119#[allow(dead_code)]
120pub(crate) struct ChoicePoint {
121    /// Goal at this choice point.
122    pub(super) goal: Expr,
123    /// Depth at this choice point.
124    pub(super) depth: u32,
125    /// Remaining candidates to try.
126    pub(super) candidates_remaining: usize,
127}
128/// A pipeline of SynthInstance analysis passes.
129#[allow(dead_code)]
130pub struct SynthInstancePipeline {
131    pub passes: Vec<SynthInstanceAnalysisPass>,
132    pub name: String,
133    pub total_inputs_processed: usize,
134}
135#[allow(dead_code)]
136impl SynthInstancePipeline {
137    pub fn new(name: &str) -> Self {
138        SynthInstancePipeline {
139            passes: Vec::new(),
140            name: name.to_string(),
141            total_inputs_processed: 0,
142        }
143    }
144    pub fn add_pass(&mut self, pass: SynthInstanceAnalysisPass) {
145        self.passes.push(pass);
146    }
147    pub fn run_all(&mut self, input: &str) -> Vec<SynthInstanceResult> {
148        self.total_inputs_processed += 1;
149        self.passes
150            .iter_mut()
151            .filter(|p| p.enabled)
152            .map(|p| p.run(input))
153            .collect()
154    }
155    pub fn num_passes(&self) -> usize {
156        self.passes.len()
157    }
158    pub fn num_enabled_passes(&self) -> usize {
159        self.passes.iter().filter(|p| p.enabled).count()
160    }
161    pub fn total_success_rate(&self) -> f64 {
162        if self.passes.is_empty() {
163            0.0
164        } else {
165            let total_rate: f64 = self.passes.iter().map(|p| p.success_rate()).sum();
166            total_rate / self.passes.len() as f64
167        }
168    }
169}
170#[allow(dead_code)]
171#[derive(Debug, Clone)]
172pub enum SynthInstanceExtConfigVal1500 {
173    Bool(bool),
174    Int(i64),
175    Float(f64),
176    Str(String),
177    List(Vec<String>),
178}
179impl SynthInstanceExtConfigVal1500 {
180    #[allow(dead_code)]
181    pub fn as_bool(&self) -> Option<bool> {
182        if let SynthInstanceExtConfigVal1500::Bool(b) = self {
183            Some(*b)
184        } else {
185            None
186        }
187    }
188    #[allow(dead_code)]
189    pub fn as_int(&self) -> Option<i64> {
190        if let SynthInstanceExtConfigVal1500::Int(i) = self {
191            Some(*i)
192        } else {
193            None
194        }
195    }
196    #[allow(dead_code)]
197    pub fn as_float(&self) -> Option<f64> {
198        if let SynthInstanceExtConfigVal1500::Float(f) = self {
199            Some(*f)
200        } else {
201            None
202        }
203    }
204    #[allow(dead_code)]
205    pub fn as_str(&self) -> Option<&str> {
206        if let SynthInstanceExtConfigVal1500::Str(s) = self {
207            Some(s)
208        } else {
209            None
210        }
211    }
212    #[allow(dead_code)]
213    pub fn as_list(&self) -> Option<&[String]> {
214        if let SynthInstanceExtConfigVal1500::List(l) = self {
215            Some(l)
216        } else {
217            None
218        }
219    }
220    #[allow(dead_code)]
221    pub fn type_name(&self) -> &'static str {
222        match self {
223            SynthInstanceExtConfigVal1500::Bool(_) => "bool",
224            SynthInstanceExtConfigVal1500::Int(_) => "int",
225            SynthInstanceExtConfigVal1500::Float(_) => "float",
226            SynthInstanceExtConfigVal1500::Str(_) => "str",
227            SynthInstanceExtConfigVal1500::List(_) => "list",
228        }
229    }
230}
231/// A registered type class instance.
232#[derive(Clone, Debug)]
233pub struct InstanceEntry {
234    /// Name of the instance declaration.
235    pub name: Name,
236    /// Type of the instance (the class application it satisfies).
237    pub ty: Expr,
238    /// Priority (lower = tried first).
239    pub priority: InstancePriority,
240    /// Whether this is a local instance (from the context).
241    pub is_local: bool,
242    /// Whether this instance is preferred (used for tie-breaking).
243    pub preferred: bool,
244}
245impl InstanceEntry {
246    /// Create a new instance entry with defaults.
247    pub fn new(name: Name, ty: Expr) -> Self {
248        Self {
249            name,
250            ty,
251            priority: DEFAULT_PRIORITY,
252            is_local: false,
253            preferred: false,
254        }
255    }
256    /// Set the priority of this instance.
257    pub fn with_priority(mut self, priority: InstancePriority) -> Self {
258        self.priority = priority;
259        self
260    }
261    /// Mark this instance as local.
262    pub fn with_local(mut self, is_local: bool) -> Self {
263        self.is_local = is_local;
264        self
265    }
266    /// Mark this instance as preferred.
267    pub fn with_preferred(mut self, preferred: bool) -> Self {
268        self.preferred = preferred;
269        self
270    }
271}
272#[allow(dead_code)]
273#[derive(Debug, Clone)]
274pub enum SynthInstanceExtResult1500 {
275    /// Operation completed successfully.
276    Ok(String),
277    /// Operation encountered an error.
278    Err(String),
279    /// Operation partially completed.
280    Partial { done: usize, total: usize },
281    /// Operation was skipped.
282    Skipped,
283}
284impl SynthInstanceExtResult1500 {
285    #[allow(dead_code)]
286    pub fn is_ok(&self) -> bool {
287        matches!(self, SynthInstanceExtResult1500::Ok(_))
288    }
289    #[allow(dead_code)]
290    pub fn is_err(&self) -> bool {
291        matches!(self, SynthInstanceExtResult1500::Err(_))
292    }
293    #[allow(dead_code)]
294    pub fn is_partial(&self) -> bool {
295        matches!(self, SynthInstanceExtResult1500::Partial { .. })
296    }
297    #[allow(dead_code)]
298    pub fn is_skipped(&self) -> bool {
299        matches!(self, SynthInstanceExtResult1500::Skipped)
300    }
301    #[allow(dead_code)]
302    pub fn ok_msg(&self) -> Option<&str> {
303        if let SynthInstanceExtResult1500::Ok(s) = self {
304            Some(s)
305        } else {
306            None
307        }
308    }
309    #[allow(dead_code)]
310    pub fn err_msg(&self) -> Option<&str> {
311        if let SynthInstanceExtResult1500::Err(s) = self {
312            Some(s)
313        } else {
314            None
315        }
316    }
317    #[allow(dead_code)]
318    pub fn progress(&self) -> f64 {
319        match self {
320            SynthInstanceExtResult1500::Ok(_) => 1.0,
321            SynthInstanceExtResult1500::Err(_) => 0.0,
322            SynthInstanceExtResult1500::Partial { done, total } => {
323                if *total == 0 {
324                    0.0
325                } else {
326                    *done as f64 / *total as f64
327                }
328            }
329            SynthInstanceExtResult1500::Skipped => 0.5,
330        }
331    }
332}
333/// Type class instance synthesizer with advanced resolution.
334///
335/// Uses tabled resolution with generator/consumer nodes
336/// for efficient instance search and sophisticated search strategies.
337pub struct InstanceSynthesizer {
338    /// Global instances indexed by discrimination tree.
339    pub(super) global_instances: DiscrTree<InstanceEntry>,
340    /// Instance entries by class name.
341    pub(super) instances_by_class: HashMap<Name, Vec<InstanceEntry>>,
342    /// Cache of successful synthesis results.
343    pub(super) cache: HashMap<Expr, Expr>,
344    /// Cache of failed synthesis attempts.
345    pub(super) failure_cache: HashMap<Expr, FailureReason>,
346    /// Maximum search depth.
347    pub(super) max_depth: u32,
348    /// Maximum number of heartbeats (work units).
349    pub(super) max_heartbeats: u64,
350    /// Current heartbeat count.
351    pub(super) heartbeats: u64,
352    /// Trail of goals being explored (for loop detection).
353    pub(super) trail: Vec<Expr>,
354    /// Resolution nodes for tabled resolution.
355    pub(super) resolution_nodes: Vec<ResolutionNode>,
356    /// Choice points for backtracking.
357    pub(super) choice_points: Vec<ChoicePoint>,
358    /// Statistics for current synthesis.
359    pub(super) current_stats: SearchStats,
360    /// Diagnostics for last synthesis.
361    pub(super) last_diagnostics: Option<SynthDiagnostics>,
362}
363impl InstanceSynthesizer {
364    /// Create a new instance synthesizer.
365    pub fn new() -> Self {
366        Self {
367            global_instances: DiscrTree::new(),
368            instances_by_class: HashMap::new(),
369            cache: HashMap::new(),
370            failure_cache: HashMap::new(),
371            max_depth: 32,
372            max_heartbeats: 20_000,
373            heartbeats: 0,
374            trail: Vec::new(),
375            resolution_nodes: Vec::new(),
376            choice_points: Vec::new(),
377            current_stats: SearchStats::default(),
378            last_diagnostics: None,
379        }
380    }
381    /// Register a global instance.
382    pub fn add_instance(&mut self, entry: InstanceEntry) {
383        let class_name = extract_class_name(&entry.ty);
384        self.global_instances.insert(&entry.ty, entry.clone());
385        self.instances_by_class
386            .entry(class_name)
387            .or_default()
388            .push(entry);
389    }
390    /// Add a local instance from the current context.
391    pub fn add_local_instance(&mut self, entry: InstanceEntry) {
392        let mut local_entry = entry;
393        local_entry.is_local = true;
394        self.add_instance(local_entry);
395    }
396    /// Get all instances for a class.
397    pub fn get_instances(&self, class_name: &Name) -> &[InstanceEntry] {
398        self.instances_by_class
399            .get(class_name)
400            .map(|v| v.as_slice())
401            .unwrap_or(&[])
402    }
403    /// Get the number of registered instances.
404    pub fn num_instances(&self) -> usize {
405        self.global_instances.num_entries()
406    }
407    /// Check for instance overlap (coherence check).
408    ///
409    /// Returns true if there are instances with the same head that
410    /// could potentially match the same goal.
411    pub fn check_overlap(&self, class_name: &Name) -> bool {
412        let instances = self.get_instances(class_name);
413        if instances.len() < 2 {
414            return false;
415        }
416        let mut seen = HashSet::new();
417        for inst in instances {
418            let key = (inst.priority, inst.preferred);
419            if seen.contains(&key) {
420                return true;
421            }
422            seen.insert(key);
423        }
424        false
425    }
426    /// Clear all cached results.
427    pub fn clear_cache(&mut self) {
428        self.cache.clear();
429        self.failure_cache.clear();
430    }
431    /// Synthesize an instance for the given type class goal.
432    ///
433    /// The `goal` should be a type class application, e.g., `Add Nat`.
434    pub fn synthesize(&mut self, goal: &Expr, ctx: &mut MetaContext) -> SynthResult {
435        self.heartbeats = 0;
436        self.current_stats = SearchStats::default();
437        self.trail.clear();
438        self.resolution_nodes.clear();
439        self.choice_points.clear();
440        let goal_inst = ctx.instantiate_mvars(goal);
441        if let Some(cached) = self.cache.get(&goal_inst) {
442            self.current_stats.cache_hits = 1;
443            return SynthResult::Success(cached.clone());
444        }
445        if let Some(reason) = self.failure_cache.get(&goal_inst) {
446            let diag = SynthDiagnostics {
447                failure_reason: reason.clone(),
448                stats: self.current_stats.clone(),
449                tried_candidates: vec![],
450            };
451            self.last_diagnostics = Some(diag);
452            return SynthResult::Failure;
453        }
454        let result = self.synthesize_internal(&goal_inst, ctx);
455        match &result {
456            SynthResult::Success(expr) => {
457                self.cache.insert(goal_inst.clone(), expr.clone());
458            }
459            SynthResult::Failure => {
460                self.failure_cache
461                    .insert(goal_inst, FailureReason::NoInstances);
462            }
463            _ => {}
464        }
465        result
466    }
467    /// Internal synthesis implementation with backtracking.
468    fn synthesize_internal(&mut self, goal: &Expr, ctx: &mut MetaContext) -> SynthResult {
469        self.trail.push(goal.clone());
470        let class_name = extract_class_name(goal);
471        let candidates = self.get_sorted_candidates(&class_name, goal);
472        if candidates.is_empty() {
473            self.trail.pop();
474            let diag = SynthDiagnostics {
475                failure_reason: FailureReason::NoInstances,
476                stats: self.current_stats.clone(),
477                tried_candidates: vec![],
478            };
479            self.last_diagnostics = Some(diag);
480            return SynthResult::Failure;
481        }
482        let mut tried = vec![];
483        for candidate in &candidates {
484            self.heartbeats += 1;
485            self.current_stats.instances_examined += 1;
486            if self.heartbeats > self.max_heartbeats {
487                self.trail.pop();
488                let diag = SynthDiagnostics {
489                    failure_reason: FailureReason::Timeout,
490                    stats: self.current_stats.clone(),
491                    tried_candidates: tried,
492                };
493                self.last_diagnostics = Some(diag);
494                return SynthResult::Failure;
495            }
496            let state = ctx.save_state();
497            match self.try_candidate(candidate, goal, ctx, 0) {
498                SynthResult::Success(result) => {
499                    self.trail.pop();
500                    self.current_stats.successful_unifications += 1;
501                    return SynthResult::Success(result);
502                }
503                SynthResult::Stuck(id) => {
504                    ctx.restore_state(state);
505                    self.trail.pop();
506                    return SynthResult::Stuck(id);
507                }
508                SynthResult::Failure => {
509                    ctx.restore_state(state);
510                    self.current_stats.failed_unifications += 1;
511                    tried.push((candidate.name.clone(), FailureReason::UnificationFailed));
512                    continue;
513                }
514            }
515        }
516        self.trail.pop();
517        let diag = SynthDiagnostics {
518            failure_reason: FailureReason::UnificationFailed,
519            stats: self.current_stats.clone(),
520            tried_candidates: tried,
521        };
522        self.last_diagnostics = Some(diag);
523        SynthResult::Failure
524    }
525    /// Get candidates sorted by priority with tie-breaking.
526    pub(crate) fn get_sorted_candidates(
527        &self,
528        class_name: &Name,
529        _goal: &Expr,
530    ) -> Vec<InstanceEntry> {
531        let mut candidates: Vec<InstanceEntry> = self.get_instances(class_name).to_vec();
532        candidates.sort_by(|a, b| match a.priority.cmp(&b.priority) {
533            std::cmp::Ordering::Equal => match b.preferred.cmp(&a.preferred) {
534                std::cmp::Ordering::Equal => b.is_local.cmp(&a.is_local),
535                other => other,
536            },
537            other => other,
538        });
539        candidates
540    }
541    /// Try a single candidate instance with unification.
542    fn try_candidate(
543        &mut self,
544        candidate: &InstanceEntry,
545        goal: &Expr,
546        ctx: &mut MetaContext,
547        depth: u32,
548    ) -> SynthResult {
549        if depth > self.max_depth {
550            self.current_stats.max_depth_reached = depth;
551            return SynthResult::Failure;
552        }
553        if self
554            .trail
555            .iter()
556            .take(self.trail.len() - 1)
557            .any(|g| goals_structurally_similar(g, goal))
558        {
559            return SynthResult::Failure;
560        }
561        let (instance_expr, instance_ty) = self.instantiate_instance(candidate, ctx);
562        let mut deq = MetaDefEq::new();
563        let result = deq.is_def_eq(&instance_ty, goal, ctx);
564        match result {
565            UnificationResult::Equal => {
566                self.current_stats.recursive_calls += 1;
567                let inst_expr = ctx.instantiate_mvars(&instance_expr);
568                if ctx.has_unassigned_mvars(&inst_expr) {
569                    self.solve_subgoals(&inst_expr, ctx, depth + 1)
570                } else {
571                    SynthResult::Success(inst_expr)
572                }
573            }
574            UnificationResult::Postponed => {
575                if let Some(constraints) = ctx.postponed_constraints().last() {
576                    if let Some(id) = MetaContext::is_mvar_expr(&constraints.lhs) {
577                        return SynthResult::Stuck(id);
578                    }
579                }
580                SynthResult::Failure
581            }
582            UnificationResult::NotEqual => SynthResult::Failure,
583        }
584    }
585    /// Create a fresh instance of an instance entry with metavariables
586    /// for all its parameters (higher-order unification).
587    fn instantiate_instance(
588        &self,
589        candidate: &InstanceEntry,
590        ctx: &mut MetaContext,
591    ) -> (Expr, Expr) {
592        let (level_params, raw_ty) = match ctx.find_const(&candidate.name) {
593            Some(ci) => (ci.level_params().to_vec(), ci.ty().clone()),
594            None => {
595                return (
596                    Expr::Const(candidate.name.clone(), vec![]),
597                    candidate.ty.clone(),
598                );
599            }
600        };
601        let level_mvars: Vec<Level> = level_params
602            .iter()
603            .map(|_| ctx.mk_fresh_level_mvar())
604            .collect();
605        let inst_ty =
606            oxilean_kernel::instantiate_level_params(&raw_ty, &level_params, &level_mvars);
607        let mut instance_expr = Expr::Const(candidate.name.clone(), level_mvars);
608        let mut cur_ty = inst_ty;
609        while let Expr::Pi(
610            BinderInfo::Implicit | BinderInfo::StrictImplicit | BinderInfo::InstImplicit,
611            _,
612            domain,
613            body,
614        ) = &cur_ty.clone()
615        {
616            let (_, mvar) =
617                ctx.mk_fresh_expr_mvar((**domain).clone(), crate::basic::MetavarKind::Natural);
618            instance_expr = Expr::App(Box::new(instance_expr), Box::new(mvar.clone()));
619            cur_ty = oxilean_kernel::instantiate(body, &mvar);
620        }
621        (instance_expr, cur_ty)
622    }
623    /// Try to solve remaining subgoals in an instance expression (recursive instance search).
624    fn solve_subgoals(&mut self, expr: &Expr, ctx: &mut MetaContext, depth: u32) -> SynthResult {
625        if depth > self.max_depth {
626            self.current_stats.max_depth_reached = depth;
627            return SynthResult::Failure;
628        }
629        let unassigned = collect_unassigned_mvars(expr, ctx);
630        for mvar_id in unassigned {
631            if let Some(mvar_ty) = ctx.get_mvar_type(mvar_id) {
632                let goal = mvar_ty.clone();
633                let goal_inst = ctx.instantiate_mvars(&goal);
634                let class_name = extract_class_name(&goal_inst);
635                if !self.instances_by_class.contains_key(&class_name) {
636                    continue;
637                }
638                if self.trail.contains(&goal_inst) {
639                    return SynthResult::Failure;
640                }
641                self.trail.push(goal_inst.clone());
642                match self.synthesize(&goal_inst, ctx) {
643                    SynthResult::Success(result) => {
644                        ctx.reassign_mvar(mvar_id, result);
645                    }
646                    SynthResult::Stuck(id) => {
647                        self.trail.pop();
648                        return SynthResult::Stuck(id);
649                    }
650                    SynthResult::Failure => {
651                        self.trail.pop();
652                        return SynthResult::Failure;
653                    }
654                }
655                self.trail.pop();
656            }
657        }
658        let final_expr = ctx.instantiate_mvars(expr);
659        if ctx.has_unassigned_mvars(&final_expr) {
660            SynthResult::Failure
661        } else {
662            SynthResult::Success(final_expr)
663        }
664    }
665    /// Set the maximum search depth.
666    pub fn set_max_depth(&mut self, depth: u32) {
667        self.max_depth = depth;
668    }
669    /// Set the maximum number of heartbeats.
670    pub fn set_max_heartbeats(&mut self, heartbeats: u64) {
671        self.max_heartbeats = heartbeats;
672    }
673    /// Get the number of heartbeats used in the last synthesis.
674    pub fn last_heartbeats(&self) -> u64 {
675        self.heartbeats
676    }
677    /// Get diagnostics from the last synthesis attempt.
678    pub fn last_diagnostics(&self) -> Option<&SynthDiagnostics> {
679        self.last_diagnostics.as_ref()
680    }
681    /// Get current search statistics.
682    pub fn current_stats(&self) -> &SearchStats {
683        &self.current_stats
684    }
685    /// Rank candidate instances for a goal (for diagnostics).
686    pub fn rank_candidates(&self, goal: &Expr) -> Vec<(Name, u32)> {
687        let class_name = extract_class_name(goal);
688        let candidates = self.get_sorted_candidates(&class_name, goal);
689        candidates
690            .iter()
691            .enumerate()
692            .map(|(rank, inst)| (inst.name.clone(), rank as u32))
693            .collect()
694    }
695}
696/// A diff for SynthInstance analysis results.
697#[allow(dead_code)]
698#[derive(Debug, Clone)]
699pub struct SynthInstanceDiff {
700    pub added: Vec<String>,
701    pub removed: Vec<String>,
702    pub unchanged: Vec<String>,
703}
704#[allow(dead_code)]
705impl SynthInstanceDiff {
706    pub fn new() -> Self {
707        SynthInstanceDiff {
708            added: Vec::new(),
709            removed: Vec::new(),
710            unchanged: Vec::new(),
711        }
712    }
713    pub fn add(&mut self, s: &str) {
714        self.added.push(s.to_string());
715    }
716    pub fn remove(&mut self, s: &str) {
717        self.removed.push(s.to_string());
718    }
719    pub fn keep(&mut self, s: &str) {
720        self.unchanged.push(s.to_string());
721    }
722    pub fn is_empty(&self) -> bool {
723        self.added.is_empty() && self.removed.is_empty()
724    }
725    pub fn total_changes(&self) -> usize {
726        self.added.len() + self.removed.len()
727    }
728    pub fn net_additions(&self) -> i64 {
729        self.added.len() as i64 - self.removed.len() as i64
730    }
731    pub fn summary(&self) -> String {
732        format!(
733            "+{} -{} =={}",
734            self.added.len(),
735            self.removed.len(),
736            self.unchanged.len()
737        )
738    }
739}
740/// A result type for SynthInstance analysis.
741#[allow(dead_code)]
742#[derive(Debug, Clone, PartialEq)]
743pub enum SynthInstanceResult {
744    Ok(String),
745    Err(String),
746    Partial { done: usize, total: usize },
747    Skipped,
748}
749#[allow(dead_code)]
750impl SynthInstanceResult {
751    pub fn is_ok(&self) -> bool {
752        matches!(self, SynthInstanceResult::Ok(_))
753    }
754    pub fn is_err(&self) -> bool {
755        matches!(self, SynthInstanceResult::Err(_))
756    }
757    pub fn is_partial(&self) -> bool {
758        matches!(self, SynthInstanceResult::Partial { .. })
759    }
760    pub fn is_skipped(&self) -> bool {
761        matches!(self, SynthInstanceResult::Skipped)
762    }
763    pub fn ok_msg(&self) -> Option<&str> {
764        match self {
765            SynthInstanceResult::Ok(s) => Some(s),
766            _ => None,
767        }
768    }
769    pub fn err_msg(&self) -> Option<&str> {
770        match self {
771            SynthInstanceResult::Err(s) => Some(s),
772            _ => None,
773        }
774    }
775    pub fn progress(&self) -> f64 {
776        match self {
777            SynthInstanceResult::Ok(_) => 1.0,
778            SynthInstanceResult::Err(_) => 0.0,
779            SynthInstanceResult::Skipped => 0.0,
780            SynthInstanceResult::Partial { done, total } => {
781                if *total == 0 {
782                    0.0
783                } else {
784                    *done as f64 / *total as f64
785                }
786            }
787        }
788    }
789}
790/// A diagnostic reporter for SynthInstance.
791#[allow(dead_code)]
792pub struct SynthInstanceDiagnostics {
793    pub errors: Vec<String>,
794    pub warnings: Vec<String>,
795    pub notes: Vec<String>,
796    pub max_errors: usize,
797}
798#[allow(dead_code)]
799impl SynthInstanceDiagnostics {
800    pub fn new(max_errors: usize) -> Self {
801        SynthInstanceDiagnostics {
802            errors: Vec::new(),
803            warnings: Vec::new(),
804            notes: Vec::new(),
805            max_errors,
806        }
807    }
808    pub fn error(&mut self, msg: &str) {
809        if self.errors.len() < self.max_errors {
810            self.errors.push(msg.to_string());
811        }
812    }
813    pub fn warning(&mut self, msg: &str) {
814        self.warnings.push(msg.to_string());
815    }
816    pub fn note(&mut self, msg: &str) {
817        self.notes.push(msg.to_string());
818    }
819    pub fn has_errors(&self) -> bool {
820        !self.errors.is_empty()
821    }
822    pub fn num_errors(&self) -> usize {
823        self.errors.len()
824    }
825    pub fn num_warnings(&self) -> usize {
826        self.warnings.len()
827    }
828    pub fn is_clean(&self) -> bool {
829        self.errors.is_empty() && self.warnings.is_empty()
830    }
831    pub fn at_error_limit(&self) -> bool {
832        self.errors.len() >= self.max_errors
833    }
834    pub fn clear(&mut self) {
835        self.errors.clear();
836        self.warnings.clear();
837        self.notes.clear();
838    }
839    pub fn summary(&self) -> String {
840        format!(
841            "{} error(s), {} warning(s)",
842            self.errors.len(),
843            self.warnings.len()
844        )
845    }
846}
847#[allow(dead_code)]
848pub struct SynthInstanceExtPipeline1500 {
849    pub name: String,
850    pub passes: Vec<SynthInstanceExtPass1500>,
851    pub run_count: usize,
852}
853impl SynthInstanceExtPipeline1500 {
854    #[allow(dead_code)]
855    pub fn new(name: &str) -> Self {
856        Self {
857            name: name.to_string(),
858            passes: Vec::new(),
859            run_count: 0,
860        }
861    }
862    #[allow(dead_code)]
863    pub fn add_pass(&mut self, pass: SynthInstanceExtPass1500) {
864        self.passes.push(pass);
865    }
866    #[allow(dead_code)]
867    pub fn run_all(&mut self, input: &str) -> Vec<SynthInstanceExtResult1500> {
868        self.run_count += 1;
869        self.passes
870            .iter_mut()
871            .filter(|p| p.enabled)
872            .map(|p| p.run(input))
873            .collect()
874    }
875    #[allow(dead_code)]
876    pub fn num_passes(&self) -> usize {
877        self.passes.len()
878    }
879    #[allow(dead_code)]
880    pub fn num_enabled_passes(&self) -> usize {
881        self.passes.iter().filter(|p| p.enabled).count()
882    }
883    #[allow(dead_code)]
884    pub fn total_success_rate(&self) -> f64 {
885        let total: usize = self.passes.iter().map(|p| p.total_runs).sum();
886        let ok: usize = self.passes.iter().map(|p| p.successes).sum();
887        if total == 0 {
888            0.0
889        } else {
890            ok as f64 / total as f64
891        }
892    }
893}
894/// Reason for instance search failure.
895#[derive(Clone, Debug)]
896pub enum FailureReason {
897    /// No matching instances found for this class.
898    NoInstances,
899    /// Unification with instance failed.
900    UnificationFailed,
901    /// Recursive loop detected in search.
902    LoopDetected,
903    /// Maximum depth exceeded.
904    MaxDepthExceeded,
905    /// Search timeout (heartbeat limit).
906    Timeout,
907    /// Unresolved postponed constraints.
908    PostponedConstraints,
909}
910/// Diagnostics for a failed synthesis attempt.
911#[derive(Clone, Debug)]
912pub struct SynthDiagnostics {
913    /// Reason for failure.
914    pub failure_reason: FailureReason,
915    /// Statistics about the search.
916    pub stats: SearchStats,
917    /// Candidate instances that were tried.
918    pub tried_candidates: Vec<(Name, FailureReason)>,
919}
920/// An analysis pass for SynthInstance.
921#[allow(dead_code)]
922pub struct SynthInstanceAnalysisPass {
923    pub name: String,
924    pub enabled: bool,
925    pub results: Vec<SynthInstanceResult>,
926    pub total_runs: usize,
927}
928#[allow(dead_code)]
929impl SynthInstanceAnalysisPass {
930    pub fn new(name: &str) -> Self {
931        SynthInstanceAnalysisPass {
932            name: name.to_string(),
933            enabled: true,
934            results: Vec::new(),
935            total_runs: 0,
936        }
937    }
938    pub fn run(&mut self, input: &str) -> SynthInstanceResult {
939        self.total_runs += 1;
940        let result = if input.is_empty() {
941            SynthInstanceResult::Err("empty input".to_string())
942        } else {
943            SynthInstanceResult::Ok(format!("processed: {}", input))
944        };
945        self.results.push(result.clone());
946        result
947    }
948    pub fn success_count(&self) -> usize {
949        self.results.iter().filter(|r| r.is_ok()).count()
950    }
951    pub fn error_count(&self) -> usize {
952        self.results.iter().filter(|r| r.is_err()).count()
953    }
954    pub fn success_rate(&self) -> f64 {
955        if self.total_runs == 0 {
956            0.0
957        } else {
958            self.success_count() as f64 / self.total_runs as f64
959        }
960    }
961    pub fn disable(&mut self) {
962        self.enabled = false;
963    }
964    pub fn enable(&mut self) {
965        self.enabled = true;
966    }
967    pub fn clear_results(&mut self) {
968        self.results.clear();
969    }
970}
971#[allow(dead_code)]
972pub struct SynthInstanceExtConfig1500 {
973    pub(super) values: std::collections::HashMap<String, SynthInstanceExtConfigVal1500>,
974    pub(super) read_only: bool,
975    pub(super) name: String,
976}
977impl SynthInstanceExtConfig1500 {
978    #[allow(dead_code)]
979    pub fn new() -> Self {
980        Self {
981            values: std::collections::HashMap::new(),
982            read_only: false,
983            name: String::new(),
984        }
985    }
986    #[allow(dead_code)]
987    pub fn named(name: &str) -> Self {
988        Self {
989            values: std::collections::HashMap::new(),
990            read_only: false,
991            name: name.to_string(),
992        }
993    }
994    #[allow(dead_code)]
995    pub fn set(&mut self, key: &str, value: SynthInstanceExtConfigVal1500) -> bool {
996        if self.read_only {
997            return false;
998        }
999        self.values.insert(key.to_string(), value);
1000        true
1001    }
1002    #[allow(dead_code)]
1003    pub fn get(&self, key: &str) -> Option<&SynthInstanceExtConfigVal1500> {
1004        self.values.get(key)
1005    }
1006    #[allow(dead_code)]
1007    pub fn get_bool(&self, key: &str) -> Option<bool> {
1008        self.get(key)?.as_bool()
1009    }
1010    #[allow(dead_code)]
1011    pub fn get_int(&self, key: &str) -> Option<i64> {
1012        self.get(key)?.as_int()
1013    }
1014    #[allow(dead_code)]
1015    pub fn get_str(&self, key: &str) -> Option<&str> {
1016        self.get(key)?.as_str()
1017    }
1018    #[allow(dead_code)]
1019    pub fn set_bool(&mut self, key: &str, v: bool) -> bool {
1020        self.set(key, SynthInstanceExtConfigVal1500::Bool(v))
1021    }
1022    #[allow(dead_code)]
1023    pub fn set_int(&mut self, key: &str, v: i64) -> bool {
1024        self.set(key, SynthInstanceExtConfigVal1500::Int(v))
1025    }
1026    #[allow(dead_code)]
1027    pub fn set_str(&mut self, key: &str, v: &str) -> bool {
1028        self.set(key, SynthInstanceExtConfigVal1500::Str(v.to_string()))
1029    }
1030    #[allow(dead_code)]
1031    pub fn lock(&mut self) {
1032        self.read_only = true;
1033    }
1034    #[allow(dead_code)]
1035    pub fn unlock(&mut self) {
1036        self.read_only = false;
1037    }
1038    #[allow(dead_code)]
1039    pub fn size(&self) -> usize {
1040        self.values.len()
1041    }
1042    #[allow(dead_code)]
1043    pub fn has(&self, key: &str) -> bool {
1044        self.values.contains_key(key)
1045    }
1046    #[allow(dead_code)]
1047    pub fn remove(&mut self, key: &str) -> bool {
1048        self.values.remove(key).is_some()
1049    }
1050}
1051/// Result of instance synthesis.
1052#[derive(Clone, Debug)]
1053pub enum SynthResult {
1054    /// Successfully synthesized an instance.
1055    Success(Expr),
1056    /// Synthesis failed (no matching instance found).
1057    Failure,
1058    /// Synthesis is stuck (waiting for metavar assignment).
1059    Stuck(MVarId),
1060}
1061impl SynthResult {
1062    /// Check if synthesis succeeded.
1063    pub fn is_success(&self) -> bool {
1064        matches!(self, SynthResult::Success(_))
1065    }
1066    /// Get the synthesized expression, if successful.
1067    pub fn expr(&self) -> Option<&Expr> {
1068        match self {
1069            SynthResult::Success(e) => Some(e),
1070            _ => None,
1071        }
1072    }
1073}
1074/// A generator/consumer node in the tabled resolution search.
1075#[derive(Clone, Debug)]
1076#[allow(dead_code)]
1077pub(crate) struct ResolutionNode {
1078    /// Goal being solved.
1079    pub(super) goal: Expr,
1080    /// Depth of this node in search tree.
1081    pub(super) depth: u32,
1082    /// Candidates to try for this goal.
1083    pub(super) candidates: Vec<InstanceEntry>,
1084    /// Current candidate index.
1085    pub(super) current_index: usize,
1086    /// Whether this node has been completed.
1087    pub(super) completed: bool,
1088    /// Cached result, if any.
1089    pub(super) cached_result: Option<Expr>,
1090}
1091/// A configuration store for SynthInstance.
1092#[allow(dead_code)]
1093pub struct SynthInstanceConfig {
1094    pub values: std::collections::HashMap<String, SynthInstanceConfigValue>,
1095    pub read_only: bool,
1096}
1097#[allow(dead_code)]
1098impl SynthInstanceConfig {
1099    pub fn new() -> Self {
1100        SynthInstanceConfig {
1101            values: std::collections::HashMap::new(),
1102            read_only: false,
1103        }
1104    }
1105    pub fn set(&mut self, key: &str, value: SynthInstanceConfigValue) -> bool {
1106        if self.read_only {
1107            return false;
1108        }
1109        self.values.insert(key.to_string(), value);
1110        true
1111    }
1112    pub fn get(&self, key: &str) -> Option<&SynthInstanceConfigValue> {
1113        self.values.get(key)
1114    }
1115    pub fn get_bool(&self, key: &str) -> Option<bool> {
1116        self.get(key)?.as_bool()
1117    }
1118    pub fn get_int(&self, key: &str) -> Option<i64> {
1119        self.get(key)?.as_int()
1120    }
1121    pub fn get_str(&self, key: &str) -> Option<&str> {
1122        self.get(key)?.as_str()
1123    }
1124    pub fn set_bool(&mut self, key: &str, v: bool) -> bool {
1125        self.set(key, SynthInstanceConfigValue::Bool(v))
1126    }
1127    pub fn set_int(&mut self, key: &str, v: i64) -> bool {
1128        self.set(key, SynthInstanceConfigValue::Int(v))
1129    }
1130    pub fn set_str(&mut self, key: &str, v: &str) -> bool {
1131        self.set(key, SynthInstanceConfigValue::Str(v.to_string()))
1132    }
1133    pub fn lock(&mut self) {
1134        self.read_only = true;
1135    }
1136    pub fn unlock(&mut self) {
1137        self.read_only = false;
1138    }
1139    pub fn size(&self) -> usize {
1140        self.values.len()
1141    }
1142    pub fn has(&self, key: &str) -> bool {
1143        self.values.contains_key(key)
1144    }
1145    pub fn remove(&mut self, key: &str) -> bool {
1146        self.values.remove(key).is_some()
1147    }
1148}
1149/// Statistics about a synthesis search.
1150#[derive(Clone, Debug, Default)]
1151pub struct SearchStats {
1152    /// Total instances examined.
1153    pub instances_examined: u32,
1154    /// Successful unifications.
1155    pub successful_unifications: u32,
1156    /// Failed unifications.
1157    pub failed_unifications: u32,
1158    /// Recursive calls made.
1159    pub recursive_calls: u32,
1160    /// Cache hits.
1161    pub cache_hits: u32,
1162    /// Heartbeats used.
1163    pub heartbeats_used: u64,
1164    /// Maximum depth reached.
1165    pub max_depth_reached: u32,
1166}
1167#[allow(dead_code)]
1168pub struct SynthInstanceExtPass1500 {
1169    pub name: String,
1170    pub total_runs: usize,
1171    pub successes: usize,
1172    pub errors: usize,
1173    pub enabled: bool,
1174    pub results: Vec<SynthInstanceExtResult1500>,
1175}
1176impl SynthInstanceExtPass1500 {
1177    #[allow(dead_code)]
1178    pub fn new(name: &str) -> Self {
1179        Self {
1180            name: name.to_string(),
1181            total_runs: 0,
1182            successes: 0,
1183            errors: 0,
1184            enabled: true,
1185            results: Vec::new(),
1186        }
1187    }
1188    #[allow(dead_code)]
1189    pub fn run(&mut self, input: &str) -> SynthInstanceExtResult1500 {
1190        if !self.enabled {
1191            return SynthInstanceExtResult1500::Skipped;
1192        }
1193        self.total_runs += 1;
1194        let result = if input.is_empty() {
1195            self.errors += 1;
1196            SynthInstanceExtResult1500::Err(format!("empty input in pass '{}'", self.name))
1197        } else {
1198            self.successes += 1;
1199            SynthInstanceExtResult1500::Ok(format!(
1200                "processed {} chars in pass '{}'",
1201                input.len(),
1202                self.name
1203            ))
1204        };
1205        self.results.push(result.clone());
1206        result
1207    }
1208    #[allow(dead_code)]
1209    pub fn success_count(&self) -> usize {
1210        self.successes
1211    }
1212    #[allow(dead_code)]
1213    pub fn error_count(&self) -> usize {
1214        self.errors
1215    }
1216    #[allow(dead_code)]
1217    pub fn success_rate(&self) -> f64 {
1218        if self.total_runs == 0 {
1219            0.0
1220        } else {
1221            self.successes as f64 / self.total_runs as f64
1222        }
1223    }
1224    #[allow(dead_code)]
1225    pub fn disable(&mut self) {
1226        self.enabled = false;
1227    }
1228    #[allow(dead_code)]
1229    pub fn enable(&mut self) {
1230        self.enabled = true;
1231    }
1232    #[allow(dead_code)]
1233    pub fn clear_results(&mut self) {
1234        self.results.clear();
1235    }
1236}
1237#[allow(dead_code)]
1238pub struct SynthInstanceExtDiag1500 {
1239    pub errors: Vec<String>,
1240    pub warnings: Vec<String>,
1241    pub notes: Vec<String>,
1242    pub max_errors: usize,
1243}
1244impl SynthInstanceExtDiag1500 {
1245    #[allow(dead_code)]
1246    pub fn new(max_errors: usize) -> Self {
1247        Self {
1248            errors: Vec::new(),
1249            warnings: Vec::new(),
1250            notes: Vec::new(),
1251            max_errors,
1252        }
1253    }
1254    #[allow(dead_code)]
1255    pub fn error(&mut self, msg: &str) {
1256        if self.errors.len() < self.max_errors {
1257            self.errors.push(msg.to_string());
1258        }
1259    }
1260    #[allow(dead_code)]
1261    pub fn warning(&mut self, msg: &str) {
1262        self.warnings.push(msg.to_string());
1263    }
1264    #[allow(dead_code)]
1265    pub fn note(&mut self, msg: &str) {
1266        self.notes.push(msg.to_string());
1267    }
1268    #[allow(dead_code)]
1269    pub fn has_errors(&self) -> bool {
1270        !self.errors.is_empty()
1271    }
1272    #[allow(dead_code)]
1273    pub fn num_errors(&self) -> usize {
1274        self.errors.len()
1275    }
1276    #[allow(dead_code)]
1277    pub fn num_warnings(&self) -> usize {
1278        self.warnings.len()
1279    }
1280    #[allow(dead_code)]
1281    pub fn is_clean(&self) -> bool {
1282        self.errors.is_empty() && self.warnings.is_empty()
1283    }
1284    #[allow(dead_code)]
1285    pub fn at_error_limit(&self) -> bool {
1286        self.errors.len() >= self.max_errors
1287    }
1288    #[allow(dead_code)]
1289    pub fn clear(&mut self) {
1290        self.errors.clear();
1291        self.warnings.clear();
1292        self.notes.clear();
1293    }
1294    #[allow(dead_code)]
1295    pub fn summary(&self) -> String {
1296        format!(
1297            "{} error(s), {} warning(s)",
1298            self.errors.len(),
1299            self.warnings.len()
1300        )
1301    }
1302}
oxilean_meta/synth_instance/types.rs

oxilean_meta/synth_instance/
types.rs
