1. default implementation.v

From mathcomp Require Import all_ssreflect.


(* Expr lang *)

Inductive expr : Type :=
| Const of nat
| Plus of expr & expr
| Minus of expr & expr
| Mult of expr & expr.

Fixpoint eval (e : expr) : nat :=
  match e with
  | Const x => x
  | Plus  a b => eval a + eval b
  | Minus a b => eval a - eval b
  | Mult  a b => eval a * eval b
  end.



(* Stack lang *)

Inductive instr := Push of nat | Add | Sub | Mul.

Fixpoint compile (e : expr) : seq instr :=
  match e with
  | Const x => [::Push x]
  | Plus  a b => compile a ++ compile b ++ [::Add]
  | Minus a b => compile a ++ compile b ++ [::Sub]
  | Mult  a b => compile a ++ compile b ++ [::Mul]
  end.



(* Stack lang runner *)

Definition run_step (s : seq nat) (i : instr) : seq nat :=
  match i with
  | Push x => x::s
  | Add => if s is b::a::s then a+b::s else s
  | Sub => if s is b::a::s then a-b::s else s
  | Mul => if s is b::a::s then a*b::s else s
  end.

Definition run (p : seq instr) (s : seq nat) : seq nat :=
  foldl run_step s p.



(* Stack lang decompiller *)

Definition dec_step (s : seq expr) (i : instr) : seq expr :=
  match i with
  | Push x => Const x :: s
  | Add => if s is b::a::s then Plus  a b :: s else s
  | Sub => if s is b::a::s then Minus a b :: s else s
  | Mul => if s is b::a::s then Mult  a b :: s else s
  end.

Definition dec (p : seq instr) (s : seq expr) : seq expr :=
  foldl dec_step s p.

Definition decompile (p : seq instr) : option expr :=
  if dec p [::] is [::result] then Some result else None.



(* Stack lang proof *)

Lemma run_cat : forall xs ys s, run (xs ++ ys) s = run ys (run xs s).
by elim=> // x xs ih ys s; rewrite /= ih. Qed.

Theorem run_compile e : run (compile e) [::] = [::eval e].
by elim: e [::] => // a iha b ihb s; rewrite !run_cat iha ihb. Qed.



(* Decompiller proof *)

Lemma dec_cat : forall xs ys s, dec (xs ++ ys) s = dec ys (dec xs s).
by elim=> // x xs ih ys s; rewrite /= ih. Qed.

Theorem dec_compile e : dec (compile e) [::] = [::e].
by elim: e [::] => // a iha b ihb s; rewrite !dec_cat iha ihb. Qed.

Lemma decompile_compile e : decompile (compile e) = Some e.
by rewrite /decompile dec_compile. Qed.

Lemma compile_inj : injective compile.
apply: pcan_inj decompile_compile. Qed.

2. generic implementation.v

From mathcomp Require Import all_ssreflect.



(* Basic definition *)

Inductive expr : Type :=
| Const of nat
| Plus of expr & expr
| Minus of expr & expr
| Mult of expr & expr.

Fixpoint eval (e : expr) : nat :=
  match e with
  | Const x => x
  | Plus  a b => eval a + eval b
  | Minus a b => eval a - eval b
  | Mult  a b => eval a * eval b
  end.

Inductive instr := Push of nat | Add | Sub | Mul.

Fixpoint compile (e : expr) : seq instr :=
  match e with
  | Const x => [::Push x]
  | Plus  a b => compile a ++ compile b ++ [::Add]
  | Minus a b => compile a ++ compile b ++ [::Sub]
  | Mult  a b => compile a ++ compile b ++ [::Mul]
  end.



(* Generic prog elim *)

Record prog_elim_alg T := mk_alg
  { on_push : nat -> T
  ; on_add  : T -> T -> T
  ; on_sub  : T -> T -> T
  ; on_mul  : T -> T -> T
  }.

Definition prog_elim_step {T} alg s i : seq T :=
  match i with
  | Push x => on_push T alg x :: s
  | Add => if s is b::a::s then on_add T alg a b :: s else s
  | Sub => if s is b::a::s then on_sub T alg a b :: s else s
  | Mul => if s is b::a::s then on_mul T alg a b :: s else s
  end.

Definition prog_elim {T} alg p s : seq T :=
  foldl (prog_elim_step alg) s p.



(* Generic proofs *)

Lemma prog_elim_cat {T} {alg : prog_elim_alg T} : forall xs ys s,
  prog_elim alg (xs ++ ys) s = prog_elim alg ys (prog_elim alg xs s).
by elim=> // x xs ih ys s; rewrite /= ih. Qed.

Record good_eval {T} (f : expr -> T) alg : Prop := mk_good_eval
  { good_on_push  : forall   x, f (Const   x) = on_push T alg x
  ; good_on_plus  : forall a b, f (Plus  a b) = on_add  T alg (f a) (f b)
  ; good_on_minus : forall a b, f (Minus a b) = on_sub  T alg (f a) (f b)
  ; good_on_mult  : forall a b, f (Mult  a b) = on_mul  T alg (f a) (f b)
  }.

Lemma prog_elim_compile {T f alg} {good : @good_eval T f alg} : forall e s,
  prog_elim alg (compile e) s = f e :: s.
Proof.
case: good => [gp ga gs gm].
elim=> [x|||]; first by rewrite gp.
all: by move=> a iha b ihb s; rewrite !prog_elim_cat iha ihb (ga, gs, gm).
Qed.



(* Example prog elims *)

Definition run := prog_elim (mk_alg _ id addn subn mult).
Definition dec := prog_elim (mk_alg _ Const Plus Minus Mult).
Definition decompile (p : seq instr) : option expr :=
  if dec p [::] is [::result] then Some result else None.

Theorem run_correct e : run (compile e) [::] = [::eval e].
by apply: prog_elim_compile. Qed.
Theorem dec_correct e : dec (compile e) [::] = [::e].
by apply: prog_elim_compile. Qed.
Lemma decompile_compile e : decompile (compile e) = Some e.
by rewrite /decompile dec_correct. Qed.
Lemma compile_inj : injective compile.
apply: pcan_inj decompile_compile. Qed.