Add support for ADTs with lifetimes

[zhassan-aws]

Code:

struct Foo<'a> {
    x: &'a i32,
}

fn main() { }

Output:

$ charon
   Compiling ref_in_struct v0.1.0 (/home/ubuntu/examples/aeneas/ref_in_struct)
[ INFO charon_driver::export:106] [gexport]: Generated the file: /home/ubuntu/examples/aeneas/ref_in_struct/ref_in_struct.llbc
    Finished release [optimized] target(s) in 0.15s
$ aeneas -backend lean ref_in_struct.llbc 
[Info ] Imported: ref_in_struct.llbc
Uncaught exception:
  
  "Assert_failure SymbolicToPure.ml:554:2"

Raised at Aeneas__SymbolicToPure.translate_type_decl in file "SymbolicToPure.ml", line 554, characters 2-23
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 277, characters 19-64
Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 992, characters 4-33
Called from Dune__exe__Main in file "Main.ml", line 279, characters 6-58

[sonmarcho]

Yes, we don't support ADTs with lifetimes for now (I intend to lift this soon).
Also, on the shorter term: we're about to start an overhaul of Aeneas to have informative error messages (I've been wanting this for a while and I think it's time).

[zhassan-aws]

This also impacts std::str::chars, e.g:

fn foo(s: &str) {
    let _c = s.chars();
}

$ aeneas -backend lean ref_in_struct.llbc 
[Info ] Imported: ref_in_struct.llbc
Uncaught exception:
  
  Not_found

Raised at Stdlib__Map.Make.find in file "map.ml", line 137, characters 10-25
Called from Stdlib__List.map in file "list.ml", line 92, characters 20-23
Called from Aeneas__Translate.export_types_group in file "Translate.ml", line 415, characters 4-72
Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15
Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 822, characters 2-52
Called from Aeneas__Translate.extract_file in file "Translate.ml", line 940, characters 2-36
Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1488, characters 5-42
Called from Dune__exe__Main in file "Main.ml", line 276, characters 9-61

[sonmarcho]

This was solved by #367
For the reference, here is the code generated from the std::str::chars example above :

axiom core.str.iter.Chars : Type

axiom core.str.str.chars : Str → Result core.str.iter.Chars

def foo (s : Str) : Result Unit :=
  do
  let _ ← core.str.str.chars s
  Result.ok ()

Note that this made noticed that Str is actually not defined in the Lean library...