Library MetaCoq.Erasure.ErasureFunction

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.





Lemma mkApps_tFix_inv t mfix n L :
  t = mkApps (tFix mfix n) L →
  (∑ a b, t = tApp a b) + ((t = tFix mfix n) × (L = [])).

Notation err := (TypeError (Msg "hnf did not return normal form")).
Program Fixpoint normal_dec Γ t : typing_result (∀ t', red1 Σ Γ t t' → False) :=
  match t with
  | tRel n ⇒ match option_map decl_body (nth_error Γ n) with
               Some (Some body) ⇒ err
             | _ ⇒ ret _
             end
  | tVar n ⇒ ret _
  | tSort u ⇒ ret _
  | tProd na A B ⇒ H1 <- normal_dec Γ A ;;
                      H2 <- normal_dec (Γ,, vass na A) B;;
                      ret _
  | tLambda na A B ⇒ H1 <- normal_dec Γ A ;;
                      H2 <- normal_dec (Γ,, vass na A) B;;
                      ret _
  | tLetIn _ _ _ _ ⇒ err
  | tConst c u ⇒ match lookup_env Σ c with Some (ConstantDecl _ (Build_constant_body _ (Some _) _)) ⇒ err
                                       | _ ⇒ ret _
                 end
  | tInd _ _ ⇒ ret _
  | tConstruct _ _ _ ⇒ ret _
  | tCase _ _ _ _ ⇒ err
  | tProj _ _ ⇒ err
  
  
  | _ ⇒ TypeError (Msg "not implemented")
  end.
Solve All Obligations with firstorder congruence.

Inductive red' (Σ : global_env) (Γ : context) : term → term → Type :=
  refl_red' M : red' Σ Γ M M
| trans_red' : ∀ M P N : term, red1 Σ Γ M P → red' Σ Γ P N → red' Σ Γ M N.

Instance red'_transitive Γ : CRelationClasses.Transitive (red' Σ Γ).

Lemma red_red' Γ t t' : red Σ Γ t t' → red' Σ Γ t t'.

Program Definition reduce_to_sort' Γ t (h : wellformed Σ Γ t)
  : typing_result ((∑ u, ∥ red (fst Σ) Γ t (tSort u) ∥) + ((∑ u, ∥ red (fst Σ) Γ t (tSort u) ∥) → False)) :=
  match t with
  | tSort u ⇒ ret (inl (u; sq (refl_red _ _ _)))
  | _ ⇒
    match hnf HΣ Γ t h with
    | tSort u ⇒ ret (inl (u; _))
    | t' ⇒ match normal_dec Γ t' with Checked H ⇒ ret (inr _) | TypeError t ⇒ TypeError t end
    end
  end.

Program Definition reduce_to_prod' Γ t (h : wellformed Σ Γ t)
  : typing_result ((∑ na a b, ∥ red (fst Σ) Γ t (tProd na a b) ∥) + ((∑ na a b, ∥ red (fst Σ) Γ t (tProd na a b) ∥) → False)) :=
  match t with
  | tProd na a b ⇒ ret (inl (na; a; b; sq (refl_red _ _ _)))
  | _ ⇒
    match hnf HΣ Γ t h with
    | tProd na a b ⇒ ret (inl (na; a; b; _))
    | t' ⇒ match normal_dec Γ t' with Checked H ⇒ ret (inr _) | _ ⇒ TypeError (Msg "hnf did not return normal form") end
    end
  end.

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' Γ T HT) ⇒ {
    | Checked (inl H) ⇒ ret (left _) ;
    | Checked (inr Hs) with inspect (@reduce_to_prod' Γ T _) ⇒ {
      | exist (Checked (inl (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 (Checked (inr _)) He ⇒ ret (right _);
      | exist (TypeError t) He ⇒ TypeError t } ;
    | TypeError t ⇒ 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) (HΓ : ∥wf_local Sigma Gamma∥) (t : PCUICAst.term) :
  typing_result ({∥isErasable Sigma Gamma t∥} +{∥(isErasable Sigma Gamma t → False) × welltyped Sigma Gamma t∥}) :=
  mlet (T; _) <- @make_graph_and_infer _ _ HΣ Gamma HΓ t ;;
  mlet b <- is_arity Sigma _ Gamma _ T _ ;;
  if b : {_} + {_} then
    ret (left _)
  else mlet (K; _) <- @make_graph_and_infer _ _ HΣ Gamma HΓ 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) (HΓ : ∥ wf_local Σ Γ ∥) (t : term), typing_result E.term).

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

  End EraseMfix.

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

      ; erase Γ HΓ (tConst kn u) _ := ret (E.tConst kn)
      ; erase Γ HΓ (tInd kn u) _ := ret E.tBox
      ; erase Γ HΓ (tConstruct kn k u) _ := ret (E.tConstruct kn k)
      ; erase Γ HΓ (tProd na b t) _ := ret E.tBox
      ; erase Γ HΓ (tLambda na b t) _ :=
                           t' <- erase (vass na b :: Γ) _ t;;
                              ret (E.tLambda na t')
      ; erase Γ HΓ (tLetIn na b t0 t1) _ :=
                              b' <- erase Γ HΓ b;;
                                 t1' <- erase (vdef na b t0 :: Γ) _ t1;;
                                 ret (E.tLetIn na b' t1')
      ; erase Γ HΓ (tApp f u) _ :=
                     f' <- erase Γ HΓ f;;
                        l' <- erase Γ HΓ u;;
                        ret (E.tApp f' l')
      ; erase Γ HΓ (tCase ip p c brs) _ :=
                             c' <- erase Γ HΓ c;;
                                brs' <- monad_map (T :=typing_result) (fun x ⇒ x' <- erase Γ HΓ (snd x);; ret (fst x, x')) brs;;
                                ret (E.tCase ip c' brs')
      ; erase Γ HΓ (tProj p c) _ :=
                      c' <- erase Γ HΓ c;;
                         ret (E.tProj p c')
      ; erase Γ HΓ (tFix mfix n) _ :=
                        mfix' <- erase_mfix (erase) Γ HΓ mfix;;
                              ret (E.tFix mfix' n)
      ; erase Γ HΓ (tCoFix mfix n) _ :=
                          mfix' <- erase_mfix (erase) Γ HΓ mfix;;
                                ret (E.tCoFix mfix' n)
    }.

End Erase.


Lemma erases_erase (Σ : global_env_ext) Γ t T (wfΣ : ∥wf_ext Σ∥) (wfΓ : ∥wf_local Σ Γ∥) t' :
  Σ ;;; Γ |- t : T →
  erase Σ (wfΣ) Γ (wfΓ) t = Checked t' →
  erases Σ Γ t t'.
Print Assumptions erases_erase.

Lemma erase_Some_typed {Σ wfΣ Γ wfΓ t r} :
  erase Σ wfΣ Γ wfΓ t = 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 Σ [] ∥.

Definition erase_constant_body Σ wfΣ (cb : constant_body) : typing_result E.constant_body :=
  ty <- erase Σ wfΣ [] wf_local_nil cb.(cst_type) ;;
  body <- optM cb.(cst_body) (fun b ⇒ erase Σ wfΣ [] wf_local_nil b);;
  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.

Definition erase_one_inductive_body Σ wfΣ npars arities Har
           (oib : one_inductive_body) : typing_result E.one_inductive_body :=
  decty <- lift_opt_typing (decompose_prod_n_assum [] npars oib.(ind_type))
        (NotAnInductive oib.(ind_type)) ;;
  let '(params, arity) := decty in
  type <- erase Σ wfΣ [] wf_local_nil oib.(ind_type) ;;
  ctors <- monad_map (fun '(x, y, z) ⇒ y' <- erase Σ wfΣ arities Har y;; ret (x, y', z)) oib.(ind_ctors);;
  let projctx := arities ,,, params ,, vass nAnon oib.(ind_type) in
  projs <- monad_map (fun '(x, y) ⇒ y' <- erase Σ wfΣ [] wf_local_nil y;; ret (x, y')) oib.(ind_projs);;
  ret {| E.ind_name := oib.(ind_name);
         E.ind_kelim := oib.(ind_kelim);
         E.ind_ctors := ctors;
         E.ind_projs := projs |}.

Program Definition erase_mutual_inductive_body Σ wfΣ
           (mib : mutual_inductive_body) (Hm : ∥ wf_local Σ (arities_context (ind_bodies mib)) ∥)
: 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 Σ Σ'.