Use quotations for extract_as argument.

src/parser/FStar.Parser.Const.fst

@@ -598,5 +598,5 @@ let tref_lid        = p2l ["FStar"; "Stubs"; "Tactics"; "Types"; "tref"]
 let document_lid = p2l ["FStar"; "Stubs"; "Pprint"; "document"]
 let issue_lid = p2l ["FStar"; "Issue"; "issue"]
 
-let extract_as_lid = p2l ["FStar"; "Pervasives"; "extract_as"]
+let extract_as_lid = p2l ["FStar"; "ExtractAs"; "extract_as"]
 let extract_as_impure_effect_lid = p2l ["FStar"; "Pervasives"; "extract_as_impure_effect"]

src/typechecker/FStar.TypeChecker.Normalize.fst

@@ -866,9 +866,10 @@ let is_forall_const cfg (phi : term) : option term =
 let is_extract_as_attr (attr: attribute) : option term =
   let head, args = head_and_args attr in
   match (Subst.compress head).n, args with
-  | Tm_uinst({n=Tm_fvar fv}, [u]), [_; (t, _)]
-        when Syntax.fv_eq_lid fv PC.extract_as_lid ->
-      Some t
+  | Tm_fvar fv, [t, _] when Syntax.fv_eq_lid fv PC.extract_as_lid ->
+    (match (Subst.compress t).n with
+    | Tm_quoted(impl, _) -> Some impl
+    | _ -> None)
   | _ -> None
 
 let has_extract_as_attr (g: Env.env) (lid: I.lid) : option term =

tests/extraction/ExtractAs.fst

@@ -1,16 +1,17 @@
 module ExtractAs
+open FStar.ExtractAs
 let fail_unless (b: bool) = if b then "ok" else magic ()
 
 // Test that extract_as works when extracting the definition itself.
 
-[@@extract_as (fun x -> x + 10)]
+[@@extract_as (`(fun (x: nat) -> x + 10))]
 let frob y = 2 + y
 
 let _ = fail_unless (frob 1 = 11)
 
 // Test that extract_as works when inlining the definition.
 
-inline_for_extraction noextract [@@extract_as (fun x -> x + 10)]
+inline_for_extraction noextract [@@extract_as (`(fun (x: nat) -> x + 10))]
 let bar_2 y = 2 + y
 let bar z = bar_2 z
 

ulib/FStar.ExtractAs.fst

@@ -0,0 +1,35 @@
+(*
+   Copyright 2024 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+
+module FStar.ExtractAs
+open FStar.Stubs.Reflection.Types
+
+(** Replaces the annotated definition
+    by the specified implementation during extraction.
+    There are no checks whether the implementation
+    has the same semantics, or even the same type.
+
+    For example, if you have:
+
+    [@@extract_as (`(fun (x: nat) -> "not a number"))]
+    let add_one (x: nat) : nat = x + 42
+
+    Then `add_one` will extract to `let add_one x = "not a number"`,
+    and most likely cause the extracted program to crash.
+
+    Note that the argument needs to be a literal quotation.
+ *)
+let extract_as (impl: term) = ()

ulib/FStar.Pervasives.fst

@@ -185,8 +185,6 @@ let primitive_extraction = ()
 
 let extract_as_impure_effect = ()
 
-let extract_as _ = ()
-
 let strictly_positive = ()
 
 let unused = ()

ulib/FStar.Pervasives.fsti

@@ -1146,20 +1146,6 @@ val primitive_extraction : unit
  *)
 val extract_as_impure_effect : unit
 
-(** Replaces the annotated definition
-    by the specified implementation during extraction.
-    There are no checks whether the implementation
-    has the same semantics, or even the same type.
-
-    For example, if you have:
-
-    [@@extract_as (fun (x: nat) -> "not a number")]
-    let add_one (x: nat) : nat = x + 42
-
-    Then `add_one` will extract to `let add_one x = "not a number"`,
-    and most likely cause the extracted program to crash.
- *)
-val extract_as (#t: Type u#a) (impl: t) : unit
 
 (** A binder in a definition/declaration may optionally be annotated as strictly_positive
     When the let definition is used in a data constructor type in an inductive