Library MetaRocq.SafeCheckerPlugin.SafeTemplateChecker

From Stdlib Require Import Program.
From MetaRocq.Utils Require Import utils.
From MetaRocq.Common Require Import config.
From MetaRocq.Template Require Import AstUtils.
From MetaRocq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICTyping
    PCUICSN BDToPCUIC PCUICProgram.
From MetaRocq.SafeChecker Require Import PCUICErrors PCUICSafeChecker PCUICWfEnv PCUICWfEnvImpl.

Import MRMonadNotation.

From MetaRocq.TemplatePCUIC Require Import TemplateToPCUIC.

Definition trans_program (p : Ast.Env.program) : program :=
  let Σ' := trans_global_env p.1 in
  (Σ', trans Σ' p.2).

Definition EnvCheck_wf_env_ext {cf:checker_flags} {guard : abstract_guard_impl} := EnvCheck wf_env_ext.

Local Instance Monad_EnvCheck_wf_env_ext {cf:checker_flags} {guard : abstract_guard_impl} : Monad EnvCheck_wf_env_ext := _.

Program Definition infer_template_program {cf : checker_flags} {nor : normalizing_flags} {guard : abstract_guard_impl}
  (p : Ast.Env.program) φ
  
  {normalization_in
    : ∀ (g : global_decl) (Hdecls' : nat) (X : X_env_type optimized_abstract_env_impl),
      (∀ Σ0 : global_env,
          Σ0 ∼ X →
          Σ0 =
            {|
              universes := (trans_program p).1;
              declarations := skipn Hdecls' (declarations (trans_program p).1);
              retroknowledge := retroknowledge (trans_program p).1
            |}) →
      ∀ X' : X_env_ext_type optimized_abstract_env_impl,
        check_wf_env_ext_prop optimized_abstract_env_impl X X' (universes_decl_of_decl g) →
        ∀ Σ0 : global_env_ext, wf_ext Σ0 → Σ0 ∼_ext X' → NormalizationIn Σ0}
  {normalization_in'
    : ∀ x : X_env_ext_type optimized_abstract_env_impl,
      ((trans_program p).1, φ) ∼_ext x →
      ∀ Σ : global_env_ext, wf_ext Σ → Σ ∼_ext x → NormalizationIn Σ}
  : EnvCheck_wf_env_ext (let p' := trans_program p in ∑ A, { X : wf_env_ext |
    ∥ (p'.1, φ) = X.(wf_env_ext_reference).(reference_impl_env_ext) × wf_ext (p'.1, φ) × (p'.1, φ) ;;; [] |- p'.2 : A ∥ }) :=
  pp <- typecheck_program (cf := cf) (nor:=nor) optimized_abstract_env_impl (trans_program p) φ ;;
  ret (pp.π1 ; (exist (proj1_sig pp.π2) _)).
Next Obligation.
  sq. destruct H; split; eauto. destruct p0; split; eauto. eapply infering_typing; tea. eapply w. constructor.
Qed.

Program Definition infer_and_print_template_program {cf : checker_flags} {nor : normalizing_flags} {guard : abstract_guard_impl}
  (p : Ast.Env.program) φ

  {normalization_in
    : ∀ (g : global_decl) (Hdecls' : nat) (X : X_env_type optimized_abstract_env_impl),
      (∀ Σ0 : global_env,
          Σ0 ∼ X →
          Σ0 =
            {|
              universes := (trans_program p).1;
              declarations := skipn Hdecls' (declarations (trans_program p).1);
              retroknowledge := retroknowledge (trans_program p).1
            |}) →
      ∀ X' : X_env_ext_type optimized_abstract_env_impl,
        check_wf_env_ext_prop optimized_abstract_env_impl X X' (universes_decl_of_decl g) →
        ∀ Σ0 : global_env_ext, wf_ext Σ0 → Σ0 ∼_ext X' → NormalizationIn Σ0}
  {normalization_in'
    : ∀ x : X_env_ext_type optimized_abstract_env_impl,
      ((trans_program p).1, φ) ∼_ext x →
      ∀ Σ : global_env_ext, wf_ext Σ → Σ ∼_ext x → NormalizationIn Σ} : string + string :=
  match infer_template_program (cf:=cf) p φ return string + string with
  | CorrectDecl t ⇒
    let Σ' := trans_global_env p.1 in
    inl ("Environment is well-formed and " ^ string_of_term (trans Σ' p.2) ^
         " has type: " ^ string_of_term t.π1)
  | EnvError Σ (AlreadyDeclared id) ⇒
    inr ("Already declared: " ^ id)
  | EnvError Σ (IllFormedDecl id e) ⇒
    inr ("Type error: " ^ string_of_type_error Σ e ^ ", while checking " ^ id)
  end.