Require Import Vector Arith.
Notation vec := Vector.t.


Class funcs_signature := { syms : Type; ar_syms : syms }.
Class preds_signature := { preds : Type; ar_preds : preds }.
Class operators := { binop : Type ; quantop : Type }.

Coercion syms : funcs_signature >-> Sortclass.
Coercion preds : preds_signature >-> Sortclass.

Section Syntax.

  Context {Σ_funcs : funcs_signature}.

  Unset Elimination Schemes.

  Inductive function : Type :=
    | var_func : ar, function ar
    | sym : f : syms, function (ar_syms f).

  Inductive term : Type :=
    | var_indi : term
    | func {ar} (_ : function ar) (v : vec term ar) : term.

  Set Elimination Schemes.

  Context {Σ_preds : preds_signature}.

  Inductive predicate : Type :=
    | var_pred : ar, predicate ar
    | pred : P : preds, predicate (ar_preds P).

  Context {ops : operators}.

  Inductive form : Type :=
    | fal : form
    | atom : {ar}, predicate ar vec term ar form
    | bin : binop form form form
    | quant_indi : quantop form form
    | quant_func : quantop form form
    | quant_pred : quantop form form.

End Syntax.

Arguments var_func {_} _ {_}, {_} _ _.
Arguments var_pred {_} _ {_}, {_} _ _.


Inductive full_logic_sym : Type :=
| Conj : full_logic_sym
| Disj : full_logic_sym
| Impl : full_logic_sym.

Inductive full_logic_quant : Type :=
| All : full_logic_quant
| Ex : full_logic_quant.

#[global]
Instance full_operators : operators :=
  {| binop := full_logic_sym ; quantop := full_logic_quant |}.


Section Tarski.

  Definition env_indi domain := domain.
  Definition env_func domain := ar, vec domain ar domain.
  Definition env_pred domain := ar, vec domain ar Prop.
  Record env domain := new_env { get_indi : env_indi domain ; get_func : env_func domain ; get_pred : env_pred domain }.
  Notation "⟨ a , b , c ⟩" := (new_env _ a b c).

  Arguments get_indi {_}.
  Arguments get_func {_}.
  Arguments get_pred {_}.

  Class Econs X Env := econs : X Env Env.
  Local Notation "x .: rho" := (econs x ) (at level 70, right associativity).

  #[global] Instance econs_indi domain : Econs domain ( domain) :=
     x env n match n with 0 x | S n env n end.

  Definition econs_ar ar p : Econs (p ar) ( ar, p ar) :=
     x env n match n with
            | 0 ar' match Nat.eq_dec ar ar' with
                              | left e match e in _ = ar' return p ar' with eq_refl x end
                              | right _ env n ar'
                              end
            | S n ar' if Nat.eq_dec ar ar' then env n ar' else env (S n) ar'
    end.
  #[global] Instance econs_func domain ar : Econs _ _ := econs_ar ar ( ar vec domain ar domain).
  #[global] Instance econs_pred domain ar : Econs _ _ := econs_ar ar ( ar vec domain ar Prop).

  Context {Σ_funcs : funcs_signature}.
  Context {Σ_preds : preds_signature}.

  Variable domain : Type.

  Class interp := B_I {
      i_f : f : syms, vec domain (ar_syms f) domain ;
      i_P : P : preds, vec domain (ar_preds P) Prop ;
  }.
  Context { I : interp }.

  Definition eval_function {ar} (rho : env domain) (f : function ar) : vec domain ar domain :=
    match f with
    | var_func f get_func f _
    | sym f i_f f
    end.

  Definition eval_predicate {ar} (rho : env domain) (P : predicate ar) : vec domain ar Prop :=
    match P with
    | var_pred P get_pred P _
    | pred P i_P P
    end.

  Fixpoint eval (rho : env domain) (t : term) : domain :=
    match t with
    | var_indi x get_indi x
    | func f v eval_function f (Vector.map (eval ) v)
    end.

  Fixpoint sat (rho : env domain) (phi : form) : Prop :=
    match with
    | atom P v eval_predicate P (Vector.map (eval ) v)
    | fal False
    | bin Impl sat sat
    | bin Conj sat sat
    | bin Disj sat sat
    | quant_indi Ex d : domain, sat d .: get_indi , get_func , get_pred
    | quant_indi All d : domain, sat d .: get_indi , get_func , get_pred
    | quant_func Ex ar (f : vec domain ar domain), sat get_indi , f .: get_func , get_pred
    | quant_func All ar (f : vec domain ar domain), sat get_indi , f .: get_func , get_pred
    | quant_pred Ex ar (P : vec domain ar Prop), sat get_indi , get_func , P .: get_pred
    | quant_pred All ar (P : vec domain ar Prop), sat get_indi , get_func , P .: get_pred
    end.

End Tarski.

Record Model `{funcs_signature, preds_signature} := {
  M_domain : Type ;
  M_interp : interp M_domain
}.

Coercion M_domain : Model >-> Sortclass.
#[global] Instance M_I `{funcs_signature, preds_signature} M : interp (M_domain M) := M_interp M.


Module SOLNotations.

  Notation "x .: rho" := (econs x ) (at level 70, right associativity).

  Notation "$ x" := (var_indi x) (at level 5, format "$ '/' x").
  Notation "i$ x" := (var_indi x) (at level 5, format "i$ '/' x").
  Notation "f$ x" := (func (var_func x)) (at level 5, format "f$ '/' x").
  Notation "p$ x" := (atom (var_pred x)) (at level 5, format "p$ '/' x").

  Notation "⊥" := fal.
  Notation "A ∧ B" := (@bin _ _ full_operators Conj A B) (at level 41).
  Notation "A ∨ B" := (@bin _ _ full_operators Disj A B) (at level 42).
  Notation "A '~>' B" := (@bin _ _ full_operators Impl A B) (at level 43, right associativity).
  Notation "A '<~>' B" := ((A ~> B) (B ~> A)) (at level 43).
  Notation "¬ A" := (A ~> ) (at level 40).

  Notation "∀i Phi" := (@quant_indi _ _ full_operators All Phi) (at level 50).
  Notation "∃i Phi" := (@quant_indi _ _ full_operators Ex Phi) (at level 50).
  Notation "∀f ( ar ) Phi" := (@quant_func _ _ full_operators All ar Phi) (at level 50).
  Notation "∃f ( ar ) Phi" := (@quant_func _ _ full_operators Ex ar Phi) (at level 50).
  Notation "∀p ( ar ) Phi" := (@quant_pred _ _ full_operators All ar Phi) (at level 50).
  Notation "∃p ( ar ) Phi" := (@quant_pred _ _ full_operators Ex ar Phi) (at level 50).

End SOLNotations.

#[global] Instance empty_funcs_sig : funcs_signature := {| syms := False; ar_syms := f match f with end |}.
#[global] Instance empty_preds_sig : preds_signature := {| preds := False; ar_preds := P match P with end |}.


Definition SOL_valid (phi : form) := (M : Model) rho, sat M .

Definition SOL_satis (phi : form) := (M : Model) rho, sat M .