Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Typed extraction integration #1030

Merged
merged 7 commits into from
Dec 13, 2023
Merged

Typed extraction integration #1030

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
5e9ae4f
Adapted extraction correctness, only remaining wf_glob proofs
mattam82 Nov 27, 2023
e60bf4d
WIP on wellformedness proof
mattam82 Nov 28, 2023
40d2284
Finished proof of correctness for typed erasure
mattam82 Nov 28, 2023
f7918c3
Generalized theorems for typed optimization
mattam82 Dec 5, 2023
c2620bb
Typed erasure variant
mattam82 Dec 7, 2023
ea4ab2d
Prove that dearging preserves eta-expanded constructors and fixpoints…
mattam82 Dec 12, 2023
f1a445b
Finish the proof of preservation of eta-expansion by dearging
mattam82 Dec 13, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 27 additions & 2 deletions erasure-plugin/_PluginProject.in
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,11 @@ src/wGraph.ml
src/wGraph.mli
src/etaExpand.mli
src/etaExpand.ml
src/utils.mli
src/utils.ml

src/resultMonad.mli
src/resultMonad.ml

# From PCUIC
src/pCUICPrimitive.mli
Expand Down Expand Up @@ -79,6 +84,24 @@ src/eSpineView.ml
src/eRemoveParams.mli
src/eRemoveParams.ml

# Typed erasure
src/exAst.mli
src/exAst.ml
src/optimize.mli
src/optimize.ml
src/vectorDef.mli
src/vectorDef.ml
src/vector.mli
src/vector.ml
src/fin.mli
src/fin.ml
src/extractionCorrectness.mli
src/extractionCorrectness.ml
src/optimizeCorrectness.mli
src/optimizeCorrectness.ml
src/erasure.mli
src/erasure.ml

src/erasureFunction.mli
src/erasureFunction.ml
src/erasureFunctionProperties.mli
Expand All @@ -87,6 +110,8 @@ src/ePretty.mli
src/ePretty.ml
src/eOptimizePropDiscr.mli
src/eOptimizePropDiscr.ml
src/optimizePropDiscr.mli
src/optimizePropDiscr.ml
src/eProgram.mli
src/eProgram.ml
src/eInlineProjections.mli
Expand All @@ -95,8 +120,8 @@ src/eConstructorsAsBlocks.mli
src/eConstructorsAsBlocks.ml
src/eTransform.mli
src/eTransform.ml
src/erasure.mli
src/erasure.ml
src/erasure0.mli
src/erasure0.ml

src/g_metacoq_erasure.mlg
src/metacoq_erasure_plugin.mlpack
Expand Down
21 changes: 18 additions & 3 deletions erasure-plugin/src/g_metacoq_erasure.mlg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,12 +25,15 @@ let pr_char_list l =
(* We allow utf8 encoding *)
str (Caml_bytestring.caml_string_of_bytestring l)

let check ~bypass ~fast env evm c =
let check ~bypass ~fast ?(with_types=false) env evm c =
debug (fun () -> str"Quoting");
let term = time (str"Quoting") (Ast_quoter.quote_term_rec ~bypass env evm) (EConstr.to_constr evm c) in
let erase = time (str"Erasure")
(if fast then Erasure.erase_fast_and_print_template_program
else Erasure.erase_and_print_template_program)
(if fast then Erasure0.erase_fast_and_print_template_program
else
if with_types then
Erasure0.typed_erase_and_print_template_program
else Erasure0.erase_and_print_template_program)
term
in
Feedback.msg_info (pr_char_list erase)
Expand All @@ -43,6 +46,18 @@ VERNAC COMMAND EXTEND MetaCoqErase CLASSIFIED AS QUERY
let (c, _) = Constrintern.interp_constr env evm c in
check ~bypass:true ~fast:false env evm c
}
| [ "MetaCoq" "Bypass" "Typed" "Erase" constr(c) ] -> {
let env = Global.env () in
let evm = Evd.from_env env in
let (c, _) = Constrintern.interp_constr env evm c in
check ~bypass:true ~fast:false ~with_types:true env evm c
}
| [ "MetaCoq" "Typed" "Erase" constr(c) ] -> {
let env = Global.env () in
let evm = Evd.from_env env in
let (c, _) = Constrintern.interp_constr env evm c in
check ~bypass:false ~fast:false ~with_types:true env evm c
}
| [ "MetaCoq" "Erase" constr(c) ] -> {
let env = Global.env () in
let evm = Evd.from_env env in
Expand Down
17 changes: 15 additions & 2 deletions erasure-plugin/src/metacoq_erasure_plugin.mlpack
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,12 +2,17 @@ MSetWeakList
EqdepFacts
Ssrbool

Utils
Fin
Vector
VectorDef

Utils
ResultMonad
WGraph
UGraph0
EtaExpand


WcbvEval
Classes0
Logic1
Expand Down Expand Up @@ -60,7 +65,15 @@ EOptimizePropDiscr
EInlineProjections
EConstructorsAsBlocks
EProgram
ETransform
OptimizePropDiscr

ExAst
Optimize
OptimizeCorrectness
Erasure
ExtractionCorrectness

ETransform
Erasure0

G_metacoq_erasure
Loading