GenProg.Utils

From FinMatrix Require Export Matrix.

Export Rbase Rtrigo.

Arguments vec : clear implicits.

Require Export Ascii String.
Open Scope string.
Open Scope nat.

Set Printing Depth 2000.

Section pair.

  Definition pair3 A B C := (A * B * C)%type.
  Definition p31 {A B C} (x:pair3 A B C) : A := fst (fst x).
  Definition p32 {A B C} (x:pair3 A B C) : B := snd (fst x).
  Definition p33 {A B C} (x:pair3 A B C) : C := snd x.

End pair.

Section option.

  Definition ofst {A B} (o:option (A*B)) : option A :=
    match o with Some x => Some (fst x) | _ => None end.

  Definition osnd {A B} (o:option (A*B)) : option B :=
    match o with Some x => Some (snd x) | _ => None end.

  Definition oget {A} (o:option A) (def:A) : A :=
    match o with Some x => x | _ => def end.

End option.

Section R.

  Record Rstring :=
    mkRstring {
        Rval : R;
        Rstr : string
      }.

  Definition nat2Rstring (n:nat) : Rstring := mkRstring (INR n) (nat2str n).
  Coercion nat2Rstring : nat >-> Rstring.

  Inductive Rop1 :=
  | Rop1_neg | Rop1_sin | Rop1_cos
  | Rop1_asin | Rop1_atan
  .

  Definition Rop1_eval (op:Rop1) : R->R :=
    match op with
    | Rop1_neg => Ropp
    | Rop1_sin => sin | Rop1_cos => cos
    | Rop1_asin => asin | Rop1_atan => atan
    end.

  Definition Rop1_str (op:Rop1) (s:string) : string :=
    match op with
    | Rop1_neg => "-(" ++ s ++ ")"
    | Rop1_sin => "sin(" ++ s ++ ")"
    | Rop1_cos => "cos(" ++ s ++ ")"
    | Rop1_asin => "asin(" ++ s ++ ")"
    | Rop1_atan => "atan(" ++ s ++ ")"
    end.

  Inductive Rop2 :=
  | Rop2_add | Rop2_sub | Rop2_mul | Rop2_div
  | Rop2_atan2
  .

  Parameter Ratan2 : R -> R -> R.
  Definition Rop2_eval (op:Rop2) : R->R->R :=
    match op with
    | Rop2_add => Rplus | Rop2_sub => (fun x y => Rplus x (Ropp y))
    | Rop2_mul => Rmult | Rop2_div => (fun x y => Rmult x (Rinv y))
    | Rop2_atan2 => Ratan2
    end.

  Definition Rop2_str (op:Rop2) (s1 s2:string) : string :=
    match op with
    | Rop2_add => "(" ++ s1 ++ " + " ++ s2 ++ ")"
    | Rop2_sub => "(" ++ s1 ++ " - " ++ s2 ++ ")"
    | Rop2_mul => s1 ++ " * " ++ s2
    | Rop2_div => s1 ++ " / " ++ s2
    | Rop2_atan2 => "atan2(" ++ s1 ++ ", " ++ s2 ++ ")"
    end.

End R.

Section LF_CR.

  Definition CharLF : ascii := ascii_of_nat 10.

  Definition CharCR : ascii := ascii_of_nat 13.

  Definition strNewlineUnix : string := String CharLF "".
  Definition strNewlineWin : string := String CharCR (String CharLF "").
  Definition strNewlineMac : string := String CharCR "".
  Definition strNewline : string := strNewlineUnix.

End LF_CR.

Section bool_missing.

  Lemma bool_eqb_prop : forall a b : bool, Bool.eqb a b = true -> a = b.
  Proof.
    destruct a,b; simpl; auto.
  Defined.

  Lemma andb_prop : forall b1 b2 : bool, b1 && b2 = true -> b1 = true /\ b2 = true.
  Proof.
    destruct b1,b2; simpl; split; intros; auto.
  Defined.

End bool_missing.

Section nat_missing.

  Lemma nat_eqb_eq : forall (n m : nat), Nat.eqb n m = true -> n = m.
  Proof.
    induction n; destruct m; simpl; auto; intros; easy.
  Defined.

  Definition lt_S_n: forall n m : nat, S n < S m -> n < m.
  Proof.
    intros. apply Nat.succ_lt_mono. auto.
  Qed.

End nat_missing.

Section string_missing.

  Lemma ascii_eqb_eq : forall c1 c2 : ascii, Ascii.eqb c1 c2 = true -> c1 = c2.
  Proof.
    destruct c1,c2. simpl.
    repeat match goal with
           | |- context[Bool.eqb ?b1 ?b2] =>
               let E := fresh "E" in
               destruct (Bool.eqb b1 b2) eqn:E; try easy;
               apply bool_eqb_prop in E
           end; subst; auto.
  Defined.

  Lemma string_eqb_eq : forall s1 s2 : string, String.eqb s1 s2 = true -> s1 = s2.
  Proof.
    induction s1; destruct s2; simpl; auto; intros; try easy.
    destruct (a =? a0)%char eqn:E1.
    - apply ascii_eqb_eq in E1. apply IHs1 in H. subst. auto.
    - easy.
  Defined.

End string_missing.

Section list_missing.

  Fixpoint removeb {A:Type} (f:A -> bool) (l:list A) (x:A) : list A :=
    match l with
    | [] => []
    | h :: tl => if f h then removeb f tl x else h :: removeb f tl x
    end.

  Definition fold_left1 {A} (f:A->A->A) (l:list A) (a:A) : A :=
    match l with
    | [] => a
    | x :: l' => fold_left f l' x
    end.

  Definition list_new_id {A} (toID:A->(bool*nat)) (l:list A) : nat :=
    let fix F (l0:list A) (newID:nat) :=
      match l0 with
      | [] => newID
      | x :: l1 =>
          let '(valid, id) := toID x in
          if valid
          then F l1 (max newID (S id))
          else F l1 newID
      end in
    F l 0.

  Section test.
    Variable A:Type. Variable (a:A) (b:A) (c:A) (a0:A). Variable f:A->A->A.

  End test.

End list_missing.

Section seq.

  Fixpoint fold_seq {A B} (seq:nat->A) (n:nat) (f:A->B->B) (b:B) : B :=
    match n with
    | O => b
    
    
    
    | S n' => fold_seq seq n' f (f (seq n') b)
    end.

  Section test.
    Variable a1 a2 a3 a4 b:nat.
    Let s (n:nat) : nat := match n with 0=>a1|1=>a2|2=>a3|_=>a4 end.
  End test.

End seq.

Section lmap.

  Context {V:Type}.   Context {v_eqb:V->V->bool}.
  Context {v_eqb_eq: forall v1 v2, v_eqb v1 v2 = true -> v1 = v2}.
  Context {v_eqb_refl: forall v, v_eqb v v = true}.

  Let K := nat.   Let KV := (K * V)%type.
  Let key_eqb (k1 k2:K) : bool := Nat.eqb k1 k2.

  Definition lmap := list KV.
  Definition empty_lmap : lmap := [].

  Definition lmap_new_key (c:lmap) : K := list_new_id (fun i => (true, fst i)) c.

  Fixpoint lmap_eqb (l1 l2 : lmap) : bool :=
    match l1, l2 with
    | [], [] => true
    | (k1,v1) :: l1', (k2,v2) :: l2' =>
        Nat.eqb k1 k2 && v_eqb v1 v2 && lmap_eqb l1' l2'
    | _, _ => false
    end.

  Definition lmap_eqb_eq : forall l1 l2 : lmap, lmap_eqb l1 l2 = true -> l1 = l2.
    induction l1; destruct l2; simpl in *; intros; try easy.
    - destruct a. easy.
    - destruct a,k. repeat (apply andb_prop in H; destruct H).
      apply nat_eqb_eq in H. apply v_eqb_eq in H1. apply IHl1 in H0. subst. auto.
  Defined.

  Definition lmap_eqb_refl : forall l : lmap, lmap_eqb l l = true.
    induction l; auto. simpl. destruct a.
    rewrite Nat.eqb_refl, v_eqb_refl, IHl. auto.
  Defined.

  Definition lmap_geto (k:K) (c:lmap) : option V :=
    match find (fun kv => key_eqb (fst kv) k) c with
    | Some kv => Some (snd kv) | _ => None
    end.

  Definition lmap_get (k:K) (c:lmap) (val_def:V) : V :=
    match lmap_geto k c with Some x => x | _ => val_def end.


  Definition lmap_exist (k:K) (c:lmap) : bool :=
    match lmap_geto k c with Some _ => true | _ => false end.

  Fixpoint lmap_find_first (c:lmap) (filter:V->bool) : option (K * V * lmap) :=
    match c with
    | [] => None
    | x :: c' =>
        if filter (snd x)
        then Some (fst x, snd x, c')
        else
          match lmap_find_first c' filter with
          | Some (k,v,l) => Some (k,v,x::l)
          | None => None
          end
    end.

  Fixpoint lmap_update (c:lmap) (k:K) (v:V) (chk_type:V->bool) : lmap :=
    match c with
    | [] => []
    | x :: c' => if key_eqb (fst x) k
                then (if chk_type (snd x)
                      then (fst x, v) :: c'
                      else c)
                else x :: (lmap_update c' k v chk_type)
    end.

  Fixpoint lmap_del (k:K) (c:lmap) : lmap :=
    match c with
    | [] => []
    | x :: c' => if key_eqb (fst x) k then lmap_del k c' else x :: (lmap_del k c')
    end.

  Fixpoint lmap_del_first (c:lmap) (filter:V->bool) : lmap :=
    match c with
    | [] => []
    | x :: c' => if filter (snd x) then c' else x :: (lmap_del_first c' filter)
    end.

  Definition lmap_add (v:V) (c:lmap) : (K * lmap) :=
    let k := lmap_new_key c in
    let kv := (k, v) in
    (k, kv::c).

  Definition lmap_add2 (v:V) (c:lmap) : lmap := snd (lmap_add v c).

  Definition lmap_init (c:list V) : lmap :=
    fold_left (fun l v => lmap_add2 v l) c empty_lmap.

End lmap.

Section test.

  Let l1 : lmap := lmap_init ["x";"y";"z"].
End test.