The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Here, I did some "unescape : string → (bool * string)" function.

It is rather faithful to Ocaml conventions. I did not tested it much,
so there may be some bugs. It expects an escaped string as argument,
and returns a non escaped one and a boolean telling if the unescaping
was or was not full (so false means some error). In case of non valid
escaped string, the resulting string is one up to the error (which
helps to locate the error, rather than simply returning Nothing).

Note also that " is always escaped in Coq by doubling it, so:

"He says \"Hello\" to the audience"

is written in Coq:

"He says ""Hello"" to the audience"

but "" really counts as only one character.
Require Import Utf8.
Set Implicit Arguments.

Require Import Ascii.
Require Import String.
Require Import Bool.

Definition format := string.

Module Escape.
  Inductive unescaper :=
  | E : unescaper               (* error *)
  | S : ascii → unescaper       (* symbol *)
  | N : unescaper               (* newline *)
  | H : unescaper               (* hexa *)
  | D : option bool → unescaper (* deci *)
  .

  Definition unescape_sym a :=
    match a with
    | " "%char   => S " "%char
    | """"%char  => S """"%char
    | "'"%char   => S "'"%char
    | "\"%char   => S "\"%char
    | "b"%char   => S "008"%char
    | "n"%char   => S "010"%char
    | "r"%char   => S "013"%char
    | "t"%char   => S "009"%char
    | "x"%char   => H
    | "0"%char   => D (Some false)
    | "1"%char   => D (Some true)
    | "2"%char   => D None
    | "010"%char => N
    | _ => E
    end.

  Definition get_blank b :=
    match b with
    | " "%char => true
    | "010"%char => true
    | "009"%char => true
    | "013"%char => true
    | "012"%char => true
    | _ => false
    end.

  Definition get_digit a :=
    match a with
    | Ascii a b c d true true false false =>
      let l := (a, b, c, d) in
      if d then if c then None else if b then None else Some l
      else Some l
    | _ => None
    end.

  Definition get_hex a :=
    match a with
    | Ascii x y z false false _ true false =>
      let l := (negb x, xorb x y, orb z (andb x y), true) in
      if z then if y then if x then None else Some l else Some l else
      if y then Some l else if x then Some l else None
    | Ascii a b c d true true false false =>
      let l := (a, b, c, d) in
      if d then if c then None else if b then None else Some l
      else Some l
    | _ => None
    end.

  Fixpoint next (x : list bool) :=
    match x with nil => cons true nil
               | cons a x => if a then cons false (next x) else cons true x
    end.

  Fixpoint cplus (c : bool) x y :=
    match x with
    | nil => if c then next y else y
    | cons a x => match y with
                  | nil => if c then next (cons a x) else cons a x
                  | cons b y => cons (xorb a (xorb b c))
                                (cplus ((if a then orb else andb) b c) x y)
                  end
    end.

  Definition pack_digit x y z :=
    let h1 := cons true (cons false (cons false (cons true (cons true nil)))) in
    let h2 := cons false h1 in
    let h3 := cons false (cons false (cons false (cons false nil))) in
    let l1 := match x with
              | None => h2
              | Some true => h1
              | Some false => nil
              end in
    match get_digit y with
    | None => None
    | Some (a, b, c, d) =>
      let l2 := cons false (cons a (cons b (cons c (cons d nil)))) in
      match get_digit z with
      | None => None
      | Some (a, b, c, d) =>
        let l3 := cons a (cons b (cons c (cons d h3))) in
        match cplus false (cons false (cons false (cplus false l1 l2)))
                          (cplus false l2 l3) with
        |  cons a (cons b (cons c (cons d
          (cons e (cons f (cons g (cons h
           nil))))))) => Some (Ascii a b c d e f g h)
        | _ => None
        end
      end
    end.

  Definition pack_hex u v :=
    match get_hex u with
    | None => None
    | Some (a,b,c,d) => match get_hex v with
                        | None => None
                        | Some (x,y,z,t) => Some (Ascii x y z t a b c d)
                        end
    end.

  Fixpoint unescape_string sb s :=
    match s with
    | EmptyString => (true, EmptyString)
    | String a s =>
      let b := match a with "\"%char => true | _ => false end in
      if b
      then match s with
           | EmptyString => (false, EmptyString)
           | String a s =>
             match unescape_sym a with
             | S sym =>
               let (a, s) := unescape_string false s in (a, String sym s)
             | D o =>
               match s with
               | String u (String v s) =>
                 match pack_digit o u v with
                 | Some sym =>
                   let (a, s) := unescape_string false s in (a, String sym s)
                 | None => (false, EmptyString)
                 end
               | _ => (false, EmptyString)
               end
             | H =>
               match s with
               | String u (String v s) =>
                 match pack_hex u v with
                 | Some sym =>
                   let (a, s) := unescape_string false s in (a, String sym s)
                 | None => (false, EmptyString)
                 end
               | _ => (false, EmptyString)
               end
             | N => unescape_string true s
             | E => (false, EmptyString)
             end
           end
      else if andb sb (get_blank a)
           then unescape_string true s
           else let (x, s) := unescape_string false s in (x, String a s)
    end.
End Escape.

Definition unescape := Escape.unescape_string false.