From Coq Require Import Lia List Init.Nat.
From PCF2.Autosubst Require Import pcf_2.
From PCF2 Require Import CE pcf_2_system pcf_2_utils.
From PCF2.external Require Import SR.
From PCF2.external.Synthetic Require Import Definitions DecidabilityFacts.

Definition T (a: str) := base_fun (2 * length a + 2) Base.

Definition rule_type '(e, f) := (T e) ⟶ (T f).

Definition make_rule_types (R: list (str * str)) :=
    map (fun r => rule_type r) R.

Definition word_encoding (f: str -> tm) (v: bool) :=
    forall (b: str), nil ⊢ (f b): T b /\ nil ⊢ (f b) ≤ (lam_T (2 * (length b) + 2) (embed v)): (T b).

Definition val_word_enc := sig (fun p :(str -> tm) * bool => word_encoding (fst p) (snd p)).

Definition rule_ineq (F: tm) (enc: str -> tm) (d1 d2 e f: str):=
    (base_context (2*(length (d1 ++ f ++ d2))+2)) ⊢ apply_args (enc (d1 ++ f ++ d2)) (var_seq 0 (2* length (d1 ++ f ++ d2) + 2))
    ≤ apply_args (app F (lam_T (2 * length e + 2) (apply_args (enc (d1 ++ e ++ d2)) ((var_seq (2 * length e + 2)(2 * length d1))++(var_seq 0 (2 * length e)) ++ (var_seq (2 * (length e + length d1 + length f) + 2) (2 * length d2))++(var_seq (2 * length e) 2))))) (var_seq (2 * length d1) (2 * length f) ++ var_seq (2 * (length (d1 ++ f ++ d2))) 2) : Base.

Definition rule_encoding enc (r: str * str) (F: tm) :=
    nil ⊢ F: rule_type r /\ (forall d1 d2, rule_ineq F enc d1 d2 (fst r) (snd r))
    /\ forall F', nil ⊢ F': rule_type r -> (forall d1 d2, rule_ineq F' enc d1 d2 (fst r) (snd r)) -> nil ⊢ F ≤ F': rule_type r.

Axiom rule_enc_exist:
    forall enc v,word_encoding enc v -> forall (r: str * str), exists F, rule_encoding enc r F.

Definition t_subst (enc: str -> tm) (R: list (str * str)) (f: str * str -> tm) (a b: str) :=
    fun n: nat =>
    if leb n (2 * (length b) + 1) then var_tm n else
        if leb n (2 * (length b) + 1 + length R) then
        match nth_error R (n - (2 * (length b) + 2)) with
        | None => bot
        | Some r => f r
        end else
        if leb n (2 * (length b) + 2 + length R) then enc a else bot.

Definition fun_rule_encoding (enc: str -> tm) (R: list (str * str)) (f: str * str -> tm) :=
    Forall (fun r => rule_encoding enc r (f r)) R.

Definition satisfies (t: tm) (v: bool) (enc: str -> tm) (R: list (str * str)) (f: str * str -> tm) (a: str) (b: str) :=
    (base_context (2*(length b) + 2)) ⊢ apply_args (enc b) (var_seq 0 (2*(length b) + 2)) ≤ Subst_tm (t_subst enc R f a b) t : Base.

Definition SATIS (E: list (val_word_enc)) (R: list (str * str)) : str * str -> Prop :=
    fun '(a, b) => exists t, ((base_context (2*(length b) + 2)) ++ ((make_rule_types R)) ++ (cons (T a) nil)) ⊢ t: Base /\
    Forall (fun p => forall (f: str * str -> tm), fun_rule_encoding (fst (proj1_sig p)) R f -> satisfies t (snd (proj1_sig p)) (fst (proj1_sig p)) R f a b) E.

Definition val_rule_enc enc r := sig (fun F : tm => rule_encoding enc r F).

Definition rule_fun (R: list(str * str)) (A: ty) :=
  list_to_fun (make_rule_types R) A.