Require Import Orders.
Require Import Ascii.
Require Import List.
Require Import String.
Require Import Arith.
Require Import Min.
Require Import Equivalence.
Require Import EquivDec.
Require Import Compare_dec.
Require Import Lia.
Require Import LibUtilsCoqLibAdd.

Total order on characters

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.

Total order on strings

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.

String prefixes

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.

  Lemma append_eq_inv1 x y z : append x y = append x z -> y = z.

  Lemma prefix_refl y : prefix y y = true.
  
  Lemma substring_append_cancel x y :
    substring (String.length x) (String.length y) (append x y) = y.

  Lemma string_length_append x y :
    String.length (append x y) = String.length x + String.length y.

  Lemma prefix_nil post : prefix ""%string post = true.

  Lemma prefix_app pre post : prefix pre (append pre post) = true.

  Lemma prefix_break {pre x} :
    prefix pre x = true ->
    {y | x = append pre y}.

  
  Lemma substring_split s n m l :
    append (substring s n l) (substring (s+n) m l) = substring s (n+m) l.

  Lemma substring_all l :
    substring 0 (String.length l) l = l.

  Lemma substring_bounded s n l :
    substring s n l = substring s (min n (String.length l - s)) l.

  Lemma substring_le_prefix s n m l :
    n <= m ->
    prefix (substring s n l) (substring s m l) = true.

  Lemma substring_prefix n l :
    prefix (substring 0 n l) l = true.

  Lemma in_of_append pre y l :
    In (append pre y) l <->
    In y (map
            (fun x => substring (String.length pre) (String.length x - String.length pre) x)
            (filter (prefix pre) l)).
  
  Lemma append_ass s1 s2 s3 : ((s1 ++ s2) ++ s3 = s1 ++ s2 ++ s3)%string.

End Prefix.

Character map over strings

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 Join.
  Definition map_concat {A} separator (f:A -> string) (elems:list A) : string :=
    match elems with
    | nil => ""
    | e :: elems' =>
      (fold_left (fun acc e => acc ++ separator ++ (f e)) elems' (f e))%string
    end.
  
End Join.

Conversion between lists of characters and strings

Section AsciiToString.

  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 AsciiToString.

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.