Require Import ZArith. From Ssreflect Require Import ssreflect ssrnat seq. (* 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. 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. Theorem compile_correct e d stack : eval_code stack (compile d e) = eval (drop d stack) e :: stack. 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)))))). Fixpoint repeat_n {A : Type} (n : nat) (f : A -> A) (x : A) := if n is S n' then repeat_n n' f (f x) else x. Print Z. Print positive. 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 repeat_n (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 (* 次のCnextまでをスタックの上分繰り返す *) | Cnext. (* 終ったら Cnext の後ろに跳ぶ *) Definition next_skip c n := match c with | Crep => S n | Cnext => n - 1 | _ => n end. Fixpoint eval_code (skip : nat) (stack : list Z) (l : list code) := match l with | nil => stack | c :: l' => if skip is S _ then eval_code (next_skip c skip) stack l' else if c is Cnext then stack else 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 => repeat_n (Pos.to_nat n) (fun st => eval_code 0 st l') st | Crep, _ :: st => st | _, _ => nil end%Z in eval_code (next_skip c skip) stack' l' 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 => compile 0 e ++ [:: Crep] ++ compile_cmd c ++ [:: Cnext] end. Eval compute in compile_cmd fact. Eval compute in eval_code 0 [:: 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 :: l ++ [:: Cnext]). Hint Constructors balanced. Lemma repeat_n_eq {A:Type} n f1 f2 (st : A) : (forall st, f1 st = f2 st) -> repeat_n n f1 st = repeat_n n f2 st. Admitted. Lemma eval_code_cat k stack (l1 l2 : seq code) : balanced l1 -> eval_code k stack (l1 ++ l2) = eval_code k (eval_code k stack l1) l2. Admitted. Lemma compile_balanced n e : balanced (compile n e). Proof. by elim: e n => /=; auto. Qed. Theorem compile_correct e d stack : eval_code 0 stack (compile d e) = eval (drop d stack) e :: stack. Admitted. Lemma compile_cmd_balanced c : balanced (compile_cmd c). Admitted. Lemma compile_cmd_S n c stack : balanced c -> eval_code (S n) stack c = stack. Admitted. Hint Resolve compile_balanced compile_cmd_balanced. Theorem compile_cmd_correct c stack : eval_code 0 stack (compile_cmd c) = eval_cmd stack c. Admitted. End Iterator. Extraction Iterator.eval_code.