From 11b40bf3da2da346692b74c99b7a24b6f6c247e9 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Wed, 11 Sep 2024 17:18:43 +0000 Subject: [PATCH] Use quotations for extract_as argument. --- .../fstar-lib/generated/FStar_Parser_Const.ml | 2 +- .../generated/FStar_TypeChecker_Normalize.ml | 19 +++++----- src/parser/FStar.Parser.Const.fst | 2 +- .../FStar.TypeChecker.Normalize.fst | 7 ++-- tests/extraction/ExtractAs.fst | 5 +-- ulib/FStar.ExtractAs.fst | 35 +++++++++++++++++++ ulib/FStar.Pervasives.fst | 2 -- ulib/FStar.Pervasives.fsti | 14 -------- 8 files changed, 54 insertions(+), 32 deletions(-) create mode 100644 ulib/FStar.ExtractAs.fst diff --git a/ocaml/fstar-lib/generated/FStar_Parser_Const.ml b/ocaml/fstar-lib/generated/FStar_Parser_Const.ml index defe0ee7e2c..0da50e28456 100644 --- a/ocaml/fstar-lib/generated/FStar_Parser_Const.ml +++ b/ocaml/fstar-lib/generated/FStar_Parser_Const.ml @@ -662,6 +662,6 @@ let (document_lid : FStar_Ident.lident) = p2l ["FStar"; "Stubs"; "Pprint"; "document"] let (issue_lid : FStar_Ident.lident) = p2l ["FStar"; "Issue"; "issue"] let (extract_as_lid : FStar_Ident.lident) = - p2l ["FStar"; "Pervasives"; "extract_as"] + p2l ["FStar"; "ExtractAs"; "extract_as"] let (extract_as_impure_effect_lid : FStar_Ident.lident) = p2l ["FStar"; "Pervasives"; "extract_as_impure_effect"] \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml index 5ef1da8d471..bec50745032 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml @@ -2077,16 +2077,17 @@ let (is_extract_as_attr : uu___3.FStar_Syntax_Syntax.n in (uu___2, args) in (match uu___1 with - | (FStar_Syntax_Syntax.Tm_uinst - ({ FStar_Syntax_Syntax.n = FStar_Syntax_Syntax.Tm_fvar fv; - FStar_Syntax_Syntax.pos = uu___2; - FStar_Syntax_Syntax.vars = uu___3; - FStar_Syntax_Syntax.hash_code = uu___4;_}, - u::[]), - uu___5::(t, uu___6)::[]) when + | (FStar_Syntax_Syntax.Tm_fvar fv, (t, uu___2)::[]) when FStar_Syntax_Syntax.fv_eq_lid fv FStar_Parser_Const.extract_as_lid - -> FStar_Pervasives_Native.Some t + -> + let uu___3 = + let uu___4 = FStar_Syntax_Subst.compress t in + uu___4.FStar_Syntax_Syntax.n in + (match uu___3 with + | FStar_Syntax_Syntax.Tm_quoted (impl, uu___4) -> + FStar_Pervasives_Native.Some impl + | uu___4 -> FStar_Pervasives_Native.None) | uu___2 -> FStar_Pervasives_Native.None) let (has_extract_as_attr : FStar_TypeChecker_Env.env -> @@ -9214,7 +9215,7 @@ let (get_n_binders : FStar_Syntax_Syntax.term -> (FStar_Syntax_Syntax.binder Prims.list * FStar_Syntax_Syntax.comp)) = fun env1 -> fun n -> fun t -> get_n_binders' env1 [] n t -let (uu___3497 : unit) = +let (uu___3496 : unit) = FStar_Compiler_Effect.op_Colon_Equals __get_n_binders get_n_binders' let (maybe_unfold_head_fv : FStar_TypeChecker_Env.env -> diff --git a/src/parser/FStar.Parser.Const.fst b/src/parser/FStar.Parser.Const.fst index cd393c8e02b..78b759519c3 100644 --- a/src/parser/FStar.Parser.Const.fst +++ b/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"] diff --git a/src/typechecker/FStar.TypeChecker.Normalize.fst b/src/typechecker/FStar.TypeChecker.Normalize.fst index 44f488eda83..b277bffa941 100644 --- a/src/typechecker/FStar.TypeChecker.Normalize.fst +++ b/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 = diff --git a/tests/extraction/ExtractAs.fst b/tests/extraction/ExtractAs.fst index 5df61055da8..0b39d8a1e0e 100644 --- a/tests/extraction/ExtractAs.fst +++ b/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 diff --git a/ulib/FStar.ExtractAs.fst b/ulib/FStar.ExtractAs.fst new file mode 100644 index 00000000000..9e5996bc959 --- /dev/null +++ b/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) = () diff --git a/ulib/FStar.Pervasives.fst b/ulib/FStar.Pervasives.fst index 86a91a47232..42987e0cdc6 100644 --- a/ulib/FStar.Pervasives.fst +++ b/ulib/FStar.Pervasives.fst @@ -185,8 +185,6 @@ let primitive_extraction = () let extract_as_impure_effect = () -let extract_as _ = () - let strictly_positive = () let unused = () diff --git a/ulib/FStar.Pervasives.fsti b/ulib/FStar.Pervasives.fsti index 8d6459e1b8f..6bb8b1076a3 100644 --- a/ulib/FStar.Pervasives.fsti +++ b/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