Module RString

Require Import Orders.
Require Import Ascii.
Require Import String.
Require Import Equivalence.
Require Import EquivDec.
Require Import Compare_dec.
Require Import Omega.

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 :
    forall 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 : forall 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 :
    forall 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 : forall 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.

  Require List.
  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.

Section Prefix.
  Lemma substring_zero s :
    substring 0 0 s = ""%string.
  
  Lemma substring_S a m s :
    substring 0 (S m) (String a s) = String a (substring 0 m s).

  Lemma append_string_distr a s1 s2 :
    (String a s1 ++ s2 = String a (s1 ++ s2))%string.


End Prefix.

Section MapString.
  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.
End MapString.

Section Like.
  Require Import RUtil.


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

  Require Import List.
  
  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.