File ProductSortWithLookup

From MatchingLogic Require Export ProductSort.
Import MatchingLogic.Logic.Notations
       MatchingLogic.Theories.Definedness_Syntax.Notations
       MatchingLogic.Theories.Sorts_Syntax.Notations
       MatchingLogic.Theories.ProductSort.Notations.


Inductive Symbols {Σ : Signature} (s1 s2 : Pattern) :=
| ml_sym_lookup
| ml_sym_product_symbols (s : ProductSort.Symbols s1 s2)
.

#[global]
Instance Symbols_eqdec {Σ : Signature} s1 s2 : EqDecision (Symbols s1 s2).

Class Syntax {Σ : Signature} (s1 s2 : Pattern) :=
{
    (* imported_product :: ProductSort.Syntax s1 s2; *)
    imported_sorts : Sorts_Syntax.Syntax ;
    sym_inj: Symbols s1 s2 → symbols;
    sym_inj_inj: Inj (=) (=) sym_inj;
}.

(*[global] Existing Instance imported_product.*)
#[global] Existing Instance imported_sorts.
#[global] Existing Instance sym_inj_inj.

Section pswl.
    Context
      {Σ : Signature}
      (s1 s2 : Pattern)
      (wfs1 : well_formed s1 = true)
      (wfs2 : well_formed s2 = true)
      {syntax : Syntax s1 s2}
    .
    Import Notations.
    Open Scope ml_scope.
    Delimit Scope ml_scope with ml. (* TODO move this somewhere else *)

    (* Typelass resolution does not terminate on this input.
       TODO: figure out why.
       So I will just define the instance via ltac.
    *)
    (*
    [global] Instance imported_product : (ProductSort.Syntax s1 s2) := {| ProductSort.imported_sorts := @imported_sorts Σ s1 s2 syntax; |}. *)
    #[global]
    Instance product_syntax
        : (ProductSort.Syntax s1 s2)
    .

    Definition ml_lookup (ϕ k : Pattern)
        := patt_app (patt_app (patt_sym (sym_inj (ml_sym_lookup s1 s2))) ϕ) k
    .

    Inductive AxiomName :=
    | AxKeyValue
    .

    Definition axiom (name : AxiomName) : Pattern :=
    match name with
    | AxKeyValue ⇒
        all s1, (
            all s2, (
                all s1, (
                    ml_lookup (mlPair { s1 , s2 } (b2 , b1)) b0 =ml (patt_and (b2 =ml b0) b1)
                )
            )
        )
    end.

    Program Definition named_axioms : NamedAxioms :=
    {| NAName := AxiomName;
        NAAxiom := axiom;
    |}.

    Definition Γprodl := theory_of_NamedAxioms named_axioms.

End pswl.