darcsweb - verified/html_pure.v

(** Verified pure functions for HTML escaping.
    Extracted to Haskell for use in the DarcsWeb application. *)

From Stdlib.Strings Require Import Byte.
From Stdlib Require Import Ascii String Bool.
From Stdlib Require Import ExtrHaskellString.

Open Scope string_scope.

(* Characters that cannot be easily written as Coq string literals *)
Definition dquote : ascii := Ascii.ascii_of_byte Byte.x22.
Definition squote : ascii := Ascii.ascii_of_byte Byte.x27.

(** HTML-escape a single character.
    Replaces <, >, &, double-quote, single-quote with their HTML entity
    equivalents. *)
Definition esc_char (c : ascii) : string :=
  if Ascii.eqb c "<"%char then "&lt;"
  else if Ascii.eqb c ">"%char then "&gt;"
  else if Ascii.eqb c "&"%char then "&amp;"
  else if Ascii.eqb c dquote then "&quot;"
  else if Ascii.eqb c squote then "&#39;"
  else String c EmptyString.

(** HTML-escape an entire string by escaping each character. *)
Fixpoint esc (s : string) : string :=
  match s with
  | EmptyString => EmptyString
  | String c rest => String.append (esc_char c) (esc rest)
  end.

(* -- Extraction setup -- *)
Set Extraction Output Directory "../gen".
Extraction Language Haskell.

Extract Inlined Constant String.append => "(Prelude.++)".

Extraction "HtmlPure" esc_char esc.