val synth_character_string
      (t: character_string_type)
      (len: asn1_value_int32_of_type t)
      (s32: parse_filter_refine (filter_character_string t len))
    : GTot (x: datatype_of_asn1_type t {len_of_character_string t x == len})
val synth_character_string
      (t: character_string_type)
      (len: asn1_value_int32_of_type t)
      (s32: parse_filter_refine (filter_character_string t len))
    : GTot (x: datatype_of_asn1_type t {len_of_character_string t x == len})
let synth_character_string
  (t: character_string_type)
  (len: asn1_value_int32_of_type t)
  (s32: parse_filter_refine (filter_character_string t len))
: GTot (x: datatype_of_asn1_type t{ len_of_character_string t x == len })
= match t with
  | IA5_STRING -> synth_asn1_ia5_string len s32
  | PRINTABLE_STRING -> synth_asn1_printable_string len s32
module ASN1.Spec.Value.CharacterString

open ASN1.Spec.Base
open LowParse.Spec.Bytes

open ASN1.Base
open ASN1.Spec.Tag
open ASN1.Spec.Length
include ASN1.Spec.Value.StringCombinator
include ASN1.Spec.Value.IA5_STRING
include ASN1.Spec.Value.PRINTABLE_STRING

open FStar.Integers

module B32 = FStar.Bytes

#set-options "--z3rlimit 32 --fuel 0 --ifuel 0"

(* ZT: I think we can leave this module exposed. *)

noextract inline_for_extraction
let len_of_character_string
  (t: character_string_type)
  (x: datatype_of_asn1_type t)
: Tot (asn1_value_int32_of_type t)
= match t with
  | IA5_STRING -> dfst (x <: datatype_of_asn1_type IA5_STRING)
  | PRINTABLE_STRING -> dfst (x <: datatype_of_asn1_type PRINTABLE_STRING)

let filter_character_string
  (t: character_string_type)
  (len: asn1_value_int32_of_type t)
  (s32: B32.lbytes32 len)
: GTot (bool)
= match t with
  | IA5_STRING -> filter_asn1_ia5_string len s32
  | PRINTABLE_STRING -> filter_asn1_printable_string len s32
/
prims.fst.checked LowParse.Spec.Bytes.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.Value.StringCombinator.fsti.checked ASN1.Spec.Value.PRINTABLE_STRING.fsti.checked ASN1.Spec.Value.IA5_STRING.fsti.checked ASN1.Spec.Tag.fsti.checked ASN1.Spec.Length.fsti.checked ASN1.Spec.Base.fst.checked ASN1.Base.fst.checked
ASN1.Spec.Value.CharacterString.fst

    t: ASN1.Base.character_string_type ->
    len: ASN1.Base.asn1_value_int32_of_type t ->
    s32:
      LowParse.Spec.Combinators.parse_filter_refine (ASN1.Spec.Value.CharacterString.filter_character_string
            t
            len)
  -> Prims.GTot
    (x:
      ASN1.Base.datatype_of_asn1_type t
        {ASN1.Spec.Value.CharacterString.len_of_character_string t x == len})
ASN1.Base.character_string_type ASN1.Base.asn1_value_int32_of_type LowParse.Spec.Combinators.parse_filter_refine FStar.Bytes.lbytes32 ASN1.Spec.Value.CharacterString.filter_character_string ASN1.Spec.Value.IA5_STRING.synth_asn1_ia5_string ASN1.Spec.Value.PRINTABLE_STRING.synth_asn1_printable_string ASN1.Base.datatype_of_asn1_type Prims.eq2 ASN1.Spec.Value.CharacterString.len_of_character_string
let synth_character_string
      (t: character_string_type)
      (len: asn1_value_int32_of_type t)
      (s32: parse_filter_refine (filter_character_string t len))
    : GTot (x: datatype_of_asn1_type t {len_of_character_string t x == len}) =
  
match t with
| IA5_STRING -> synth_asn1_ia5_string len s32
| PRINTABLE_STRING -> synth_asn1_printable_string len s32