Source

calcoq / main.v

Require Import QArith.
Open Scope Q_scope.

Require Import List.
Inductive deci : Set :=
  | D0 : deci | D1 : deci | D2 : deci | D3 : deci | D4 : deci
  | D5 : deci | D6 : deci | D7 : deci | D8 : deci | D9 : deci.
Definition decimal := list deci.

Inductive prod_op : Set :=
  | Mult : prod_op | Div : prod_op.
Inductive sum_op : Set :=
  | Add : sum_op | Sub : sum_op.

Inductive value : Set := VNum : decimal -> value | VExpr : expr -> value
with product : Set := Prod : value -> list (prod_op * value) -> product
with expr : Set := Expr : product -> list (sum_op * product) -> expr.

Definition q_of_deci d := match d with
  | D0 => 0 # 1
  | D1 => 1 # 1
  | D2 => 2 # 1
  | D3 => 3 # 1
  | D4 => 4 # 1
  | D5 => 5 # 1
  | D6 => 6 # 1
  | D7 => 7 # 1
  | D8 => 8 # 1
  | D9 => 9 # 1
  end.
Definition q10 := 10 # 1.
Fixpoint q_of_decimal ds := match ds with
  | nil => 0
  | cons d_i ds => q_of_deci d_i + q10 * q_of_decimal ds
  end.

Inductive term : Set :=
  | TVal : Q -> term
  | TExpr : expr -> term
  | TProd : prod_op -> term -> term -> term
  | TSum  : sum_op  -> term -> term -> term.

Definition term_of_val v := match v with
  | VNum n  => TVal (q_of_decimal n)
  | VExpr e => TExpr e
  end.
Fixpoint reduce t := match t with
  | TVal q => TVal q
  | TExpr (Expr (Prod v nil) nil) => term_of_val v
  | TExpr (Expr (Prod v1 (cons (Mult, v2) tl)) nil) =>
      TProd Mult (term_of_val v1) (TExpr (Expr (Prod v2 tl) nil))
  | TExpr (Expr (Prod v1 (cons (Div,  v2) tl)) nil) =>
      TProd Div  (term_of_val v1) (TExpr (Expr (Prod v2 tl) nil))
  | TExpr (Expr p1 (cons (Add, p2) tl)) =>
      TSum Add (TExpr (Expr p1 nil)) (TExpr (Expr p2 tl))
  | TExpr (Expr p1 (cons (Sub, p2) tl)) =>
      TSum Sub (TExpr (Expr p1 nil)) (TExpr (Expr p2 tl))
  | TProd Mult (TVal q1) (TVal q2) => TVal (q1 * q2)
  | TProd Div  (TVal q1) (TVal q2) => TVal (q1 / q2)
  | TProd op t1 t2 => TProd op (reduce t1) (reduce t2)
  | TSum Add (TVal q1) (TVal q2) => TVal (q1 + q2)
  | TSum Sub (TVal q1) (TVal q2) => TVal (q1 - q2)
  | TSum op t1 t2 => TSum op (reduce t1) (reduce t2)
  end.


Extraction "coqMain.ml" rev reduce Qred.