Library MetaCoq.PCUIC.PCUICToTemplate

From Coq Require Import Uint63 FloatOps FloatAxioms.
From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICCases.
Set Warnings "-notation-overridden".
From MetaCoq.Template Require Import config utils AstUtils BasicAst Ast.
Set Warnings "+notation-overridden".

Definition uint63_from_model (i : uint63_model) : Uint63.int :=
  Uint63.of_Z (proj1_sig i).

Definition float64_from_model (f : float64_model) : PrimFloat.float :=
  FloatOps.SF2Prim (proj1_sig f).


Definition trans_predicate (t : PCUICAst.predicate Ast.term) : predicate Ast.term :=
  {| pparams := t.(PCUICAst.pparams);
     puinst := t.(PCUICAst.puinst);
     pcontext := forget_types t.(PCUICAst.pcontext);
     preturn := t.(PCUICAst.preturn) |}.

Definition trans_branch (t : PCUICAst.branch Ast.term) : branch Ast.term :=
  {| bcontext := forget_types t.(PCUICAst.bcontext);
     bbody := t.(PCUICAst.bbody) |}.

Fixpoint trans (t : PCUICAst.term) : Ast.term :=
  match t with
  | PCUICAst.tRel n ⇒ tRel n
  | PCUICAst.tVar n ⇒ tVar n
  | PCUICAst.tEvar ev args ⇒ tEvar ev (List.map trans args)
  | PCUICAst.tSort u ⇒ tSort u
  | PCUICAst.tConst c u ⇒ tConst c u
  | PCUICAst.tInd c u ⇒ tInd c u
  | PCUICAst.tConstruct c k u ⇒ tConstruct c k u
  | PCUICAst.tLambda na T M ⇒ tLambda na (trans T) (trans M)
  | PCUICAst.tApp u v ⇒ mkApp (trans u) (trans v)
  | PCUICAst.tProd na A B ⇒ tProd na (trans A) (trans B)
  | PCUICAst.tLetIn na b t b' ⇒ tLetIn na (trans b) (trans t) (trans b')
  | PCUICAst.tCase ind p c brs ⇒
    let p' := PCUICAst.map_predicate id trans trans (map_context trans) p in
    let brs' := List.map (PCUICAst.map_branch trans (map_context trans)) brs in
    tCase ind (trans_predicate p') (trans c) (map trans_branch brs')
  | PCUICAst.tProj p c ⇒ tProj p (trans c)
  | PCUICAst.tFix mfix idx ⇒
    let mfix' := List.map (map_def trans trans) mfix in
    tFix mfix' idx
  | PCUICAst.tCoFix mfix idx ⇒
    let mfix' := List.map (map_def trans trans) mfix in
    tCoFix mfix' idx
  
  end.

Notation trans_decl := (map_decl trans).

Definition trans_local Γ := List.map trans_decl Γ.

Definition trans_constructor_body (d : PCUICEnvironment.constructor_body) :=
  {| cstr_name := d.(PCUICEnvironment.cstr_name);
     cstr_args := trans_local d.(PCUICEnvironment.cstr_args);
     cstr_indices := map trans d.(PCUICEnvironment.cstr_indices);
     cstr_type := trans d.(PCUICEnvironment.cstr_type);
     cstr_arity := d.(PCUICEnvironment.cstr_arity) |}.

Definition trans_projection_body (d : PCUICEnvironment.projection_body) :=
 {| proj_name := d.(PCUICEnvironment.proj_name);
    proj_type := trans d.(PCUICEnvironment.proj_type);
    proj_relevance := d.(PCUICEnvironment.proj_relevance) |}.

Definition trans_one_ind_body (d : PCUICEnvironment.one_inductive_body) :=
  {| ind_name := d.(PCUICEnvironment.ind_name);
     ind_relevance := d.(PCUICEnvironment.ind_relevance);
     ind_indices := trans_local d.(PCUICEnvironment.ind_indices);
     ind_type := trans d.(PCUICEnvironment.ind_type);
     ind_sort := d.(PCUICEnvironment.ind_sort);
     ind_kelim := d.(PCUICEnvironment.ind_kelim);
     ind_ctors := List.map trans_constructor_body d.(PCUICEnvironment.ind_ctors);
     ind_projs := List.map trans_projection_body d.(PCUICEnvironment.ind_projs) |}.

Definition trans_constant_body bd :=
  {| cst_type := trans bd.(PCUICEnvironment.cst_type); cst_body := option_map trans bd.(PCUICEnvironment.cst_body);
     cst_universes := bd.(PCUICEnvironment.cst_universes);
     cst_relevance := bd.(PCUICEnvironment.cst_relevance) |}.

Definition trans_minductive_body md :=
  {| ind_finite := md.(PCUICEnvironment.ind_finite);
     ind_npars := md.(PCUICEnvironment.ind_npars);
     ind_params := trans_local md.(PCUICEnvironment.ind_params);
     ind_bodies := map trans_one_ind_body md.(PCUICEnvironment.ind_bodies);
     ind_universes := md.(PCUICEnvironment.ind_universes);
     ind_variance := md.(PCUICEnvironment.ind_variance)
  |}.

Definition trans_global_decl (d : PCUICEnvironment.global_decl) :=
  match d with
  | PCUICEnvironment.ConstantDecl bd ⇒ ConstantDecl (trans_constant_body bd)
  | PCUICEnvironment.InductiveDecl bd ⇒ InductiveDecl (trans_minductive_body bd)
  end.

Definition trans_global_decls (d : PCUICEnvironment.global_declarations) : global_declarations :=
  List.map (on_snd trans_global_decl) d.

Definition trans_global_env (d : PCUICEnvironment.global_env) : global_env :=
  {| universes := d.(PCUICEnvironment.universes);
     declarations := trans_global_decls d.(PCUICEnvironment.declarations) |}.

Definition trans_global (Σ : PCUICEnvironment.global_env_ext) : global_env_ext :=
  (trans_global_env (fst Σ), snd Σ).