Qcert.Compiler.Model.StringModelPart

Defines the foreign support for a native string type. Posits axioms for the basic data/operators, and defines how they are extracted to ocaml (using helper functions defined in qcert/ocaml/...../Util.ml)

Axiom STRING : Set.

Axiom STRING_eq : STRING → STRING → bool.
Hypothesis STRING_eq_correct :
∀ f1 f2, (STRING_eq f1 f2 = true ↔ f1 = f2).

Axiom STRING_tostring : STRING → String.string.

Extract Constant STRING ⇒ "string".
Extract Inlined Constant STRING_eq ⇒ "(fun x y -> x = y)".
Extract Inlined Constant STRING_tostring ⇒ "(fun x -> Util.char_list_of_string x)".