Typed erasure variant

MetaCoq · Dec 7, 2023 · c2620bb · c2620bb
1 parent f7918c3
commit c2620bb
Show file tree

Hide file tree

Showing 9 changed files with 602 additions and 103 deletions.
diff --git a/erasure-plugin/_PluginProject.in b/erasure-plugin/_PluginProject.in
@@ -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
@@ -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
@@ -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
@@ -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

diff --git a/erasure-plugin/src/g_metacoq_erasure.mlg b/erasure-plugin/src/g_metacoq_erasure.mlg
@@ -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)
@@ -43,6 +46,12 @@ 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" "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" "Erase" constr(c) ] -> {
     let env = Global.env () in
     let evm = Evd.from_env env in

diff --git a/erasure-plugin/src/metacoq_erasure_plugin.mlpack b/erasure-plugin/src/metacoq_erasure_plugin.mlpack
@@ -2,12 +2,17 @@ MSetWeakList
 EqdepFacts
 Ssrbool
 
-Utils
+Fin
+Vector
+VectorDef
 
+Utils
+ResultMonad
 WGraph
 UGraph0
 EtaExpand
 
+
 WcbvEval
 Classes0
 Logic1
@@ -60,7 +65,15 @@ EOptimizePropDiscr
 EInlineProjections
 EConstructorsAsBlocks
 EProgram
-ETransform
+OptimizePropDiscr
+
+ExAst
+Optimize
+OptimizeCorrectness
 Erasure
+ExtractionCorrectness
+
+ETransform
+Erasure0
 
 G_metacoq_erasure