<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
Require Import ZArith Extraction.
From mathcomp Require Import all_ssreflect.

(* Simple Calculator *)

Module Simple.

Inductive expr : Set :=
  | Cst of Z
  | Var of nat
  | Add of expr & expr
  | Min of expr
  | Mul of expr & expr.

Print expr.
Extraction expr.

Fixpoint eval (env : list Z) (e : expr) : Z :=
  match e with
  | Cst x => x
  | Var n => nth 0 env n
  | Add e1 e2 => eval env e1 + eval env e2
  | Min e1 => 0-eval env e1
  | Mul e1 e2 => eval env e1 * eval env e2
  end%Z.

(* (x+3)*4 for x=2 *)
Eval compute in eval [:: 2%Z] (Mul (Add (Var 0) (Cst 3)) (Cst 4)).

Inductive code : Set :=
  | Cimm of Z          (* immediate *)
  | Cget of nat        (* スタックのん番目の値を上にコピーする *)
  | Cadd               (* 上の二つを足して、代わりに結果を置く *)
  | Cmin
  | Cmul.

Fixpoint eval_code (stack : list Z) (l : list code) :=
  match l with
  | nil => stack
  | c :: l' =>
    let stack' :=
        match c, stack with
        | Cimm x, _ => x :: stack
        | Cget n, _ => nth 0 stack n :: stack
        | Cadd, x :: y :: st => x+y :: st
        | Cmin, x :: st => 0-x :: st
        | Cmul, x :: y :: st => x*y :: st
        | _, _ => nil
        end%Z
    in eval_code stack' l'
  end.

Eval compute in eval_code [:: 2%Z] [:: Cget 0; Cimm 3; Cadd; Cimm 4; Cmul].

Fixpoint compile d (e : expr) : list code :=
  match e with
  | Cst x => [:: Cimm x]
  | Var n => [:: Cget (d+n)]    (* スタックに積んだものの下に見に行く *)
  | Add e1 e2 => compile d e2 ++ compile (S d) e1 ++ [:: Cadd]
  | Min e1 =>    compile d e1 ++ [:: Cmin]
  | Mul e1 e2 => compile d e2 ++ compile (S d) e1 ++ [:: Cmul]
  end.

Eval compute in compile 0 (Mul (Add (Var 0) (Cst 3)) (Cst 4)).
Eval compute in
  eval_code [:: 2%Z] (compile 0 (Mul (Add (Var 0) (Cst 3)) (Cst 4))).

Lemma eval_code_cat stack l1 l2 :
  eval_code stack (l1 ++ l2) = eval_code (eval_code stack l1) l2.
Proof. by elim: l1 stack => //=. Qed.

(* drop n s == s minus its first n items ([::] if size s <= n)     *)
Theorem compile_correct e d stack :
  eval_code stack (compile d e) = eval (drop d stack) e :: stack.
Proof.
  elim: e d stack => //= [n|e1 IHe1 e2 IHe2|e IHe|e1 IHe1 e2 IHe2] d stack.
  - by rewrite nth_drop.
  - by rewrite eval_code_cat IHe2 eval_code_cat IHe1.
Admitted.

End Simple.

(* Iterating calculator *)

Module Iterator.

Inductive expr : Set :=
  | Cst of Z
  | Var of nat
  | Add of expr & expr
  | Min of expr
  | Mul of expr & expr.

Fixpoint eval (env : list Z) (e : expr) : Z :=
  match e with
  | Cst x => x
  | Var n => nth 0 env n
  | Add e1 e2 => eval env e1 + eval env e2
  | Min e1 => 0-eval env e1
  | Mul e1 e2 => eval env e1 * eval env e2
  end%Z.

Inductive cmd : Set :=
  | Assign of nat & expr  (* env[n] に結果を入れる *)
  | Seq    of cmd & cmd   (* 順番に実行 *)
  | Repeat of expr & cmd. (* n 回繰り返す *)

(* r <- 1; repeat (i-1) {r <- i * r; i <- i-1} *)

Definition fact :=
  Seq (Assign 1 (Cst 1))
      (Repeat (Add (Var 0) (Cst (-1)))
         (Seq (Assign 1 (Mul (Var 0) (Var 1)))
              (Assign 0 (Add (Var 0) (Cst (-1)))))).

Print Z.
Print positive.
Print iter.

Fixpoint eval_cmd (env : list Z) (c : cmd) : list Z :=
  match c with
  | Assign n e => set_nth 0%Z env n (eval env e)
  | Seq c1 c2 => eval_cmd (eval_cmd env c1) c2
  | Repeat e c =>
    if eval env e is Zpos n
    then iter (Pos.to_nat n) (fun e => eval_cmd e c) env
    else env
  end.

Eval compute in eval_cmd [:: 5%Z] fact.

Inductive code : Set :=
  | Cimm of Z
  | Cget of nat
  | Cadd
  | Cmin
  | Cmul
  | Cset of nat    (* スタックの上をn番目に書き込む *)
  | Crep of nat    (* 次のn個の命令ををスタックの上分繰り返す *)
  | Cnext.         (* 終ったら Cnext の後ろに跳ぶ *)

Fixpoint eval_code (stack : list Z) (l : list code) :=
  match l with
  | nil => stack
  | c :: l' =>
    let stack' :=
        match c, stack with
        | Cimm x, _ => x :: stack
        | Cget n, _ => nth 0 stack n :: stack
        | Cadd, x :: y :: st => x+y :: st
        | Cmin, x :: st => 0-x :: st
        | Cmul, x :: y :: st => x*y :: st
        | Cset n, x :: st => set_nth 0%Z st n x
        | Crep _, Zpos n :: st => (* seq の iter を使う *)
          iter (Pos.to_nat n) (fun st => eval_code st l') st
        | Crep _, _ :: st => st
        | Cnext, _ => stack
        | _, _ => nil
        end%Z
    in
    match c with
    | Crep n => eval_drop n stack' l'
    | Cnext => stack'
    | _ => eval_code stack' l'
    end 
  end
with eval_drop n st (l : list code) :=  (* 相互再帰 *)
  match l, n with
  | _ :: l', 0 => eval_code st l'
  | _ :: l', S n' => eval_drop n' st l'
  | [::], _ => st
  end.

Fixpoint compile d (e : expr) : list code :=
  match e with
  | Cst x => [:: Cimm x]
  | Var n => [:: Cget (d+n)]
  | Add e1 e2 => compile d e2 ++ compile (S d) e1 ++ [:: Cadd]
  | Min e1 =>    compile d e1 ++ [:: Cmin]
  | Mul e1 e2 => compile d e2 ++ compile (S d) e1 ++ [:: Cmul]
  end.

Fixpoint compile_cmd (c : cmd) : list code :=
  match c with
  | Assign n e => compile 0 e ++ [:: Cset n]
  | Seq c1 c2  => compile_cmd c1 ++ compile_cmd c2
  | Repeat e c =>
      let l := compile_cmd c in
      compile 0 e ++ [:: Crep (length l)] ++ l ++ [:: Cnext]
  end.

Eval compute in compile_cmd fact.
Eval compute in eval_code [:: 5%Z] (compile_cmd fact).

Definition neutral c :=
  match c with Cnext | Crep _ => false | _ => true end.

Inductive balanced : list code -> Prop :=
  | Bneutral : forall c, neutral c = true -> balanced [:: c]
  | Bcat : forall l1 l2, balanced l1 -> balanced l2 -> balanced (l1 ++ l2)
  | Brep : forall l, balanced l ->
                     balanced (Crep (length l) :: l ++ [:: Cnext]).

Lemma eval_drop_cat st l1 l2 :
  eval_drop (length l1) st (l1 ++ Cnext :: l2) = eval_code st l2.
Admitted.

Check eq_iter.

Lemma eval_code_cat stack (l1 l2 : seq code) :
  balanced l1 ->
  eval_code stack (l1 ++ l2) =
  eval_code (eval_code stack l1) l2.
Admitted.

Hint Constructors balanced.

Lemma compile_balanced n e : balanced (compile n e).
Proof. by elim: e n => /=; auto. Qed.

Theorem compile_correct e d stack :
  eval_code stack (compile d e) = eval (drop d stack) e :: stack.
Admitted.

Lemma compile_cmd_balanced c : balanced (compile_cmd c).
Proof. by elim: c => /=; auto using compile_balanced. Qed.

Hint Resolve compile_balanced compile_cmd_balanced.

Theorem compile_cmd_correct c stack :
  eval_code stack (compile_cmd c) = eval_cmd stack c.
Admitted.

End Iterator.

Extraction Iterator.eval_code.