diff --git a/ocaml/fstar-lib/FStar_Tactics_V2_Builtins.ml b/ocaml/fstar-lib/FStar_Tactics_V2_Builtins.ml index 37aeddfed30..e9e1ea19382 100644 --- a/ocaml/fstar-lib/FStar_Tactics_V2_Builtins.ml +++ b/ocaml/fstar-lib/FStar_Tactics_V2_Builtins.ml @@ -34,35 +34,31 @@ let to_tac_1 (t: 'b -> 'a __tac): 'b -> 'a TM.tac = fun x -> (fun (ps: proofstate) -> uninterpret_tac (t x) ps) |> TM.mk_tac -let from_tac_1 s (t: 'a -> 'b TM.tac): 'a -> 'b __tac = - fun (x: 'a) -> - fun (ps: proofstate) -> - let m = t x in - interpret_tac s m ps - -let from_tac_2 s (t: 'a -> 'b -> 'c TM.tac): 'a -> 'b -> 'c __tac = - fun (x: 'a) -> - fun (y: 'b) -> - fun (ps: proofstate) -> - let m = t x y in - interpret_tac s m ps - -let from_tac_3 s (t: 'a -> 'b -> 'c -> 'd TM.tac): 'a -> 'b -> 'c -> 'd __tac = - fun (x: 'a) -> - fun (y: 'b) -> - fun (z: 'c) -> - fun (ps: proofstate) -> - let m = t x y z in - interpret_tac s m ps - -let from_tac_4 s (t: 'a -> 'b -> 'c -> 'd -> 'e TM.tac): 'a -> 'b -> 'c -> 'd -> 'e __tac = - fun (x: 'a) -> - fun (y: 'b) -> - fun (z: 'c) -> - fun (w: 'd) -> - fun (ps: proofstate) -> - let m = t x y z w in - interpret_tac s m ps +let from_tac_1 s (t: 'a -> 'r TM.tac): 'a -> 'r __tac = + fun (xa: 'a) (ps : proofstate) -> + let m = t xa in + interpret_tac s m ps + +let from_tac_2 s (t: 'a -> 'b -> 'r TM.tac): 'a -> 'b -> 'r __tac = + fun (xa: 'a) (xb: 'b) (ps : proofstate) -> + let m = t xa xb in + interpret_tac s m ps + +let from_tac_3 s (t: 'a -> 'b -> 'c -> 'r TM.tac): 'a -> 'b -> 'c -> 'r __tac = + fun (xa: 'a) (xb: 'b) (xc: 'c) (ps : proofstate) -> + let m = t xa xb xc in + interpret_tac s m ps + +let from_tac_4 s (t: 'a -> 'b -> 'c -> 'd -> 'r TM.tac): 'a -> 'b -> 'c -> 'd -> 'r __tac = + fun (xa: 'a) (xb: 'b) (xc: 'c) (xd: 'd) (ps : proofstate) -> + let m = t xa xb xc xd in + interpret_tac s m ps + +let from_tac_5 s (t: 'a -> 'b -> 'c -> 'd -> 'e -> 'r TM.tac): 'a -> 'b -> 'c -> 'd -> 'e -> 'r __tac = + fun (xa: 'a) (xb: 'b) (xc: 'c) (xd: 'd) (xe: 'e) (ps : proofstate) -> + let m = t xa xb xc xd xe in + interpret_tac s m ps + (* Pointing to the internal primitives *) let compress = from_tac_1 "B.compress" B.compress @@ -146,7 +142,7 @@ type ('env, 'sc, 't, 'pats, 'bnds) match_complete_token = unit let is_non_informative = from_tac_2 "B.refl_is_non_informative" B.refl_is_non_informative let check_subtyping = from_tac_3 "B.refl_check_subtyping" B.refl_check_subtyping -let check_equiv = from_tac_3 "B.refl_check_equiv" B.refl_check_equiv +let t_check_equiv = from_tac_5 "B.t_refl_check_equiv" B.t_refl_check_equiv let core_compute_term_type = from_tac_2 "B.refl_core_compute_term_type" B.refl_core_compute_term_type let core_check_term = from_tac_4 "B.refl_core_check_term" B.refl_core_check_term let core_check_term_at_type = from_tac_3 "B.refl_core_check_term_at_type" B.refl_core_check_term_at_type diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_InterpFuns.ml b/ocaml/fstar-lib/generated/FStar_Tactics_InterpFuns.ml index c814b0d2302..fa15e66c967 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_InterpFuns.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_InterpFuns.ml @@ -371,6 +371,90 @@ let mk_tac_step_4 : FStar_Pervasives_Native.Some uu___11) in set_auto_reflect (Prims.of_int (4)) uu___10 +let mk_tac_step_5 : + 'nres 'nt1 'nt2 'nt3 'nt4 'nt5 'res 't1 't2 't3 't4 't5 . + Prims.int -> + Prims.string -> + 't1 FStar_Syntax_Embeddings_Base.embedding -> + 't2 FStar_Syntax_Embeddings_Base.embedding -> + 't3 FStar_Syntax_Embeddings_Base.embedding -> + 't4 FStar_Syntax_Embeddings_Base.embedding -> + 't5 FStar_Syntax_Embeddings_Base.embedding -> + 'res FStar_Syntax_Embeddings_Base.embedding -> + 'nt1 FStar_TypeChecker_NBETerm.embedding -> + 'nt2 FStar_TypeChecker_NBETerm.embedding -> + 'nt3 FStar_TypeChecker_NBETerm.embedding -> + 'nt4 FStar_TypeChecker_NBETerm.embedding -> + 'nt5 FStar_TypeChecker_NBETerm.embedding -> + 'nres FStar_TypeChecker_NBETerm.embedding -> + ('t1 -> + 't2 -> + 't3 -> + 't4 -> + 't5 -> 'res FStar_Tactics_Monad.tac) + -> + ('nt1 -> + 'nt2 -> + 'nt3 -> + 'nt4 -> + 'nt5 -> + 'nres FStar_Tactics_Monad.tac) + -> + FStar_TypeChecker_Primops_Base.primitive_step + = + fun univ_arity -> + fun nm -> + fun uu___ -> + fun uu___1 -> + fun uu___2 -> + fun uu___3 -> + fun uu___4 -> + fun uu___5 -> + fun uu___6 -> + fun uu___7 -> + fun uu___8 -> + fun uu___9 -> + fun uu___10 -> + fun uu___11 -> + fun f -> + fun nbe_f -> + let lid = builtin_lid nm in + let uu___12 = + FStar_TypeChecker_Primops_Base.mk6' + univ_arity lid uu___ uu___6 uu___1 + uu___7 uu___2 uu___8 uu___3 uu___9 + uu___4 uu___10 + FStar_Tactics_Embedding.e_proofstate + FStar_Tactics_Embedding.e_proofstate_nbe + (FStar_Tactics_Embedding.e_result + uu___5) + (FStar_Tactics_Embedding.e_result_nbe + uu___11) + (fun a -> + fun b -> + fun c -> + fun d -> + fun e -> + fun ps -> + let uu___13 = + let uu___14 = + f a b c d e in + run_wrap nm uu___14 ps in + FStar_Pervasives_Native.Some + uu___13) + (fun a -> + fun b -> + fun c -> + fun d -> + fun e -> + fun ps -> + let uu___13 = + let uu___14 = + nbe_f a b c d e in + run_wrap nm uu___14 ps in + FStar_Pervasives_Native.Some + uu___13) in + set_auto_reflect (Prims.of_int (5)) uu___12 let (max_tac_arity : Prims.int) = (Prims.of_int (20)) let mk_tactic_interpretation_1 : 'r 't1 . diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml index de22aaf32af..b1e575d08af 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml @@ -5418,7 +5418,7 @@ let (_t_trefl : | FStar_Pervasives.Inl (uu___13, t_ty) -> let uu___14 = FStar_TypeChecker_Core.check_term_subtyping - env1 ty t_ty in + true true env1 ty t_ty in (match uu___14 with | FStar_Pervasives.Inl (FStar_Pervasives_Native.None) -> diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml index c1d8061b37a..5c51f84018c 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml @@ -6004,7 +6004,7 @@ let (_t_trefl : | FStar_Pervasives.Inl (uu___13, t_ty) -> let uu___14 = FStar_TypeChecker_Core.check_term_subtyping - env1 ty t_ty in + true true env1 ty t_ty in (match uu___14 with | FStar_Pervasives.Inl (FStar_Pervasives_Native.None) -> @@ -9957,117 +9957,136 @@ let (refl_is_non_informative : FStar_Class_Monad.return FStar_Tactics_Monad.monad_tac () (Obj.magic uu___2)))) uu___1 uu___ let (refl_check_relation : - env -> - FStar_Syntax_Syntax.typ -> - FStar_Syntax_Syntax.typ -> - relation -> - (unit FStar_Pervasives_Native.option * issues) - FStar_Tactics_Monad.tac) + relation -> + Prims.bool -> + Prims.bool -> + env -> + FStar_Syntax_Syntax.typ -> + FStar_Syntax_Syntax.typ -> + (unit FStar_Pervasives_Native.option * issues) + FStar_Tactics_Monad.tac) = - fun uu___3 -> - fun uu___2 -> - fun uu___1 -> - fun uu___ -> - (fun g -> - fun t0 -> - fun t1 -> - fun rel -> - let uu___ = - ((no_uvars_in_g g) && (no_uvars_in_term t0)) && - (no_uvars_in_term t1) in - if uu___ - then - Obj.magic - (Obj.repr - (refl_typing_builtin_wrapper "refl_check_relation" - (fun uu___1 -> - let g1 = - FStar_TypeChecker_Env.set_range g - t0.FStar_Syntax_Syntax.pos in - dbg_refl g1 - (fun uu___3 -> - let uu___4 = - FStar_Class_Show.show - FStar_Syntax_Print.showable_term t0 in - let uu___5 = - FStar_Class_Show.show - FStar_Syntax_Print.showable_term t1 in - FStar_Compiler_Util.format3 - "refl_check_relation: %s %s %s\n" - uu___4 - (if rel = Subtyping - then "<:?" - else "=?=") uu___5); - (let f = - if rel = Subtyping - then - FStar_TypeChecker_Core.check_term_subtyping - else - FStar_TypeChecker_Core.check_term_equality in - let uu___3 = f g1 t0 t1 in - match uu___3 with - | FStar_Pervasives.Inl - (FStar_Pervasives_Native.None) -> - (dbg_refl g1 - (fun uu___5 -> - "refl_check_relation: succeeded (no guard)"); - ((), [])) - | FStar_Pervasives.Inl - (FStar_Pervasives_Native.Some guard_f) - -> - (dbg_refl g1 - (fun uu___5 -> - "refl_check_relation: succeeded"); - ((), [(g1, guard_f)])) - | FStar_Pervasives.Inr err -> - (dbg_refl g1 - (fun uu___5 -> - let uu___6 = - FStar_TypeChecker_Core.print_error - err in - FStar_Compiler_Util.format1 - "refl_check_relation failed: %s\n" - uu___6); - (let uu___5 = - let uu___6 = - let uu___7 = - FStar_TypeChecker_Core.print_error - err in - Prims.strcat - "check_relation failed: " uu___7 in - (FStar_Errors_Codes.Fatal_IllTyped, - uu___6) in - let uu___6 = - FStar_TypeChecker_Env.get_range g1 in - FStar_Errors.raise_error uu___5 uu___6)))))) - else - Obj.magic - (Obj.repr - (let uu___2 = - let uu___3 = - let uu___4 = - let uu___5 = - FStar_TypeChecker_Env.get_range g in - unexpected_uvars_issue uu___5 in - [uu___4] in - (FStar_Pervasives_Native.None, uu___3) in - FStar_Class_Monad.return - FStar_Tactics_Monad.monad_tac () - (Obj.magic uu___2)))) uu___3 uu___2 uu___1 uu___ + fun uu___5 -> + fun uu___4 -> + fun uu___3 -> + fun uu___2 -> + fun uu___1 -> + fun uu___ -> + (fun rel -> + fun smt_ok -> + fun unfolding_ok -> + fun g -> + fun t0 -> + fun t1 -> + let uu___ = + ((no_uvars_in_g g) && (no_uvars_in_term t0)) && + (no_uvars_in_term t1) in + if uu___ + then + Obj.magic + (Obj.repr + (refl_typing_builtin_wrapper + "refl_check_relation" + (fun uu___1 -> + let g1 = + FStar_TypeChecker_Env.set_range g + t0.FStar_Syntax_Syntax.pos in + dbg_refl g1 + (fun uu___3 -> + let uu___4 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term + t0 in + let uu___5 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term + t1 in + FStar_Compiler_Util.format3 + "refl_check_relation: %s %s %s\n" + uu___4 + (if rel = Subtyping + then "<:?" + else "=?=") uu___5); + (let f = + if rel = Subtyping + then + FStar_TypeChecker_Core.check_term_subtyping + else + FStar_TypeChecker_Core.check_term_equality in + let uu___3 = + f smt_ok unfolding_ok g1 t0 t1 in + match uu___3 with + | FStar_Pervasives.Inl + (FStar_Pervasives_Native.None) + -> + (dbg_refl g1 + (fun uu___5 -> + "refl_check_relation: succeeded (no guard)"); + ((), [])) + | FStar_Pervasives.Inl + (FStar_Pervasives_Native.Some + guard_f) -> + (dbg_refl g1 + (fun uu___5 -> + "refl_check_relation: succeeded"); + ((), [(g1, guard_f)])) + | FStar_Pervasives.Inr err -> + (dbg_refl g1 + (fun uu___5 -> + let uu___6 = + FStar_TypeChecker_Core.print_error + err in + FStar_Compiler_Util.format1 + "refl_check_relation failed: %s\n" + uu___6); + (let uu___5 = + let uu___6 = + let uu___7 = + FStar_TypeChecker_Core.print_error + err in + Prims.strcat + "check_relation failed: " + uu___7 in + (FStar_Errors_Codes.Fatal_IllTyped, + uu___6) in + let uu___6 = + FStar_TypeChecker_Env.get_range + g1 in + FStar_Errors.raise_error + uu___5 uu___6)))))) + else + Obj.magic + (Obj.repr + (let uu___2 = + let uu___3 = + let uu___4 = + let uu___5 = + FStar_TypeChecker_Env.get_range g in + unexpected_uvars_issue uu___5 in + [uu___4] in + (FStar_Pervasives_Native.None, uu___3) in + FStar_Class_Monad.return + FStar_Tactics_Monad.monad_tac () + (Obj.magic uu___2)))) uu___5 uu___4 + uu___3 uu___2 uu___1 uu___ let (refl_check_subtyping : env -> FStar_Syntax_Syntax.typ -> FStar_Syntax_Syntax.typ -> (unit FStar_Pervasives_Native.option * issues) FStar_Tactics_Monad.tac) - = fun g -> fun t0 -> fun t1 -> refl_check_relation g t0 t1 Subtyping -let (refl_check_equiv : - env -> - FStar_Syntax_Syntax.typ -> - FStar_Syntax_Syntax.typ -> - (unit FStar_Pervasives_Native.option * issues) - FStar_Tactics_Monad.tac) - = fun g -> fun t0 -> fun t1 -> refl_check_relation g t0 t1 Equality + = + fun g -> + fun t0 -> fun t1 -> refl_check_relation Subtyping true true g t0 t1 +let (t_refl_check_equiv : + Prims.bool -> + Prims.bool -> + env -> + FStar_Syntax_Syntax.typ -> + FStar_Syntax_Syntax.typ -> + (unit FStar_Pervasives_Native.option * issues) + FStar_Tactics_Monad.tac) + = refl_check_relation Equality let (to_must_tot : FStar_TypeChecker_Core.tot_or_ghost -> Prims.bool) = fun eff -> match eff with diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Derived.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Derived.ml index 2e2a41e9b6f..af3561abadb 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Derived.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Derived.ml @@ -5340,4 +5340,26 @@ let (smt_sync' : (fun vcfg' -> Obj.magic (FStar_Tactics_V2_Builtins.t_smt_sync vcfg')) - uu___))) uu___) \ No newline at end of file + uu___))) uu___) +let (check_equiv : + FStar_Reflection_Types.env -> + FStar_Reflection_Types.typ -> + FStar_Reflection_Types.typ -> + (((unit, unit, unit) FStar_Tactics_Types.equiv_token + FStar_Pervasives_Native.option * FStar_Issue.issue Prims.list), + unit) FStar_Tactics_Effect.tac_repr) + = + fun g -> + fun t0 -> + fun t1 -> FStar_Tactics_V2_Builtins.t_check_equiv true true g t0 t1 +let (check_equiv_nosmt : + FStar_Reflection_Types.env -> + FStar_Reflection_Types.typ -> + FStar_Reflection_Types.typ -> + (((unit, unit, unit) FStar_Tactics_Types.equiv_token + FStar_Pervasives_Native.option * FStar_Issue.issue Prims.list), + unit) FStar_Tactics_Effect.tac_repr) + = + fun g -> + fun t0 -> + fun t1 -> FStar_Tactics_V2_Builtins.t_check_equiv false false g t0 t1 \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Primops.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Primops.ml index 56661c063a0..487bf630c30 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Primops.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Primops.ml @@ -127,8 +127,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = let uu___14 = let uu___15 = FStar_Tactics_InterpFuns.mk_tot_step_1 Prims.int_zero - "goal_type" FStar_Tactics_Embedding.e_goal - FStar_Reflection_V2_Embeddings.e_term + "goal_type" FStar_Tactics_Embedding.e_goal uu___2 FStar_Tactics_Embedding.e_goal_nbe FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_Tactics_Types.goal_type @@ -136,8 +135,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = let uu___16 = let uu___17 = FStar_Tactics_InterpFuns.mk_tot_step_1 Prims.int_zero - "goal_witness" FStar_Tactics_Embedding.e_goal - FStar_Reflection_V2_Embeddings.e_term + "goal_witness" FStar_Tactics_Embedding.e_goal uu___2 FStar_Tactics_Embedding.e_goal_nbe FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_Tactics_Types.goal_witness @@ -176,9 +174,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = let uu___25 = let uu___26 = FStar_Tactics_InterpFuns.mk_tac_step_1 - Prims.int_zero "compress" - FStar_Reflection_V2_Embeddings.e_term - FStar_Reflection_V2_Embeddings.e_term + Prims.int_zero "compress" uu___2 uu___2 FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_Tactics_V2_Basic.compress @@ -296,8 +292,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_Embeddings.e_env (FStar_Syntax_Embeddings.e_list FStar_Syntax_Embeddings.e_norm_step) - FStar_Reflection_V2_Embeddings.e_term - FStar_Reflection_V2_Embeddings.e_term + uu___2 uu___2 FStar_Reflection_V2_NBEEmbeddings.e_env (FStar_TypeChecker_NBETerm.e_list FStar_TypeChecker_NBETerm.e_norm_step) @@ -406,7 +401,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = "t_exact" FStar_Syntax_Embeddings.e_bool FStar_Syntax_Embeddings.e_bool - FStar_Reflection_V2_Embeddings.e_term + uu___2 FStar_Syntax_Embeddings.e_unit FStar_TypeChecker_NBETerm.e_bool FStar_TypeChecker_NBETerm.e_bool @@ -422,7 +417,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Syntax_Embeddings.e_bool FStar_Syntax_Embeddings.e_bool FStar_Syntax_Embeddings.e_bool - FStar_Reflection_V2_Embeddings.e_term + uu___2 FStar_Syntax_Embeddings.e_unit FStar_TypeChecker_NBETerm.e_bool FStar_TypeChecker_NBETerm.e_bool @@ -439,7 +434,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = "t_apply_lemma" FStar_Syntax_Embeddings.e_bool FStar_Syntax_Embeddings.e_bool - FStar_Reflection_V2_Embeddings.e_term + uu___2 FStar_Syntax_Embeddings.e_unit FStar_TypeChecker_NBETerm.e_bool FStar_TypeChecker_NBETerm.e_bool @@ -468,7 +463,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = Prims.int_zero "tcc" FStar_Reflection_V2_Embeddings.e_env - FStar_Reflection_V2_Embeddings.e_term + uu___2 FStar_Reflection_V2_Embeddings.e_comp FStar_Reflection_V2_NBEEmbeddings.e_env FStar_Reflection_V2_NBEEmbeddings.e_attribute @@ -483,8 +478,8 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = Prims.int_zero "tc" FStar_Reflection_V2_Embeddings.e_env - FStar_Reflection_V2_Embeddings.e_term - FStar_Reflection_V2_Embeddings.e_term + uu___2 + uu___2 FStar_Reflection_V2_NBEEmbeddings.e_env FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_Reflection_V2_NBEEmbeddings.e_attribute @@ -497,7 +492,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero "unshelve" - FStar_Reflection_V2_Embeddings.e_term + uu___2 FStar_Syntax_Embeddings.e_unit FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_TypeChecker_NBETerm.e_unit @@ -692,7 +687,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero "tadmit_t" - FStar_Reflection_V2_Embeddings.e_term + uu___2 FStar_Syntax_Embeddings.e_unit FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_TypeChecker_NBETerm.e_unit @@ -718,7 +713,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero "t_destruct" - FStar_Reflection_V2_Embeddings.e_term + uu___2 (FStar_Syntax_Embeddings.e_list (FStar_Syntax_Embeddings.e_tuple2 FStar_Reflection_V2_Embeddings.e_fv @@ -778,8 +773,8 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = "uvar_env" FStar_Reflection_V2_Embeddings.e_env (FStar_Syntax_Embeddings.e_option - FStar_Reflection_V2_Embeddings.e_term) - FStar_Reflection_V2_Embeddings.e_term + uu___2) + uu___2 FStar_Reflection_V2_NBEEmbeddings.e_env (FStar_TypeChecker_NBETerm.e_option FStar_Reflection_V2_NBEEmbeddings.e_attribute) @@ -794,8 +789,8 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = Prims.int_zero "ghost_uvar_env" FStar_Reflection_V2_Embeddings.e_env - FStar_Reflection_V2_Embeddings.e_term - FStar_Reflection_V2_Embeddings.e_term + uu___2 + uu___2 FStar_Reflection_V2_NBEEmbeddings.e_env FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_Reflection_V2_NBEEmbeddings.e_attribute @@ -809,7 +804,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = Prims.int_zero "fresh_universe_uvar" FStar_Syntax_Embeddings.e_unit - FStar_Reflection_V2_Embeddings.e_term + uu___2 FStar_TypeChecker_NBETerm.e_unit FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_Tactics_V2_Basic.fresh_universe_uvar @@ -822,8 +817,8 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = Prims.int_zero "unify_env" FStar_Reflection_V2_Embeddings.e_env - FStar_Reflection_V2_Embeddings.e_term - FStar_Reflection_V2_Embeddings.e_term + uu___2 + uu___2 FStar_Syntax_Embeddings.e_bool FStar_Reflection_V2_NBEEmbeddings.e_env FStar_Reflection_V2_NBEEmbeddings.e_attribute @@ -839,8 +834,8 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = Prims.int_zero "unify_guard_env" FStar_Reflection_V2_Embeddings.e_env - FStar_Reflection_V2_Embeddings.e_term - FStar_Reflection_V2_Embeddings.e_term + uu___2 + uu___2 FStar_Syntax_Embeddings.e_bool FStar_Reflection_V2_NBEEmbeddings.e_env FStar_Reflection_V2_NBEEmbeddings.e_attribute @@ -856,8 +851,8 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = Prims.int_zero "match_env" FStar_Reflection_V2_Embeddings.e_env - FStar_Reflection_V2_Embeddings.e_term - FStar_Reflection_V2_Embeddings.e_term + uu___2 + uu___2 FStar_Syntax_Embeddings.e_bool FStar_Reflection_V2_NBEEmbeddings.e_env FStar_Reflection_V2_NBEEmbeddings.e_attribute @@ -889,7 +884,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero "change" - FStar_Reflection_V2_Embeddings.e_term + uu___2 FStar_Syntax_Embeddings.e_unit FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_TypeChecker_NBETerm.e_unit @@ -1031,7 +1026,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = "string_to_term" FStar_Reflection_V2_Embeddings.e_env FStar_Syntax_Embeddings.e_string - FStar_Reflection_V2_Embeddings.e_term + uu___2 FStar_Reflection_V2_NBEEmbeddings.e_env FStar_TypeChecker_NBETerm.e_string FStar_Reflection_V2_NBEEmbeddings.e_attribute @@ -1063,7 +1058,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero "term_to_string" - FStar_Reflection_V2_Embeddings.e_term + uu___2 FStar_Syntax_Embeddings.e_string FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_TypeChecker_NBETerm.e_string @@ -1089,7 +1084,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero "term_to_doc" - FStar_Reflection_V2_Embeddings.e_term + uu___2 FStar_Syntax_Embeddings.e_document FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_TypeChecker_NBETerm.e_document @@ -1128,8 +1123,8 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero "term_eq_old" - FStar_Reflection_V2_Embeddings.e_term - FStar_Reflection_V2_Embeddings.e_term + uu___2 + uu___2 FStar_Syntax_Embeddings.e_bool FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_Reflection_V2_NBEEmbeddings.e_attribute @@ -1213,7 +1208,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero "free_uvars" - FStar_Reflection_V2_Embeddings.e_term + uu___2 (FStar_Syntax_Embeddings.e_list FStar_Syntax_Embeddings.e_int) FStar_Reflection_V2_NBEEmbeddings.e_attribute @@ -1351,7 +1346,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = Prims.int_zero "is_non_informative" FStar_Reflection_V2_Embeddings.e_env - FStar_Reflection_V2_Embeddings.e_term + uu___2 (FStar_Syntax_Embeddings.e_tuple2 (FStar_Syntax_Embeddings.e_option FStar_Syntax_Embeddings.e_unit) @@ -1374,8 +1369,8 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = Prims.int_zero "check_subtyping" FStar_Reflection_V2_Embeddings.e_env - FStar_Reflection_V2_Embeddings.e_term - FStar_Reflection_V2_Embeddings.e_term + uu___2 + uu___2 (FStar_Syntax_Embeddings.e_tuple2 (FStar_Syntax_Embeddings.e_option FStar_Syntax_Embeddings.e_unit) @@ -1395,17 +1390,21 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = = let uu___182 = - FStar_Tactics_InterpFuns.mk_tac_step_3 + FStar_Tactics_InterpFuns.mk_tac_step_5 Prims.int_zero - "check_equiv" + "t_check_equiv" + FStar_Syntax_Embeddings.e_bool + FStar_Syntax_Embeddings.e_bool FStar_Reflection_V2_Embeddings.e_env - FStar_Reflection_V2_Embeddings.e_term - FStar_Reflection_V2_Embeddings.e_term + uu___2 + uu___2 (FStar_Syntax_Embeddings.e_tuple2 (FStar_Syntax_Embeddings.e_option FStar_Syntax_Embeddings.e_unit) (FStar_Syntax_Embeddings.e_list FStar_Syntax_Embeddings.e_issue)) + FStar_TypeChecker_NBETerm.e_bool + FStar_TypeChecker_NBETerm.e_bool FStar_Reflection_V2_NBEEmbeddings.e_env FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_Reflection_V2_NBEEmbeddings.e_attribute @@ -1414,25 +1413,24 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit) (FStar_TypeChecker_NBETerm.e_list FStar_TypeChecker_NBETerm.e_issue)) - FStar_Tactics_V2_Basic.refl_check_equiv - FStar_Tactics_V2_Basic.refl_check_equiv in + FStar_Tactics_V2_Basic.t_refl_check_equiv + FStar_Tactics_V2_Basic.t_refl_check_equiv in let uu___183 = let uu___184 = - let uu___185 - = - e_ret_t - (FStar_Syntax_Embeddings.e_tuple2 - (solve - FStar_Tactics_Embedding.e_tot_or_ghost) - FStar_Reflection_V2_Embeddings.e_term) in FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero "core_compute_term_type" FStar_Reflection_V2_Embeddings.e_env - FStar_Reflection_V2_Embeddings.e_term - uu___185 + uu___2 + (FStar_Syntax_Embeddings.e_tuple2 + (FStar_Syntax_Embeddings.e_option + (FStar_Syntax_Embeddings.e_tuple2 + FStar_Tactics_Embedding.e_tot_or_ghost + uu___2)) + (FStar_Syntax_Embeddings.e_list + FStar_Syntax_Embeddings.e_issue)) FStar_Reflection_V2_NBEEmbeddings.e_env FStar_Reflection_V2_NBEEmbeddings.e_attribute (FStar_TypeChecker_NBETerm.e_tuple2 @@ -1452,8 +1450,8 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = Prims.int_zero "core_check_term" FStar_Reflection_V2_Embeddings.e_env - FStar_Reflection_V2_Embeddings.e_term - FStar_Reflection_V2_Embeddings.e_term + uu___2 + uu___2 FStar_Tactics_Embedding.e_tot_or_ghost (FStar_Syntax_Embeddings.e_tuple2 (FStar_Syntax_Embeddings.e_option @@ -1479,8 +1477,8 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = Prims.int_zero "core_check_term_at_type" FStar_Reflection_V2_Embeddings.e_env - FStar_Reflection_V2_Embeddings.e_term - FStar_Reflection_V2_Embeddings.e_term + uu___2 + uu___2 (FStar_Syntax_Embeddings.e_tuple2 (FStar_Syntax_Embeddings.e_option FStar_Tactics_Embedding.e_tot_or_ghost) @@ -1500,21 +1498,20 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = = let uu___190 = - let uu___191 - = - e_ret_t - (FStar_Syntax_Embeddings.e_tuple2 - FStar_Reflection_V2_Embeddings.e_term - (FStar_Syntax_Embeddings.e_tuple2 - (solve - FStar_Tactics_Embedding.e_tot_or_ghost) - FStar_Reflection_V2_Embeddings.e_term)) in FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero "tc_term" FStar_Reflection_V2_Embeddings.e_env - FStar_Reflection_V2_Embeddings.e_term - uu___191 + uu___2 + (FStar_Syntax_Embeddings.e_tuple2 + (FStar_Syntax_Embeddings.e_option + (FStar_Syntax_Embeddings.e_tuple2 + uu___2 + (FStar_Syntax_Embeddings.e_tuple2 + FStar_Tactics_Embedding.e_tot_or_ghost + uu___2))) + (FStar_Syntax_Embeddings.e_list + FStar_Syntax_Embeddings.e_issue)) FStar_Reflection_V2_NBEEmbeddings.e_env FStar_Reflection_V2_NBEEmbeddings.e_attribute (FStar_TypeChecker_NBETerm.e_tuple2 @@ -1536,7 +1533,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = Prims.int_zero "universe_of" FStar_Reflection_V2_Embeddings.e_env - FStar_Reflection_V2_Embeddings.e_term + uu___2 (FStar_Syntax_Embeddings.e_tuple2 (FStar_Syntax_Embeddings.e_option FStar_Reflection_V2_Embeddings.e_universe) @@ -1559,7 +1556,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = Prims.int_zero "check_prop_validity" FStar_Reflection_V2_Embeddings.e_env - FStar_Reflection_V2_Embeddings.e_term + uu___2 (FStar_Syntax_Embeddings.e_tuple2 (FStar_Syntax_Embeddings.e_option FStar_Syntax_Embeddings.e_unit) @@ -1582,8 +1579,8 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = Prims.int_zero "check_match_complete" FStar_Reflection_V2_Embeddings.e_env - FStar_Reflection_V2_Embeddings.e_term - FStar_Reflection_V2_Embeddings.e_term + uu___2 + uu___2 (FStar_Syntax_Embeddings.e_list FStar_Reflection_V2_Embeddings.e_pattern) (FStar_Syntax_Embeddings.e_option @@ -1674,16 +1671,16 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = (FStar_Syntax_Embeddings.e_tuple2 FStar_Reflection_V2_Embeddings.e_namedv FStar_Reflection_V2_Embeddings.e_term)) - FStar_Reflection_V2_Embeddings.e_term - FStar_Reflection_V2_Embeddings.e_term + uu___2 + uu___2 uu___201 FStar_Reflection_V2_NBEEmbeddings.e_env (FStar_TypeChecker_NBETerm.e_list (FStar_TypeChecker_NBETerm.e_tuple2 FStar_Reflection_V2_NBEEmbeddings.e_namedv FStar_Reflection_V2_NBEEmbeddings.e_term)) - FStar_Reflection_V2_NBEEmbeddings.e_term - FStar_Reflection_V2_NBEEmbeddings.e_term + FStar_Reflection_V2_NBEEmbeddings.e_attribute + FStar_Reflection_V2_NBEEmbeddings.e_attribute uu___202 FStar_Tactics_V2_Basic.refl_try_unify FStar_Tactics_V2_Basic.refl_try_unify in diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml index bfeaa3b68b4..b13f18135fb 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml @@ -390,17 +390,24 @@ let (context_term_to_string : context_term -> Prims.string) = type context = { no_guard: Prims.bool ; + unfolding_ok: Prims.bool ; error_context: (Prims.string * context_term FStar_Pervasives_Native.option) Prims.list } let (__proj__Mkcontext__item__no_guard : context -> Prims.bool) = fun projectee -> - match projectee with | { no_guard; error_context;_} -> no_guard + match projectee with + | { no_guard; unfolding_ok; error_context;_} -> no_guard +let (__proj__Mkcontext__item__unfolding_ok : context -> Prims.bool) = + fun projectee -> + match projectee with + | { no_guard; unfolding_ok; error_context;_} -> unfolding_ok let (__proj__Mkcontext__item__error_context : context -> (Prims.string * context_term FStar_Pervasives_Native.option) Prims.list) = fun projectee -> - match projectee with | { no_guard; error_context;_} -> error_context + match projectee with + | { no_guard; unfolding_ok; error_context;_} -> error_context let (showable_context : context FStar_Class_Show.showable) = { FStar_Class_Show.show = @@ -410,15 +417,20 @@ let (showable_context : context FStar_Class_Show.showable) = (FStar_Class_Show.printableshow FStar_Class_Printable.printable_bool) context1.no_guard in let uu___1 = - let uu___2 = + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_bool) context1.unfolding_ok in + let uu___2 = + let uu___3 = FStar_Compiler_List.map FStar_Pervasives_Native.fst context1.error_context in FStar_Class_Show.show (FStar_Class_Show.show_list (FStar_Class_Show.printableshow - FStar_Class_Printable.printable_string)) uu___2 in - FStar_Compiler_Util.format2 "{no_guard=%s, error_context=%s}" uu___ - uu___1) + FStar_Class_Printable.printable_string)) uu___3 in + FStar_Compiler_Util.format3 + "{no_guard=%s; unfolding_ok=%s; error_context=%s}" uu___ uu___1 + uu___2) } let (print_context : context -> Prims.string) = fun ctx -> @@ -668,6 +680,7 @@ let with_context : let ctx1 = { no_guard = (ctx.no_guard); + unfolding_ok = (ctx.unfolding_ok); error_context = ((msg, t) :: (ctx.error_context)) } in let uu___ = x () in uu___ ctx1 @@ -698,6 +711,7 @@ let (is_type : let ctx1 = { no_guard = (ctx.no_guard); + unfolding_ok = (ctx.unfolding_ok); error_context = (("is_type", (FStar_Pervasives_Native.Some (CtxTerm t))) :: (ctx.error_context)) @@ -865,6 +879,7 @@ let rec (is_arrow : let ctx1 = { no_guard = (ctx.no_guard); + unfolding_ok = (ctx.unfolding_ok); error_context = (("is_arrow", FStar_Pervasives_Native.None) :: (ctx.error_context)) } in @@ -1146,7 +1161,13 @@ let strengthen : let no_guard : 'a . 'a result -> 'a result = fun g -> fun ctx -> - let uu___ = g { no_guard = true; error_context = (ctx.error_context) } in + let uu___ = + g + { + no_guard = true; + unfolding_ok = (ctx.unfolding_ok); + error_context = (ctx.error_context) + } in match uu___ with | Success (x, FStar_Pervasives_Native.None) -> Success (x, FStar_Pervasives_Native.None) @@ -1571,6 +1592,8 @@ let (join_eff_l : tot_or_ghost Prims.list -> tot_or_ghost) = fun es -> FStar_List_Tot_Base.fold_right join_eff es E_Total let (guard_not_allowed : Prims.bool result) = fun ctx -> Success ((ctx.no_guard), FStar_Pervasives_Native.None) +let (unfolding_ok : Prims.bool result) = + fun ctx -> Success ((ctx.unfolding_ok), FStar_Pervasives_Native.None) let (debug : env -> (unit -> unit) -> unit) = fun g -> fun f -> @@ -1793,11 +1816,45 @@ let rec (check_relation : | uu___6 -> FStar_Pervasives_Native.None)) FStar_Pervasives_Native.None "FStar.TypeChecker.Core.maybe_unfold_side" in - let maybe_unfold t01 t11 = - let uu___4 = which_side_to_unfold t01 t11 in - maybe_unfold_side uu___4 t01 t11 in + let maybe_unfold t01 t11 ctx01 = + let uu___4 = unfolding_ok ctx01 in + match uu___4 with + | Success (x1, g11) -> + let uu___5 = + let uu___6 = + if x1 + then + let uu___7 = + let uu___8 = which_side_to_unfold t01 t11 in + maybe_unfold_side uu___8 t01 t11 in + fun uu___8 -> + Success + (uu___7, FStar_Pervasives_Native.None) + else + (fun uu___8 -> + Success + (FStar_Pervasives_Native.None, + FStar_Pervasives_Native.None)) in + uu___6 ctx01 in + (match uu___5 with + | Success (y, g2) -> + let uu___6 = + let uu___7 = and_pre g11 g2 in (y, uu___7) in + Success uu___6 + | err1 -> err1) + | Error err1 -> Error err1 in let emit_guard t01 t11 = - let uu___4 = do_check g t01 in + let uu___4 ctx = + let ctx1 = + { + no_guard = (ctx.no_guard); + unfolding_ok = (ctx.unfolding_ok); + error_context = + (("checking lhs while emitting guard", + FStar_Pervasives_Native.None) :: + (ctx.error_context)) + } in + let uu___5 = do_check g t01 in uu___5 ctx1 in fun ctx01 -> let uu___5 = uu___4 ctx01 in match uu___5 with @@ -1842,43 +1899,45 @@ let rec (check_relation : let uu___4 = (equatable g t01) || (equatable g t11) in (if uu___4 then emit_guard t01 t11 else err ()) else err () in - let maybe_unfold_side_and_retry side1 t01 t11 = - let uu___4 = maybe_unfold_side side1 t01 t11 in + let maybe_unfold_side_and_retry side1 t01 t11 ctx01 = + let uu___4 = unfolding_ok ctx01 in match uu___4 with - | FStar_Pervasives_Native.None -> fallback t01 t11 - | FStar_Pervasives_Native.Some (t02, t12) -> - check_relation g rel t02 t12 in + | Success (x1, g11) -> + let uu___5 = + let uu___6 = + if x1 + then + let uu___7 = maybe_unfold_side side1 t01 t11 in + match uu___7 with + | FStar_Pervasives_Native.None -> + fallback t01 t11 + | FStar_Pervasives_Native.Some (t02, t12) -> + check_relation g rel t02 t12 + else fallback t01 t11 in + uu___6 ctx01 in + (match uu___5 with + | Success (y, g2) -> + let uu___6 = + let uu___7 = and_pre g11 g2 in ((), uu___7) in + Success uu___6 + | err1 -> err1) + | Error err1 -> Error err1 in let maybe_unfold_and_retry t01 t11 = let uu___4 = which_side_to_unfold t01 t11 in maybe_unfold_side_and_retry uu___4 t01 t11 in let beta_iota_reduce t = let t2 = FStar_Syntax_Subst.compress t in - match t2.FStar_Syntax_Syntax.n with - | FStar_Syntax_Syntax.Tm_app uu___4 -> - let head = FStar_Syntax_Util.leftmost_head t2 in - let uu___5 = - let uu___6 = FStar_Syntax_Subst.compress head in - uu___6.FStar_Syntax_Syntax.n in - (match uu___5 with - | FStar_Syntax_Syntax.Tm_abs uu___6 -> - FStar_TypeChecker_Normalize.normalize - [FStar_TypeChecker_Env.Beta; - FStar_TypeChecker_Env.Iota; - FStar_TypeChecker_Env.Primops] g.tcenv t2 - | uu___6 -> t2) - | FStar_Syntax_Syntax.Tm_let uu___4 -> - FStar_TypeChecker_Normalize.normalize - [FStar_TypeChecker_Env.Beta; - FStar_TypeChecker_Env.Iota; - FStar_TypeChecker_Env.Primops] g.tcenv t2 - | FStar_Syntax_Syntax.Tm_match uu___4 -> - FStar_TypeChecker_Normalize.normalize - [FStar_TypeChecker_Env.Beta; - FStar_TypeChecker_Env.Iota; - FStar_TypeChecker_Env.Primops] g.tcenv t2 + let t3 = + FStar_TypeChecker_Normalize.normalize + [FStar_TypeChecker_Env.HNF; + FStar_TypeChecker_Env.Weak; + FStar_TypeChecker_Env.Beta; + FStar_TypeChecker_Env.Iota; + FStar_TypeChecker_Env.Primops] g.tcenv t2 in + match t3.FStar_Syntax_Syntax.n with | FStar_Syntax_Syntax.Tm_refine uu___4 -> - FStar_Syntax_Util.flatten_refinement t2 - | uu___4 -> t2 in + FStar_Syntax_Util.flatten_refinement t3 + | uu___4 -> t3 in let beta_iota_reduce1 t = FStar_Profiling.profile (fun uu___4 -> beta_iota_reduce t) @@ -1898,6 +1957,7 @@ let rec (check_relation : let ctx1 = { no_guard = (ctx.no_guard); + unfolding_ok = (ctx.unfolding_ok); error_context = (("check_relation", (FStar_Pervasives_Native.Some @@ -2177,45 +2237,91 @@ let rec (check_relation : (let uu___8 = maybe_unfold x0.FStar_Syntax_Syntax.sort x1.FStar_Syntax_Syntax.sort in - match uu___8 with - | FStar_Pervasives_Native.None -> - fallback t01 t11 - | FStar_Pervasives_Native.Some (t02, t12) -> - let lhs = - FStar_Syntax_Syntax.mk - (FStar_Syntax_Syntax.Tm_refine - { - FStar_Syntax_Syntax.b = - { - FStar_Syntax_Syntax.ppname = - (x0.FStar_Syntax_Syntax.ppname); - FStar_Syntax_Syntax.index = - (x0.FStar_Syntax_Syntax.index); - FStar_Syntax_Syntax.sort = - t02 - }; - FStar_Syntax_Syntax.phi = f0 - }) t02.FStar_Syntax_Syntax.pos in - let rhs = - FStar_Syntax_Syntax.mk - (FStar_Syntax_Syntax.Tm_refine - { - FStar_Syntax_Syntax.b = - { - FStar_Syntax_Syntax.ppname = - (x1.FStar_Syntax_Syntax.ppname); - FStar_Syntax_Syntax.index = - (x1.FStar_Syntax_Syntax.index); - FStar_Syntax_Syntax.sort = - t12 - }; - FStar_Syntax_Syntax.phi = f1 - }) t12.FStar_Syntax_Syntax.pos in - let uu___9 = - FStar_Syntax_Util.flatten_refinement lhs in - let uu___10 = - FStar_Syntax_Util.flatten_refinement rhs in - check_relation1 g rel uu___9 uu___10) + fun ctx01 -> + let uu___9 = uu___8 ctx01 in + match uu___9 with + | Success (x2, g11) -> + let uu___10 = + let uu___11 = + match x2 with + | FStar_Pervasives_Native.None -> + ((let uu___13 = + FStar_TypeChecker_Env.debug + g.tcenv + (FStar_Options.Other + "Core") in + if uu___13 + then + let uu___14 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term + x0.FStar_Syntax_Syntax.sort in + let uu___15 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term + x1.FStar_Syntax_Syntax.sort in + FStar_Compiler_Util.print2 + "Cannot match ref heads %s and %s\n" + uu___14 uu___15 + else ()); + fallback t01 t11) + | FStar_Pervasives_Native.Some + (t02, t12) -> + let lhs = + FStar_Syntax_Syntax.mk + (FStar_Syntax_Syntax.Tm_refine + { + FStar_Syntax_Syntax.b = + { + FStar_Syntax_Syntax.ppname + = + (x0.FStar_Syntax_Syntax.ppname); + FStar_Syntax_Syntax.index + = + (x0.FStar_Syntax_Syntax.index); + FStar_Syntax_Syntax.sort + = t02 + }; + FStar_Syntax_Syntax.phi + = f0 + }) + t02.FStar_Syntax_Syntax.pos in + let rhs = + FStar_Syntax_Syntax.mk + (FStar_Syntax_Syntax.Tm_refine + { + FStar_Syntax_Syntax.b = + { + FStar_Syntax_Syntax.ppname + = + (x1.FStar_Syntax_Syntax.ppname); + FStar_Syntax_Syntax.index + = + (x1.FStar_Syntax_Syntax.index); + FStar_Syntax_Syntax.sort + = t12 + }; + FStar_Syntax_Syntax.phi + = f1 + }) + t12.FStar_Syntax_Syntax.pos in + let uu___12 = + FStar_Syntax_Util.flatten_refinement + lhs in + let uu___13 = + FStar_Syntax_Util.flatten_refinement + rhs in + check_relation1 g rel uu___12 + uu___13 in + uu___11 ctx01 in + (match uu___10 with + | Success (y, g2) -> + let uu___11 = + let uu___12 = and_pre g11 g2 in + ((), uu___12) in + Success uu___11 + | err1 -> err1) + | Error err1 -> Error err1) | (FStar_Syntax_Syntax.Tm_refine { FStar_Syntax_Syntax.b = x0; FStar_Syntax_Syntax.phi = f0;_}, @@ -2229,28 +2335,50 @@ let rec (check_relation : else (let uu___9 = maybe_unfold x0.FStar_Syntax_Syntax.sort t11 in - match uu___9 with - | FStar_Pervasives_Native.None -> - fallback t01 t11 - | FStar_Pervasives_Native.Some (t02, t12) -> - let lhs = - FStar_Syntax_Syntax.mk - (FStar_Syntax_Syntax.Tm_refine - { - FStar_Syntax_Syntax.b = - { - FStar_Syntax_Syntax.ppname = - (x0.FStar_Syntax_Syntax.ppname); - FStar_Syntax_Syntax.index = - (x0.FStar_Syntax_Syntax.index); - FStar_Syntax_Syntax.sort = - t02 - }; - FStar_Syntax_Syntax.phi = f0 - }) t02.FStar_Syntax_Syntax.pos in - let uu___10 = - FStar_Syntax_Util.flatten_refinement lhs in - check_relation1 g rel uu___10 t12) + fun ctx01 -> + let uu___10 = uu___9 ctx01 in + match uu___10 with + | Success (x1, g11) -> + let uu___11 = + let uu___12 = + match x1 with + | FStar_Pervasives_Native.None -> + fallback t01 t11 + | FStar_Pervasives_Native.Some + (t02, t12) -> + let lhs = + FStar_Syntax_Syntax.mk + (FStar_Syntax_Syntax.Tm_refine + { + FStar_Syntax_Syntax.b = + { + FStar_Syntax_Syntax.ppname + = + (x0.FStar_Syntax_Syntax.ppname); + FStar_Syntax_Syntax.index + = + (x0.FStar_Syntax_Syntax.index); + FStar_Syntax_Syntax.sort + = t02 + }; + FStar_Syntax_Syntax.phi + = f0 + }) + t02.FStar_Syntax_Syntax.pos in + let uu___13 = + FStar_Syntax_Util.flatten_refinement + lhs in + check_relation1 g rel uu___13 + t12 in + uu___12 ctx01 in + (match uu___11 with + | Success (y, g2) -> + let uu___12 = + let uu___13 = and_pre g11 g2 in + ((), uu___13) in + Success uu___12 + | err1 -> err1) + | Error err1 -> Error err1) | (uu___6, FStar_Syntax_Syntax.Tm_refine { FStar_Syntax_Syntax.b = x1; FStar_Syntax_Syntax.phi = f1;_}) @@ -2411,28 +2539,50 @@ let rec (check_relation : else (let uu___9 = maybe_unfold t01 x1.FStar_Syntax_Syntax.sort in - match uu___9 with - | FStar_Pervasives_Native.None -> - fallback t01 t11 - | FStar_Pervasives_Native.Some (t02, t12) -> - let rhs = - FStar_Syntax_Syntax.mk - (FStar_Syntax_Syntax.Tm_refine - { - FStar_Syntax_Syntax.b = - { - FStar_Syntax_Syntax.ppname = - (x1.FStar_Syntax_Syntax.ppname); - FStar_Syntax_Syntax.index = - (x1.FStar_Syntax_Syntax.index); - FStar_Syntax_Syntax.sort = - t12 - }; - FStar_Syntax_Syntax.phi = f1 - }) t12.FStar_Syntax_Syntax.pos in - let uu___10 = - FStar_Syntax_Util.flatten_refinement rhs in - check_relation1 g rel t02 uu___10) + fun ctx01 -> + let uu___10 = uu___9 ctx01 in + match uu___10 with + | Success (x2, g11) -> + let uu___11 = + let uu___12 = + match x2 with + | FStar_Pervasives_Native.None -> + fallback t01 t11 + | FStar_Pervasives_Native.Some + (t02, t12) -> + let rhs = + FStar_Syntax_Syntax.mk + (FStar_Syntax_Syntax.Tm_refine + { + FStar_Syntax_Syntax.b = + { + FStar_Syntax_Syntax.ppname + = + (x1.FStar_Syntax_Syntax.ppname); + FStar_Syntax_Syntax.index + = + (x1.FStar_Syntax_Syntax.index); + FStar_Syntax_Syntax.sort + = t12 + }; + FStar_Syntax_Syntax.phi + = f1 + }) + t12.FStar_Syntax_Syntax.pos in + let uu___13 = + FStar_Syntax_Util.flatten_refinement + rhs in + check_relation1 g rel t02 + uu___13 in + uu___12 ctx01 in + (match uu___11 with + | Success (y, g2) -> + let uu___12 = + let uu___13 = and_pre g11 g2 in + ((), uu___13) in + Success uu___12 + | err1 -> err1) + | Error err1 -> Error err1) | (FStar_Syntax_Syntax.Tm_uinst uu___6, uu___7) -> let head_matches1 = head_matches t01 t11 in let uu___8 = @@ -3038,6 +3188,7 @@ let rec (check_relation : let ctx1 = { no_guard = (ctx.no_guard); + unfolding_ok = (ctx.unfolding_ok); error_context = (("subtype arrow", FStar_Pervasives_Native.None) :: @@ -3183,6 +3334,9 @@ let rec (check_relation : no_guard = (ctx2.no_guard); + unfolding_ok + = + (ctx2.unfolding_ok); error_context = (("check_subcomp", @@ -3314,13 +3468,27 @@ let rec (check_relation : match uu___19 with | Success (x1, g11) -> let uu___20 = - let uu___21 = + let uu___21 ctx = + let ctx1 = + { + no_guard = + (ctx.no_guard); + unfolding_ok = + (ctx.unfolding_ok); + error_context = + (("relate_branch", + FStar_Pervasives_Native.None) + :: + (ctx.error_context)) + } in let uu___22 = - check_relation1 g' - rel body01 - body11 in - with_binders bs0 x1 - uu___22 in + let uu___23 = + check_relation1 + g' rel body01 + body11 in + with_binders bs0 + x1 uu___23 in + uu___22 ctx1 in uu___21 ctx01 in (match uu___20 with | Success (y, g2) -> @@ -3587,6 +3755,7 @@ and (check_subtype : let ctx2 = { no_guard = (ctx1.no_guard); + unfolding_ok = (ctx1.unfolding_ok); error_context = (((if ctx.no_guard then "check_subtype(no_guard)" @@ -3660,6 +3829,7 @@ and (check : let ctx1 = { no_guard = (ctx.no_guard); + unfolding_ok = (ctx.unfolding_ok); error_context = ((msg, (FStar_Pervasives_Native.Some (CtxTerm e))) :: (ctx.error_context)) @@ -3895,6 +4065,7 @@ and (do_check : let ctx1 = { no_guard = (ctx.no_guard); + unfolding_ok = (ctx.unfolding_ok); error_context = (("abs binders", FStar_Pervasives_Native.None) :: (ctx.error_context)) @@ -3950,6 +4121,7 @@ and (do_check : let ctx1 = { no_guard = (ctx.no_guard); + unfolding_ok = (ctx.unfolding_ok); error_context = (("arrow binders", FStar_Pervasives_Native.None) :: (ctx.error_context)) @@ -3966,6 +4138,7 @@ and (do_check : let ctx1 = { no_guard = (ctx.no_guard); + unfolding_ok = (ctx.unfolding_ok); error_context = (("arrow comp", FStar_Pervasives_Native.None) :: @@ -4032,6 +4205,8 @@ and (do_check : let ctx1 = { no_guard = (ctx.no_guard); + unfolding_ok = + (ctx.unfolding_ok); error_context = (("app subtyping", FStar_Pervasives_Native.None) @@ -4054,6 +4229,8 @@ and (do_check : { no_guard = (ctx.no_guard); + unfolding_ok = + (ctx.unfolding_ok); error_context = (("app arg qual", @@ -4204,6 +4381,9 @@ and (do_check : no_guard = (ctx.no_guard); + unfolding_ok + = + (ctx.unfolding_ok); error_context = (("operator arg1", @@ -4325,6 +4505,9 @@ and (do_check : no_guard = (ctx.no_guard); + unfolding_ok + = + (ctx.unfolding_ok); error_context = (("operator arg2", @@ -4544,6 +4727,8 @@ and (do_check : { no_guard = (ctx.no_guard); + unfolding_ok = + (ctx.unfolding_ok); error_context = (("ascription subtyping", FStar_Pervasives_Native.None) @@ -4625,6 +4810,7 @@ and (do_check : let ctx1 = { no_guard = (ctx.no_guard); + unfolding_ok = (ctx.unfolding_ok); error_context = (("ascription comp", FStar_Pervasives_Native.None) :: @@ -4638,11 +4824,22 @@ and (do_check : let uu___10 = let uu___11 = let c_e = as_comp g (eff, te) in - let uu___12 = - check_relation_comp g - (SUBTYPING - (FStar_Pervasives_Native.Some e2)) - c_e c in + let uu___12 ctx = + let ctx1 = + { + no_guard = (ctx.no_guard); + unfolding_ok = (ctx.unfolding_ok); + error_context = + (("ascription subtyping (comp)", + FStar_Pervasives_Native.None) + :: (ctx.error_context)) + } in + let uu___13 = + check_relation_comp g + (SUBTYPING + (FStar_Pervasives_Native.Some + e2)) c_e c in + uu___13 ctx1 in fun ctx02 -> let uu___13 = uu___12 ctx02 in match uu___13 with @@ -4705,8 +4902,8 @@ and (do_check : (match uu___1 with | (g', x1, body1) -> let uu___2 = - FStar_Ident.lid_equals lb.FStar_Syntax_Syntax.lbeff - FStar_Parser_Const.effect_Tot_lid in + FStar_Syntax_Util.is_pure_or_ghost_effect + lb.FStar_Syntax_Syntax.lbeff in if uu___2 then let uu___3 = @@ -4746,6 +4943,9 @@ and (do_check : no_guard = (ctx.no_guard); + unfolding_ok + = + (ctx.unfolding_ok); error_context = (("let subtyping", @@ -4759,7 +4959,8 @@ and (do_check : g (FStar_Pervasives_Native.Some (lb.FStar_Syntax_Syntax.lbdef)) - tdef ttyp in + tdef + lb.FStar_Syntax_Syntax.lbtyp in uu___17 ctx1 in fun ctx03 -> let uu___17 @@ -4962,6 +5163,7 @@ and (do_check : let ctx1 = { no_guard = (ctx.no_guard); + unfolding_ok = (ctx.unfolding_ok); error_context = (("universe_of", (FStar_Pervasives_Native.Some @@ -5044,6 +5246,8 @@ and (do_check : { no_guard = (ctx.no_guard); + unfolding_ok = + (ctx.unfolding_ok); error_context = (("check_pat", FStar_Pervasives_Native.None) @@ -5130,6 +5334,9 @@ and (do_check : no_guard = (ctx.no_guard); + unfolding_ok + = + (ctx.unfolding_ok); error_context = (("branch", @@ -5233,6 +5440,9 @@ and (do_check : no_guard = (ctx.no_guard); + unfolding_ok + = + (ctx.unfolding_ok); error_context = (("check_branch_subtype", @@ -5462,6 +5672,8 @@ and (do_check : let ctx1 = { no_guard = (ctx.no_guard); + unfolding_ok = + (ctx.unfolding_ok); error_context = (("residual type", (FStar_Pervasives_Native.Some @@ -5516,6 +5728,8 @@ and (do_check : { no_guard = (ctx1.no_guard); + unfolding_ok = + (ctx1.unfolding_ok); error_context = (("check_branches", ctx) :: @@ -5598,6 +5812,7 @@ and (do_check : let ctx1 = { no_guard = (ctx.no_guard); + unfolding_ok = (ctx.unfolding_ok); error_context = (("universe_of", (FStar_Pervasives_Native.Some @@ -5764,6 +5979,9 @@ and (do_check : no_guard = (ctx.no_guard); + unfolding_ok + = + (ctx.unfolding_ok); error_context = (("check_pat", @@ -5905,11 +6123,31 @@ and (do_check : (FStar_Pervasives_Native.Some b1) in let uu___36 + ctx = + let ctx1 + = + { + no_guard + = + (ctx.no_guard); + unfolding_ok + = + (ctx.unfolding_ok); + error_context + = + (("branch check relation", + FStar_Pervasives_Native.None) + :: + (ctx.error_context)) + } in + let uu___37 = check_relation g'1 rel tbr expect_tbr in + uu___37 + ctx1 in (fun ctx07 -> let uu___37 @@ -6367,6 +6605,7 @@ and (check_comp : let ctx1 = { no_guard = (ctx.no_guard); + unfolding_ok = (ctx.unfolding_ok); error_context = (("comp fully applied", FStar_Pervasives_Native.None) :: @@ -6501,10 +6740,22 @@ and (check_pat : let uu___3 = match x with | (uu___4, t_const) -> - let uu___5 = - let uu___6 = unrefine_tsc t_sc in - check_subtype g (FStar_Pervasives_Native.Some e) - t_const uu___6 in + let uu___5 ctx = + let ctx1 = + { + no_guard = (ctx.no_guard); + unfolding_ok = (ctx.unfolding_ok); + error_context = + (("check_pat constant", + FStar_Pervasives_Native.None) :: + (ctx.error_context)) + } in + let uu___6 = + let uu___7 = unrefine_tsc t_sc in + check_subtype g + (FStar_Pervasives_Native.Some e) t_const + uu___7 in + uu___6 ctx1 in (fun ctx01 -> let uu___6 = uu___5 ctx01 in match uu___6 with @@ -6544,6 +6795,7 @@ and (check_pat : let ctx1 = { no_guard = (ctx.no_guard); + unfolding_ok = (ctx.unfolding_ok); error_context = (("check_pat_binder", FStar_Pervasives_Native.None) :: (ctx.error_context)) @@ -6654,26 +6906,49 @@ and (check_pat : match x1 with | (uu___16, p_t) -> - (fun ctx02 - -> - let uu___17 + let uu___17 + ctx = + let ctx1 + = + { + no_guard + = + (ctx.no_guard); + unfolding_ok + = + (ctx.unfolding_ok); + error_context + = + (("check_pat cons", + FStar_Pervasives_Native.None) + :: + (ctx.error_context)) + } in + let uu___18 = check_subtype g (FStar_Pervasives_Native.Some x) p_t - expected_t + expected_t in + uu___18 + ctx1 in + (fun ctx02 + -> + let uu___18 + = + uu___17 ctx02 in - match uu___17 + match uu___18 with | Success (x2, g12) -> - let uu___18 - = let uu___19 - uu___20 = + = + let uu___20 + uu___21 = Success ((FStar_List_Tot_Base.op_At ss @@ -6681,24 +6956,24 @@ and (check_pat : FStar_Syntax_Syntax.NT (f, x)]), FStar_Pervasives_Native.None) in - uu___19 + uu___20 ctx02 in - (match uu___18 + (match uu___19 with | Success (y, g2) -> - let uu___19 - = let uu___20 = + let uu___21 + = and_pre g12 g2 in (y, - uu___20) in + uu___21) in Success - uu___19 + uu___20 | err -> err) @@ -7429,6 +7704,7 @@ let (check_term_top : let ctx1 = { no_guard = (ctx.no_guard); + unfolding_ok = (ctx.unfolding_ok); error_context = (("top-level subtyping", FStar_Pervasives_Native.None) :: @@ -7533,6 +7809,7 @@ let (check_term_top_gh : (let ctx = { no_guard = false; + unfolding_ok = true; error_context = [("Top", FStar_Pervasives_Native.None)] } in let res = @@ -7729,80 +8006,101 @@ let (open_binders_in_comp : let uu___ = open_comp_binders g bs c in match uu___ with | (g', bs1, c1) -> ((g'.tcenv), bs1, c1) let (check_term_equality : - FStar_TypeChecker_Env.env -> - FStar_Syntax_Syntax.typ -> - FStar_Syntax_Syntax.typ -> - (FStar_Syntax_Syntax.typ FStar_Pervasives_Native.option, error) - FStar_Pervasives.either) + Prims.bool -> + Prims.bool -> + FStar_TypeChecker_Env.env -> + FStar_Syntax_Syntax.typ -> + FStar_Syntax_Syntax.typ -> + (FStar_Syntax_Syntax.typ FStar_Pervasives_Native.option, + error) FStar_Pervasives.either) = - fun g -> - fun t0 -> - fun t1 -> - let g1 = initial_env g FStar_Pervasives_Native.None in - (let uu___1 = - FStar_TypeChecker_Env.debug g1.tcenv - (FStar_Options.Other "CoreTop") in - if uu___1 - then - let uu___2 = - FStar_Class_Show.show FStar_Syntax_Print.showable_term t0 in - let uu___3 = - FStar_Class_Show.show FStar_Syntax_Print.showable_term t1 in - FStar_Compiler_Util.print2 - "Entering check_term_equality with %s and %s {\n" uu___2 uu___3 - else ()); - (let ctx = - { - no_guard = false; - error_context = [("Eq", FStar_Pervasives_Native.None)] - } in - let r = let uu___1 = check_relation g1 EQUALITY t0 t1 in uu___1 ctx in - (let uu___2 = - FStar_TypeChecker_Env.debug g1.tcenv - (FStar_Options.Other "CoreTop") in - if uu___2 - then - let uu___3 = - FStar_Class_Show.show FStar_Syntax_Print.showable_term t0 in - let uu___4 = - FStar_Class_Show.show FStar_Syntax_Print.showable_term t1 in - let uu___5 = - FStar_Class_Show.show - (showable_result - (FStar_Class_Show.show_tuple2 - (FStar_Class_Show.printableshow - FStar_Class_Printable.printable_unit) - (FStar_Class_Show.show_option - FStar_Syntax_Print.showable_term))) r in - FStar_Compiler_Util.print3 - "} Exiting check_term_equality (%s, %s). Result = %s.\n" uu___3 - uu___4 uu___5 - else ()); - (let r1 = - match r with - | Success (uu___2, g2) -> FStar_Pervasives.Inl g2 - | Error err -> FStar_Pervasives.Inr err in - r1)) + fun guard_ok -> + fun unfolding_ok1 -> + fun g -> + fun t0 -> + fun t1 -> + let g1 = initial_env g FStar_Pervasives_Native.None in + (let uu___1 = + FStar_TypeChecker_Env.debug g1.tcenv + (FStar_Options.Other "CoreTop") in + if uu___1 + then + let uu___2 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t0 in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t1 in + let uu___4 = + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_bool) guard_ok in + let uu___5 = + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_bool) unfolding_ok1 in + FStar_Compiler_Util.print4 + "Entering check_term_equality with %s and %s (guard_ok=%s; unfolding_ok=%s) {\n" + uu___2 uu___3 uu___4 uu___5 + else ()); + (let ctx = + { + no_guard = (Prims.op_Negation guard_ok); + unfolding_ok = unfolding_ok1; + error_context = [("Eq", FStar_Pervasives_Native.None)] + } in + let r = + let uu___1 = check_relation g1 EQUALITY t0 t1 in uu___1 ctx in + (let uu___2 = + FStar_TypeChecker_Env.debug g1.tcenv + (FStar_Options.Other "CoreTop") in + if uu___2 + then + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t0 in + let uu___4 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t1 in + let uu___5 = + FStar_Class_Show.show + (showable_result + (FStar_Class_Show.show_tuple2 + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_unit) + (FStar_Class_Show.show_option + FStar_Syntax_Print.showable_term))) r in + FStar_Compiler_Util.print3 + "} Exiting check_term_equality (%s, %s). Result = %s.\n" + uu___3 uu___4 uu___5 + else ()); + (let r1 = + match r with + | Success (uu___2, g2) -> FStar_Pervasives.Inl g2 + | Error err -> FStar_Pervasives.Inr err in + r1)) let (check_term_subtyping : - FStar_TypeChecker_Env.env -> - FStar_Syntax_Syntax.typ -> - FStar_Syntax_Syntax.typ -> - (FStar_Syntax_Syntax.typ FStar_Pervasives_Native.option, error) - FStar_Pervasives.either) + Prims.bool -> + Prims.bool -> + FStar_TypeChecker_Env.env -> + FStar_Syntax_Syntax.typ -> + FStar_Syntax_Syntax.typ -> + (FStar_Syntax_Syntax.typ FStar_Pervasives_Native.option, + error) FStar_Pervasives.either) = - fun g -> - fun t0 -> - fun t1 -> - let g1 = initial_env g FStar_Pervasives_Native.None in - let ctx = - { - no_guard = false; - error_context = [("Subtyping", FStar_Pervasives_Native.None)] - } in - let uu___ = - let uu___1 = - check_relation g1 (SUBTYPING FStar_Pervasives_Native.None) t0 t1 in - uu___1 ctx in - match uu___ with - | Success (uu___1, g2) -> FStar_Pervasives.Inl g2 - | Error err -> FStar_Pervasives.Inr err \ No newline at end of file + fun guard_ok -> + fun unfolding_ok1 -> + fun g -> + fun t0 -> + fun t1 -> + let g1 = initial_env g FStar_Pervasives_Native.None in + let ctx = + { + no_guard = (Prims.op_Negation guard_ok); + unfolding_ok = unfolding_ok1; + error_context = [("Subtyping", FStar_Pervasives_Native.None)] + } in + let uu___ = + let uu___1 = + check_relation g1 (SUBTYPING FStar_Pervasives_Native.None) t0 + t1 in + uu___1 ctx in + match uu___ with + | Success (uu___1, g2) -> FStar_Pervasives.Inl g2 + | Error err -> FStar_Pervasives.Inr err \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Primops_Base.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Primops_Base.ml index d1342807be4..bb035047116 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Primops_Base.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Primops_Base.ml @@ -1981,4 +1981,303 @@ let mk5' : "arity")) in as_primitive_step_nbecbs true (name, (Prims.of_int (5)), u_arity, - interp, nbe_interp) \ No newline at end of file + interp, nbe_interp) +let mk6' : + 'a 'b 'c 'd 'e 'f 'r 'na 'nb 'nc 'nd 'ne 'nf 'nr . + Prims.int -> + FStar_Ident.lid -> + 'a FStar_Syntax_Embeddings_Base.embedding -> + 'na FStar_TypeChecker_NBETerm.embedding -> + 'b FStar_Syntax_Embeddings_Base.embedding -> + 'nb FStar_TypeChecker_NBETerm.embedding -> + 'c FStar_Syntax_Embeddings_Base.embedding -> + 'nc FStar_TypeChecker_NBETerm.embedding -> + 'd FStar_Syntax_Embeddings_Base.embedding -> + 'nd FStar_TypeChecker_NBETerm.embedding -> + 'e FStar_Syntax_Embeddings_Base.embedding -> + 'ne FStar_TypeChecker_NBETerm.embedding -> + 'f FStar_Syntax_Embeddings_Base.embedding -> + 'nf FStar_TypeChecker_NBETerm.embedding -> + 'r FStar_Syntax_Embeddings_Base.embedding -> + 'nr FStar_TypeChecker_NBETerm.embedding -> + ('a -> + 'b -> + 'c -> + 'd -> + 'e -> + 'f -> + 'r + FStar_Pervasives_Native.option) + -> + ('na -> + 'nb -> + 'nc -> + 'nd -> + 'ne -> + 'nf -> + 'nr + FStar_Pervasives_Native.option) + -> primitive_step + = + fun u_arity -> + fun name -> + fun uu___ -> + fun uu___1 -> + fun uu___2 -> + fun uu___3 -> + fun uu___4 -> + fun uu___5 -> + fun uu___6 -> + fun uu___7 -> + fun uu___8 -> + fun uu___9 -> + fun uu___10 -> + fun uu___11 -> + fun uu___12 -> + fun uu___13 -> + fun ff -> + fun nbe_ff -> + let interp psc1 cb us args = + match args with + | (a1, uu___14)::(b1, uu___15):: + (c1, uu___16)::(d1, uu___17):: + (e1, uu___18)::(f1, uu___19)::[] + -> + Obj.magic + (Obj.repr + (let uu___20 = + let uu___21 = + let uu___22 = + let uu___23 = + let uu___24 = + let uu___25 = + let uu___26 = + try_unembed_simple + uu___ a1 in + Obj.magic + (FStar_Class_Monad.op_Less_Dollar_Greater + FStar_Class_Monad.monad_option + () () + (fun + uu___27 + -> + (Obj.magic + ff) + uu___27) + (Obj.magic + uu___26)) in + let uu___26 = + try_unembed_simple + uu___2 b1 in + Obj.magic + (FStar_Class_Monad.op_Less_Star_Greater + FStar_Class_Monad.monad_option + () () + (Obj.magic + uu___25) + (Obj.magic + uu___26)) in + let uu___25 = + try_unembed_simple + uu___4 c1 in + Obj.magic + (FStar_Class_Monad.op_Less_Star_Greater + FStar_Class_Monad.monad_option + () () + (Obj.magic + uu___24) + (Obj.magic + uu___25)) in + let uu___24 = + try_unembed_simple + uu___6 d1 in + Obj.magic + (FStar_Class_Monad.op_Less_Star_Greater + FStar_Class_Monad.monad_option + () () + (Obj.magic + uu___23) + (Obj.magic + uu___24)) in + let uu___23 = + try_unembed_simple + uu___8 e1 in + Obj.magic + (FStar_Class_Monad.op_Less_Star_Greater + FStar_Class_Monad.monad_option + () () + (Obj.magic uu___22) + (Obj.magic uu___23)) in + let uu___22 = + try_unembed_simple + uu___10 f1 in + Obj.magic + (FStar_Class_Monad.op_Less_Star_Greater + FStar_Class_Monad.monad_option + () () + (Obj.magic uu___21) + (Obj.magic uu___22)) in + FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option + () () (Obj.magic uu___20) + (fun uu___21 -> + (fun r1 -> + let r1 = + Obj.magic r1 in + Obj.magic + (FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option + () () + (Obj.magic r1) + (fun uu___21 + -> + (fun r2 -> + let r2 = + Obj.magic + r2 in + let uu___21 + = + embed_simple + uu___12 + psc1.psc_range + r2 in + Obj.magic + (FStar_Class_Monad.return + FStar_Class_Monad.monad_option + () + (Obj.magic + uu___21))) + uu___21))) + uu___21))) + | uu___14 -> + Obj.magic + (Obj.repr + (FStar_Compiler_Effect.failwith + "arity")) in + let nbe_interp cbs us args = + match args with + | (a1, uu___14)::(b1, uu___15):: + (c1, uu___16)::(d1, uu___17):: + (e1, uu___18)::(f1, uu___19)::[] + -> + Obj.magic + (Obj.repr + (let uu___20 = + let uu___21 = + let uu___22 = + let uu___23 = + let uu___24 = + let uu___25 = + let uu___26 = + FStar_TypeChecker_NBETerm.unembed + (solve + uu___1) + cbs a1 in + Obj.magic + (FStar_Class_Monad.op_Less_Dollar_Greater + FStar_Class_Monad.monad_option + () () + (fun + uu___27 + -> + (Obj.magic + nbe_ff) + uu___27) + (Obj.magic + uu___26)) in + let uu___26 = + FStar_TypeChecker_NBETerm.unembed + (solve uu___3) + cbs b1 in + Obj.magic + (FStar_Class_Monad.op_Less_Star_Greater + FStar_Class_Monad.monad_option + () () + (Obj.magic + uu___25) + (Obj.magic + uu___26)) in + let uu___25 = + FStar_TypeChecker_NBETerm.unembed + (solve uu___5) + cbs c1 in + Obj.magic + (FStar_Class_Monad.op_Less_Star_Greater + FStar_Class_Monad.monad_option + () () + (Obj.magic + uu___24) + (Obj.magic + uu___25)) in + let uu___24 = + FStar_TypeChecker_NBETerm.unembed + (solve uu___7) + cbs d1 in + Obj.magic + (FStar_Class_Monad.op_Less_Star_Greater + FStar_Class_Monad.monad_option + () () + (Obj.magic + uu___23) + (Obj.magic + uu___24)) in + let uu___23 = + FStar_TypeChecker_NBETerm.unembed + (solve uu___9) cbs + e1 in + Obj.magic + (FStar_Class_Monad.op_Less_Star_Greater + FStar_Class_Monad.monad_option + () () + (Obj.magic uu___22) + (Obj.magic uu___23)) in + let uu___22 = + FStar_TypeChecker_NBETerm.unembed + (solve uu___11) cbs + f1 in + Obj.magic + (FStar_Class_Monad.op_Less_Star_Greater + FStar_Class_Monad.monad_option + () () + (Obj.magic uu___21) + (Obj.magic uu___22)) in + FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option + () () (Obj.magic uu___20) + (fun uu___21 -> + (fun r1 -> + let r1 = + Obj.magic r1 in + Obj.magic + (FStar_Class_Monad.op_let_Bang + FStar_Class_Monad.monad_option + () () + (Obj.magic r1) + (fun uu___21 + -> + (fun r2 -> + let r2 = + Obj.magic + r2 in + let uu___21 + = + FStar_TypeChecker_NBETerm.embed + (solve + uu___13) + cbs r2 in + Obj.magic + (FStar_Class_Monad.return + FStar_Class_Monad.monad_option + () + (Obj.magic + uu___21))) + uu___21))) + uu___21))) + | uu___14 -> + Obj.magic + (Obj.repr + (FStar_Compiler_Effect.failwith + "arity")) in + as_primitive_step_nbecbs true + (name, (Prims.of_int (6)), u_arity, + interp, nbe_interp) \ No newline at end of file diff --git a/ocaml/fstar-tests/generated/FStar_Tests_Unif.ml b/ocaml/fstar-tests/generated/FStar_Tests_Unif.ml index 64fefa85358..5ea2b133be9 100644 --- a/ocaml/fstar-tests/generated/FStar_Tests_Unif.ml +++ b/ocaml/fstar-tests/generated/FStar_Tests_Unif.ml @@ -155,8 +155,11 @@ let (check_core : (let env = tcenv () in let res = if subtyping - then FStar_TypeChecker_Core.check_term_subtyping env x y - else FStar_TypeChecker_Core.check_term_equality env x y in + then + FStar_TypeChecker_Core.check_term_subtyping true true env x + y + else + FStar_TypeChecker_Core.check_term_equality true true env x y in (match res with | FStar_Pervasives.Inl (FStar_Pervasives_Native.None) -> let uu___2 = FStar_Compiler_Util.string_of_int i in diff --git a/src/tactics/FStar.Tactics.InterpFuns.fst b/src/tactics/FStar.Tactics.InterpFuns.fst index 84a64884c12..3bedc1a9ed5 100644 --- a/src/tactics/FStar.Tactics.InterpFuns.fst +++ b/src/tactics/FStar.Tactics.InterpFuns.fst @@ -103,6 +103,13 @@ let mk_tac_step_4 univ_arity nm f nbe_f : PO.primitive_step = (fun a b c d ps -> Some (run_wrap nm (f a b c d) ps)) (fun a b c d ps -> Some (run_wrap nm (nbe_f a b c d) ps)) +let mk_tac_step_5 univ_arity nm f nbe_f : PO.primitive_step = + let lid = builtin_lid nm in + set_auto_reflect 5 <| + PO.mk6' univ_arity lid + (fun a b c d e ps -> Some (run_wrap nm (f a b c d e) ps)) + (fun a b c d e ps -> Some (run_wrap nm (nbe_f a b c d e) ps)) + let max_tac_arity = 20 (* NOTE: THE REST OF THIS MODULE IS AUTOGENERATED diff --git a/src/tactics/FStar.Tactics.InterpFuns.fsti b/src/tactics/FStar.Tactics.InterpFuns.fsti index f22c51f0203..a1d40c37d64 100644 --- a/src/tactics/FStar.Tactics.InterpFuns.fsti +++ b/src/tactics/FStar.Tactics.InterpFuns.fsti @@ -127,3 +127,22 @@ val mk_tac_step_4 : ('t1 -> 't2 -> 't3 -> 't4 -> tac 'res) -> ('nt1 -> 'nt2 -> 'nt3 -> 'nt4 -> tac 'nres) -> PO.primitive_step + +val mk_tac_step_5 : + univ_arity:int -> + string -> + {| embedding 't1 |} -> + {| embedding 't2 |} -> + {| embedding 't3 |} -> + {| embedding 't4 |} -> + {| embedding 't5 |} -> + {| embedding 'res |} -> + {| NBET.embedding 'nt1 |} -> + {| NBET.embedding 'nt2 |} -> + {| NBET.embedding 'nt3 |} -> + {| NBET.embedding 'nt4 |} -> + {| NBET.embedding 'nt5 |} -> + {| NBET.embedding 'nres |} -> + ('t1 -> 't2 -> 't3 -> 't4 -> 't5 -> tac 'res) -> + ('nt1 -> 'nt2 -> 'nt3 -> 'nt4 -> 'nt5 -> tac 'nres) -> + PO.primitive_step diff --git a/src/tactics/FStar.Tactics.V1.Basic.fst b/src/tactics/FStar.Tactics.V1.Basic.fst index fd20fc9a57d..bfdff0c017c 100644 --- a/src/tactics/FStar.Tactics.V1.Basic.fst +++ b/src/tactics/FStar.Tactics.V1.Basic.fst @@ -1423,7 +1423,7 @@ let _t_trefl (allow_guards:bool) (l : term) (r : term) : tac unit = with | Inr _ -> false | Inl (_, t_ty) -> ( // ignoring the effect, ghost is ok - match Core.check_term_subtyping env ty t_ty with + match Core.check_term_subtyping true true env ty t_ty with | Inl None -> //unconditional subtype mark_uvar_as_already_checked u; true diff --git a/src/tactics/FStar.Tactics.V2.Basic.fst b/src/tactics/FStar.Tactics.V2.Basic.fst index 054f886ecbd..9b885c41bc5 100644 --- a/src/tactics/FStar.Tactics.V2.Basic.fst +++ b/src/tactics/FStar.Tactics.V2.Basic.fst @@ -1426,7 +1426,7 @@ let _t_trefl (allow_guards:bool) (l : term) (r : term) : tac unit = with | Inr _ -> false | Inl (_, t_ty) -> ( // ignoring effect, ghost is ok - match Core.check_term_subtyping env ty t_ty with + match Core.check_term_subtyping true true env ty t_ty with | Inl None -> //unconditional subtype mark_uvar_as_already_checked u; true @@ -2268,7 +2268,7 @@ let refl_is_non_informative (g:env) (t:typ) : tac (option unit & issues) = return (None, [unexpected_uvars_issue (Env.get_range g)]) ) -let refl_check_relation (g:env) (t0 t1:typ) (rel:relation) +let refl_check_relation (rel:relation) (smt_ok:bool) (unfolding_ok:bool) (g:env) (t0 t1:typ) : tac (option unit * issues) = if no_uvars_in_g g && @@ -2285,7 +2285,7 @@ let refl_check_relation (g:env) (t0 t1:typ) (rel:relation) if rel = Subtyping then Core.check_term_subtyping else Core.check_term_equality in - match f g t0 t1 with + match f smt_ok unfolding_ok g t0 t1 with | Inl None -> dbg_refl g (fun _ -> "refl_check_relation: succeeded (no guard)"); ((), []) @@ -2301,10 +2301,9 @@ let refl_check_relation (g:env) (t0 t1:typ) (rel:relation) ) let refl_check_subtyping (g:env) (t0 t1:typ) : tac (option unit & issues) = - refl_check_relation g t0 t1 Subtyping + refl_check_relation Subtyping true true g t0 t1 -let refl_check_equiv (g:env) (t0 t1:typ) : tac (option unit & issues) = - refl_check_relation g t0 t1 Equality +let t_refl_check_equiv = refl_check_relation Equality let to_must_tot (eff:Core.tot_or_ghost) : bool = match eff with diff --git a/src/tactics/FStar.Tactics.V2.Basic.fsti b/src/tactics/FStar.Tactics.V2.Basic.fsti index e0a2308c80d..ae3379cc5ce 100644 --- a/src/tactics/FStar.Tactics.V2.Basic.fsti +++ b/src/tactics/FStar.Tactics.V2.Basic.fsti @@ -127,7 +127,7 @@ val write : tref 'a -> 'a -> tac unit let issues = list FStar.Errors.issue val refl_is_non_informative : env -> typ -> tac (option unit & issues) val refl_check_subtyping : env -> typ -> typ -> tac (option unit & issues) -val refl_check_equiv : env -> typ -> typ -> tac (option unit & issues) +val t_refl_check_equiv : smt_ok:bool -> unfolding_ok:bool -> env -> typ -> typ -> tac (option unit & issues) val refl_core_compute_term_type : env -> term -> tac (option (Core.tot_or_ghost & typ) & issues) val refl_core_check_term : env -> term -> typ -> Core.tot_or_ghost -> tac (option unit & issues) val refl_core_check_term_at_type : env -> term -> typ -> tac (option Core.tot_or_ghost & issues) diff --git a/src/tactics/FStar.Tactics.V2.Primops.fst b/src/tactics/FStar.Tactics.V2.Primops.fst index bfc652203ac..cff3bb45cc6 100644 --- a/src/tactics/FStar.Tactics.V2.Primops.fst +++ b/src/tactics/FStar.Tactics.V2.Primops.fst @@ -90,8 +90,8 @@ let ops = [ mk_tot_step_1 0 "goals_of" goals_of goals_of; mk_tot_step_1 0 "smt_goals_of" smt_goals_of smt_goals_of; mk_tot_step_1 0 "goal_env" goal_env goal_env; - mk_tot_step_1 0 "goal_type" #_ #RE.e_term goal_type goal_type; - mk_tot_step_1 0 "goal_witness" #_ #RE.e_term goal_witness goal_witness; + mk_tot_step_1 0 "goal_type" goal_type goal_type; + mk_tot_step_1 0 "goal_witness" goal_witness goal_witness; mk_tot_step_1 0 "is_guard" is_guard is_guard; mk_tot_step_1 0 "get_label" get_label get_label; mk_tot_step_2 0 "set_label" set_label set_label; @@ -100,7 +100,7 @@ let ops = [ unseal_step; - mk_tac_step_1 0 "compress" #RE.e_term #RE.e_term compress compress; + mk_tac_step_1 0 "compress" compress compress; mk_tac_step_1 0 "set_goals" set_goals set_goals; mk_tac_step_1 0 "set_smt_goals" set_smt_goals set_smt_goals; @@ -119,7 +119,7 @@ let ops = [ mk_tac_step_1 0 "intro" intro intro; mk_tac_step_1 0 "intro_rec" intro_rec intro_rec; mk_tac_step_1 0 "norm" norm norm; - mk_tac_step_3 0 "norm_term_env" #_ #_ #RE.e_term #RE.e_term norm_term_env norm_term_env; + mk_tac_step_3 0 "norm_term_env" norm_term_env norm_term_env; mk_tac_step_2 0 "norm_binding_type" norm_binding_type norm_binding_type; mk_tac_step_2 0 "rename_to" rename_to rename_to; mk_tac_step_1 0 "var_retype" var_retype var_retype; @@ -128,13 +128,13 @@ let ops = [ mk_tac_step_1 0 "clear" clear clear; mk_tac_step_1 0 "rewrite" rewrite rewrite; mk_tac_step_1 0 "refine_intro" refine_intro refine_intro; - mk_tac_step_3 0 "t_exact" #_ #_ #RE.e_term t_exact t_exact; - mk_tac_step_4 0 "t_apply" #_ #_ #_ #RE.e_term t_apply t_apply; - mk_tac_step_3 0 "t_apply_lemma" #_ #_ #RE.e_term t_apply_lemma t_apply_lemma; + mk_tac_step_3 0 "t_exact" t_exact t_exact; + mk_tac_step_4 0 "t_apply" t_apply t_apply; + mk_tac_step_3 0 "t_apply_lemma" t_apply_lemma t_apply_lemma; mk_tac_step_1 0 "set_options" set_options set_options; - mk_tac_step_2 0 "tcc" #_ #RE.e_term tcc tcc; - mk_tac_step_2 0 "tc" #_ #RE.e_term #RE.e_term tc tc; - mk_tac_step_1 0 "unshelve" #RE.e_term unshelve unshelve; + mk_tac_step_2 0 "tcc" tcc tcc; + mk_tac_step_2 0 "tc" tc tc; + mk_tac_step_1 0 "unshelve" unshelve unshelve; mk_tac_step_2 1 "unquote" #e_any #RE.e_term #e_any @@ -162,20 +162,20 @@ let ops = [ mk_tac_step_1 0 "t_trefl" t_trefl t_trefl; mk_tac_step_1 0 "dup" dup dup; - mk_tac_step_1 0 "tadmit_t" #RE.e_term tadmit_t tadmit_t; + mk_tac_step_1 0 "tadmit_t" tadmit_t tadmit_t; mk_tac_step_1 0 "join" join join; - mk_tac_step_1 0 "t_destruct" #RE.e_term t_destruct t_destruct; + mk_tac_step_1 0 "t_destruct" t_destruct t_destruct; mk_tac_step_1 0 "top_env" top_env top_env; mk_tac_step_1 0 "fresh" fresh fresh; mk_tac_step_1 0 "curms" curms curms; - mk_tac_step_2 0 "uvar_env" #_ #(e_option RE.e_term) #RE.e_term uvar_env uvar_env; - mk_tac_step_2 0 "ghost_uvar_env" #_ #RE.e_term #RE.e_term ghost_uvar_env ghost_uvar_env; - mk_tac_step_1 0 "fresh_universe_uvar" #_ #RE.e_term fresh_universe_uvar fresh_universe_uvar; - mk_tac_step_3 0 "unify_env" #_ #RE.e_term #RE.e_term unify_env unify_env; - mk_tac_step_3 0 "unify_guard_env" #_ #RE.e_term #RE.e_term unify_guard_env unify_guard_env; - mk_tac_step_3 0 "match_env" #_ #RE.e_term #RE.e_term match_env match_env; + mk_tac_step_2 0 "uvar_env" uvar_env uvar_env; + mk_tac_step_2 0 "ghost_uvar_env" ghost_uvar_env ghost_uvar_env; + mk_tac_step_1 0 "fresh_universe_uvar" fresh_universe_uvar fresh_universe_uvar; + mk_tac_step_3 0 "unify_env" unify_env unify_env; + mk_tac_step_3 0 "unify_guard_env" unify_guard_env unify_guard_env; + mk_tac_step_3 0 "match_env" match_env match_env; mk_tac_step_3 0 "launch_process" launch_process launch_process; - mk_tac_step_1 0 "change" #RE.e_term change change; + mk_tac_step_1 0 "change" change change; mk_tac_step_1 0 "get_guard_policy" get_guard_policy get_guard_policy; mk_tac_step_1 0 "set_guard_policy" set_guard_policy set_guard_policy; mk_tac_step_1 0 "lax_on" lax_on lax_on; @@ -197,14 +197,14 @@ let ops = [ mk_tac_step_1 0 "gather_or_solve_explicit_guards_for_resolved_goals" gather_explicit_guards_for_resolved_goals gather_explicit_guards_for_resolved_goals; - mk_tac_step_2 0 "string_to_term" #_ #_ #RE.e_term string_to_term string_to_term; + mk_tac_step_2 0 "string_to_term" string_to_term string_to_term; mk_tac_step_2 0 "push_bv_dsenv" push_bv_dsenv push_bv_dsenv; - mk_tac_step_1 0 "term_to_string" #RE.e_term term_to_string term_to_string; + mk_tac_step_1 0 "term_to_string" term_to_string term_to_string; mk_tac_step_1 0 "comp_to_string" comp_to_string comp_to_string; - mk_tac_step_1 0 "term_to_doc" #RE.e_term term_to_doc term_to_doc; + mk_tac_step_1 0 "term_to_doc" term_to_doc term_to_doc; mk_tac_step_1 0 "comp_to_doc" comp_to_doc comp_to_doc; mk_tac_step_1 0 "range_to_string" range_to_string range_to_string; - mk_tac_step_2 0 "term_eq_old" #RE.e_term #RE.e_term term_eq_old term_eq_old; + mk_tac_step_2 0 "term_eq_old" term_eq_old term_eq_old; mk_tac_step_3 1 "with_compat_pre_core" #e_any #e_int #(TI.e_tactic_thunk e_any) #e_any @@ -215,7 +215,7 @@ let ops = [ mk_tac_step_1 0 "get_vconfig" get_vconfig get_vconfig; mk_tac_step_1 0 "set_vconfig" set_vconfig set_vconfig; mk_tac_step_1 0 "t_smt_sync" t_smt_sync t_smt_sync; - mk_tac_step_1 0 "free_uvars" #RE.e_term free_uvars free_uvars; + mk_tac_step_1 0 "free_uvars" free_uvars free_uvars; mk_tac_step_1 0 "all_ext_options" all_ext_options all_ext_options; mk_tac_step_1 0 "ext_getv" ext_getv ext_getv; mk_tac_step_1 0 "ext_getns" ext_getns ext_getns; @@ -240,23 +240,23 @@ let ops = [ // reflection typechecker callbacks (part of the DSL framework) - mk_tac_step_2 0 "is_non_informative" #_ #RE.e_term refl_is_non_informative refl_is_non_informative; - mk_tac_step_3 0 "check_subtyping" #_ #RE.e_term #RE.e_term refl_check_subtyping refl_check_subtyping; - mk_tac_step_3 0 "check_equiv" #_ #RE.e_term #RE.e_term refl_check_equiv refl_check_equiv; - mk_tac_step_2 0 "core_compute_term_type" #_ #RE.e_term #(e_ret_t (e_tuple2 solve RE.e_term)) refl_core_compute_term_type refl_core_compute_term_type; - mk_tac_step_4 0 "core_check_term" #_ #RE.e_term #RE.e_term refl_core_check_term refl_core_check_term; - mk_tac_step_3 0 "core_check_term_at_type" #_ #RE.e_term #RE.e_term refl_core_check_term_at_type refl_core_check_term_at_type; - mk_tac_step_2 0 "tc_term" #_ #RE.e_term #(e_ret_t (e_tuple2 RE.e_term (e_tuple2 solve RE.e_term))) refl_tc_term refl_tc_term; - mk_tac_step_2 0 "universe_of" #_ #RE.e_term refl_universe_of refl_universe_of; - mk_tac_step_2 0 "check_prop_validity" #_ #RE.e_term refl_check_prop_validity refl_check_prop_validity; - mk_tac_step_4 0 "check_match_complete" #_ #RE.e_term #RE.e_term refl_check_match_complete refl_check_match_complete; + mk_tac_step_2 0 "is_non_informative" refl_is_non_informative refl_is_non_informative; + mk_tac_step_3 0 "check_subtyping" refl_check_subtyping refl_check_subtyping; + mk_tac_step_5 0 "t_check_equiv" t_refl_check_equiv t_refl_check_equiv; + mk_tac_step_2 0 "core_compute_term_type" refl_core_compute_term_type refl_core_compute_term_type; + mk_tac_step_4 0 "core_check_term" refl_core_check_term refl_core_check_term; + mk_tac_step_3 0 "core_check_term_at_type" refl_core_check_term_at_type refl_core_check_term_at_type; + mk_tac_step_2 0 "tc_term" refl_tc_term refl_tc_term; + mk_tac_step_2 0 "universe_of" refl_universe_of refl_universe_of; + mk_tac_step_2 0 "check_prop_validity" refl_check_prop_validity refl_check_prop_validity; + mk_tac_step_4 0 "check_match_complete" refl_check_match_complete refl_check_match_complete; mk_tac_step_2 0 "instantiate_implicits" #_ #_ #(e_ret_t (e_tuple3 (e_list (e_tuple2 RE.e_namedv solve)) solve solve)) #_ #_ #(nbe_e_ret_t (NBET.e_tuple3 (NBET.e_list (NBET.e_tuple2 NRE.e_namedv solve)) solve solve)) refl_instantiate_implicits refl_instantiate_implicits; mk_tac_step_4 0 "try_unify" - #RE.e_env #(e_list (e_tuple2 RE.e_namedv RE.e_term)) #RE.e_term #RE.e_term #(e_ret_t (e_list (e_tuple2 RE.e_namedv RE.e_term))) - #NRE.e_env #(NBET.e_list (NBET.e_tuple2 NRE.e_namedv NRE.e_term)) #NRE.e_term #NRE.e_term #(nbe_e_ret_t (NBET.e_list (NBET.e_tuple2 NRE.e_namedv NRE.e_term))) + #_ #(e_list (e_tuple2 RE.e_namedv RE.e_term)) #_ #_ #(e_ret_t (e_list (e_tuple2 RE.e_namedv RE.e_term))) + #_ #(NBET.e_list (NBET.e_tuple2 NRE.e_namedv NRE.e_term)) #_ #_ #(nbe_e_ret_t (NBET.e_list (NBET.e_tuple2 NRE.e_namedv NRE.e_term))) refl_try_unify refl_try_unify; mk_tac_step_3 0 "maybe_relate_after_unfolding" refl_maybe_relate_after_unfolding refl_maybe_relate_after_unfolding; mk_tac_step_2 0 "maybe_unfold_head" refl_maybe_unfold_head refl_maybe_unfold_head; diff --git a/src/tests/FStar.Tests.Unif.fst b/src/tests/FStar.Tests.Unif.fst index 570d2344380..a6fe86d36c6 100644 --- a/src/tests/FStar.Tests.Unif.fst +++ b/src/tests/FStar.Tests.Unif.fst @@ -96,8 +96,8 @@ let check_core i subtyping guard_ok x y = let env = tcenv () in let res = if subtyping - then FStar.TypeChecker.Core.check_term_subtyping env x y - else FStar.TypeChecker.Core.check_term_equality env x y + then FStar.TypeChecker.Core.check_term_subtyping true true env x y + else FStar.TypeChecker.Core.check_term_equality true true env x y in let _ = match res with diff --git a/src/typechecker/FStar.TypeChecker.Core.fst b/src/typechecker/FStar.TypeChecker.Core.fst index ee59a716f2b..237e0494493 100644 --- a/src/typechecker/FStar.TypeChecker.Core.fst +++ b/src/typechecker/FStar.TypeChecker.Core.fst @@ -163,14 +163,16 @@ let context_term_to_string (c:context_term) = type context = { no_guard : bool; + unfolding_ok : bool; error_context: list (string & option context_term) } (* The instance prints some brief info on the error_context. `print_context` below is a full printer. *) instance showable_context : showable context = { - show = (fun context -> BU.format2 "{no_guard=%s, error_context=%s}" + show = (fun context -> BU.format3 "{no_guard=%s; unfolding_ok=%s; error_context=%s}" (show context.no_guard) + (show context.unfolding_ok) (show (List.map fst context.error_context))); } @@ -691,6 +693,10 @@ let guard_not_allowed : result bool = fun ctx -> Success (ctx.no_guard, None) +let unfolding_ok + : result bool + = fun ctx -> Success (ctx.unfolding_ok, None) + let debug g f = if Env.debug g.tcenv (Options.Other "Core") then f () @@ -830,11 +836,13 @@ let rec check_relation (g:env) (rel:relation) (t0 t1:typ) "FStar.TypeChecker.Core.maybe_unfold_side" in let maybe_unfold t0 t1 - : option (term & term) - = maybe_unfold_side (which_side_to_unfold t0 t1) t0 t1 + : result (option (term & term)) + = if! unfolding_ok + then return (maybe_unfold_side (which_side_to_unfold t0 t1) t0 t1) + else return None in let emit_guard t0 t1 = - let! _, t_typ = do_check g t0 in + let! _, t_typ = with_context "checking lhs while emitting guard" None (fun _ -> do_check g t0) in let! u = universe_of g t_typ in guard (U.mk_eq2 u t_typ t0 t1) in @@ -847,29 +855,22 @@ let rec check_relation (g:env) (rel:relation) (t0 t1:typ) else err () in let maybe_unfold_side_and_retry side t0 t1 = - match maybe_unfold_side side t0 t1 with - | None -> fallback t0 t1 - | Some (t0, t1) -> check_relation g rel t0 t1 + if! unfolding_ok then + match maybe_unfold_side side t0 t1 with + | None -> fallback t0 t1 + | Some (t0, t1) -> check_relation g rel t0 t1 + else + fallback t0 t1 in let maybe_unfold_and_retry t0 t1 = maybe_unfold_side_and_retry (which_side_to_unfold t0 t1) t0 t1 in let beta_iota_reduce t = let t = Subst.compress t in + let t = N.normalize [Env.HNF; Env.Weak; Env.Beta; Env.Iota; Env.Primops] g.tcenv t in match t.n with - | Tm_app _ -> - let head = U.leftmost_head t in - (match (Subst.compress head).n with - | Tm_abs _ -> N.normalize [Env.Beta; Env.Iota; Env.Primops] g.tcenv t - | _ -> t) - - | Tm_let _ - | Tm_match _ -> - N.normalize [Env.Beta;Env.Iota;Env.Primops] g.tcenv t - | Tm_refine _ -> U.flatten_refinement t - | _ -> t in let beta_iota_reduce t = @@ -948,8 +949,11 @@ let rec check_relation (g:env) (rel:relation) (t0 t1:typ) guard (U.mk_forall u b.binder_bv (U.mk_imp f0 f1))) ) else ( - match maybe_unfold x0.sort x1.sort with - | None -> fallback t0 t1 + match! maybe_unfold x0.sort x1.sort with + | None -> + if Env.debug g.tcenv (Options.Other "Core") then + BU.print2 "Cannot match ref heads %s and %s\n" (show x0.sort) (show x1.sort); + fallback t0 t1 | Some (t0, t1) -> let lhs = S.mk (Tm_refine {b={x0 with sort = t0}; phi=f0}) t0.pos in let rhs = S.mk (Tm_refine {b={x1 with sort = t1}; phi=f1}) t1.pos in @@ -960,7 +964,7 @@ let rec check_relation (g:env) (rel:relation) (t0 t1:typ) if head_matches x0.sort t1 then check_relation g rel x0.sort t1 else ( - match maybe_unfold x0.sort t1 with + match! maybe_unfold x0.sort t1 with | None -> fallback t0 t1 | Some (t0, t1) -> let lhs = S.mk (Tm_refine {b={x0 with sort = t0}; phi=f0}) t0.pos in @@ -994,7 +998,7 @@ let rec check_relation (g:env) (rel:relation) (t0 t1:typ) guard (U.mk_forall u1 b1.binder_bv f1) ) else ( - match maybe_unfold t0 x1.sort with + match! maybe_unfold t0 x1.sort with | None -> fallback t0 t1 | Some (t0, t1) -> let rhs = S.mk (Tm_refine {b={x1 with sort = t1}; phi=f1}) t1.pos in @@ -1104,7 +1108,7 @@ let rec check_relation (g:env) (rel:relation) (t0 t1:typ) let bs0 = List.map S.mk_binder bvs0 in // We need universes for the binders let! us = check_binders g bs0 in - with_binders bs0 us (check_relation g' rel body0 body1) + with_context "relate_branch" None (fun _ -> with_binders bs0 us (check_relation g' rel body0 body1)) | _ -> fail "raw_pat_as_exp failed in check_equality match rule" end | _ -> fail "Core does not support branches with when" @@ -1374,7 +1378,7 @@ and do_check (g:env) (e:term) let! eff, te = check "ascription head" g e in let! _ = with_context "ascription comp" None (fun _ -> check_comp g c) in let c_e = as_comp g (eff, te) in - check_relation_comp g (SUBTYPING (Some e)) c_e c;! + with_context "ascription subtyping (comp)" None (fun _ -> check_relation_comp g (SUBTYPING (Some e)) c_e c);! let Some (eff, t) = comp_as_tot_or_ghost_and_type c in return (eff, t) ) @@ -1383,12 +1387,12 @@ and do_check (g:env) (e:term) | Tm_let {lbs=(false, [lb]); body} -> let Inl x = lb.lbname in let g', x, body = open_term g (S.mk_binder x) body in - if I.lid_equals lb.lbeff PC.effect_Tot_lid + if U.is_pure_or_ghost_effect lb.lbeff then ( let! eff_def, tdef = check "let definition" g lb.lbdef in let! _, ttyp = check "let type" g lb.lbtyp in let! u = is_type g ttyp in - with_context "let subtyping" None (fun _ -> check_subtype g (Some lb.lbdef) tdef ttyp) ;! + with_context "let subtyping" None (fun _ -> check_subtype g (Some lb.lbdef) tdef lb.lbtyp) ;! with_definition x u lb.lbdef ( let! eff_body, t = check "let body" g' body in check_no_escape [x] t;! @@ -1523,7 +1527,7 @@ and do_check (g:env) (e:term) then EQUALITY else SUBTYPING (Some b) in - check_relation g' rel tbr expect_tbr;! + with_context "branch check relation" None (fun _ -> check_relation g' rel tbr expect_tbr);! return (join_eff eff_br acc_eff, expect_tbr))) in match p.v with | Pat_var _ -> @@ -1615,7 +1619,7 @@ and check_pat (g:env) (p:pat) (t_sc:typ) : result (binders & universes) = | _ -> mk (Tm_constant c) p.p in let! _, t_const = check "pat_const" g e in - let! _ = check_subtype g (Some e) t_const (unrefine_tsc t_sc) in + let! _ = with_context "check_pat constant" None (fun () -> check_subtype g (Some e) t_const (unrefine_tsc t_sc)) in return ([], []) | Pat_var bv -> @@ -1649,7 +1653,7 @@ and check_pat (g:env) (p:pat) (t_sc:typ) : result (binders & universes) = | _ -> fail "check_pat in core has unset dot pattern" in let! _, p_t = check "pat dot term" g pat_dot_t in - let!_ = check_subtype g (Some pat_dot_t) p_t expected_t in + let!_ = with_context "check_pat cons" None (fun _ -> check_subtype g (Some pat_dot_t) p_t expected_t) in return (ss@[NT (f, pat_dot_t)])) [] dot_formals dot_pats in @@ -1855,7 +1859,7 @@ let check_term_top_gh g e topt (must_tot:bool) (gh:option guard_handler_t) (match topt with None -> "" | Some t -> P.term_to_string t); THT.reset_counters table; reset_cache_stats(); - let ctx = { no_guard = false; error_context = [("Top", None)] } in + let ctx = { unfolding_ok = true; no_guard = false; error_context = [("Top", None)] } in let res = Profiling.profile (fun () -> @@ -1946,11 +1950,12 @@ let open_binders_in_comp (env:Env.env) (bs:binders) (c:comp) = let g', bs, c = open_comp_binders g bs c in g'.tcenv, bs, c -let check_term_equality g t0 t1 +let check_term_equality guard_ok unfolding_ok g t0 t1 = let g = initial_env g None in if Env.debug g.tcenv (Options.Other "CoreTop") then - BU.print2 "Entering check_term_equality with %s and %s {\n" (show t0) (show t1); - let ctx = { no_guard = false ; error_context = [("Eq", None)] } in + BU.print4 "Entering check_term_equality with %s and %s (guard_ok=%s; unfolding_ok=%s) {\n" + (show t0) (show t1) (show guard_ok) (show unfolding_ok); + let ctx = { unfolding_ok = unfolding_ok; no_guard = not guard_ok; error_context = [("Eq", None)] } in let r = check_relation g EQUALITY t0 t1 ctx in if Env.debug g.tcenv (Options.Other "CoreTop") then BU.print3 "} Exiting check_term_equality (%s, %s). Result = %s.\n" (show t0) (show t1) (show r); @@ -1961,9 +1966,9 @@ let check_term_equality g t0 t1 in r -let check_term_subtyping g t0 t1 +let check_term_subtyping guard_ok unfolding_ok g t0 t1 = let g = initial_env g None in - let ctx = { no_guard = false; error_context = [("Subtyping", None)] } in + let ctx = { unfolding_ok = unfolding_ok; no_guard = not guard_ok; error_context = [("Subtyping", None)] } in match check_relation g (SUBTYPING None) t0 t1 ctx with | Success (_, g) -> Inl g | Error err -> Inr err diff --git a/src/typechecker/FStar.TypeChecker.Core.fsti b/src/typechecker/FStar.TypeChecker.Core.fsti index 9d2e3432609..6f05e4fa321 100644 --- a/src/typechecker/FStar.TypeChecker.Core.fsti +++ b/src/typechecker/FStar.TypeChecker.Core.fsti @@ -43,11 +43,11 @@ val open_binders_in_term (g:Env.env) (bs:binders) (t:term) val open_binders_in_comp (g:Env.env) (bs:binders) (c:comp) : Env.env & binders & comp -(* for unit testing *) -val check_term_equality (g:Env.env) (t0 t1:typ) +(* For unit testing, and exposed to tactics *) +val check_term_equality (guard_ok:bool) (unfolding_ok:bool) (g:Env.env) (t0 t1:typ) : either (option typ) error -val check_term_subtyping (g:Env.env) (t0 t1:typ) +val check_term_subtyping (guard_ok:bool) (unfolding_ok:bool) (g:Env.env) (t0 t1:typ) : either (option typ) error val print_error (err:error) diff --git a/src/typechecker/FStar.TypeChecker.Primops.Base.fst b/src/typechecker/FStar.TypeChecker.Primops.Base.fst index 0ebe55d5c31..14efd9337f2 100644 --- a/src/typechecker/FStar.TypeChecker.Primops.Base.fst +++ b/src/typechecker/FStar.TypeChecker.Primops.Base.fst @@ -424,3 +424,36 @@ let mk5' #a #b #c #d #e #r #na #nb #nc #nd #ne #nr | _ -> failwith "arity" in as_primitive_step_nbecbs true (name, 5, u_arity, interp, nbe_interp) + +let mk6' #a #b #c #d #e #f #r #na #nb #nc #nd #ne #nf #nr + (u_arity : int) + (name : Ident.lid) + {| EMB.embedding a |} {| NBE.embedding na |} + {| EMB.embedding b |} {| NBE.embedding nb |} + {| EMB.embedding c |} {| NBE.embedding nc |} + {| EMB.embedding d |} {| NBE.embedding nd |} + {| EMB.embedding e |} {| NBE.embedding ne |} + {| EMB.embedding f |} {| NBE.embedding nf |} + {| EMB.embedding r |} {| NBE.embedding nr |} + (ff : a -> b -> c -> d -> e -> f -> option r) + (nbe_ff : na -> nb -> nc -> nd -> ne -> nf -> option nr) + : primitive_step = + let interp : interp_t = + fun psc cb us args -> + match args with + | [(a, _); (b, _); (c, _); (d, _); (e, _); (f, _)] -> + let! r = ff <$> try_unembed_simple a <*> try_unembed_simple b <*> try_unembed_simple c <*> try_unembed_simple d <*> try_unembed_simple e <*> try_unembed_simple f in + let! r = r in + return (embed_simple psc.psc_range r) + | _ -> failwith "arity" + in + let nbe_interp : nbe_interp_t = + fun cbs us args -> + match args with + | [(a, _); (b, _); (c, _); (d, _); (e, _); (f, _)] -> + let! r = nbe_ff <$> NBE.unembed solve cbs a <*> NBE.unembed solve cbs b <*> NBE.unembed solve cbs c <*> NBE.unembed solve cbs d <*> NBE.unembed solve cbs e <*> NBE.unembed solve cbs f in + let! r = r in + return (NBE.embed solve cbs r) + | _ -> failwith "arity" + in + as_primitive_step_nbecbs true (name, 6, u_arity, interp, nbe_interp) diff --git a/src/typechecker/FStar.TypeChecker.Primops.Base.fsti b/src/typechecker/FStar.TypeChecker.Primops.Base.fsti index 1cf83250573..f8cc19d07dc 100644 --- a/src/typechecker/FStar.TypeChecker.Primops.Base.fsti +++ b/src/typechecker/FStar.TypeChecker.Primops.Base.fsti @@ -222,3 +222,17 @@ val mk5' #a #b #c #d #e #r #na #nb #nc #nd #ne #nr (f : a -> b -> c -> d -> e -> option r) (f : na -> nb -> nc -> nd -> ne -> option nr) : primitive_step + +val mk6' #a #b #c #d #e #f #r #na #nb #nc #nd #ne #nf #nr + (u_arity : int) + (name : Ident.lid) + {| EMB.embedding a |} {| NBE.embedding na |} + {| EMB.embedding b |} {| NBE.embedding nb |} + {| EMB.embedding c |} {| NBE.embedding nc |} + {| EMB.embedding d |} {| NBE.embedding nd |} + {| EMB.embedding e |} {| NBE.embedding ne |} + {| EMB.embedding f |} {| NBE.embedding nf |} + {| EMB.embedding r |} {| NBE.embedding nr |} + (f : a -> b -> c -> d -> e -> f -> option r) + (f : na -> nb -> nc -> nd -> ne -> nf -> option nr) + : primitive_step diff --git a/tests/tactics/CheckEquiv.fst b/tests/tactics/CheckEquiv.fst index 38a378bf72e..59c727778ca 100644 --- a/tests/tactics/CheckEquiv.fst +++ b/tests/tactics/CheckEquiv.fst @@ -36,3 +36,30 @@ let _ = assert True by begin let _ = must <| check_equiv env (`1) (`(reveal u#0 #int (hide u#0 #int 1))) in () end + +[@@expect_failure] // this is fine, as nosmt implies nodelta +let _ = assert True by begin + let env = cur_env () in + let _ = must <| check_equiv_nosmt env (`1) (`(g 1)) in + () +end + +let _ = assert True by begin + let env = cur_env () in + let _ = must <| check_equiv_nosmt env (`1) (`1) in + () +end + +let _ = assert True by begin + let env = cur_env () in + let _ = must <| check_equiv_nosmt env (`(1+1)) (`(3-1)) in + () +end + +let _ = assert True by begin + let env = cur_env () in + let _ = must <| check_equiv_nosmt env (`1) (`(reveal #int (hide #int 1))) in + () +end + +#pop-options diff --git a/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti b/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti index 2c84152aaec..71a985a900d 100644 --- a/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti +++ b/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti @@ -484,7 +484,7 @@ val is_non_informative (g:env) (t:typ) val check_subtyping (g:env) (t0 t1:typ) : Tac (ret_t (subtyping_token g t0 t1)) -val check_equiv (g:env) (t0 t1:typ) +val t_check_equiv (smt_ok:bool) (unfolding_ok:bool) (g:env) (t0 t1:typ) : Tac (ret_t (equiv_token g t0 t1)) // diff --git a/ulib/FStar.Tactics.V2.Derived.fst b/ulib/FStar.Tactics.V2.Derived.fst index ba3f32a7bbe..0b791d5cb6a 100644 --- a/ulib/FStar.Tactics.V2.Derived.fst +++ b/ulib/FStar.Tactics.V2.Derived.fst @@ -942,3 +942,7 @@ let smt_sync' (fuel ifuel : nat) : Tac unit = ; initial_ifuel = ifuel; max_ifuel = ifuel } in t_smt_sync vcfg' + +(* t_check_equiv wrappers. *) +let check_equiv g t0 t1 = t_check_equiv true true g t0 t1 +let check_equiv_nosmt g t0 t1 = t_check_equiv false false g t0 t1