Library MetaCoq.Erasure.SafeTemplateErasure
Program Definition erase_template_program_check (p : Ast.program)
: EnvCheck (EAst.global_context × EAst.term) :=
let Σ := List.rev (trans_global (AstUtils.empty_ext p.1)).1 in
G <- check_wf_env Σ ;;
Σ' <- wrap_error "erasure of the global context" (erase_global Σ _) ;;
t <- wrap_error ("During erasure of " ++ string_of_term (trans p.2)) (erase (empty_ext Σ) _ nil _ (trans p.2));;
ret (Monad:=envcheck_monad) (Σ', t).
This is a hack to avoid having to handle template polymorphism and make
erasure fast: we actually admit the proof of wf Σ and never build it.
Definition assume_wf_decl {cf : checker_flags} (Σ : global_env_ext) :
∥ wf Σ ∥ →
∥ on_udecl Σ.1 Σ.2 ∥ →
∀ G : universes_graph,
is_graph_of_uctx G (global_ext_uctx Σ) →
∀ d : global_decl, EnvCheck (∥ on_global_decl (lift_typing typing) Σ d ∥).
Program Fixpoint check_wf_env_only_univs (Σ : global_env)
: EnvCheck (∑ G, (is_graph_of_uctx G (global_uctx Σ) ∧ ∥ wf Σ ∥)) :=
match Σ with
| nil ⇒ ret (init_graph; _)
| d :: Σ ⇒
G <- check_wf_env_only_univs Σ ;;
check_fresh (PCUICTyping.global_decl_ident d) Σ ;;
let udecl := universes_decl_of_decl d in
uctx <- check_udecl (PCUICTyping.global_decl_ident d) Σ _ G.π1 (proj1 G.π2) udecl ;;
let G' := add_uctx uctx.π1 G.π1 in
assume_wf_decl (Σ, udecl) _ _ G' _ d ;;
match udecl with
| Monomorphic_ctx _ ⇒ ret (G'; _)
| Polymorphic_ctx _ ⇒ ret (G.π1; _)
| Cumulative_ctx _ ⇒ ret (G.π1; _)
end
end.
Program Definition erase_template_program (p : Ast.program)
: EnvCheck (EAst.global_context × EAst.term) :=
let Σ := List.rev (trans_global (AstUtils.empty_ext p.1)).1 in
G <- check_wf_env_only_univs Σ ;;
Σ' <- wrap_error "erasure of the global context" (SafeErasureFunction.erase_global Σ _) ;;
t <- wrap_error ("During erasure of " ++ string_of_term (trans p.2)) (SafeErasureFunction.erase (empty_ext Σ) _ nil (trans p.2) _);;
ret (Monad:=envcheck_monad) (Σ', t).
This uses the checker-based erasure
Program Definition erase_and_print_template_program_check {cf : checker_flags} (p : Ast.program)
: string + string :=
let p := fix_program_universes p in
match erase_template_program_check p return string + string with
| CorrectDecl (Σ', t) ⇒
inl ("Environment is well-formed and " ++ Pretty.print_term (AstUtils.empty_ext p.1) [] true p.2 ++
" erases to: " ++ nl ++ EPretty.print_term Σ' [] true false t)
| EnvError (AlreadyDeclared id) ⇒
inr ("Already declared: " ++ id)
| EnvError (IllFormedDecl id e) ⇒
inr ("Type error: " ++ PCUICSafeChecker.string_of_type_error e ++ ", while checking " ++ id)
end.
: string + string :=
let p := fix_program_universes p in
match erase_template_program_check p return string + string with
| CorrectDecl (Σ', t) ⇒
inl ("Environment is well-formed and " ++ Pretty.print_term (AstUtils.empty_ext p.1) [] true p.2 ++
" erases to: " ++ nl ++ EPretty.print_term Σ' [] true false t)
| EnvError (AlreadyDeclared id) ⇒
inr ("Already declared: " ++ id)
| EnvError (IllFormedDecl id e) ⇒
inr ("Type error: " ++ PCUICSafeChecker.string_of_type_error e ++ ", while checking " ++ id)
end.
This uses the retyping-based erasure
Program Definition erase_and_print_template_program {cf : checker_flags} (p : Ast.program)
: string + string :=
let p := fix_program_universes p in
match erase_template_program p return string + string with
| CorrectDecl (Σ', t) ⇒
inl ("Environment is well-formed and " ++ Pretty.print_term (AstUtils.empty_ext p.1) [] true p.2 ++
" erases to: " ++ nl ++ EPretty.print_term Σ' [] true false t)
| EnvError (AlreadyDeclared id) ⇒
inr ("Already declared: " ++ id)
| EnvError (IllFormedDecl id e) ⇒
inr ("Type error: " ++ PCUICSafeChecker.string_of_type_error e ++ ", while checking " ++ id)
end.
: string + string :=
let p := fix_program_universes p in
match erase_template_program p return string + string with
| CorrectDecl (Σ', t) ⇒
inl ("Environment is well-formed and " ++ Pretty.print_term (AstUtils.empty_ext p.1) [] true p.2 ++
" erases to: " ++ nl ++ EPretty.print_term Σ' [] true false t)
| EnvError (AlreadyDeclared id) ⇒
inr ("Already declared: " ++ id)
| EnvError (IllFormedDecl id e) ⇒
inr ("Type error: " ++ PCUICSafeChecker.string_of_type_error e ++ ", while checking " ++ id)
end.