From b887b0f598068380f99cdd383ad5812ed52339c0 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 26 Sep 2024 14:30:52 -0700 Subject: [PATCH] Comment on extract_as being recursive. --- src/extraction/FStar.Extraction.ML.Modul.fst | 2 ++ ulib/FStar.ExtractAs.fst | 2 ++ 2 files changed, 4 insertions(+) diff --git a/src/extraction/FStar.Extraction.ML.Modul.fst b/src/extraction/FStar.Extraction.ML.Modul.fst index 8554a846f6d..bda2a1dce32 100644 --- a/src/extraction/FStar.Extraction.ML.Modul.fst +++ b/src/extraction/FStar.Extraction.ML.Modul.fst @@ -756,6 +756,8 @@ let mark_sigelt_erased (se:sigelt) (g:uenv) : uenv = let fixup_sigelt_extract_as se = match se.sigel, find_map se.sigattrs N.is_extract_as_attr with | Sig_let {lids; lbs=(_, [lb])}, Some impl -> + // The specified implementation can be recursive, + // to be on the safe side we always mark the replaced sigelt as recursive. {se with sigel = Sig_let {lids; lbs=(true, [{lb with lbdef = impl}])}} | _ -> se diff --git a/ulib/FStar.ExtractAs.fst b/ulib/FStar.ExtractAs.fst index 9e5996bc959..11a785dafac 100644 --- a/ulib/FStar.ExtractAs.fst +++ b/ulib/FStar.ExtractAs.fst @@ -31,5 +31,7 @@ open FStar.Stubs.Reflection.Types and most likely cause the extracted program to crash. Note that the argument needs to be a literal quotation. + The implementation can be recursive, + but then you need to construct the attribute via a tactic. *) let extract_as (impl: term) = ()