theory.setoids ne_list.
Require Import
  abstract_algebra util jections.
Require Export

Section for_signature.
  Variable : Signature.

  Notation OpType := (OpType (sorts )).

  Inductive Term (V: Type): OpType Type :=
    | Var: V a, Term V ( a)
    | App t y: Term V (ne_list.cons y t) Term V ( y) Term V t
    | Op o: Term V ( o).

  Implicit Arguments Var [[V]].

  Fixpoint map_var `(f: V W) `(t: Term V o): Term W o :=
    match t in Term _ o return Term W o with
    | Var v s => Var (f v) s
    | App _ _ x y => App _ _ _ (map_var f x) (map_var f y)
    | Op s => Op _ s

  Definition Term0 v sort := Term v ( sort).

  Section applications_ind.
    Context V (P: {a}, Term0 V a Type).

    Implicit Arguments P [[a]].

    Fixpoint applications {ot}: Term V ot Type :=
      match ot with
      | x => @P x
      | ne_list.cons x y => λ z, v, P v applications (App V _ _ z v)

    Lemma applications_rect:
      ( v a, P (Var v a))
      ( o, applications (Op _ o))
      ( a (t: Term0 V a), P t).

  End applications_ind.

  Definition T := Term nat.
  Definition T0 := Term0 nat.

  Definition Identity t := prod (T t) (T t).
  Definition Identity0 sort := Identity ( sort).

  Definition mkIdentity0 {sort}: T ( sort) T ( sort) Identity0 sort := pair.

  Record Entailment (P: Type): Type := { entailment_premises: list P; entailment_conclusion: P }.

  Definition EqEntailment := Entailment (sigT Identity0).

  Inductive Statement: Type :=
    | Eq t (i: Identity t)
    | Impl (a b: Statement)
    | Conj (a b: Statement)
    | Disj (a b: Statement)
    | Ext (P: Prop).

  Definition identity_as_eq (s: sigT Identity0): Statement := Eq _ (projT2 s).
  Coercion identity_as_entailment sort (e: Identity0 sort): EqEntailment := Build_Entailment _ nil (existT _ _ e).

  Coercion entailment_as_statement (e: EqEntailment): Statement :=
     (fold_right Impl (identity_as_eq (entailment_conclusion _ e)) (map identity_as_eq (entailment_premises _ e))).

  Definition entailment_as_conjunctive_statement (e: EqEntailment): Statement :=
    Impl (fold_right Conj (Ext True) (map identity_as_eq (entailment_premises _ e)))
      (identity_as_eq (entailment_conclusion _ e)).

  Section Vars.
    Context (A: sorts Type) (V: Type) `{e: a, Equiv (A a)} `{ a, Equivalence (e a)}.

    Definition Vars := a, V A a.

    Global Instance ua_vars_equiv: Equiv Vars :=
     @pointwise_dependent_relation (sorts ) (λ a, V A a)
      (λ _, pointwise_relation _ (=)).

    Global Instance: Equivalence ((=): relation Vars) := {}.
  End Vars.

  Definition no_vars x: Vars x False := λ _, False_rect _.

  Fixpoint close {V} {o} (v: Vars (λ x, Term False ( x)) V) (t: Term V o): Term False o :=
    match t in Term _ o return Term False o with
    | Var x y => v y x
    | App x y z r => App _ x y (close v z) (close v r)
    | Op o => Op _ o

  Section eval.
    Context `{Algebra A}.

    Fixpoint eval {V} {n: OpType} (vars: Vars A V) (t: Term V n) {struct t}: op_type A n :=
      match t with
      | Var v a => vars a v
      | Op o => algebra_op o
      | App n a f p => eval vars f (eval vars p)

    Global Instance eval_proper {V} (n: OpType):
      Proper ((=) ==> eq ==> (=)) (@eval V n).

    Global Instance eval_strong_proper {V} (n: OpType):
      Proper ((pointwise_dependent_relation (sorts ) _
        (λ _, pointwise_relation V eq)) ==> eq ==> eq) (@eval V n).

    Hint Extern 4 (Equiv (Term _ _)) => exact eq: typeclass_instances.
    Hint Extern 4 (Equiv (Term0 _ _)) => exact eq: typeclass_instances.

    Instance: V n v, Setoid_Morphism (@eval V ( n) v).

    Fixpoint app_tree {V} {o}: Term V o op_type (Term0 V) o :=
      match o with
      | _ => id
      | ne_list.cons _ _ => λ x y, app_tree (App _ _ _ x y)
    Lemma eval_map_var `(f: V W) v s (t: Term V s):
      eval v (map_var f t) eval (λ s, v s f) t.

    Definition eval_stmt (vars: Vars A nat): Statement Prop :=
      fix F (s: Statement) :=
       match s with
       | Eq _ i => eval vars (fst i) = eval vars (snd i)
       | Impl a b => F a F b
       | Ext P => P
       | Conj a b => F a F b
       | Disj a b => F a F b

    Global Instance eval_stmt_proper: Proper ((=) ==> eq ==> iff) eval_stmt.

    Definition boring_eval_entailment (vars: Vars A nat) (ee: EqEntailment):
      eval_stmt vars ee eval_stmt vars (entailment_as_conjunctive_statement ee).

  End eval.
End for_signature.

Hint Extern 0 (Equiv (Vars _ _ _)) => eapply @ua_vars_equiv : typeclass_instances.

Record EquationalTheory :=
  { et_sig:> Signature
  ; et_laws:> EqEntailment et_sig Prop }.

Class InVariety
  (et: EquationalTheory)
  (carriers: sorts et Type)
  {e: a, Equiv (carriers a)}
  `{!AlgebraOps et carriers}: Prop :=
  { variety_algebra:> Algebra et carriers
  ; variety_laws: s, et_laws et s vars, eval_stmt et vars s }.

Module op_type_notations.
  Global Infix "-=>" := (ne_list.cons) (at level 95, right associativity).
End op_type_notations.
Module notations.
  Global Infix "===" := (mkIdentity0 _) (at level 70, no associativity).
  Global Infix "-=>" := (Impl _) (at level 95, right associativity).
End notations.