// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0

pub fn ostring_to_dafny(
    input: &Option<String>,
) -> ::dafny_runtime::Rc<
    crate::_Wrappers_Compile::Option<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>,
> {
    let dafny_value = match input {
    Some(b) => crate::_Wrappers_Compile::Option::Some { value:
        dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(&b)
        },
    None => crate::_Wrappers_Compile::Option::None {},
};
    ::dafny_runtime::Rc::new(dafny_value)
}

pub fn ostring_from_dafny(
    input: ::dafny_runtime::Rc<
        crate::_Wrappers_Compile::Option<
            ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>,
        >,
    >,
) -> Option<String> {
    if matches!(
        input.as_ref(),
        crate::_Wrappers_Compile::Option::Some { .. }
    ) {
        Some(
            dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(
                &input.Extract(),
            ),
        )
    } else {
        None
    }
}

pub fn obool_to_dafny(
    input: &Option<bool>,
) -> ::dafny_runtime::Rc<crate::_Wrappers_Compile::Option<bool>> {
    let dafny_value = match input {
        Some(b) => crate::_Wrappers_Compile::Option::Some { value: *b },
        None => crate::_Wrappers_Compile::Option::None {},
    };
    ::dafny_runtime::Rc::new(dafny_value)
}

pub fn obool_from_dafny(
    input: ::dafny_runtime::Rc<crate::_Wrappers_Compile::Option<bool>>,
) -> Option<bool> {
    if matches!(
        input.as_ref(),
        crate::_Wrappers_Compile::Option::Some { .. }
    ) {
        Some(input.Extract())
    } else {
        None
    }
}

pub fn oint_to_dafny(
    input: Option<i32>,
) -> ::dafny_runtime::Rc<crate::_Wrappers_Compile::Option<i32>> {
    let dafny_value = match input {
        Some(b) => crate::_Wrappers_Compile::Option::Some { value: b },
        None => crate::_Wrappers_Compile::Option::None {},
    };
    ::dafny_runtime::Rc::new(dafny_value)
}

pub fn oint_from_dafny(
    input: ::dafny_runtime::Rc<crate::_Wrappers_Compile::Option<i32>>,
) -> Option<i32> {
    if matches!(
        input.as_ref(),
        crate::_Wrappers_Compile::Option::Some { .. }
    ) {
        Some(input.Extract())
    } else {
        None
    }
}

pub fn olong_to_dafny(
    input: &Option<i64>,
) -> ::dafny_runtime::Rc<crate::_Wrappers_Compile::Option<i64>> {
    let dafny_value = match input {
        Some(b) => crate::_Wrappers_Compile::Option::Some { value: *b },
        None => crate::_Wrappers_Compile::Option::None {},
    };
    ::dafny_runtime::Rc::new(dafny_value)
}

pub fn olong_from_dafny(
    input: ::dafny_runtime::Rc<crate::_Wrappers_Compile::Option<i64>>,
) -> Option<i64> {
    if matches!(
        input.as_ref(),
        crate::_Wrappers_Compile::Option::Some { .. }
    ) {
        Some(input.Extract())
    } else {
        None
    }
}

pub fn blob_to_dafny(input: &::aws_smithy_types::Blob) -> ::dafny_runtime::Sequence<u8> {
    ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(
        &input.clone().into_inner(),
        |x| *x,
    )
}

pub fn oblob_to_dafny(
    input: &Option<::aws_smithy_types::Blob>,
) -> ::dafny_runtime::Rc<crate::_Wrappers_Compile::Option<::dafny_runtime::Sequence<u8>>> {
    let dafny_value = match input {
        Some(b) => crate::_Wrappers_Compile::Option::Some {
            value: blob_to_dafny(&b),
        },
        None => crate::_Wrappers_Compile::Option::None {},
    };
    ::dafny_runtime::Rc::new(dafny_value)
}

pub fn blob_from_dafny(input: ::dafny_runtime::Sequence<u8>) -> ::aws_smithy_types::Blob {
    ::aws_smithy_types::Blob::new(
        ::dafny_runtime::Rc::try_unwrap(input.to_array()).unwrap_or_else(|rc| (*rc).clone()),
    )
}

pub fn oblob_from_dafny(
    input: ::dafny_runtime::Rc<crate::_Wrappers_Compile::Option<::dafny_runtime::Sequence<u8>>>,
) -> Option<::aws_smithy_types::Blob> {
    if matches!(
        input.as_ref(),
        crate::_Wrappers_Compile::Option::Some { .. }
    ) {
        Some(blob_from_dafny(input.Extract()))
    } else {
        None
    }
}

pub fn double_to_dafny(input: f64) -> ::dafny_runtime::Sequence<u8> {
    ::dafny_runtime::dafny_runtime_conversions::vec_to_dafny_sequence(
        &f64::to_be_bytes(input).to_vec(),
        |x| *x,
    )
}

pub fn odouble_to_dafny(
    input: &Option<f64>,
) -> ::dafny_runtime::Rc<crate::_Wrappers_Compile::Option<::dafny_runtime::Sequence<u8>>> {
    let dafny_value = match input {
        Some(f) => crate::_Wrappers_Compile::Option::Some {
            value: double_to_dafny(*f),
        },
        None => crate::_Wrappers_Compile::Option::None {},
    };
    ::dafny_runtime::Rc::new(dafny_value)
}

pub fn double_from_dafny(input: &::dafny_runtime::Sequence<u8>) -> f64 {
    let v = ::dafny_runtime::dafny_runtime_conversions::dafny_sequence_to_vec(input, |x| *x);
    f64::from_be_bytes(v.try_into().expect("Error converting Sequence to f64"))
}

pub fn odouble_from_dafny(
    input: ::dafny_runtime::Rc<crate::_Wrappers_Compile::Option<::dafny_runtime::Sequence<u8>>>,
) -> Option<f64> {
    if matches!(
        input.as_ref(),
        crate::_Wrappers_Compile::Option::Some { .. }
    ) {
        Some(double_from_dafny(&input.Extract()))
    } else {
        None
    }
}

pub fn timestamp_to_dafny(
    input: &::aws_smithy_types::DateTime,
) -> ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16> {
    ::dafny_runtime::dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string(
        &input.to_string(),
    )
}

pub fn otimestamp_to_dafny(
    input: &Option<::aws_smithy_types::DateTime>,
) -> ::dafny_runtime::Rc<
    crate::_Wrappers_Compile::Option<::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>>,
> {
    let dafny_value = match input {
        Some(f) => crate::_Wrappers_Compile::Option::Some {
            value: timestamp_to_dafny(f),
        },
        None => crate::_Wrappers_Compile::Option::None {},
    };
    ::dafny_runtime::Rc::new(dafny_value)
}

pub fn timestamp_from_dafny(
    input: ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>,
) -> ::aws_smithy_types::DateTime {
    let s = dafny_runtime::dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string(
        &input,
    );
    ::aws_smithy_types::DateTime::from_str(&s, aws_smithy_types::date_time::Format::DateTime)
        .unwrap()
}

pub fn otimestamp_from_dafny(
    input: ::dafny_runtime::Rc<
        crate::_Wrappers_Compile::Option<
            ::dafny_runtime::Sequence<::dafny_runtime::DafnyCharUTF16>,
        >,
    >,
) -> Option<::aws_smithy_types::DateTime> {
    if matches!(
        input.as_ref(),
        crate::_Wrappers_Compile::Option::Some { .. }
    ) {
        Some(timestamp_from_dafny(input.Extract()))
    } else {
        None
    }
}

pub fn option_from_dafny<T: ::dafny_runtime::DafnyType, TR>(
    input: ::dafny_runtime::Rc<crate::_Wrappers_Compile::Option<T>>,
    converter: fn(&T) -> TR,
) -> Option<TR> {
    match &*input {
        crate::_Wrappers_Compile::Option::Some { value } => Some(converter(value)),
        crate::_Wrappers_Compile::Option::None {} => None,
    }
}

pub fn option_to_dafny<T: ::dafny_runtime::DafnyType, TR>(
    input: &Option<TR>,
    converter: fn(&TR) -> T,
) -> ::dafny_runtime::Rc<crate::_Wrappers_Compile::Option<T>> {
    match input {
        Some(value) => ::dafny_runtime::Rc::new(crate::_Wrappers_Compile::Option::Some {
            value: converter(&value),
        }),
        None => ::dafny_runtime::Rc::new(crate::_Wrappers_Compile::Option::None {}),
    }
}

pub fn result_from_dafny<T: ::dafny_runtime::DafnyType, TR, E: ::dafny_runtime::DafnyType, ER>(
    input: ::dafny_runtime::Rc<crate::_Wrappers_Compile::Result<T, E>>,
    converter_t: fn(&T) -> TR,
    converter_e: fn(&E) -> ER,
) -> Result<TR, ER> {
    match &*input {
        crate::_Wrappers_Compile::Result::Success { value } => Ok(converter_t(value)),
        crate::_Wrappers_Compile::Result::Failure { error } => Err(converter_e(error)),
    }
}

pub fn result_to_dafny<T: ::dafny_runtime::DafnyType, TR, E: ::dafny_runtime::DafnyType, ER>(
    input: &Result<TR, ER>,
    converter_t: fn(&TR) -> T,
    converter_e: fn(&ER) -> E,
) -> ::dafny_runtime::Rc<crate::_Wrappers_Compile::Result<T, E>> {
    match input {
        Ok(value) => ::dafny_runtime::Rc::new(crate::_Wrappers_Compile::Result::Success {
            value: converter_t(&value),
        }),
        Err(error) => ::dafny_runtime::Rc::new(crate::_Wrappers_Compile::Result::Failure {
            error: converter_e(&error),
        }),
    }
}
