View Source cure_lsp_diagnostics (cure v0.7.0)

LSP Rich Diagnostics with SMT Counterexamples

This module enhances LSP diagnostics with:

  • Concrete counterexamples from SMT solver (e.g., \"x = -5 violates x > 0\")
  • Constraint context (shows where constraint was defined)
  • Related information links (jump to constraint definition)
  • Human-readable formatting of SMT output

Example Enhanced Diagnostic 

Error: Refinement type constraint violated
  Type: Positive
  Required: x > 0
  Counterexample: x = -5 violates constraint
  
  Defined at: examples/test.cure:10:15
  
  Hint: Add a guard clause 'when x > 0' or use runtime assertion

Features

Counterexample Formatting

  • Extract concrete values from SMT models
  • Format in Cure syntax (not SMT-LIB)
  • Show multiple variables if constraint involves them

Constraint Context

  • Track constraint definition locations
  • Show original Cure code for constraint
  • Link to definition via LSP relatedInformation

Hover Information

  • Show inferred refinement types on hover
  • Display active constraints for variables
  • Preview constraint satisfaction status

Summary

Functions

add_constraint_context(Diagnostic, Constraint, DefinitionLoc)
create_hover_info(VarName, RefinementType, Location)
create_pattern_diagnostic(MatchExpr, CounterExample, Location)
create_refinement_diagnostic(TypeName, Constraint, Location, SmtResult)
create_type_mismatch_diagnostic(Expected, Got, Reason, Location)
extract_counterexample/2
format_constraint_in_cure_syntax/1
format_counterexample_detailed/2
format_refinement_type_hover/2

Functions

add_constraint_context(Diagnostic, Constraint, DefinitionLoc)

-spec add_constraint_context(map(), term(), term()) -> map().

create_hover_info(VarName, RefinementType, Location)

-spec create_hover_info(atom(), term(), term()) -> map().

create_pattern_diagnostic(MatchExpr, CounterExample, Location)

-spec create_pattern_diagnostic(term(), term(), term()) -> map().

create_refinement_diagnostic(TypeName, Constraint, Location, SmtResult)

-spec create_refinement_diagnostic(atom(), term(), term(), term()) -> map().

create_type_mismatch_diagnostic(Expected, Got, Reason, Location)

-spec create_type_mismatch_diagnostic(term(), term(), term(), term()) -> map().

extract_counterexample/2

-spec extract_counterexample(term(), term()) -> map() | undefined.

format_constraint_in_cure_syntax/1

-spec format_constraint_in_cure_syntax(term()) -> binary().

format_counterexample_detailed/2

-spec format_counterexample_detailed(map(), term()) -> binary().

format_refinement_type_hover/2

-spec format_refinement_type_hover(atom(), term()) -> binary().