-
Notifications
You must be signed in to change notification settings - Fork 8
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge branch 'main-1.x' into Golang/dev
- Loading branch information
Showing
409 changed files
with
9,523 additions
and
10,543 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
80 changes: 80 additions & 0 deletions
80
TestModels/Aggregate/runtimes/rust/src/standard_library_externs.rs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,80 @@ | ||
| // Annotation to ignore the case of this module | ||
| use crate::r#_Wrappers_Compile; | ||
| use crate::UTF8; | ||
|
|
||
| impl crate::UTF8::_default { | ||
| pub fn Encode( | ||
| s: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, | ||
| ) -> ::std::rc::Rc< | ||
| r#_Wrappers_Compile::Result< | ||
| UTF8::ValidUTF8Bytes, | ||
| ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, | ||
| >, | ||
| > { | ||
| let v = s.to_array(); | ||
| let mut _accumulator: Vec<u8> = vec![]; | ||
| // Use of .encode_utf8 method. | ||
| let mut surrogate: Option<u16> = None; | ||
| for c in v.iter() { | ||
| let s = if let Some(s) = surrogate { | ||
| String::from_utf16(&[s, c.0]) | ||
| } else { | ||
| String::from_utf16(&[c.0]) | ||
| }; | ||
| surrogate = None; | ||
| match s { | ||
| Ok(value) => { | ||
| _accumulator.extend(value.as_bytes()); | ||
| continue; | ||
| } | ||
| Err(e) => { | ||
| if 0xD800 <= c.0 && c.0 <= 0xDFFF { | ||
| surrogate = Some(c.0); | ||
| continue; | ||
| } | ||
| return ::std::rc::Rc::new(r#_Wrappers_Compile::Result::<UTF8::ValidUTF8Bytes, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>::Failure { | ||
| error: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string( | ||
| &e.to_string()) | ||
| }); | ||
| } | ||
| } | ||
| } | ||
| if let Some(s) = surrogate { | ||
| return ::std::rc::Rc::new(r#_Wrappers_Compile::Result::<UTF8::ValidUTF8Bytes, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>::Failure { | ||
| error: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string( | ||
| &format!("Surrogate pair missing: 0x{:04x}", s)) | ||
| }); | ||
| } | ||
| ::std::rc::Rc::new(r#_Wrappers_Compile::Result::< | ||
| UTF8::ValidUTF8Bytes, | ||
| ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, | ||
| >::Success { | ||
| value: ::dafny_runtime::Sequence::from_array_owned(_accumulator), | ||
| }) | ||
| } | ||
| pub fn Decode( | ||
| b: &::dafny_runtime::Sequence<u8>, | ||
| ) -> ::std::rc::Rc< | ||
| r#_Wrappers_Compile::Result< | ||
| ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, | ||
| ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, | ||
| >, | ||
| > { | ||
| let b = String::from_utf8(b.to_array().as_ref().clone()); | ||
| match b { | ||
| Ok(s) => { | ||
| ::std::rc::Rc::new(r#_Wrappers_Compile::Result::<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, | ||
| ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>::Success { | ||
| value: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&s) | ||
| }) | ||
| }, | ||
| Err(e) => { | ||
| return ::std::rc::Rc::new(r#_Wrappers_Compile::Result::<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, | ||
| ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>::Failure { | ||
| error: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string( | ||
| &e.to_string()) | ||
| }) | ||
| } | ||
| } | ||
| } | ||
| } |
80 changes: 80 additions & 0 deletions
80
TestModels/Constructor/runtimes/rust/src/standard_library_externs.rs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,80 @@ | ||
| // Annotation to ignore the case of this module | ||
| use crate::r#_Wrappers_Compile; | ||
| use crate::UTF8; | ||
|
|
||
| impl crate::UTF8::_default { | ||
| pub fn Encode( | ||
| s: &::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, | ||
| ) -> ::std::rc::Rc< | ||
| r#_Wrappers_Compile::Result< | ||
| UTF8::ValidUTF8Bytes, | ||
| ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, | ||
| >, | ||
| > { | ||
| let v = s.to_array(); | ||
| let mut _accumulator: Vec<u8> = vec![]; | ||
| // Use of .encode_utf8 method. | ||
| let mut surrogate: Option<u16> = None; | ||
| for c in v.iter() { | ||
| let s = if let Some(s) = surrogate { | ||
| String::from_utf16(&[s, c.0]) | ||
| } else { | ||
| String::from_utf16(&[c.0]) | ||
| }; | ||
| surrogate = None; | ||
| match s { | ||
| Ok(value) => { | ||
| _accumulator.extend(value.as_bytes()); | ||
| continue; | ||
| } | ||
| Err(e) => { | ||
| if 0xD800 <= c.0 && c.0 <= 0xDFFF { | ||
| surrogate = Some(c.0); | ||
| continue; | ||
| } | ||
| return ::std::rc::Rc::new(r#_Wrappers_Compile::Result::<UTF8::ValidUTF8Bytes, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>::Failure { | ||
| error: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string( | ||
| &e.to_string()) | ||
| }); | ||
| } | ||
| } | ||
| } | ||
| if let Some(s) = surrogate { | ||
| return ::std::rc::Rc::new(r#_Wrappers_Compile::Result::<UTF8::ValidUTF8Bytes, ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>::Failure { | ||
| error: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string( | ||
| &format!("Surrogate pair missing: 0x{:04x}", s)) | ||
| }); | ||
| } | ||
| ::std::rc::Rc::new(r#_Wrappers_Compile::Result::< | ||
| UTF8::ValidUTF8Bytes, | ||
| ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, | ||
| >::Success { | ||
| value: ::dafny_runtime::Sequence::from_array_owned(_accumulator), | ||
| }) | ||
| } | ||
| pub fn Decode( | ||
| b: &::dafny_runtime::Sequence<u8>, | ||
| ) -> ::std::rc::Rc< | ||
| r#_Wrappers_Compile::Result< | ||
| ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, | ||
| ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, | ||
| >, | ||
| > { | ||
| let b = String::from_utf8(b.to_array().as_ref().clone()); | ||
| match b { | ||
| Ok(s) => { | ||
| ::std::rc::Rc::new(r#_Wrappers_Compile::Result::<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, | ||
| ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>::Success { | ||
| value: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&s) | ||
| }) | ||
| }, | ||
| Err(e) => { | ||
| return ::std::rc::Rc::new(r#_Wrappers_Compile::Result::<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>, | ||
| ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>::Failure { | ||
| error: ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string( | ||
| &e.to_string()) | ||
| }) | ||
| } | ||
| } | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.