Library EVMOpSem.Lem.lem_show

Require Import Arith.
Require Import Bool.
Require Import List.
Require Import String.
Require Import Program.Wf.

Require Import coqharness.

Open Scope nat_scope.
Open Scope string_scope.

Require Import lem_string.
Require Export lem_string.
Require Import lem_maybe.
Require Export lem_maybe.
Require Import lem_num.
Require Export lem_num.
Require Import lem_basic_classes.
Require Export lem_basic_classes.

Class Show (a: Type): Type := {
  show:a -> string
}.

Instance x219_Show : Show string := {
   show s := String.append"""" (String.append s """")
}.


Definition stringFromMaybe {a : Type} (showX : a -> string ) (x : option a ) : string :=
  match ( x) with
    | Some x => String.append"Just (" (String.append(showX x) ")")
    | None => "Nothing"
  end.

Instance x218_Show{a: Type} `{Show a}: Show (option a ):= {
   show x_opt := stringFromMaybe show x_opt
}.


Program Fixpoint stringFromListAux {a : Type} (showX : a -> string ) (x : list a) : string :=
  match ( x) with
    | [] => ""
    | x::xs' =>
      match ( xs') with
      | [] => showX x
      | _ => String.append(showX x) (String.append"; " (stringFromListAux showX xs'))
      end
  end.

Definition stringFromList {a : Type} (showX : a -> string ) (xs : list a) : string :=
  String.append"[" (String.append(stringFromListAux showX xs) "]").

Instance x217_Show{a: Type} `{Show a}: Show (list a):= {
   show xs := stringFromList show xs
}.


Definition stringFromPair {a b : Type} (showX : a -> string ) (showY : b -> string ) (p : (a*b) % type) : string :=
  match ( (showX,showY,p)) with ( showX, showY, (x, y)) =>
    String.append "("
      (String.append (showX x)
         (String.append ", " (String.append (showY y) ")"))) end.

Instance x216_Show{a b: Type} `{Show a} `{Show b}: Show ((a * b) % type):= {
   show := stringFromPair show show
}.

Instance x215_Show : Show bool := {
   show b := if b then "true" else "false"
}.