theory.monoid_normalization

Require Import Omega.
Require Import abstract_algebra ua_packed.
Require universal_algebra varieties.monoids.

Notation msig := varieties.monoids.sig.
Notation Op := (universal_algebra.Op msig False).
Notation App := (universal_algebra.App msig False _ _).

Import universal_algebra.

Section contents.


  Context (V: Type).

  Notation uaTerm := (universal_algebra.Term0 msig V tt).
  Notation Applied := (@ua_packed.Applied msig V tt).

  Inductive Term := Var (v: V) | Unit | Comp (x y: Term).

  Fixpoint to_ua (e: Term): Applied :=
    match e with
    | Var v => ua_packed.AppliedVar msig v tt
    | Unit => ua_packed.AppliedOp msig monoids.one (ua_packed.NoMoreArguments msig tt)
    | Comp x y => ua_packed.AppliedOp msig monoids.mult
       (MoreArguments msig tt _ (to_ua x) (MoreArguments msig tt _ (to_ua y) (NoMoreArguments msig tt)))
    end.

  Definition from_ua (t: Applied): { r: Term | to_ua r t }.

  Fixpoint measure (e: Term): nat :=
    match e with
    | Var v => 0%nat
    | Unit => 1%nat
    | Comp x y => S (2 * measure x + measure y)
    end.

  Context `{Monoid M}.

  Notation eval vs := (universal_algebra.eval msig (λ _, (vs: V M))).

  Program Fixpoint internal_simplify (t: Term) {measure (measure t)}:
      { r: Term | v, eval v (curry (to_ua r)) = eval v (curry (to_ua t)) } :=
    match t with
    | Var _ => t
    | Unit => t
    | Comp Unit y => internal_simplify y
    | Comp x Unit => internal_simplify x
    | Comp ((Var _) as x) y => Comp x (internal_simplify y)
    | Comp (Comp x y) z => internal_simplify (Comp x (Comp y z))
    end.

  Solve Obligations using (program_simpl; simpl; try apply reflexivity; omega).




  Program Definition simplify (t: uaTerm): { r: uaTerm | v, eval v r = eval v t } :=
    curry (to_ua (internal_simplify (from_ua (decode0 t)))).



End contents.