Library C_pp
Require Import ssreflect ssrbool eqtype.
Require Import Coq.Program.Wf.
Require Import Bool_ext ZArith_ext Lists_ext String_ext.
Require Import machine_int.
Import MachineInt.
Require Import C_types C_expr C_bipl C_cmd C_seplog.
Local Open Scope minC_expr_scope.
Local Open Scope minC_cmd_scope.
Definition pp_Zdigit (z:Z) (tl:string) : string :=
match z with
| 0 => "0" ++ tl
| 1 => "1" ++ tl
| 2 => "2" ++ tl
| 3 => "3" ++ tl
| 4 => "4" ++ tl
| 5 => "5" ++ tl
| 6 => "6" ++ tl
| 7 => "7" ++ tl
| 8 => "8" ++ tl
| 9 => "9" ++ tl
| _ => tl
end%string.
Program Fixpoint pp_positive (p:positive) (tl:string) {measure (nat_of_P p)}: string :=
let tl' := pp_Zdigit (Zpos p mod 10) tl in
match (Zpos p) / 10 with
| Zpos q => pp_positive q tl'
| Z0 => tl'
| _ => ""
end%string.
Definition pp_Z (z:Z) (tl:string) : string :=
match z with
| Zpos p => pp_positive p tl
| Z0 => "0" ++ tl
| Zneg p => "-" ++ (pp_positive p tl)
end%string.
Definition pp_var (v:var) (tl:string) : string :=
(v ++ tl)%string.
Definition pp_uint {n : nat} (i:int n) (tl:string) : string :=
pp_Z (u2Z i) tl.
Definition pp_sint {n : nat} (i:int n) (tl:string) : string :=
pp_Z (s2Z i) tl.
Definition pp_binop (op:binop_e) (tl:string) : string :=
(match op with
| add_e => "+"
| sub_e => "-"
| mul_e => "*"
| and_e => "&"
| or_e => "|"
| shl_e => "<<"
| le_e => "<="
| lt_e => "<"
| gt_e => ">"
| land_e => "&&"
| lor_e => "||"
| eq_e => "=="
| neq_e => "!="
end ++ tl)%string.
Definition binopk_to_string (op:binopk_e) (tl:string) : string :=
(match op with
| mod2n_e => "%"
end ++ tl)%string.
Definition ityp_to_string (t:ityp) (tl:string) : string :=
(match t with
| uint32 => "unsigned int"
| sint32 => "int"
| char => "char"
end ++ tl)%string.
Definition struct_tag_to_string (tag : stag) (tl:string) : string :=
(match tag with
| mkStag s => s
end ++ tl)%string.
Fixpoint typ_to_string (t:typ) (tl:string) {struct t} : string :=
(match t with
| btyp t => ityp_to_string t tl
| ptyp t => typ_to_string t (" *" ++ tl)
| rtyp tg => "struct " ++ (struct_tag_to_string tg (" *"++ tl))
| styp tg ss_ts => "struct " ++ (struct_tag_to_string tg (" { " ++ (fold_right (fun s_t tl => (typ_to_string (snd s_t) (" " ++ ((fst s_t) ++ ("; " ++ tl))))) ("}" ++ tl) ss_ts)))
end)%string.
Fixpoint typ_to_string' (t:typ) (tl:string) {struct t} : string :=
(match t with
| btyp t => ityp_to_string t tl
| ptyp t => typ_to_string t (" *" ++ tl)
| rtyp tg => "struct " ++ (struct_tag_to_string tg (" *" ++ tl))
| styp tg _ => "struct " ++ (struct_tag_to_string tg tl)
end)%string.
Fixpoint typ_value_to_string_n (n:nat) (t:typ) (v:value) (tl:string) : string :=
match n with
| O =>
match (t, v) with
| (btyp uint32, bval32 i) => pp_uint i tl
| (btyp sint32, bval32 i) => pp_sint i tl
| (btyp char, bval32 i) => pp_sint i tl
| _ => "/* ERROR */" ++ tl
end
| S n =>
match (t, v) with
| (ptyp t, pval iptr) => "(" ++ (typ_to_string t (" *)" ++ (pp_uint iptr tl)))
| (styp _ nil, sval nil) => "{}" ++ tl
| (styp _ ((_, t)::nil), sval (v::nil)) => "{ " ++ typ_value_to_string_n n t v ("}" ++ tl)
| (styp _ ((_, t)::ss_ts), sval (v::vs)) => "{ " ++ typ_value_to_string_n n t v (fold_right (fun t_v tl => ", " ++ (typ_value_to_string_n n (fst t_v) (snd t_v) tl)) (" }" ++ tl) (combine (uzip2 ss_ts) vs))
| _ => "/* ERROR */" ++ tl
end
end%string.
Definition typ_value_to_string (t:typ) (v:value) (tl:string) : string :=
typ_value_to_string_n (typ_max_depth t) t v tl.
Definition pp_cast c :=
match c with
| uchar_to_int => "(int)"
end%string.
Fixpoint pp_exp (e:exp) (tl:string) : string :=
match e with
| var_e v => pp_var v tl
| cst32 i32 => pp_sint i32 tl
| cst8 i8 => pp_sint i8 tl
| cast_e c e' => "(" ++ pp_cast c ++ (pp_exp e' (")" ++ tl))
| bop_ne op e1 e2 => "(" ++ (pp_exp e1 (") " ++ (pp_binop op (" (" ++ (pp_exp e2 (")" ++ tl))))))
| bopk_ne op e n => "(" ++ (pp_exp e (") " ++ (binopk_to_string op (" (1 << " ++ (pp_Z (Z_of_nat n) (")" ++ tl))))))
| ifte_e e e1 e2 => "(" ++ (pp_exp e (") ? (" ++ (pp_exp e1 (") : (" ++ (pp_exp e2 (")" ++ tl))))))
| fld e name => (pp_exp e ("." ++ (name ++ tl)))
| fld' e name => "&(" ++ (pp_exp e ("->" ++ (name ++ (")" ++ tl))))
| cst_pe t _ iptr => "(" ++ (typ_to_string' t (" *)(" ++ (pp_uint iptr (")" ++ tl))))
| add_pe p e => "(" ++ (pp_exp p (") + (" ++ (pp_exp e (")" ++ tl))))
| sub_pe e1 e2 => "(" ++ (pp_exp e1 (" - " ++ pp_exp e2 (")" ++ tl)))
| bop_pe p1 p2 => "(" ++ (pp_exp p1 (") == (" ++ (pp_exp p2 (")" ++ tl))))
| cst_se _ ((_, t)::ss_ts) (v::vs) _ _ _ => "{ " ++ typ_value_to_string t v (fold_right (fun t_v tl => ", " ++ (typ_value_to_string (fst t_v) (snd t_v) tl)) (" }" ++ tl) (combine (uzip2 ss_ts) vs))
| cst_se _ nil nil _ _ _ => "{}" ++ tl
| _ => "/* ERROR */" ++ tl
end%string.
Fixpoint bpp_exp (e:bexp) (tl:string) : string :=
match e with
| exp2bexp e => "(_Bool)(" ++ (pp_exp e (")" ++ tl))
| bneg b => "!(" ++ bpp_exp b (")" ++ tl)
end%string.
Fixpoint pp_cmd (c:while.cmd ) (tl:string) : string :=
match c with
| while.seq c1 c2 => pp_cmd c1 (" " ++ pp_cmd c2 tl)
| while.ifte e c1 c2 => "if (" ++ bpp_exp e (") { " ++ pp_cmd c1 (" } else { " ++ (pp_cmd c2 (" }" ++ tl))))
| while.while e c => "while (" ++ bpp_exp e (") { " ++ pp_cmd c (" }" ++ tl))
| skip => ";" ++ tl
| assign v e => pp_var v (" = " ++ (pp_exp e (";" ++ tl)))
| lookup v e => pp_var v (" = *(" ++ (pp_exp e (");" ++ tl)))
| mutation e1 e2 => "*(" ++ pp_exp e1 (") = " ++ (pp_exp e2 (";" ++ tl)))
| malloc v e => pp_var v (" = malloc(" ++ pp_exp e (");" ++ tl))
| free e => "free(" ++ pp_exp e (");" ++ tl)
end%string.
Require Import ZArith.
Require Import Setoid.
Lemma s2Z_Z2u : forall {n:nat} (z:Z), 0 <= z < Zpower 2 (Peano.pred n) -> s2Z (Z2u n z) = z.
Lemma s2Z_Z2u' : forall {n:nat} (z:Z), -(Zpower 2 (Peano.pred n)) <= z < 0 -> s2Z (Z2u n z) = z.
Goal (pp_exp (cst32_0 \+e cst32_0) "" = "(0) + (0)")%string.
Goal (pp_exp ((var_e "apair") .\ "a") "" = "apair.a")%string.
Require Import Coq.Program.Wf.
Require Import Bool_ext ZArith_ext Lists_ext String_ext.
Require Import machine_int.
Import MachineInt.
Require Import C_types C_expr C_bipl C_cmd C_seplog.
Local Open Scope minC_expr_scope.
Local Open Scope minC_cmd_scope.
Definition pp_Zdigit (z:Z) (tl:string) : string :=
match z with
| 0 => "0" ++ tl
| 1 => "1" ++ tl
| 2 => "2" ++ tl
| 3 => "3" ++ tl
| 4 => "4" ++ tl
| 5 => "5" ++ tl
| 6 => "6" ++ tl
| 7 => "7" ++ tl
| 8 => "8" ++ tl
| 9 => "9" ++ tl
| _ => tl
end%string.
Program Fixpoint pp_positive (p:positive) (tl:string) {measure (nat_of_P p)}: string :=
let tl' := pp_Zdigit (Zpos p mod 10) tl in
match (Zpos p) / 10 with
| Zpos q => pp_positive q tl'
| Z0 => tl'
| _ => ""
end%string.
Definition pp_Z (z:Z) (tl:string) : string :=
match z with
| Zpos p => pp_positive p tl
| Z0 => "0" ++ tl
| Zneg p => "-" ++ (pp_positive p tl)
end%string.
Definition pp_var (v:var) (tl:string) : string :=
(v ++ tl)%string.
Definition pp_uint {n : nat} (i:int n) (tl:string) : string :=
pp_Z (u2Z i) tl.
Definition pp_sint {n : nat} (i:int n) (tl:string) : string :=
pp_Z (s2Z i) tl.
Definition pp_binop (op:binop_e) (tl:string) : string :=
(match op with
| add_e => "+"
| sub_e => "-"
| mul_e => "*"
| and_e => "&"
| or_e => "|"
| shl_e => "<<"
| le_e => "<="
| lt_e => "<"
| gt_e => ">"
| land_e => "&&"
| lor_e => "||"
| eq_e => "=="
| neq_e => "!="
end ++ tl)%string.
Definition binopk_to_string (op:binopk_e) (tl:string) : string :=
(match op with
| mod2n_e => "%"
end ++ tl)%string.
Definition ityp_to_string (t:ityp) (tl:string) : string :=
(match t with
| uint32 => "unsigned int"
| sint32 => "int"
| char => "char"
end ++ tl)%string.
Definition struct_tag_to_string (tag : stag) (tl:string) : string :=
(match tag with
| mkStag s => s
end ++ tl)%string.
Fixpoint typ_to_string (t:typ) (tl:string) {struct t} : string :=
(match t with
| btyp t => ityp_to_string t tl
| ptyp t => typ_to_string t (" *" ++ tl)
| rtyp tg => "struct " ++ (struct_tag_to_string tg (" *"++ tl))
| styp tg ss_ts => "struct " ++ (struct_tag_to_string tg (" { " ++ (fold_right (fun s_t tl => (typ_to_string (snd s_t) (" " ++ ((fst s_t) ++ ("; " ++ tl))))) ("}" ++ tl) ss_ts)))
end)%string.
Fixpoint typ_to_string' (t:typ) (tl:string) {struct t} : string :=
(match t with
| btyp t => ityp_to_string t tl
| ptyp t => typ_to_string t (" *" ++ tl)
| rtyp tg => "struct " ++ (struct_tag_to_string tg (" *" ++ tl))
| styp tg _ => "struct " ++ (struct_tag_to_string tg tl)
end)%string.
Fixpoint typ_value_to_string_n (n:nat) (t:typ) (v:value) (tl:string) : string :=
match n with
| O =>
match (t, v) with
| (btyp uint32, bval32 i) => pp_uint i tl
| (btyp sint32, bval32 i) => pp_sint i tl
| (btyp char, bval32 i) => pp_sint i tl
| _ => "/* ERROR */" ++ tl
end
| S n =>
match (t, v) with
| (ptyp t, pval iptr) => "(" ++ (typ_to_string t (" *)" ++ (pp_uint iptr tl)))
| (styp _ nil, sval nil) => "{}" ++ tl
| (styp _ ((_, t)::nil), sval (v::nil)) => "{ " ++ typ_value_to_string_n n t v ("}" ++ tl)
| (styp _ ((_, t)::ss_ts), sval (v::vs)) => "{ " ++ typ_value_to_string_n n t v (fold_right (fun t_v tl => ", " ++ (typ_value_to_string_n n (fst t_v) (snd t_v) tl)) (" }" ++ tl) (combine (uzip2 ss_ts) vs))
| _ => "/* ERROR */" ++ tl
end
end%string.
Definition typ_value_to_string (t:typ) (v:value) (tl:string) : string :=
typ_value_to_string_n (typ_max_depth t) t v tl.
Definition pp_cast c :=
match c with
| uchar_to_int => "(int)"
end%string.
Fixpoint pp_exp (e:exp) (tl:string) : string :=
match e with
| var_e v => pp_var v tl
| cst32 i32 => pp_sint i32 tl
| cst8 i8 => pp_sint i8 tl
| cast_e c e' => "(" ++ pp_cast c ++ (pp_exp e' (")" ++ tl))
| bop_ne op e1 e2 => "(" ++ (pp_exp e1 (") " ++ (pp_binop op (" (" ++ (pp_exp e2 (")" ++ tl))))))
| bopk_ne op e n => "(" ++ (pp_exp e (") " ++ (binopk_to_string op (" (1 << " ++ (pp_Z (Z_of_nat n) (")" ++ tl))))))
| ifte_e e e1 e2 => "(" ++ (pp_exp e (") ? (" ++ (pp_exp e1 (") : (" ++ (pp_exp e2 (")" ++ tl))))))
| fld e name => (pp_exp e ("." ++ (name ++ tl)))
| fld' e name => "&(" ++ (pp_exp e ("->" ++ (name ++ (")" ++ tl))))
| cst_pe t _ iptr => "(" ++ (typ_to_string' t (" *)(" ++ (pp_uint iptr (")" ++ tl))))
| add_pe p e => "(" ++ (pp_exp p (") + (" ++ (pp_exp e (")" ++ tl))))
| sub_pe e1 e2 => "(" ++ (pp_exp e1 (" - " ++ pp_exp e2 (")" ++ tl)))
| bop_pe p1 p2 => "(" ++ (pp_exp p1 (") == (" ++ (pp_exp p2 (")" ++ tl))))
| cst_se _ ((_, t)::ss_ts) (v::vs) _ _ _ => "{ " ++ typ_value_to_string t v (fold_right (fun t_v tl => ", " ++ (typ_value_to_string (fst t_v) (snd t_v) tl)) (" }" ++ tl) (combine (uzip2 ss_ts) vs))
| cst_se _ nil nil _ _ _ => "{}" ++ tl
| _ => "/* ERROR */" ++ tl
end%string.
Fixpoint bpp_exp (e:bexp) (tl:string) : string :=
match e with
| exp2bexp e => "(_Bool)(" ++ (pp_exp e (")" ++ tl))
| bneg b => "!(" ++ bpp_exp b (")" ++ tl)
end%string.
Fixpoint pp_cmd (c:while.cmd ) (tl:string) : string :=
match c with
| while.seq c1 c2 => pp_cmd c1 (" " ++ pp_cmd c2 tl)
| while.ifte e c1 c2 => "if (" ++ bpp_exp e (") { " ++ pp_cmd c1 (" } else { " ++ (pp_cmd c2 (" }" ++ tl))))
| while.while e c => "while (" ++ bpp_exp e (") { " ++ pp_cmd c (" }" ++ tl))
| skip => ";" ++ tl
| assign v e => pp_var v (" = " ++ (pp_exp e (";" ++ tl)))
| lookup v e => pp_var v (" = *(" ++ (pp_exp e (");" ++ tl)))
| mutation e1 e2 => "*(" ++ pp_exp e1 (") = " ++ (pp_exp e2 (";" ++ tl)))
| malloc v e => pp_var v (" = malloc(" ++ pp_exp e (");" ++ tl))
| free e => "free(" ++ pp_exp e (");" ++ tl)
end%string.
Require Import ZArith.
Require Import Setoid.
Lemma s2Z_Z2u : forall {n:nat} (z:Z), 0 <= z < Zpower 2 (Peano.pred n) -> s2Z (Z2u n z) = z.
Lemma s2Z_Z2u' : forall {n:nat} (z:Z), -(Zpower 2 (Peano.pred n)) <= z < 0 -> s2Z (Z2u n z) = z.
Goal (pp_exp (cst32_0 \+e cst32_0) "" = "(0) + (0)")%string.
Goal (pp_exp ((var_e "apair") .\ "a") "" = "apair.a")%string.