diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml index fa9abccbd33..ec7e26e1722 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml @@ -643,22 +643,40 @@ let (head_and_args : { FStar_Syntax_Syntax.hd = head; FStar_Syntax_Syntax.args = args;_} -> (head, args) | uu___ -> (t1, []) -let rec (head_and_args_full : +let rec (__head_and_args_full : + Prims.bool -> + FStar_Syntax_Syntax.term -> + (FStar_Syntax_Syntax.term * (FStar_Syntax_Syntax.term' + FStar_Syntax_Syntax.syntax * FStar_Syntax_Syntax.arg_qualifier + FStar_Pervasives_Native.option) Prims.list)) + = + fun unmeta1 -> + fun t -> + let t1 = FStar_Syntax_Subst.compress t in + match t1.FStar_Syntax_Syntax.n with + | FStar_Syntax_Syntax.Tm_app + { FStar_Syntax_Syntax.hd = head; FStar_Syntax_Syntax.args = args;_} + -> + let uu___ = __head_and_args_full unmeta1 head in + (match uu___ with + | (head1, args') -> + (head1, (FStar_Compiler_List.op_At args' args))) + | FStar_Syntax_Syntax.Tm_meta + { FStar_Syntax_Syntax.tm2 = tm; FStar_Syntax_Syntax.meta = uu___;_} + when unmeta1 -> __head_and_args_full unmeta1 tm + | uu___ -> (t1, []) +let (head_and_args_full : FStar_Syntax_Syntax.term -> (FStar_Syntax_Syntax.term * (FStar_Syntax_Syntax.term' FStar_Syntax_Syntax.syntax * FStar_Syntax_Syntax.arg_qualifier FStar_Pervasives_Native.option) Prims.list)) - = - fun t -> - let t1 = FStar_Syntax_Subst.compress t in - match t1.FStar_Syntax_Syntax.n with - | FStar_Syntax_Syntax.Tm_app - { FStar_Syntax_Syntax.hd = head; FStar_Syntax_Syntax.args = args;_} - -> - let uu___ = head_and_args_full head in - (match uu___ with - | (head1, args') -> (head1, (FStar_Compiler_List.op_At args' args))) - | uu___ -> (t1, []) + = fun t -> __head_and_args_full false t +let (head_and_args_full_unmeta : + FStar_Syntax_Syntax.term -> + (FStar_Syntax_Syntax.term * (FStar_Syntax_Syntax.term' + FStar_Syntax_Syntax.syntax * FStar_Syntax_Syntax.arg_qualifier + FStar_Pervasives_Native.option) Prims.list)) + = fun t -> __head_and_args_full true t let rec (leftmost_head : FStar_Syntax_Syntax.term -> FStar_Syntax_Syntax.term) = fun t -> diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml index 2c93cae52fd..2dd6a14bf19 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml @@ -694,11 +694,13 @@ let (reduce_primops : (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.primops then (tm, false) else - (let uu___1 = FStar_Syntax_Util.head_and_args tm in + (let uu___1 = FStar_Syntax_Util.head_and_args_full tm in match uu___1 with | (head, args) -> let uu___2 = - let head1 = FStar_Syntax_Subst.compress head in + let head1 = + let uu___3 = FStar_Syntax_Util.unmeta head in + FStar_Syntax_Subst.compress uu___3 in match head1.FStar_Syntax_Syntax.n with | FStar_Syntax_Syntax.Tm_uinst (fv, us) -> (fv, us) | uu___3 -> (head1, []) in @@ -6782,7 +6784,7 @@ and (do_rebuild : | FStar_Syntax_Syntax.Tm_app uu___1 when (cfg.FStar_TypeChecker_Cfg.steps).FStar_TypeChecker_Cfg.primops -> - let uu___2 = FStar_Syntax_Util.head_and_args t in + let uu___2 = FStar_Syntax_Util.head_and_args_full_unmeta t in (match uu___2 with | (hd, args) -> let uu___3 = diff --git a/src/syntax/FStar.Syntax.Util.fst b/src/syntax/FStar.Syntax.Util.fst index 6bf7b0f5bb6..f9bfde503f6 100644 --- a/src/syntax/FStar.Syntax.Util.fst +++ b/src/syntax/FStar.Syntax.Util.fst @@ -356,14 +356,19 @@ let head_and_args t = | Tm_app {hd=head; args} -> head, args | _ -> t, [] -let rec head_and_args_full t = +let rec __head_and_args_full unmeta t = let t = compress t in match t.n with | Tm_app {hd=head; args} -> - let (head, args') = head_and_args_full head + let (head, args') = __head_and_args_full unmeta head in (head, args'@args) + | Tm_meta {tm} when unmeta -> + __head_and_args_full unmeta tm | _ -> t, [] +let head_and_args_full t = __head_and_args_full false t +let head_and_args_full_unmeta t = __head_and_args_full true t + let rec leftmost_head t = let t = compress t in match t.n with diff --git a/src/typechecker/FStar.TypeChecker.Normalize.fst b/src/typechecker/FStar.TypeChecker.Normalize.fst index c3e0dcbf96a..96bcf042723 100644 --- a/src/typechecker/FStar.TypeChecker.Normalize.fst +++ b/src/typechecker/FStar.TypeChecker.Normalize.fst @@ -381,9 +381,9 @@ let reduce_primops norm_cb cfg (env:env) tm : term & bool = if not cfg.steps.primops then tm, false else begin - let head, args = U.head_and_args tm in + let head, args = U.head_and_args_full tm in let head_term, universes = - let head = SS.compress head in + let head = SS.compress (U.unmeta head) in match head.n with | Tm_uinst(fv, us) -> fv, us | _ -> head, [] @@ -2429,7 +2429,7 @@ and do_rebuild (cfg:cfg) (env:env) (stack:stack) (t:term) : term = norm cfg env stack' e | Tm_app _ when cfg.steps.primops -> - let hd, args = U.head_and_args t in + let hd, args = U.head_and_args_full_unmeta t in (match (U.un_uinst hd).n with | Tm_fvar fv -> begin diff --git a/tests/tactics/PluginReturned.fst b/tests/tactics/PluginReturned.fst new file mode 100644 index 00000000000..c5f45eface5 --- /dev/null +++ b/tests/tactics/PluginReturned.fst @@ -0,0 +1,31 @@ +module PluginReturned + +open FStar.Tactics.V2 + +(* This used to trip the normalizer due to an extra Meta_monadic +node on the returned and_elim or inspect (which are plugins). *) + +assume val p : prop +assume val q : prop + +let foo (b:bool) : Tac (term -> Tac unit) = + if b + then and_elim + else fail "no" + +let test (x : squash (p /\ q)) = + assert True by ( + let f = foo true in + f (quote x); + dump "" + ) + +let bar () : Tac (term -> Tac term_view) = + inspect + +let test2 () = + assert True by ( + let f = bar () in + let tv = f (`1) in + dump "" + )