Require Import List. (* source language *) Inductive binop : Set := Plus | Times. Inductive exp : Set := | Const : nat -> exp | Binop : binop -> exp -> exp -> exp. Definition evalBinop (b : binop) : nat -> nat -> nat := match b with | Plus => plus | Times => mult end. Fixpoint evalExp (e : exp) : nat := match e with | Const n => n | Binop b e1 e2 => (evalBinop b) (evalExp e1) (evalExp e2) end. Eval simpl in evalExp (Const 42). Eval simpl in evalExp (Binop Times (Binop Plus (Const 2) (Const 3)) (Const 4)). (* stack machine *) Inductive instr : Set := | iConst : nat -> instr | iBinop : binop -> instr. Definition prog := list instr. Definition stack := list nat. Print option. Definition runInstr (i: instr) (s: stack): option stack := match i with | iConst n => Some (n :: s) | iBinop b => match s with | arg1 :: arg2 :: s' => Some (((evalBinop b) arg1 arg2) :: s') | _ => None end end. Fixpoint runProg (p: prog) (s: stack) : option stack := match p with | nil => Some s | i :: p' => match runInstr i s with | None => None | Some s' => runProg p' s' end end. Eval simpl in runProg ((iConst 2) :: (iConst 4) :: (iBinop Times) :: nil) nil. Eval simpl in runProg ((iConst 2) :: (iBinop Times) :: nil) nil. (* compiler *) (* compiler correctness *)