aeneas icon indicating copy to clipboard operation
aeneas copied to clipboard

Update the way spans of external definitions are printed

Open sonmarcho opened this issue 1 year ago • 0 comments

Today, when printing spans for external declarations we generated ugly strings, leading to noise in the generated code. For instance:

/- [core::cell::{core::cell::Cell<T>#10}::get]:
   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 497:4-497:26
   Name pattern: core::cell::{core::cell::Cell<@T>}::get -/
axiom core.cell.Cell.get
  (T : Type) (markerCopyInst : core.marker.Copy T) :
  core.cell.Cell T → State → Result (State × T)

/- [core::cell::{core::cell::Cell<T>#11}::get_mut]:
   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 574:4-574:39
   Name pattern: core::cell::{core::cell::Cell<@T>}::get_mut -/
axiom core.cell.Cell.get_mut
  (T : Type) :
  core.cell.Cell T → State → Result (State × (T × (T → State → Result
    (State × (core.cell.Cell T)))))

We would like to have something like:

/- [core::cell::{core::cell::Cell<T>#10}::get]:
   Source: 'core/src/cell.rs', lines 497:4-497:26
   Name pattern: core::cell::{core::cell::Cell<@T>}::get -/
axiom core.cell.Cell.get
  (T : Type) (markerCopyInst : core.marker.Copy T) :
  core.cell.Cell T → State → Result (State × T)

/- [core::cell::{core::cell::Cell<T>#11}::get_mut]:
   Source: 'core/src/cell.rs', lines 574:4-574:39
   Name pattern: core::cell::{core::cell::Cell<@T>}::get_mut -/
axiom core.cell.Cell.get_mut
  (T : Type) :
  core.cell.Cell T → State → Result (State × (T × (T → State → Result
    (State × (core.cell.Cell T)))))

sonmarcho avatar Apr 25 '24 11:04 sonmarcho