Library MetaCoq.Erasure.SafeErasureFunction

Section fix_sigma.
Variable Σ : global_env_ext.
Variable HΣ : ∥wf Σ∥.

Definition term_rel : Relation_Definitions.relation (∑ Γ t, wellformed Σ Γ t) :=
  fun '(Γ2; B; H) '(Γ1; t1; H2) ⇒
    ∥∑ na A, red (fst Σ) Γ1 t1 (tProd na A B) × (Γ1,, vass na A) = Γ2∥.

Definition cod B t := match t with tProd _ _ B' ⇒ B = B' | _ ⇒ False end.

Lemma wf_cod : WellFounded cod.

Lemma wf_cod' : WellFounded (Relation_Operators.clos_trans _ cod).

Lemma Acc_no_loop X (R : X → X → Prop) t : Acc R t → R t t → False.


Instance wf_reduction : WellFounded term_rel.


Equations is_arity Γ (HΓ : ∥wf_local Σ Γ∥) T (HT : wellformed Σ Γ T) :
  typing_result ({Is_conv_to_Arity Σ Γ T} + {¬ Is_conv_to_Arity Σ Γ T})
  by wf ((Γ;T;HT) : (∑ Γ t, wellformed Σ Γ t)) term_rel :=
  {
    is_arity Γ HΓ T HT with (@reduce_to_sort _ Σ HΣ Γ T HT) ⇒ {
    | Checked H ⇒ ret (left _) ;
    | TypeError _ with inspect (@reduce_to_prod _ Σ HΣ Γ T _) ⇒ {
      | exist (Checked (na; A; B; H)) He ⇒
        match is_arity (Γ,, vass na A) _ B _ with
        | Checked (left H) ⇒ ret (left _)
        | Checked (right H) ⇒ ret (right _)
        | TypeError t ⇒ TypeError t
        end;
      | exist (TypeError (NotAProduct _ _)) He ⇒ ret (right _);
      | exist (TypeError t) He ⇒ TypeError t }
    }
  }.


End fix_sigma.

Definition wf_ext_wf Σ : wf_ext Σ → wf Σ := fst.

Program Definition is_erasable (Sigma : PCUICAst.global_env_ext) (HΣ : ∥wf_ext Sigma∥) (Gamma : context) (t : PCUICAst.term) (Ht : welltyped Sigma Gamma t) :
  typing_result ({∥isErasable Sigma Gamma t∥} +{∥(isErasable Sigma Gamma t → False)∥}) :=
  mlet (T; _) <- @type_of extraction_checker_flags Sigma _ _ Gamma t Ht ;;
  mlet b <- is_arity Sigma _ Gamma _ T _ ;;
  if b : {_} + {_} then
    ret (left _)
  else mlet (K; _) <- @type_of extraction_checker_flags Sigma _ _ Gamma T _ ;;
       mlet (u;_) <- @reduce_to_sort _ Sigma _ Gamma K _ ;;
      match is_prop_sort u with true ⇒ ret (left _) | false ⇒ ret (right _) end
.









Section Erase.

  Definition is_box c :=
    match c with
    | E.tBox ⇒ true
    | _ ⇒ false
    end.

  Fixpoint mkAppBox c n :=
    match n with
    | 0 ⇒ c
    | S n ⇒ mkAppBox (E.tApp c E.tBox) n
    end.

  Definition on_snd_map {A B C} (f : B → C) (p : A × B) :=
    (fst p, f (snd p)).

  Variable (Σ : global_env_ext)( HΣ :∥ wf_ext Σ ∥).


  Section EraseMfix.
    Context (erase : ∀ (Γ : context) (t : term) (Ht : welltyped Σ Γ t), typing_result E.term).

    Program Definition erase_mfix Γ (defs : mfixpoint term) : typing_result (EAst.mfixpoint E.term) :=
      let Γ' := (PCUICLiftSubst.fix_context defs ++ Γ)%list in
      monad_map (fun d ⇒ H <- _ ;;
                   dbody' <- erase Γ' d.(dbody) H;;
                          ret ({| E.dname := d.(dname); E.rarg := d.(rarg);
                                  E.dbody := dbody' |})) defs.

  End EraseMfix.

  Equations(noind) erase (Γ : context) (t : term) (Ht : welltyped Σ Γ t) : typing_result E.term :=
    erase Γ t Ht with (is_erasable Σ HΣ Γ t Ht) :=
    {
      erase Γ _ Ht (Checked (left _)) := ret (E.tBox);
      erase Γ _ Ht (TypeError t) := TypeError t ;
      erase Γ (tRel i) Ht _ := ret (E.tRel i) ;
      erase Γ (tVar n) Ht _ := ret (E.tVar n) ;
      erase Γ (tEvar m l) Ht _ := l' <- monad_map (fun x ⇒ erase Γ x _) l;; ret (E.tEvar m l') ;
      erase Γ (tSort u) Ht _ := ret E.tBox

      ; erase Γ (tConst kn u) Ht _ := ret (E.tConst kn)
      ; erase Γ (tInd kn u) Ht _ := ret E.tBox
      ; erase Γ (tConstruct kn k u) Ht _ := ret (E.tConstruct kn k)
      ; erase Γ (tProd na b t) Ht _ := ret E.tBox
      ; erase Γ (tLambda na b t) Ht _ :=
                           t' <- erase (vass na b :: Γ) t _;;
                              ret (E.tLambda na t')
      ; erase Γ (tLetIn na b t0 t1) Ht _ :=
                              b' <- erase Γ b _;;
                                 t1' <- erase (vdef na b t0 :: Γ) t1 _;;
                                 ret (E.tLetIn na b' t1')
      ; erase Γ (tApp f u) Ht _ :=
                     f' <- erase Γ f _;;
                     l' <- erase Γ u _;;
                     ret (E.tApp f' l')
      ; erase Γ (tCase ip p c brs) Ht _ :=
          c' <- erase Γ c _;;
          if is_box c' then
            match brs with
            | (a, b) :: brs ⇒ b' <- erase Γ b _ ;; ret (E.mkApps b' (repeat E.tBox a))
            | [] ⇒ ret (E.tCase ip c' [])
            end
          else
            brs' <- monad_map (T :=typing_result) (fun x ⇒ x' <- erase Γ (snd x) _;; ret (fst x, x')) brs;;
            ret (E.tCase ip c' brs')
      ; erase Γ (tProj p c) Ht _ :=
          c' <- erase Γ c _;;
          if is_box c' then ret (E.tBox) else
          ret (E.tProj p c')
      ; erase Γ (tFix mfix n) Ht _ :=
          mfix' <- erase_mfix erase Γ mfix;;
          ret (E.tFix mfix' n)
      ; erase Γ (tCoFix mfix n) Ht _ :=
                          mfix' <- erase_mfix (erase) Γ mfix;;
                                ret (E.tCoFix mfix' n)
    }.

End Erase.

Lemma erases_erase (Σ : global_env_ext) Γ t T (wfΣ : ∥wf_ext Σ∥) t' :
  Σ ;;; Γ |- t : T →
                 ∀ (wt : welltyped Σ Γ t),
  erase Σ wfΣ Γ t wt = Checked t' →
  erases Σ Γ t t'.

Lemma erase_Some_typed {Σ wfΣ Γ t wft r} :
  erase Σ wfΣ Γ t wft = Checked r → ∃ T, ∥Σ ;;; Γ |- t : T∥.

Definition optM {M : Type → Type} `{Monad M} {A B} (x : option A) (f : A → M B) : M (option B) :=
  match x with
  | Some x ⇒ y <- f x ;; ret (Some y)
  | None ⇒ ret None
  end.

Lemma wf_local_nil {Σ} : ∥ wf_local Σ [] ∥.

Program Definition erase_constant_body Σ wfΣ (cb : constant_body)
  (Hcb : ∥ on_constant_decl (lift_typing typing) Σ cb ∥) : typing_result E.constant_body :=
  
  body <- match cb.(cst_body) with
          | Some b ⇒
            t <- (erase Σ wfΣ [] b _) ;;
            ret (Some t)
          | None ⇒ ret None
          end;;
  ret {| E.cst_body := body; |}.

Definition lift_opt_typing {A} (a : option A) (e : type_error) : typing_result A :=
  match a with
  | Some x ⇒ ret x
  | None ⇒ raise e
  end.


Program Definition erase_mutual_inductive_body Σ wfΣ
           (mib : mutual_inductive_body)
: typing_result E.mutual_inductive_body :=
  let bds := mib.(ind_bodies) in
  let arities := arities_context bds in
  bodies <- monad_map (erase_one_inductive_body Σ wfΣ mib.(ind_npars) arities) bds ;;
  ret {| E.ind_npars := mib.(ind_npars);
         E.ind_bodies := bodies; |}.

Program Fixpoint erase_global_decls Σ : ∥ wf Σ ∥ → typing_result E.global_declarations := fun wfΣ ⇒
  match Σ with
  | [] ⇒ ret []
  | ConstantDecl kn cb :: Σ ⇒
    cb' <- erase_constant_body (Σ, cst_universes cb) _ cb _;;
    Σ' <- erase_global_decls Σ _;;
    ret (E.ConstantDecl kn cb' :: Σ')
  | InductiveDecl kn mib :: Σ ⇒
    mib' <- erase_mutual_inductive_body (Σ, ind_universes mib) _ mib ;;
    Σ' <- erase_global_decls Σ _;;
    ret (E.InductiveDecl kn mib' :: Σ')
  end.


Program Definition erase_global Σ : ∥wf Σ∥ → _:=
  fun wfΣ ⇒
  Σ' <- erase_global_decls Σ wfΣ ;;
  ret Σ'.

Lemma erase_global_correct Σ (wfΣ : ∥ wf Σ∥) Σ' :
  erase_global Σ wfΣ = Checked Σ' →
  erases_global Σ Σ'.