Require Import ZArith String List extracted_io.

Inductive aexpr : Type :=
  avar (s : string) | anum (n :Z) | aplus (a1 a2:aexpr).

Inductive bexpr : Type :=  blt (e1 e2 : aexpr).

Inductive instr : Type :=
  assign (x : string) (e : aexpr) | sequence (i1 i2: instr)
 | while (b :bexpr)(i : instr).


(* output functions on these data types. *)

Fixpoint aexpr_to_string (e : aexpr) : string :=
  match e with
    avar x => x
  | anum n => string_of_z n
  | aplus e1 ((aplus _ _) as e2) => 
    aexpr_to_string e1 ++ " + (" ++ aexpr_to_string e2 ++ ")"
  | aplus e1 e2 => aexpr_to_string e1 ++ " + " ++ aexpr_to_string e2
  end.

Fixpoint env_to_string (r : list(string*Z)) : string :=
  match r with
    nil => "nil"
  | (x, n)::tl => "(" ++ x ++ "," ++ string_of_z n ++ ")." ++ env_to_string tl
  end.

(* Can you write a similar function for instructions? *)