Qcert.Basic.Operators.RUtilOps

Section RUtilOps.




  Context {fdata:foreign_data}.

  Definition boolToString (b:bool) : string
    := if b then "TRUE"%string else "FALSE"%string.

  Definition bracketString (open s close:string)
    := append open (append s close).

  Definition stringToString (s:string) : string

    := s.

  Fixpoint joinStrings (delim:string) (l:list string) : string
    := match l with
         | nil ⇒ EmptyString
         | x::nil ⇒ x
         | x::ls ⇒ append x (append delim (joinStrings delim ls))
       end.

  Definition string_sort := insertion_sort StringOrder.le_dec.

  Global Instance ToString_Z : ToString Z
    := { toString := Z_to_string10}.

  Global Instance ToString_nat : ToString nat
    := { toString := nat_to_string10}.

  Global Instance ToString_bool : ToString bool
    := { toString := boolToString}.

  Instance ToString_brands : ToString brands
    := { toString := fun b ⇒ (joinStrings " & " b)}.

  Fixpoint dataToString (d:data) : string
    := match d with
           | dunit ⇒ "UNIT"%string
           | dnat n ⇒ toString n
           | dbool b ⇒ toString b
           | dstring s ⇒ stringToString s
           | dcoll l ⇒ bracketString
                          "["%string
                          (joinStrings ", "
                                       (string_sort (map dataToString l)))
                          "]"%string
           | drec lsd ⇒ bracketString
             "{"%string
                (joinStrings ","
                             (map (fun xy ⇒ let '(x,y):=xy in
                                             (append (stringToString x) (append "->"%string
                                             (dataToString y)))
                                  ) lsd))
                "}"%string
           | dleft d ⇒ bracketString
                          "Left("%string
                          (dataToString d)
                          ")"%string
           | dright d ⇒ bracketString
                          "Right("%string
                          (dataToString d)
                          ")"%string
           | dbrand b d ⇒ (bracketString
                              "<"
                              (append (@toString _ ToString_brands b)
                                      (append ":" (dataToString d)))
                              ">")
           | dforeign fd ⇒ toString fd
       end.

  Global Instance ToString_data : ToString data
    := { toString := dataToString}.

  Fixpoint dsum (ns:list data) : option Z
    := match ns with
         | nil ⇒ Some 0%Z
         | dnat n::ls ⇒ lift (Zplus n) (dsum ls)
         | _ ⇒ None
       end.

  Definition darithmean (ns:list data) : option Z
    := match ns with
         | nil ⇒ Some (0%Z)
         | _ ⇒ lift (fun x ⇒ Z.quot x (Z_of_nat (length ns))) (dsum ns)
       end.

End RUtilOps.