Qcert.Basic.Util.RString

Module AsciiOrder <: OrderedTypeFull with Definition t:=ascii.
  Definition t:= ascii.
  Definition eq := @eq t.
  Definition eq_equiv : (Equivalence eq) := eq_equivalence.
  Definition eq_dec := ascii_dec.

  Definition compare (a b:ascii) : comparison :=
    nat_compare (nat_of_ascii a) (nat_of_ascii b).

  Definition lt (a b:ascii) := compare a b = Lt.

  Lemma lt_strorder : StrictOrder lt.

  Lemma lt_compat : Proper (eq ==> eq ==> iff) lt.

  Lemma compare_eq_iff a b: compare a b = Eq ↔ a = b.

  Lemma compare_spec :
    ∀ x y : t, CompareSpec (eq x y) (lt x y) (lt y x) (compare x y).

  Lemma trichotemy a b : {lt a b} + {eq a b} + {lt b a}.

  Definition le (a b:ascii) :=
    match compare a b with
      | Lt ⇒ True
      | Eq ⇒ True
      | Gt ⇒ False
    end.

  Lemma le_lteq : ∀ x y : t, le x y ↔ lt x y ∨ eq x y.

  Lemma compare_refl_eq a: compare a a = Eq.

End AsciiOrder.

Module StringOrder <: OrderedTypeFull with Definition t:=string.
  Definition t:= string.
  Definition eq := @eq t.
  Definition eq_equiv : (Equivalence eq) := eq_equivalence.
  Definition eq_dec := string_dec.

  Fixpoint compare (a:string) (b:string) : comparison :=
    match a, b with
      | EmptyString, EmptyString ⇒ Eq
      | EmptyString, String _ _ ⇒ Lt
      | String _ _, EmptyString ⇒ Gt
      | String a' a's, String b' b's ⇒
        match AsciiOrder.compare a' b' with
          | Lt ⇒ Lt
          | Eq ⇒ compare a's b's
          | Gt ⇒ Gt
        end
    end.

  Definition lt (a b:string) := compare a b = Lt.

  Lemma compare_spec :
    ∀ x y : t, CompareSpec (eq x y) (lt x y) (lt y x) (compare x y).

  Lemma trichotemy a b : {lt a b} + {eq a b} + {lt b a}.

  Lemma compare_refl_eq a: compare a a = Eq.

  Lemma compare_eq_iff a b: compare a b = Eq ↔ a = b.

  Instance lt_strorder : StrictOrder lt.

  Lemma lt_compat : Proper (eq ==> eq ==> iff) lt.

  Program Definition lt_dec (a b:string) : {lt a b} + {¬lt a b}
    := match compare a b with
         | Lt ⇒ left _
         | Eq ⇒ right _
         | Gt ⇒ right _
       end.

  Definition le (a b:string) :=
    match compare a b with
      | Lt ⇒ True
      | Eq ⇒ True
      | Gt ⇒ False
    end.

  Lemma le_lteq : ∀ x y : t, le x y ↔ lt x y ∨ eq x y.

  Program Definition le_dec (a b:string) : {le a b} + {¬le a b}
    := match compare a b with
         | Lt ⇒ left _
         | Eq ⇒ left _
         | Gt ⇒ right _
       end.

End StringOrder.

Section ToString.

Fixpoint string_reverse_helper (s:string) (acc:string)
  := match s with
         | EmptyString ⇒ acc
         | String x xs ⇒ string_reverse_helper xs (String x acc)
     end.

Definition string_reverse (s:string) := string_reverse_helper s EmptyString.

Fixpoint string_to_list (s:string) : list ascii
  := match s with
         | EmptyString ⇒ nil
         | String x xs ⇒ cons x (string_to_list xs)
     end.

Fixpoint list_to_string (l:list ascii) : string
  := match l with
         | nil ⇒ EmptyString
         | cons x xs ⇒ String x (list_to_string xs)
     end.

Lemma string_to_list_to_string (s:string) :
  list_to_string (string_to_list s) = s.

Lemma list_to_string_to_list (l:list ascii) :
  string_to_list (list_to_string l) = l.

Lemma string_to_list_inj (x y:string) :
  string_to_list x = string_to_list y → x = y.

Lemma list_to_string_inj (x y:list ascii) :
  list_to_string x = list_to_string y → x = y.

Lemma string_reverse_helper_reverse_append s acc:
  string_reverse_helper s acc = list_to_string (List.rev_append (string_to_list s) (string_to_list acc)).

Lemma string_reverse_reverse s :
  string_reverse s = list_to_string (List.rev (string_to_list s)).

Lemma string_reverse_involutive x : string_reverse (string_reverse x) = x.

Lemma string_reverse_inj x y :
  string_reverse x = string_reverse y →
  x = y.

  Lemma lt_contr1 s1 s2 :
    ¬StringOrder.lt s1 s2 → ¬StringOrder.lt s2 s1 → StringOrder.eq s1 s2.

  Lemma lt_contr2 s1 s2 :
    StringOrder.lt s1 s2 → ¬StringOrder.eq s1 s2.

  Lemma lt_contr3 s :
    StringOrder.lt s s → False.

End ToString.

Fixpoint map_string (f:ascii→ascii) (s:string)
  := match s with
     | EmptyString ⇒ EmptyString
     | String a s' ⇒ String (f a) (map_string f s')
     end.

Fixpoint flat_map_string (f:ascii→string) (s:string)
  := match s with
     | EmptyString ⇒ EmptyString
     | String a s' ⇒ append (f a) (flat_map_string f s')
     end.

Global Instance ascii_dec : EqDec ascii eq
  := ascii_dec.

Section like.


  Inductive like_clause :=
  | like_literal (literal:string) : like_clause
  | like_any_char : like_clause
  | like_any_string : like_clause.


  Fixpoint make_like_clause (s:string) (escape:option ascii) {struct s}: list like_clause
    := match s with
       | EmptyString ⇒ nil
       | String "_"%char tail ⇒ like_any_char :: make_like_clause tail escape
       | String "%"%char tail ⇒ like_any_string :: make_like_clause tail escape
       | other ⇒
         (fix make_like_literal_clause (ss:string) (acc:string) {struct ss} : list like_clause
          := match ss with
             | EmptyString ⇒ like_literal (string_reverse acc) :: nil
             | String "_"%char tail ⇒ like_literal (string_reverse acc) :: like_any_char :: make_like_clause tail escape
             | String "%"%char tail ⇒ like_literal (string_reverse acc) :: like_any_string :: make_like_clause tail escape
             | String h tail ⇒
               if Some h == escape
               then
                 match tail with
                 | EmptyString ⇒
                 
                   like_literal (string_reverse (String h acc)) :: nil
                 | String "_"%char tail ⇒ make_like_literal_clause tail (String "_" acc)
                 | String "%"%char tail ⇒ make_like_literal_clause tail (String "%" acc)
                 | String nh ntail ⇒
                   if Some nh == escape
                   then make_like_literal_clause ntail (String nh acc)
                   else
                     
                     make_like_literal_clause ntail (String nh (String h acc))
                 end
               else
                 make_like_literal_clause tail (String h acc)
             end
                     ) other ""%string
         
       end.

  Example make_like_clause_example1 := make_like_clause "hello_there^^^%%" None.
  Example make_like_clause_example2 := make_like_clause "hello_there^^^%%" (Some "^"%char).


  Fixpoint string_exists_suffix (f:string→bool) (s:string) : bool
    := f s ||
         match s with
         | EmptyString ⇒ false
         | String _ tail ⇒ string_exists_suffix f tail
         end.

  Fixpoint like_clause_matches_string (pat:list like_clause) (s:string)
    := match pat with
       | nil ⇒ s ==b EmptyString
       | (like_literal literal)::rest ⇒
         andb (prefix literal s)
                (like_clause_matches_string rest (substring (String.length literal) (String.length s - String.length literal) s))
       | like_any_char::rest ⇒
         match s with
         | EmptyString ⇒ false
         | String _ tail ⇒ like_clause_matches_string rest tail
         end
       | like_any_string::rest ⇒
         string_exists_suffix (like_clause_matches_string rest) s
       end.

  Definition string_like (str pattern:string) (escape:option ascii) : bool
    := let pat_clause := make_like_clause pattern escape in
       like_clause_matches_string pat_clause str.

  Example string_like_example1 := string_like "hello there" "hello there" None.
  Example string_like_example2 := string_like "hello there" "hello %there" None.
  Example string_like_example3 := string_like "hello there" "he%th_re" None.
  Example string_like_example4 := string_like "hello there " "he%th_re" None.
  Example string_like_example5 := string_like "hello thethare" "he%th_re" None.
  Example string_like_example6 := string_like "hello thetheare" "he%th_re" None.


End like.