val string_of_result : f: (_: _ -> Prims.string) -> _: FStar.Error.optResult (MiTLS.Parsers.Alert.alert * Prims.string) _
  -> Prims.string
let string_of_result f = function
  | Error z -> "Error: "^string_of_error z
  | Correct v -> f v
﻿module MiTLS.TLSError
open MiTLS
open FStar.String
(* TLS explicitly returns run-time errors:
   results carry either values or error descriptions *)

include MiTLS.Parsers.AlertDescription
include MiTLS.Parsers.AlertLevel
include MiTLS.Parsers.Alert

let string_of_alertDescription (a:alertDescription) = "alertDescription"
let string_of_alertLevel (a:alertLevel) = "alertLevel"
let string_of_alert (a:alert) = 
  "level="^string_of_alertLevel a.level^
  "description="^string_of_alertDescription a.description

let fatalAlert ad = {level=Fatal; description=ad}

(* TODO functions checking consistency of levels and descriptions *)

// let isFatal ad =
//     match ad with
//     | AD_unexpected_message
//     | AD_bad_record_mac
//     | AD_decryption_failed
//     | AD_record_overflow
//     | AD_decompression_failure
//     | AD_handshake_failure
//     | AD_bad_certificate_fatal
//     | AD_unsupported_certificate_fatal
//     | AD_certificate_revoked_fatal
//     | AD_certificate_expired_fatal
//     | AD_certificate_unknown_fatal
//     | AD_illegal_parameter
//     | AD_unknown_ca
//     | AD_access_denied
//     | AD_decode_error
//     | AD_decrypt_error
//     | AD_export_restriction
//     | AD_protocol_version
//     | AD_insufficient_security
//     | AD_internal_error
//     | AD_user_cancelled_fatal
//     | AD_missing_extension
//     | AD_unsupported_extension
//     | AD_no_application_protocol -> true
//     | _ -> false

type error = alert * string
let string_of_error (a,s)= string_of_alertDescription a.description^" ("^s^")"

type result 'a = FStar.Error.optResult error 'a
/
prims.fst.checked MiTLS.Parsers.AlertLevel.fsti.checked MiTLS.Parsers.AlertDescription.fsti.checked MiTLS.Parsers.Alert.fsti.checked FStar.String.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Error.fst.checked
MiTLS.TLSError.fst
f: (_: _ -> Prims.string) -> _: FStar.Error.optResult (MiTLS.Parsers.Alert.alert * Prims.string) _
  -> Prims.string
Prims.string FStar.Error.optResult FStar.Pervasives.Native.tuple2 MiTLS.Parsers.Alert.alert Prims.op_Hat MiTLS.TLSError.string_of_error
let string_of_result f =
  
function
| Error z -> "Error: " ^ string_of_error z
| Correct v -> f v