diff --git a/ocaml/fstar-lib/FStar_Tactics_V2_Builtins.ml b/ocaml/fstar-lib/FStar_Tactics_V2_Builtins.ml index 98497276d55..ecda04f0606 100644 --- a/ocaml/fstar-lib/FStar_Tactics_V2_Builtins.ml +++ b/ocaml/fstar-lib/FStar_Tactics_V2_Builtins.ml @@ -136,12 +136,13 @@ let free_uvars = from_tac_1 "B.free_uvars" B.free_uvars type ('env, 't) prop_validity_token = unit 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 core_compute_term_type = from_tac_3 "B.refl_core_compute_term_type" B.refl_core_compute_term_type +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 check_match_complete = from_tac_4 "B.refl_check_match_complete" B.refl_check_match_complete -let tc_term = from_tac_3 "B.refl_tc_term" B.refl_tc_term +let tc_term = from_tac_2 "B.refl_tc_term" B.refl_tc_term let universe_of = from_tac_2 "B.refl_universe_of" B.refl_universe_of let check_prop_validity = from_tac_2 "B.refl_check_prop_validity" B.refl_check_prop_validity let instantiate_implicits = from_tac_2 "B.refl_instantiate_implicits" B.refl_instantiate_implicits diff --git a/ocaml/fstar-lib/generated/FStar_Reflection_Typing.ml b/ocaml/fstar-lib/generated/FStar_Reflection_Typing.ml index c16d0c473d8..996999672ad 100644 --- a/ocaml/fstar-lib/generated/FStar_Reflection_Typing.ml +++ b/ocaml/fstar-lib/generated/FStar_Reflection_Typing.ml @@ -1051,12 +1051,12 @@ let (mk_if : ((FStar_Reflection_V2_Data.Pat_Constant FStar_Reflection_V2_Data.C_False), else_)])) type comp_typ = - (FStar_Tactics_Types.tot_or_ghost * FStar_Reflection_Types.typ) + (FStar_TypeChecker_Core.tot_or_ghost * FStar_Reflection_Types.typ) let (close_comp_typ' : comp_typ -> FStar_Reflection_V2_Data.var -> Prims.nat -> - (FStar_Tactics_Types.tot_or_ghost * FStar_Reflection_Types.term)) + (FStar_TypeChecker_Core.tot_or_ghost * FStar_Reflection_Types.term)) = fun c -> fun x -> @@ -1066,13 +1066,13 @@ let (close_comp_typ' : let (close_comp_typ : comp_typ -> FStar_Reflection_V2_Data.var -> - (FStar_Tactics_Types.tot_or_ghost * FStar_Reflection_Types.term)) + (FStar_TypeChecker_Core.tot_or_ghost * FStar_Reflection_Types.term)) = fun c -> fun x -> close_comp_typ' c x Prims.int_zero let (open_comp_typ' : comp_typ -> FStar_Reflection_V2_Data.var -> Prims.nat -> - (FStar_Tactics_Types.tot_or_ghost * FStar_Reflection_Types.term)) + (FStar_TypeChecker_Core.tot_or_ghost * FStar_Reflection_Types.term)) = fun c -> fun x -> @@ -1082,7 +1082,7 @@ let (open_comp_typ' : let (open_comp_typ : comp_typ -> FStar_Reflection_V2_Data.var -> - (FStar_Tactics_Types.tot_or_ghost * FStar_Reflection_Types.term)) + (FStar_TypeChecker_Core.tot_or_ghost * FStar_Reflection_Types.term)) = fun c -> fun x -> open_comp_typ' c x Prims.int_zero let (freevars_comp_typ : comp_typ -> FStar_Reflection_V2_Data.var FStar_Set.set) = @@ -1090,8 +1090,10 @@ let (freevars_comp_typ : let (mk_comp : comp_typ -> FStar_Reflection_Types.comp) = fun c -> match FStar_Pervasives_Native.fst c with - | FStar_Tactics_Types.E_Total -> mk_total (FStar_Pervasives_Native.snd c) - | FStar_Tactics_Types.E_Ghost -> mk_ghost (FStar_Pervasives_Native.snd c) + | FStar_TypeChecker_Core.E_Total -> + mk_total (FStar_Pervasives_Native.snd c) + | FStar_TypeChecker_Core.E_Ghost -> + mk_ghost (FStar_Pervasives_Native.snd c) let (mk_arrow_ct : FStar_Reflection_Types.term -> FStar_Reflection_V2_Data.aqualv -> @@ -1183,30 +1185,38 @@ let (refl_bindings_to_bindings : (fun b -> ((b.FStar_Reflection_V2_Data.uniq1), (b.FStar_Reflection_V2_Data.sort3))) bs -type 'dummyV0 non_informative = - | Non_informative_type of FStar_Reflection_Types.universe - | Non_informative_fv of FStar_Reflection_Types.fv - | Non_informative_uinst of FStar_Reflection_Types.fv * - FStar_Reflection_Types.universe Prims.list - | Non_informative_app of FStar_Reflection_Types.term * - FStar_Reflection_V2_Data.argv * unit non_informative - | Non_informative_total_arrow of FStar_Reflection_Types.term * - FStar_Reflection_V2_Data.aqualv * FStar_Reflection_Types.term * unit - non_informative - | Non_informative_ghost_arrow of FStar_Reflection_Types.term * - FStar_Reflection_V2_Data.aqualv * FStar_Reflection_Types.term -let uu___is_Non_informative_type uu___ uu___1 = - match uu___1 with | Non_informative_type _ -> true | _ -> false -let uu___is_Non_informative_fv uu___ uu___1 = - match uu___1 with | Non_informative_fv _ -> true | _ -> false -let uu___is_Non_informative_uinst uu___ uu___1 = - match uu___1 with | Non_informative_uinst _ -> true | _ -> false -let uu___is_Non_informative_app uu___ uu___1 = - match uu___1 with | Non_informative_app _ -> true | _ -> false -let uu___is_Non_informative_total_arrow uu___ uu___1 = - match uu___1 with | Non_informative_total_arrow _ -> true | _ -> false -let uu___is_Non_informative_ghost_arrow uu___ uu___1 = - match uu___1 with | Non_informative_ghost_arrow _ -> true | _ -> false +type ('dummyV0, 'dummyV1) non_informative = + | Non_informative_type of FStar_Reflection_Types.env * + FStar_Reflection_Types.universe + | Non_informative_fv of FStar_Reflection_Types.env * + FStar_Reflection_Types.fv + | Non_informative_uinst of FStar_Reflection_Types.env * + FStar_Reflection_Types.fv * FStar_Reflection_Types.universe Prims.list + | Non_informative_app of FStar_Reflection_Types.env * + FStar_Reflection_Types.term * FStar_Reflection_V2_Data.argv * (unit, + unit) non_informative + | Non_informative_total_arrow of FStar_Reflection_Types.env * + FStar_Reflection_Types.term * FStar_Reflection_V2_Data.aqualv * + FStar_Reflection_Types.term * (unit, unit) non_informative + | Non_informative_ghost_arrow of FStar_Reflection_Types.env * + FStar_Reflection_Types.term * FStar_Reflection_V2_Data.aqualv * + FStar_Reflection_Types.term + | Non_informative_token of FStar_Reflection_Types.env * + FStar_Reflection_Types.typ * unit +let uu___is_Non_informative_type uu___1 uu___ uu___2 = + match uu___2 with | Non_informative_type _ -> true | _ -> false +let uu___is_Non_informative_fv uu___1 uu___ uu___2 = + match uu___2 with | Non_informative_fv _ -> true | _ -> false +let uu___is_Non_informative_uinst uu___1 uu___ uu___2 = + match uu___2 with | Non_informative_uinst _ -> true | _ -> false +let uu___is_Non_informative_app uu___1 uu___ uu___2 = + match uu___2 with | Non_informative_app _ -> true | _ -> false +let uu___is_Non_informative_total_arrow uu___1 uu___ uu___2 = + match uu___2 with | Non_informative_total_arrow _ -> true | _ -> false +let uu___is_Non_informative_ghost_arrow uu___1 uu___ uu___2 = + match uu___2 with | Non_informative_ghost_arrow _ -> true | _ -> false +let uu___is_Non_informative_token uu___1 uu___ uu___2 = + match uu___2 with | Non_informative_token _ -> true | _ -> false type ('bnds, 'pat, 'uuuuu) bindings_ok_for_pat = Obj.t type ('g, 'bs, 'br) bindings_ok_for_branch = Obj.t type ('g, 'bss, 'brs) bindings_ok_for_branch_N = Obj.t @@ -1286,32 +1296,32 @@ type ('dummyV0, 'dummyV1, 'dummyV2) typing = | T_Abs of FStar_Reflection_Types.env * FStar_Reflection_V2_Data.var * FStar_Reflection_Types.term * FStar_Reflection_Types.term * comp_typ * FStar_Reflection_Types.universe * pp_name_t * - FStar_Reflection_V2_Data.aqualv * FStar_Tactics_Types.tot_or_ghost * ( - unit, unit, unit) typing * (unit, unit, unit) typing + FStar_Reflection_V2_Data.aqualv * FStar_TypeChecker_Core.tot_or_ghost * + (unit, unit, unit) typing * (unit, unit, unit) typing | T_App of FStar_Reflection_Types.env * FStar_Reflection_Types.term * FStar_Reflection_Types.term * FStar_Reflection_Types.binder * - FStar_Reflection_Types.term * FStar_Tactics_Types.tot_or_ghost * (unit, - unit, unit) typing * (unit, unit, unit) typing + FStar_Reflection_Types.term * FStar_TypeChecker_Core.tot_or_ghost * ( + unit, unit, unit) typing * (unit, unit, unit) typing | T_Let of FStar_Reflection_Types.env * FStar_Reflection_V2_Data.var * FStar_Reflection_Types.term * FStar_Reflection_Types.typ * FStar_Reflection_Types.term * FStar_Reflection_Types.typ * - FStar_Tactics_Types.tot_or_ghost * pp_name_t * (unit, unit, unit) typing * - (unit, unit, unit) typing + FStar_TypeChecker_Core.tot_or_ghost * pp_name_t * (unit, unit, unit) typing + * (unit, unit, unit) typing | T_Arrow of FStar_Reflection_Types.env * FStar_Reflection_V2_Data.var * FStar_Reflection_Types.term * FStar_Reflection_Types.term * FStar_Reflection_Types.universe * FStar_Reflection_Types.universe * pp_name_t * FStar_Reflection_V2_Data.aqualv * - FStar_Tactics_Types.tot_or_ghost * FStar_Tactics_Types.tot_or_ghost * - FStar_Tactics_Types.tot_or_ghost * (unit, unit, unit) typing * (unit, - unit, unit) typing + FStar_TypeChecker_Core.tot_or_ghost * FStar_TypeChecker_Core.tot_or_ghost * + FStar_TypeChecker_Core.tot_or_ghost * (unit, unit, unit) typing * ( + unit, unit, unit) typing | T_Refine of FStar_Reflection_Types.env * FStar_Reflection_V2_Data.var * FStar_Reflection_Types.term * FStar_Reflection_Types.term * FStar_Reflection_Types.universe * FStar_Reflection_Types.universe * - FStar_Tactics_Types.tot_or_ghost * FStar_Tactics_Types.tot_or_ghost * + FStar_TypeChecker_Core.tot_or_ghost * FStar_TypeChecker_Core.tot_or_ghost * (unit, unit, unit) typing * (unit, unit, unit) typing | T_PropIrrelevance of FStar_Reflection_Types.env * FStar_Reflection_Types.term * FStar_Reflection_Types.term * - FStar_Tactics_Types.tot_or_ghost * FStar_Tactics_Types.tot_or_ghost * + FStar_TypeChecker_Core.tot_or_ghost * FStar_TypeChecker_Core.tot_or_ghost * (unit, unit, unit) typing * (unit, unit, unit) typing | T_Sub of FStar_Reflection_Types.env * FStar_Reflection_Types.term * comp_typ * comp_typ * (unit, unit, unit) typing * (unit, unit, unit, @@ -1319,14 +1329,14 @@ type ('dummyV0, 'dummyV1, 'dummyV2) typing = | T_If of FStar_Reflection_Types.env * FStar_Reflection_Types.term * FStar_Reflection_Types.term * FStar_Reflection_Types.term * FStar_Reflection_Types.term * FStar_Reflection_Types.universe * - FStar_Reflection_V2_Data.var * FStar_Tactics_Types.tot_or_ghost * - FStar_Tactics_Types.tot_or_ghost * (unit, unit, unit) typing * (unit, - unit, unit) typing * (unit, unit, unit) typing * (unit, unit, unit) typing - + FStar_Reflection_V2_Data.var * FStar_TypeChecker_Core.tot_or_ghost * + FStar_TypeChecker_Core.tot_or_ghost * (unit, unit, unit) typing * ( + unit, unit, unit) typing * (unit, unit, unit) typing * (unit, unit, + unit) typing | T_Match of FStar_Reflection_Types.env * FStar_Reflection_Types.universe * FStar_Reflection_Types.typ * FStar_Reflection_Types.term * - FStar_Tactics_Types.tot_or_ghost * (unit, unit, unit) typing * - FStar_Tactics_Types.tot_or_ghost * (unit, unit, unit) typing * + FStar_TypeChecker_Core.tot_or_ghost * (unit, unit, unit) typing * + FStar_TypeChecker_Core.tot_or_ghost * (unit, unit, unit) typing * FStar_Reflection_V2_Data.branch Prims.list * comp_typ * FStar_Reflection_V2_Data.binding Prims.list Prims.list * (unit, unit, unit, unit, unit) match_is_complete * (unit, unit, unit, unit, unit, @@ -1363,12 +1373,12 @@ and ('dummyV0, 'dummyV1, 'dummyV2) equiv = FStar_Reflection_Types.term * term_ctxt * (unit, unit, unit) equiv and ('dummyV0, 'dummyV1, 'dummyV2, 'dummyV3) related_comp = | Relc_typ of FStar_Reflection_Types.env * FStar_Reflection_Types.term * - FStar_Reflection_Types.term * FStar_Tactics_Types.tot_or_ghost * relation * - (unit, unit, unit, unit) related + FStar_Reflection_Types.term * FStar_TypeChecker_Core.tot_or_ghost * + relation * (unit, unit, unit, unit) related | Relc_total_ghost of FStar_Reflection_Types.env * FStar_Reflection_Types.term | Relc_ghost_total of FStar_Reflection_Types.env * - FStar_Reflection_Types.term * unit non_informative + FStar_Reflection_Types.term * (unit, unit) non_informative and ('g, 'scuu, 'scuty, 'sc, 'rty, 'dummyV0, 'dummyV1) branches_typing = | BT_Nil | BT_S of FStar_Reflection_V2_Data.branch * @@ -1496,11 +1506,11 @@ let (simplify_umax : fun d -> let ue = UN_MaxLeq (u, u, (UNLEQ_Refl u)) in T_Sub - (g, t, (FStar_Tactics_Types.E_Total, (tm_type (u_max u u))), - (FStar_Tactics_Types.E_Total, (tm_type u)), d, + (g, t, (FStar_TypeChecker_Core.E_Total, (tm_type (u_max u u))), + (FStar_TypeChecker_Core.E_Total, (tm_type u)), d, (Relc_typ (g, (tm_type (u_max u u)), (tm_type u), - FStar_Tactics_Types.E_Total, R_Sub, + FStar_TypeChecker_Core.E_Total, R_Sub, (Rel_equiv (g, (tm_type (u_max u u)), (tm_type u), R_Sub, (EQ_Univ (g, (u_max u u), u, ue))))))) @@ -1570,8 +1580,8 @@ let (mkif : FStar_Reflection_Types.term -> FStar_Reflection_Types.universe -> FStar_Reflection_V2_Data.var -> - FStar_Tactics_Types.tot_or_ghost -> - FStar_Tactics_Types.tot_or_ghost -> + FStar_TypeChecker_Core.tot_or_ghost -> + FStar_TypeChecker_Core.tot_or_ghost -> (unit, unit, unit) typing -> (unit, unit, unit) typing -> (unit, unit, unit) typing -> @@ -1620,7 +1630,7 @@ let (mkif : BT_Nil))) in T_Match (g, u_zero, bool_ty, scrutinee, - FStar_Tactics_Types.E_Total, + FStar_TypeChecker_Core.E_Total, (T_FVar (g, bool_fv)), eff, ts, [brt; bre], (eff, ty), [[]; []], (MC_Tok diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Embedding.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Embedding.ml index 7e24d360623..0ced4b140a7 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_Embedding.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_Embedding.ml @@ -38,6 +38,22 @@ let (fstar_tactics_const : Prims.string Prims.list -> tac_constant) = let uu___ = FStar_Syntax_Syntax.fvconst lid in let uu___1 = FStar_Syntax_Syntax.tconst lid in { lid; fv = uu___; t = uu___1 } +let (fstar_tc_core_lid : Prims.string -> FStar_Ident.lid) = + fun s -> + FStar_Ident.lid_of_path + (FStar_Compiler_List.op_At ["FStar"; "Stubs"; "TypeChecker"; "Core"] + [s]) FStar_Compiler_Range_Type.dummyRange +let (fstar_tc_core_data : Prims.string -> tac_constant) = + fun s -> + let lid = fstar_tc_core_lid s in + let uu___ = lid_as_data_fv lid in + let uu___1 = lid_as_data_tm lid in { lid; fv = uu___; t = uu___1 } +let (fstar_tc_core_const : Prims.string -> tac_constant) = + fun s -> + let lid = fstar_tc_core_lid s in + let uu___ = FStar_Syntax_Syntax.fvconst lid in + let uu___1 = FStar_Syntax_Syntax.tconst lid in + { lid; fv = uu___; t = uu___1 } let (fstar_tactics_proofstate : tac_constant) = fstar_tactics_const ["Types"; "proofstate"] let (fstar_tactics_goal : tac_constant) = @@ -64,22 +80,22 @@ let (fstar_tactics_Skip : tac_constant) = fstar_tactics_data ["Types"; "Skip"] let (fstar_tactics_Abort : tac_constant) = fstar_tactics_data ["Types"; "Abort"] -let (fstar_tactics_unfold_side : tac_constant) = - fstar_tactics_const ["Types"; "unfold_side"] -let (fstar_tactics_unfold_side_Left : tac_constant) = - fstar_tactics_data ["Types"; "Left"] -let (fstar_tactics_unfold_side_Right : tac_constant) = - fstar_tactics_data ["Types"; "Right"] -let (fstar_tactics_unfold_side_Both : tac_constant) = - fstar_tactics_data ["Types"; "Both"] -let (fstar_tactics_unfold_side_Neither : tac_constant) = - fstar_tactics_data ["Types"; "Neither"] -let (fstar_tactics_tot_or_ghost : tac_constant) = - fstar_tactics_const ["Types"; "tot_or_ghost"] -let (fstar_tactics_tot_or_ghost_ETotal : tac_constant) = - fstar_tactics_data ["Types"; "E_Total"] -let (fstar_tactics_tot_or_ghost_EGhost : tac_constant) = - fstar_tactics_data ["Types"; "E_Ghost"] +let (fstar_tc_core_unfold_side : tac_constant) = + fstar_tc_core_const "unfold_side" +let (fstar_tc_core_unfold_side_Left : tac_constant) = + fstar_tc_core_data "Left" +let (fstar_tc_core_unfold_side_Right : tac_constant) = + fstar_tc_core_data "Right" +let (fstar_tc_core_unfold_side_Both : tac_constant) = + fstar_tc_core_data "Both" +let (fstar_tc_core_unfold_side_Neither : tac_constant) = + fstar_tc_core_data "Neither" +let (fstar_tc_core_tot_or_ghost : tac_constant) = + fstar_tc_core_const "tot_or_ghost" +let (fstar_tc_core_tot_or_ghost_ETotal : tac_constant) = + fstar_tc_core_data "E_Total" +let (fstar_tc_core_tot_or_ghost_EGhost : tac_constant) = + fstar_tc_core_data "E_Ghost" let (fstar_tactics_guard_policy : tac_constant) = fstar_tactics_const ["Types"; "guard_policy"] let (fstar_tactics_SMT : tac_constant) = fstar_tactics_data ["Types"; "SMT"] @@ -690,57 +706,57 @@ let (e_unfold_side : FStar_TypeChecker_Core.side FStar_Syntax_Embeddings_Base.embedding) = let embed_unfold_side rng s = match s with - | FStar_TypeChecker_Core.Left -> fstar_tactics_unfold_side_Left.t - | FStar_TypeChecker_Core.Right -> fstar_tactics_unfold_side_Right.t - | FStar_TypeChecker_Core.Both -> fstar_tactics_unfold_side_Both.t - | FStar_TypeChecker_Core.Neither -> fstar_tactics_unfold_side_Neither.t in + | FStar_TypeChecker_Core.Left -> fstar_tc_core_unfold_side_Left.t + | FStar_TypeChecker_Core.Right -> fstar_tc_core_unfold_side_Right.t + | FStar_TypeChecker_Core.Both -> fstar_tc_core_unfold_side_Both.t + | FStar_TypeChecker_Core.Neither -> fstar_tc_core_unfold_side_Neither.t in let unembed_unfold_side t = let uu___ = let uu___1 = FStar_Syntax_Subst.compress t in uu___1.FStar_Syntax_Syntax.n in match uu___ with | FStar_Syntax_Syntax.Tm_fvar fv when - FStar_Syntax_Syntax.fv_eq_lid fv fstar_tactics_unfold_side_Left.lid + FStar_Syntax_Syntax.fv_eq_lid fv fstar_tc_core_unfold_side_Left.lid -> FStar_Pervasives_Native.Some FStar_TypeChecker_Core.Left | FStar_Syntax_Syntax.Tm_fvar fv when - FStar_Syntax_Syntax.fv_eq_lid fv fstar_tactics_unfold_side_Right.lid + FStar_Syntax_Syntax.fv_eq_lid fv fstar_tc_core_unfold_side_Right.lid -> FStar_Pervasives_Native.Some FStar_TypeChecker_Core.Right | FStar_Syntax_Syntax.Tm_fvar fv when - FStar_Syntax_Syntax.fv_eq_lid fv fstar_tactics_unfold_side_Both.lid + FStar_Syntax_Syntax.fv_eq_lid fv fstar_tc_core_unfold_side_Both.lid -> FStar_Pervasives_Native.Some FStar_TypeChecker_Core.Both | FStar_Syntax_Syntax.Tm_fvar fv when FStar_Syntax_Syntax.fv_eq_lid fv - fstar_tactics_unfold_side_Neither.lid + fstar_tc_core_unfold_side_Neither.lid -> FStar_Pervasives_Native.Some FStar_TypeChecker_Core.Neither | uu___1 -> FStar_Pervasives_Native.None in - mk_emb embed_unfold_side unembed_unfold_side fstar_tactics_unfold_side.t + mk_emb embed_unfold_side unembed_unfold_side fstar_tc_core_unfold_side.t let (e_unfold_side_nbe : FStar_TypeChecker_Core.side FStar_TypeChecker_NBETerm.embedding) = let embed_unfold_side cb res = match res with | FStar_TypeChecker_Core.Left -> - mkConstruct fstar_tactics_unfold_side_Left.fv [] [] + mkConstruct fstar_tc_core_unfold_side_Left.fv [] [] | FStar_TypeChecker_Core.Right -> - mkConstruct fstar_tactics_unfold_side_Right.fv [] [] + mkConstruct fstar_tc_core_unfold_side_Right.fv [] [] | FStar_TypeChecker_Core.Both -> - mkConstruct fstar_tactics_unfold_side_Both.fv [] [] + mkConstruct fstar_tc_core_unfold_side_Both.fv [] [] | FStar_TypeChecker_Core.Neither -> - mkConstruct fstar_tactics_unfold_side_Neither.fv [] [] in + mkConstruct fstar_tc_core_unfold_side_Neither.fv [] [] in let unembed_unfold_side cb t = let uu___ = FStar_TypeChecker_NBETerm.nbe_t_of_t t in match uu___ with | FStar_TypeChecker_NBETerm.Construct (fv, uu___1, []) when - FStar_Syntax_Syntax.fv_eq_lid fv fstar_tactics_unfold_side_Left.lid + FStar_Syntax_Syntax.fv_eq_lid fv fstar_tc_core_unfold_side_Left.lid -> FStar_Pervasives_Native.Some FStar_TypeChecker_Core.Left | FStar_TypeChecker_NBETerm.Construct (fv, uu___1, []) when - FStar_Syntax_Syntax.fv_eq_lid fv fstar_tactics_unfold_side_Right.lid + FStar_Syntax_Syntax.fv_eq_lid fv fstar_tc_core_unfold_side_Right.lid -> FStar_Pervasives_Native.Some FStar_TypeChecker_Core.Right | FStar_TypeChecker_NBETerm.Construct (fv, uu___1, []) when - FStar_Syntax_Syntax.fv_eq_lid fv fstar_tactics_unfold_side_Both.lid + FStar_Syntax_Syntax.fv_eq_lid fv fstar_tc_core_unfold_side_Both.lid -> FStar_Pervasives_Native.Some FStar_TypeChecker_Core.Both | FStar_TypeChecker_NBETerm.Construct (fv, uu___1, []) when FStar_Syntax_Syntax.fv_eq_lid fv - fstar_tactics_unfold_side_Neither.lid + fstar_tc_core_unfold_side_Neither.lid -> FStar_Pervasives_Native.Some FStar_TypeChecker_Core.Neither | uu___1 -> ((let uu___3 = @@ -757,8 +773,8 @@ let (e_unfold_side_nbe : uu___4 else ()); FStar_Pervasives_Native.None) in - let uu___ = mkFV fstar_tactics_unfold_side.fv [] [] in - let uu___1 = fv_as_emb_typ fstar_tactics_unfold_side.fv in + let uu___ = mkFV fstar_tc_core_unfold_side.fv [] [] in + let uu___1 = fv_as_emb_typ fstar_tc_core_unfold_side.fv in { FStar_TypeChecker_NBETerm.em = embed_unfold_side; FStar_TypeChecker_NBETerm.un = unembed_unfold_side; @@ -766,11 +782,12 @@ let (e_unfold_side_nbe : FStar_TypeChecker_NBETerm.emb_typ = uu___1 } let (e_tot_or_ghost : - FStar_Tactics_Types.tot_or_ghost FStar_Syntax_Embeddings_Base.embedding) = + FStar_TypeChecker_Core.tot_or_ghost FStar_Syntax_Embeddings_Base.embedding) + = let embed_tot_or_ghost rng s = match s with - | FStar_Tactics_Types.E_Total -> fstar_tactics_tot_or_ghost_ETotal.t - | FStar_Tactics_Types.E_Ghost -> fstar_tactics_tot_or_ghost_EGhost.t in + | FStar_TypeChecker_Core.E_Total -> fstar_tc_core_tot_or_ghost_ETotal.t + | FStar_TypeChecker_Core.E_Ghost -> fstar_tc_core_tot_or_ghost_EGhost.t in let unembed_tot_or_ghost t = let uu___ = let uu___1 = FStar_Syntax_Subst.compress t in @@ -778,33 +795,33 @@ let (e_tot_or_ghost : match uu___ with | FStar_Syntax_Syntax.Tm_fvar fv when FStar_Syntax_Syntax.fv_eq_lid fv - fstar_tactics_tot_or_ghost_ETotal.lid - -> FStar_Pervasives_Native.Some FStar_Tactics_Types.E_Total + fstar_tc_core_tot_or_ghost_ETotal.lid + -> FStar_Pervasives_Native.Some FStar_TypeChecker_Core.E_Total | FStar_Syntax_Syntax.Tm_fvar fv when FStar_Syntax_Syntax.fv_eq_lid fv - fstar_tactics_tot_or_ghost_EGhost.lid - -> FStar_Pervasives_Native.Some FStar_Tactics_Types.E_Ghost + fstar_tc_core_tot_or_ghost_EGhost.lid + -> FStar_Pervasives_Native.Some FStar_TypeChecker_Core.E_Ghost | uu___1 -> FStar_Pervasives_Native.None in - mk_emb embed_tot_or_ghost unembed_tot_or_ghost fstar_tactics_tot_or_ghost.t + mk_emb embed_tot_or_ghost unembed_tot_or_ghost fstar_tc_core_tot_or_ghost.t let (e_tot_or_ghost_nbe : - FStar_Tactics_Types.tot_or_ghost FStar_TypeChecker_NBETerm.embedding) = + FStar_TypeChecker_Core.tot_or_ghost FStar_TypeChecker_NBETerm.embedding) = let embed_tot_or_ghost cb res = match res with - | FStar_Tactics_Types.E_Total -> - mkConstruct fstar_tactics_tot_or_ghost_ETotal.fv [] [] - | FStar_Tactics_Types.E_Ghost -> - mkConstruct fstar_tactics_tot_or_ghost_EGhost.fv [] [] in + | FStar_TypeChecker_Core.E_Total -> + mkConstruct fstar_tc_core_tot_or_ghost_ETotal.fv [] [] + | FStar_TypeChecker_Core.E_Ghost -> + mkConstruct fstar_tc_core_tot_or_ghost_EGhost.fv [] [] in let unembed_tot_or_ghost cb t = let uu___ = FStar_TypeChecker_NBETerm.nbe_t_of_t t in match uu___ with | FStar_TypeChecker_NBETerm.Construct (fv, uu___1, []) when FStar_Syntax_Syntax.fv_eq_lid fv - fstar_tactics_tot_or_ghost_ETotal.lid - -> FStar_Pervasives_Native.Some FStar_Tactics_Types.E_Total + fstar_tc_core_tot_or_ghost_ETotal.lid + -> FStar_Pervasives_Native.Some FStar_TypeChecker_Core.E_Total | FStar_TypeChecker_NBETerm.Construct (fv, uu___1, []) when FStar_Syntax_Syntax.fv_eq_lid fv - fstar_tactics_tot_or_ghost_EGhost.lid - -> FStar_Pervasives_Native.Some FStar_Tactics_Types.E_Ghost + fstar_tc_core_tot_or_ghost_EGhost.lid + -> FStar_Pervasives_Native.Some FStar_TypeChecker_Core.E_Ghost | uu___1 -> ((let uu___3 = FStar_Compiler_Effect.op_Bang FStar_Options.debug_embedding in @@ -820,8 +837,8 @@ let (e_tot_or_ghost_nbe : uu___4 else ()); FStar_Pervasives_Native.None) in - let uu___ = mkFV fstar_tactics_tot_or_ghost.fv [] [] in - let uu___1 = fv_as_emb_typ fstar_tactics_tot_or_ghost.fv in + let uu___ = mkFV fstar_tc_core_tot_or_ghost.fv [] [] in + let uu___1 = fv_as_emb_typ fstar_tc_core_tot_or_ghost.fv in { FStar_TypeChecker_NBETerm.em = embed_tot_or_ghost; FStar_TypeChecker_NBETerm.un = unembed_tot_or_ghost; diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Monad.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Monad.ml index 7d61d32b858..1938e19eba5 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_Monad.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_Monad.ml @@ -194,7 +194,7 @@ let (register_goal : FStar_Tactics_Types.goal -> unit) = (let goal_ty = FStar_Syntax_Util.ctx_uvar_typ uv in let uu___8 = FStar_TypeChecker_Core.compute_term_type_handle_guards - env1 goal_ty false (fun uu___9 -> fun uu___10 -> true) in + env1 goal_ty (fun uu___9 -> fun uu___10 -> true) in match uu___8 with | FStar_Pervasives.Inl uu___9 -> () | FStar_Pervasives.Inr err -> diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Types.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Types.ml index 03b2bffe08c..e1a8559f6c5 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_Types.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_Types.ml @@ -470,26 +470,7 @@ let (get_phi : FStar_Syntax_Util.un_squash uu___ let (is_irrelevant : goal -> Prims.bool) = fun g -> let uu___ = get_phi g in FStar_Compiler_Option.isSome uu___ -type unfold_side = - | Left - | Right - | Both - | Neither -let (uu___is_Left : unfold_side -> Prims.bool) = - fun projectee -> match projectee with | Left -> true | uu___ -> false -let (uu___is_Right : unfold_side -> Prims.bool) = - fun projectee -> match projectee with | Right -> true | uu___ -> false -let (uu___is_Both : unfold_side -> Prims.bool) = - fun projectee -> match projectee with | Both -> true | uu___ -> false -let (uu___is_Neither : unfold_side -> Prims.bool) = - fun projectee -> match projectee with | Neither -> true | uu___ -> false -type tot_or_ghost = - | E_Total - | E_Ghost -let (uu___is_E_Total : tot_or_ghost -> Prims.bool) = - fun projectee -> match projectee with | E_Total -> true | uu___ -> false -let (uu___is_E_Ghost : tot_or_ghost -> Prims.bool) = - fun projectee -> match projectee with | E_Ghost -> true | uu___ -> false +type ('g, 't) non_informative_token = unit type ('g, 't0, 't1) subtyping_token = unit type ('g, 't0, 't1) equiv_token = unit type ('g, 'e, 'c) typing_token = unit diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml index 6755bf86c11..51c4c1fde01 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V1_Basic.ml @@ -4302,20 +4302,20 @@ let (_t_trefl : } in let uu___12 = FStar_TypeChecker_Core.compute_term_type_handle_guards - env1 t3 false + env1 t3 (fun uu___13 -> fun uu___14 -> true) in match uu___12 with | FStar_Pervasives.Inr uu___13 -> false - | FStar_Pervasives.Inl t_ty -> - let uu___13 = + | FStar_Pervasives.Inl (uu___13, t_ty) -> + let uu___14 = FStar_TypeChecker_Core.check_term_subtyping env1 ty t_ty in - (match uu___13 with + (match uu___14 with | FStar_Pervasives.Inl (FStar_Pervasives_Native.None) -> (mark_uvar_as_already_checked u; true) - | uu___14 -> false) in + | uu___15 -> false) in let uu___12 = let uu___13 = is_uvar t1 in let uu___14 = is_uvar t2 in diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml index a9293f573d6..1af7c1b45a1 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml @@ -4359,20 +4359,20 @@ let (_t_trefl : } in let uu___12 = FStar_TypeChecker_Core.compute_term_type_handle_guards - env1 t3 false + env1 t3 (fun uu___13 -> fun uu___14 -> true) in match uu___12 with | FStar_Pervasives.Inr uu___13 -> false - | FStar_Pervasives.Inl t_ty -> - let uu___13 = + | FStar_Pervasives.Inl (uu___13, t_ty) -> + let uu___14 = FStar_TypeChecker_Core.check_term_subtyping env1 ty t_ty in - (match uu___13 with + (match uu___14 with | FStar_Pervasives.Inl (FStar_Pervasives_Native.None) -> (mark_uvar_as_already_checked u; true) - | uu___14 -> false) in + | uu___15 -> false) in let uu___12 = let uu___13 = is_uvar t1 in let uu___14 = is_uvar t2 in @@ -6941,6 +6941,45 @@ let (unexpected_uvars_issue : FStar_Errors.issue_ctx = [] } in i +let (refl_is_non_informative : + env -> + FStar_Syntax_Syntax.typ -> + (unit FStar_Pervasives_Native.option * issues) FStar_Tactics_Monad.tac) + = + fun g -> + fun t -> + let uu___ = (no_uvars_in_g g) && (no_uvars_in_term t) in + if uu___ + then + refl_typing_builtin_wrapper + (fun uu___1 -> + dbg_refl g + (fun uu___3 -> + let uu___4 = FStar_Syntax_Print.term_to_string t in + FStar_Compiler_Util.format1 "refl_is_non_informative: %s\n" + uu___4); + (let b = FStar_TypeChecker_Core.is_non_informative g t in + dbg_refl g + (fun uu___4 -> + let uu___5 = FStar_Compiler_Util.string_of_bool b in + FStar_Compiler_Util.format1 + "refl_is_non_informative: returned %s" uu___5); + if b + then ((), []) + else + FStar_Errors.raise_error + (FStar_Errors_Codes.Fatal_UnexpectedTerm, + "is_non_informative returned false ") + FStar_Compiler_Range_Type.dummyRange)) + else + (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_Tactics_Monad.ret uu___2) let (refl_check_relation : env -> FStar_Syntax_Syntax.typ -> @@ -7021,11 +7060,11 @@ let (refl_check_equiv : (unit FStar_Pervasives_Native.option * issues) FStar_Tactics_Monad.tac) = fun g -> fun t0 -> fun t1 -> refl_check_relation g t0 t1 Equality -let (to_must_tot : FStar_Tactics_Types.tot_or_ghost -> Prims.bool) = +let (to_must_tot : FStar_TypeChecker_Core.tot_or_ghost -> Prims.bool) = fun eff -> match eff with - | FStar_Tactics_Types.E_Total -> true - | FStar_Tactics_Types.E_Ghost -> false + | FStar_TypeChecker_Core.E_Total -> true + | FStar_TypeChecker_Core.E_Ghost -> false let (refl_norm_type : env -> FStar_Syntax_Syntax.typ -> FStar_Syntax_Syntax.typ) = fun g -> @@ -7036,74 +7075,69 @@ let (refl_norm_type : let (refl_core_compute_term_type : env -> FStar_Syntax_Syntax.term -> - FStar_Tactics_Types.tot_or_ghost -> - (FStar_Syntax_Syntax.typ FStar_Pervasives_Native.option * issues) - FStar_Tactics_Monad.tac) + ((FStar_TypeChecker_Core.tot_or_ghost * FStar_Syntax_Syntax.typ) + FStar_Pervasives_Native.option * issues) FStar_Tactics_Monad.tac) = fun g -> fun e -> - fun eff -> - let uu___ = (no_uvars_in_g g) && (no_uvars_in_term e) in - if uu___ - then - refl_typing_builtin_wrapper - (fun uu___1 -> - dbg_refl g - (fun uu___3 -> - let uu___4 = FStar_Syntax_Print.term_to_string e in - FStar_Compiler_Util.format1 - "refl_core_compute_term_type: %s\n" uu___4); - (let must_tot = to_must_tot eff in - let guards = FStar_Compiler_Util.mk_ref [] in - let gh g1 guard = - (let uu___4 = - let uu___5 = FStar_Compiler_Effect.op_Bang guards in - (g1, guard) :: uu___5 in - FStar_Compiler_Effect.op_Colon_Equals guards uu___4); - true in - let uu___3 = - FStar_TypeChecker_Core.compute_term_type_handle_guards g e - must_tot gh in - match uu___3 with - | FStar_Pervasives.Inl t -> - let t1 = refl_norm_type g t in - (dbg_refl g - (fun uu___5 -> - let uu___6 = FStar_Syntax_Print.term_to_string e in - let uu___7 = FStar_Syntax_Print.term_to_string t1 in - FStar_Compiler_Util.format2 - "refl_core_compute_term_type for %s computed type %s\n" - uu___6 uu___7); - (let uu___5 = FStar_Compiler_Effect.op_Bang guards in - (t1, uu___5))) - | FStar_Pervasives.Inr err -> - (dbg_refl g - (fun uu___5 -> - let uu___6 = FStar_TypeChecker_Core.print_error err in - FStar_Compiler_Util.format1 - "refl_core_compute_term_type: %s\n" uu___6); - (let uu___5 = - let uu___6 = - let uu___7 = FStar_TypeChecker_Core.print_error err in - Prims.op_Hat "core_compute_term_type failed: " - uu___7 in - (FStar_Errors_Codes.Fatal_IllTyped, uu___6) in - FStar_Errors.raise_error uu___5 - FStar_Compiler_Range_Type.dummyRange)))) - else - (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_Tactics_Monad.ret uu___2) + let uu___ = (no_uvars_in_g g) && (no_uvars_in_term e) in + if uu___ + then + refl_typing_builtin_wrapper + (fun uu___1 -> + dbg_refl g + (fun uu___3 -> + let uu___4 = FStar_Syntax_Print.term_to_string e in + FStar_Compiler_Util.format1 + "refl_core_compute_term_type: %s\n" uu___4); + (let guards = FStar_Compiler_Util.mk_ref [] in + let gh g1 guard = + (let uu___4 = + let uu___5 = FStar_Compiler_Effect.op_Bang guards in + (g1, guard) :: uu___5 in + FStar_Compiler_Effect.op_Colon_Equals guards uu___4); + true in + let uu___3 = + FStar_TypeChecker_Core.compute_term_type_handle_guards g e gh in + match uu___3 with + | FStar_Pervasives.Inl (eff, t) -> + let t1 = refl_norm_type g t in + (dbg_refl g + (fun uu___5 -> + let uu___6 = FStar_Syntax_Print.term_to_string e in + let uu___7 = FStar_Syntax_Print.term_to_string t1 in + FStar_Compiler_Util.format2 + "refl_core_compute_term_type for %s computed type %s\n" + uu___6 uu___7); + (let uu___5 = FStar_Compiler_Effect.op_Bang guards in + ((eff, t1), uu___5))) + | FStar_Pervasives.Inr err -> + (dbg_refl g + (fun uu___5 -> + let uu___6 = FStar_TypeChecker_Core.print_error err in + FStar_Compiler_Util.format1 + "refl_core_compute_term_type: %s\n" uu___6); + (let uu___5 = + let uu___6 = + let uu___7 = FStar_TypeChecker_Core.print_error err in + Prims.op_Hat "core_compute_term_type failed: " uu___7 in + (FStar_Errors_Codes.Fatal_IllTyped, uu___6) in + FStar_Errors.raise_error uu___5 + FStar_Compiler_Range_Type.dummyRange)))) + else + (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_Tactics_Monad.ret uu___2) let (refl_core_check_term : env -> FStar_Syntax_Syntax.term -> FStar_Syntax_Syntax.typ -> - FStar_Tactics_Types.tot_or_ghost -> + FStar_TypeChecker_Core.tot_or_ghost -> (unit FStar_Pervasives_Native.option * issues) FStar_Tactics_Monad.tac) = @@ -7168,312 +7202,308 @@ let (refl_core_check_term : let (refl_tc_term : env -> FStar_Syntax_Syntax.term -> - FStar_Tactics_Types.tot_or_ghost -> - ((FStar_Syntax_Syntax.term * FStar_Syntax_Syntax.typ) - FStar_Pervasives_Native.option * issues) FStar_Tactics_Monad.tac) + ((FStar_Syntax_Syntax.term * (FStar_TypeChecker_Core.tot_or_ghost * + FStar_Syntax_Syntax.typ)) FStar_Pervasives_Native.option * issues) + FStar_Tactics_Monad.tac) = fun g -> fun e -> - fun eff -> - let uu___ = (no_uvars_in_g g) && (no_uvars_in_term e) in - if uu___ - then - refl_typing_builtin_wrapper - (fun uu___1 -> - dbg_refl g - (fun uu___3 -> - let uu___4 = FStar_Syntax_Print.term_to_string e in - FStar_Compiler_Util.format1 "refl_tc_term: %s\n" uu___4); - dbg_refl g (fun uu___4 -> "refl_tc_term: starting tc {\n"); - (let must_tot = to_must_tot eff in - let g1 = + let uu___ = (no_uvars_in_g g) && (no_uvars_in_term e) in + if uu___ + then + refl_typing_builtin_wrapper + (fun uu___1 -> + dbg_refl g + (fun uu___3 -> + let uu___4 = FStar_Syntax_Print.term_to_string e in + FStar_Compiler_Util.format1 "refl_tc_term: %s\n" uu___4); + dbg_refl g (fun uu___4 -> "refl_tc_term: starting tc {\n"); + (let g1 = + { + FStar_TypeChecker_Env.solver = + (g.FStar_TypeChecker_Env.solver); + FStar_TypeChecker_Env.range = + (g.FStar_TypeChecker_Env.range); + FStar_TypeChecker_Env.curmodule = + (g.FStar_TypeChecker_Env.curmodule); + FStar_TypeChecker_Env.gamma = + (g.FStar_TypeChecker_Env.gamma); + FStar_TypeChecker_Env.gamma_sig = + (g.FStar_TypeChecker_Env.gamma_sig); + FStar_TypeChecker_Env.gamma_cache = + (g.FStar_TypeChecker_Env.gamma_cache); + FStar_TypeChecker_Env.modules = + (g.FStar_TypeChecker_Env.modules); + FStar_TypeChecker_Env.expected_typ = + (g.FStar_TypeChecker_Env.expected_typ); + FStar_TypeChecker_Env.sigtab = + (g.FStar_TypeChecker_Env.sigtab); + FStar_TypeChecker_Env.attrtab = + (g.FStar_TypeChecker_Env.attrtab); + FStar_TypeChecker_Env.instantiate_imp = false; + FStar_TypeChecker_Env.effects = + (g.FStar_TypeChecker_Env.effects); + FStar_TypeChecker_Env.generalize = + (g.FStar_TypeChecker_Env.generalize); + FStar_TypeChecker_Env.letrecs = + (g.FStar_TypeChecker_Env.letrecs); + FStar_TypeChecker_Env.top_level = + (g.FStar_TypeChecker_Env.top_level); + FStar_TypeChecker_Env.check_uvars = + (g.FStar_TypeChecker_Env.check_uvars); + FStar_TypeChecker_Env.use_eq_strict = + (g.FStar_TypeChecker_Env.use_eq_strict); + FStar_TypeChecker_Env.is_iface = + (g.FStar_TypeChecker_Env.is_iface); + FStar_TypeChecker_Env.admit = + (g.FStar_TypeChecker_Env.admit); + FStar_TypeChecker_Env.lax = (g.FStar_TypeChecker_Env.lax); + FStar_TypeChecker_Env.lax_universes = + (g.FStar_TypeChecker_Env.lax_universes); + FStar_TypeChecker_Env.phase1 = + (g.FStar_TypeChecker_Env.phase1); + FStar_TypeChecker_Env.failhard = + (g.FStar_TypeChecker_Env.failhard); + FStar_TypeChecker_Env.nosynth = + (g.FStar_TypeChecker_Env.nosynth); + FStar_TypeChecker_Env.uvar_subtyping = + (g.FStar_TypeChecker_Env.uvar_subtyping); + FStar_TypeChecker_Env.intactics = + (g.FStar_TypeChecker_Env.intactics); + FStar_TypeChecker_Env.tc_term = + (g.FStar_TypeChecker_Env.tc_term); + FStar_TypeChecker_Env.typeof_tot_or_gtot_term = + (g.FStar_TypeChecker_Env.typeof_tot_or_gtot_term); + FStar_TypeChecker_Env.universe_of = + (g.FStar_TypeChecker_Env.universe_of); + FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term = + (g.FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term); + FStar_TypeChecker_Env.teq_nosmt_force = + (g.FStar_TypeChecker_Env.teq_nosmt_force); + FStar_TypeChecker_Env.subtype_nosmt_force = + (g.FStar_TypeChecker_Env.subtype_nosmt_force); + FStar_TypeChecker_Env.qtbl_name_and_index = + (g.FStar_TypeChecker_Env.qtbl_name_and_index); + FStar_TypeChecker_Env.normalized_eff_names = + (g.FStar_TypeChecker_Env.normalized_eff_names); + FStar_TypeChecker_Env.fv_delta_depths = + (g.FStar_TypeChecker_Env.fv_delta_depths); + FStar_TypeChecker_Env.proof_ns = + (g.FStar_TypeChecker_Env.proof_ns); + FStar_TypeChecker_Env.synth_hook = + (g.FStar_TypeChecker_Env.synth_hook); + FStar_TypeChecker_Env.try_solve_implicits_hook = + (g.FStar_TypeChecker_Env.try_solve_implicits_hook); + FStar_TypeChecker_Env.splice = + (g.FStar_TypeChecker_Env.splice); + FStar_TypeChecker_Env.mpreprocess = + (g.FStar_TypeChecker_Env.mpreprocess); + FStar_TypeChecker_Env.postprocess = + (g.FStar_TypeChecker_Env.postprocess); + FStar_TypeChecker_Env.identifier_info = + (g.FStar_TypeChecker_Env.identifier_info); + FStar_TypeChecker_Env.tc_hooks = + (g.FStar_TypeChecker_Env.tc_hooks); + FStar_TypeChecker_Env.dsenv = + (g.FStar_TypeChecker_Env.dsenv); + FStar_TypeChecker_Env.nbe = (g.FStar_TypeChecker_Env.nbe); + FStar_TypeChecker_Env.strict_args_tab = + (g.FStar_TypeChecker_Env.strict_args_tab); + FStar_TypeChecker_Env.erasable_types_tab = + (g.FStar_TypeChecker_Env.erasable_types_tab); + FStar_TypeChecker_Env.enable_defer_to_tac = + (g.FStar_TypeChecker_Env.enable_defer_to_tac); + FStar_TypeChecker_Env.unif_allow_ref_guards = + (g.FStar_TypeChecker_Env.unif_allow_ref_guards); + FStar_TypeChecker_Env.erase_erasable_args = + (g.FStar_TypeChecker_Env.erase_erasable_args); + FStar_TypeChecker_Env.core_check = + (g.FStar_TypeChecker_Env.core_check) + } in + let e1 = + let g2 = { FStar_TypeChecker_Env.solver = - (g.FStar_TypeChecker_Env.solver); + (g1.FStar_TypeChecker_Env.solver); FStar_TypeChecker_Env.range = - (g.FStar_TypeChecker_Env.range); + (g1.FStar_TypeChecker_Env.range); FStar_TypeChecker_Env.curmodule = - (g.FStar_TypeChecker_Env.curmodule); + (g1.FStar_TypeChecker_Env.curmodule); FStar_TypeChecker_Env.gamma = - (g.FStar_TypeChecker_Env.gamma); + (g1.FStar_TypeChecker_Env.gamma); FStar_TypeChecker_Env.gamma_sig = - (g.FStar_TypeChecker_Env.gamma_sig); + (g1.FStar_TypeChecker_Env.gamma_sig); FStar_TypeChecker_Env.gamma_cache = - (g.FStar_TypeChecker_Env.gamma_cache); + (g1.FStar_TypeChecker_Env.gamma_cache); FStar_TypeChecker_Env.modules = - (g.FStar_TypeChecker_Env.modules); + (g1.FStar_TypeChecker_Env.modules); FStar_TypeChecker_Env.expected_typ = - (g.FStar_TypeChecker_Env.expected_typ); + (g1.FStar_TypeChecker_Env.expected_typ); FStar_TypeChecker_Env.sigtab = - (g.FStar_TypeChecker_Env.sigtab); + (g1.FStar_TypeChecker_Env.sigtab); FStar_TypeChecker_Env.attrtab = - (g.FStar_TypeChecker_Env.attrtab); - FStar_TypeChecker_Env.instantiate_imp = false; + (g1.FStar_TypeChecker_Env.attrtab); + FStar_TypeChecker_Env.instantiate_imp = + (g1.FStar_TypeChecker_Env.instantiate_imp); FStar_TypeChecker_Env.effects = - (g.FStar_TypeChecker_Env.effects); + (g1.FStar_TypeChecker_Env.effects); FStar_TypeChecker_Env.generalize = - (g.FStar_TypeChecker_Env.generalize); + (g1.FStar_TypeChecker_Env.generalize); FStar_TypeChecker_Env.letrecs = - (g.FStar_TypeChecker_Env.letrecs); + (g1.FStar_TypeChecker_Env.letrecs); FStar_TypeChecker_Env.top_level = - (g.FStar_TypeChecker_Env.top_level); + (g1.FStar_TypeChecker_Env.top_level); FStar_TypeChecker_Env.check_uvars = - (g.FStar_TypeChecker_Env.check_uvars); + (g1.FStar_TypeChecker_Env.check_uvars); FStar_TypeChecker_Env.use_eq_strict = - (g.FStar_TypeChecker_Env.use_eq_strict); + (g1.FStar_TypeChecker_Env.use_eq_strict); FStar_TypeChecker_Env.is_iface = - (g.FStar_TypeChecker_Env.is_iface); + (g1.FStar_TypeChecker_Env.is_iface); FStar_TypeChecker_Env.admit = - (g.FStar_TypeChecker_Env.admit); - FStar_TypeChecker_Env.lax = (g.FStar_TypeChecker_Env.lax); + (g1.FStar_TypeChecker_Env.admit); + FStar_TypeChecker_Env.lax = true; FStar_TypeChecker_Env.lax_universes = - (g.FStar_TypeChecker_Env.lax_universes); - FStar_TypeChecker_Env.phase1 = - (g.FStar_TypeChecker_Env.phase1); + (g1.FStar_TypeChecker_Env.lax_universes); + FStar_TypeChecker_Env.phase1 = true; FStar_TypeChecker_Env.failhard = - (g.FStar_TypeChecker_Env.failhard); + (g1.FStar_TypeChecker_Env.failhard); FStar_TypeChecker_Env.nosynth = - (g.FStar_TypeChecker_Env.nosynth); + (g1.FStar_TypeChecker_Env.nosynth); FStar_TypeChecker_Env.uvar_subtyping = - (g.FStar_TypeChecker_Env.uvar_subtyping); + (g1.FStar_TypeChecker_Env.uvar_subtyping); FStar_TypeChecker_Env.intactics = - (g.FStar_TypeChecker_Env.intactics); + (g1.FStar_TypeChecker_Env.intactics); FStar_TypeChecker_Env.tc_term = - (g.FStar_TypeChecker_Env.tc_term); + (g1.FStar_TypeChecker_Env.tc_term); FStar_TypeChecker_Env.typeof_tot_or_gtot_term = - (g.FStar_TypeChecker_Env.typeof_tot_or_gtot_term); + (g1.FStar_TypeChecker_Env.typeof_tot_or_gtot_term); FStar_TypeChecker_Env.universe_of = - (g.FStar_TypeChecker_Env.universe_of); + (g1.FStar_TypeChecker_Env.universe_of); FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term = - (g.FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term); + (g1.FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term); FStar_TypeChecker_Env.teq_nosmt_force = - (g.FStar_TypeChecker_Env.teq_nosmt_force); + (g1.FStar_TypeChecker_Env.teq_nosmt_force); FStar_TypeChecker_Env.subtype_nosmt_force = - (g.FStar_TypeChecker_Env.subtype_nosmt_force); + (g1.FStar_TypeChecker_Env.subtype_nosmt_force); FStar_TypeChecker_Env.qtbl_name_and_index = - (g.FStar_TypeChecker_Env.qtbl_name_and_index); + (g1.FStar_TypeChecker_Env.qtbl_name_and_index); FStar_TypeChecker_Env.normalized_eff_names = - (g.FStar_TypeChecker_Env.normalized_eff_names); + (g1.FStar_TypeChecker_Env.normalized_eff_names); FStar_TypeChecker_Env.fv_delta_depths = - (g.FStar_TypeChecker_Env.fv_delta_depths); + (g1.FStar_TypeChecker_Env.fv_delta_depths); FStar_TypeChecker_Env.proof_ns = - (g.FStar_TypeChecker_Env.proof_ns); + (g1.FStar_TypeChecker_Env.proof_ns); FStar_TypeChecker_Env.synth_hook = - (g.FStar_TypeChecker_Env.synth_hook); + (g1.FStar_TypeChecker_Env.synth_hook); FStar_TypeChecker_Env.try_solve_implicits_hook = - (g.FStar_TypeChecker_Env.try_solve_implicits_hook); + (g1.FStar_TypeChecker_Env.try_solve_implicits_hook); FStar_TypeChecker_Env.splice = - (g.FStar_TypeChecker_Env.splice); + (g1.FStar_TypeChecker_Env.splice); FStar_TypeChecker_Env.mpreprocess = - (g.FStar_TypeChecker_Env.mpreprocess); + (g1.FStar_TypeChecker_Env.mpreprocess); FStar_TypeChecker_Env.postprocess = - (g.FStar_TypeChecker_Env.postprocess); + (g1.FStar_TypeChecker_Env.postprocess); FStar_TypeChecker_Env.identifier_info = - (g.FStar_TypeChecker_Env.identifier_info); + (g1.FStar_TypeChecker_Env.identifier_info); FStar_TypeChecker_Env.tc_hooks = - (g.FStar_TypeChecker_Env.tc_hooks); + (g1.FStar_TypeChecker_Env.tc_hooks); FStar_TypeChecker_Env.dsenv = - (g.FStar_TypeChecker_Env.dsenv); - FStar_TypeChecker_Env.nbe = (g.FStar_TypeChecker_Env.nbe); + (g1.FStar_TypeChecker_Env.dsenv); + FStar_TypeChecker_Env.nbe = + (g1.FStar_TypeChecker_Env.nbe); FStar_TypeChecker_Env.strict_args_tab = - (g.FStar_TypeChecker_Env.strict_args_tab); + (g1.FStar_TypeChecker_Env.strict_args_tab); FStar_TypeChecker_Env.erasable_types_tab = - (g.FStar_TypeChecker_Env.erasable_types_tab); + (g1.FStar_TypeChecker_Env.erasable_types_tab); FStar_TypeChecker_Env.enable_defer_to_tac = - (g.FStar_TypeChecker_Env.enable_defer_to_tac); + (g1.FStar_TypeChecker_Env.enable_defer_to_tac); FStar_TypeChecker_Env.unif_allow_ref_guards = - (g.FStar_TypeChecker_Env.unif_allow_ref_guards); + (g1.FStar_TypeChecker_Env.unif_allow_ref_guards); FStar_TypeChecker_Env.erase_erasable_args = - (g.FStar_TypeChecker_Env.erase_erasable_args); + (g1.FStar_TypeChecker_Env.erase_erasable_args); FStar_TypeChecker_Env.core_check = - (g.FStar_TypeChecker_Env.core_check) + (g1.FStar_TypeChecker_Env.core_check) } in - let e1 = - let g2 = - { - FStar_TypeChecker_Env.solver = - (g1.FStar_TypeChecker_Env.solver); - FStar_TypeChecker_Env.range = - (g1.FStar_TypeChecker_Env.range); - FStar_TypeChecker_Env.curmodule = - (g1.FStar_TypeChecker_Env.curmodule); - FStar_TypeChecker_Env.gamma = - (g1.FStar_TypeChecker_Env.gamma); - FStar_TypeChecker_Env.gamma_sig = - (g1.FStar_TypeChecker_Env.gamma_sig); - FStar_TypeChecker_Env.gamma_cache = - (g1.FStar_TypeChecker_Env.gamma_cache); - FStar_TypeChecker_Env.modules = - (g1.FStar_TypeChecker_Env.modules); - FStar_TypeChecker_Env.expected_typ = - (g1.FStar_TypeChecker_Env.expected_typ); - FStar_TypeChecker_Env.sigtab = - (g1.FStar_TypeChecker_Env.sigtab); - FStar_TypeChecker_Env.attrtab = - (g1.FStar_TypeChecker_Env.attrtab); - FStar_TypeChecker_Env.instantiate_imp = - (g1.FStar_TypeChecker_Env.instantiate_imp); - FStar_TypeChecker_Env.effects = - (g1.FStar_TypeChecker_Env.effects); - FStar_TypeChecker_Env.generalize = - (g1.FStar_TypeChecker_Env.generalize); - FStar_TypeChecker_Env.letrecs = - (g1.FStar_TypeChecker_Env.letrecs); - FStar_TypeChecker_Env.top_level = - (g1.FStar_TypeChecker_Env.top_level); - FStar_TypeChecker_Env.check_uvars = - (g1.FStar_TypeChecker_Env.check_uvars); - FStar_TypeChecker_Env.use_eq_strict = - (g1.FStar_TypeChecker_Env.use_eq_strict); - FStar_TypeChecker_Env.is_iface = - (g1.FStar_TypeChecker_Env.is_iface); - FStar_TypeChecker_Env.admit = - (g1.FStar_TypeChecker_Env.admit); - FStar_TypeChecker_Env.lax = true; - FStar_TypeChecker_Env.lax_universes = - (g1.FStar_TypeChecker_Env.lax_universes); - FStar_TypeChecker_Env.phase1 = true; - FStar_TypeChecker_Env.failhard = - (g1.FStar_TypeChecker_Env.failhard); - FStar_TypeChecker_Env.nosynth = - (g1.FStar_TypeChecker_Env.nosynth); - FStar_TypeChecker_Env.uvar_subtyping = - (g1.FStar_TypeChecker_Env.uvar_subtyping); - FStar_TypeChecker_Env.intactics = - (g1.FStar_TypeChecker_Env.intactics); - FStar_TypeChecker_Env.tc_term = - (g1.FStar_TypeChecker_Env.tc_term); - FStar_TypeChecker_Env.typeof_tot_or_gtot_term = - (g1.FStar_TypeChecker_Env.typeof_tot_or_gtot_term); - FStar_TypeChecker_Env.universe_of = - (g1.FStar_TypeChecker_Env.universe_of); - FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term - = - (g1.FStar_TypeChecker_Env.typeof_well_typed_tot_or_gtot_term); - FStar_TypeChecker_Env.teq_nosmt_force = - (g1.FStar_TypeChecker_Env.teq_nosmt_force); - FStar_TypeChecker_Env.subtype_nosmt_force = - (g1.FStar_TypeChecker_Env.subtype_nosmt_force); - FStar_TypeChecker_Env.qtbl_name_and_index = - (g1.FStar_TypeChecker_Env.qtbl_name_and_index); - FStar_TypeChecker_Env.normalized_eff_names = - (g1.FStar_TypeChecker_Env.normalized_eff_names); - FStar_TypeChecker_Env.fv_delta_depths = - (g1.FStar_TypeChecker_Env.fv_delta_depths); - FStar_TypeChecker_Env.proof_ns = - (g1.FStar_TypeChecker_Env.proof_ns); - FStar_TypeChecker_Env.synth_hook = - (g1.FStar_TypeChecker_Env.synth_hook); - FStar_TypeChecker_Env.try_solve_implicits_hook = - (g1.FStar_TypeChecker_Env.try_solve_implicits_hook); - FStar_TypeChecker_Env.splice = - (g1.FStar_TypeChecker_Env.splice); - FStar_TypeChecker_Env.mpreprocess = - (g1.FStar_TypeChecker_Env.mpreprocess); - FStar_TypeChecker_Env.postprocess = - (g1.FStar_TypeChecker_Env.postprocess); - FStar_TypeChecker_Env.identifier_info = - (g1.FStar_TypeChecker_Env.identifier_info); - FStar_TypeChecker_Env.tc_hooks = - (g1.FStar_TypeChecker_Env.tc_hooks); - FStar_TypeChecker_Env.dsenv = - (g1.FStar_TypeChecker_Env.dsenv); - FStar_TypeChecker_Env.nbe = - (g1.FStar_TypeChecker_Env.nbe); - FStar_TypeChecker_Env.strict_args_tab = - (g1.FStar_TypeChecker_Env.strict_args_tab); - FStar_TypeChecker_Env.erasable_types_tab = - (g1.FStar_TypeChecker_Env.erasable_types_tab); - FStar_TypeChecker_Env.enable_defer_to_tac = - (g1.FStar_TypeChecker_Env.enable_defer_to_tac); - FStar_TypeChecker_Env.unif_allow_ref_guards = - (g1.FStar_TypeChecker_Env.unif_allow_ref_guards); - FStar_TypeChecker_Env.erase_erasable_args = - (g1.FStar_TypeChecker_Env.erase_erasable_args); - FStar_TypeChecker_Env.core_check = - (g1.FStar_TypeChecker_Env.core_check) - } in - let uu___4 = - g2.FStar_TypeChecker_Env.typeof_tot_or_gtot_term g2 e - must_tot in - match uu___4 with - | (e2, uu___5, guard) -> - (FStar_TypeChecker_Rel.force_trivial_guard g2 guard; e2) in - try - (fun uu___4 -> - match () with - | () -> - let e2 = - FStar_Syntax_Compress.deep_compress false e1 in - (dbg_refl g1 - (fun uu___6 -> - let uu___7 = - FStar_Syntax_Print.term_to_string e2 in - FStar_Compiler_Util.format1 - "} finished tc with e = %s\n" uu___7); - (let guards = FStar_Compiler_Util.mk_ref [] in - let gh g2 guard = - (let uu___7 = - let uu___8 = - FStar_Compiler_Effect.op_Bang guards in - (g2, guard) :: uu___8 in - FStar_Compiler_Effect.op_Colon_Equals guards - uu___7); - true in - let uu___6 = - FStar_TypeChecker_Core.compute_term_type_handle_guards - g1 e2 must_tot gh in - match uu___6 with - | FStar_Pervasives.Inl t -> - let t1 = refl_norm_type g1 t in - (dbg_refl g1 - (fun uu___8 -> - let uu___9 = - FStar_Syntax_Print.term_to_string e2 in - let uu___10 = - FStar_Syntax_Print.term_to_string t1 in - FStar_Compiler_Util.format2 - "refl_tc_term for %s computed type %s\n" - uu___9 uu___10); - (let uu___8 = - FStar_Compiler_Effect.op_Bang guards in - ((e2, t1), uu___8))) - | FStar_Pervasives.Inr err -> - (dbg_refl g1 - (fun uu___8 -> - let uu___9 = - FStar_TypeChecker_Core.print_error err in - FStar_Compiler_Util.format1 - "refl_tc_term failed: %s\n" uu___9); - (let uu___8 = + let must_tot = false in + let uu___4 = + g2.FStar_TypeChecker_Env.typeof_tot_or_gtot_term g2 e + must_tot in + match uu___4 with + | (e2, uu___5, guard) -> + (FStar_TypeChecker_Rel.force_trivial_guard g2 guard; e2) in + try + (fun uu___4 -> + match () with + | () -> + let e2 = FStar_Syntax_Compress.deep_compress false e1 in + (dbg_refl g1 + (fun uu___6 -> + let uu___7 = + FStar_Syntax_Print.term_to_string e2 in + FStar_Compiler_Util.format1 + "} finished tc with e = %s\n" uu___7); + (let guards = FStar_Compiler_Util.mk_ref [] in + let gh g2 guard = + (let uu___7 = + let uu___8 = + FStar_Compiler_Effect.op_Bang guards in + (g2, guard) :: uu___8 in + FStar_Compiler_Effect.op_Colon_Equals guards + uu___7); + true in + let uu___6 = + FStar_TypeChecker_Core.compute_term_type_handle_guards + g1 e2 gh in + match uu___6 with + | FStar_Pervasives.Inl (eff, t) -> + let t1 = refl_norm_type g1 t in + (dbg_refl g1 + (fun uu___8 -> let uu___9 = - let uu___10 = - FStar_TypeChecker_Core.print_error err in - Prims.op_Hat "tc_term callback failed: " - uu___10 in - (FStar_Errors_Codes.Fatal_IllTyped, - uu___9) in - FStar_Errors.raise_error uu___8 - e2.FStar_Syntax_Syntax.pos))))) () - with - | FStar_Errors.Error - (FStar_Errors_Codes.Error_UnexpectedUnresolvedUvar, - uu___5, uu___6, uu___7) - -> - FStar_Errors.raise_error - (FStar_Errors_Codes.Fatal_IllTyped, - "UVars remaing in term after tc_term callback") - e1.FStar_Syntax_Syntax.pos)) - else - (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_Tactics_Monad.ret uu___2) + FStar_Syntax_Print.term_to_string e2 in + let uu___10 = + FStar_Syntax_Print.term_to_string t1 in + FStar_Compiler_Util.format2 + "refl_tc_term for %s computed type %s\n" + uu___9 uu___10); + (let uu___8 = + FStar_Compiler_Effect.op_Bang guards in + ((e2, (eff, t1)), uu___8))) + | FStar_Pervasives.Inr err -> + (dbg_refl g1 + (fun uu___8 -> + let uu___9 = + FStar_TypeChecker_Core.print_error err in + FStar_Compiler_Util.format1 + "refl_tc_term failed: %s\n" uu___9); + (let uu___8 = + let uu___9 = + let uu___10 = + FStar_TypeChecker_Core.print_error err in + Prims.op_Hat "tc_term callback failed: " + uu___10 in + (FStar_Errors_Codes.Fatal_IllTyped, uu___9) in + FStar_Errors.raise_error uu___8 + e2.FStar_Syntax_Syntax.pos))))) () + with + | FStar_Errors.Error + (FStar_Errors_Codes.Error_UnexpectedUnresolvedUvar, uu___5, + uu___6, uu___7) + -> + FStar_Errors.raise_error + (FStar_Errors_Codes.Fatal_IllTyped, + "UVars remaing in term after tc_term callback") + e1.FStar_Syntax_Syntax.pos)) + else + (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_Tactics_Monad.ret uu___2) let (refl_universe_of : env -> FStar_Syntax_Syntax.term -> @@ -7718,7 +7748,7 @@ let (refl_instantiate_implicits : "refl_instantiate_implicits: %s\n" uu___4); dbg_refl g (fun uu___4 -> "refl_instantiate_implicits: starting tc {\n"); - (let must_tot = true in + (let must_tot = false in let g1 = { FStar_TypeChecker_Env.solver = diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Interpreter.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Interpreter.ml index d17cafb60aa..8ab11b83ddd 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Interpreter.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Interpreter.ml @@ -1788,18 +1788,16 @@ let (uu___193 : unit) = FStar_TypeChecker_NBETerm.e_tuple2 uu___169 uu___170 in - FStar_Tactics_V2_InterpFuns.mk_tac_step_3 + FStar_Tactics_V2_InterpFuns.mk_tac_step_2 Prims.int_zero - "check_subtyping" - FStar_Tactics_V2_Basic.refl_check_subtyping + "is_non_informative" + FStar_Tactics_V2_Basic.refl_is_non_informative FStar_Reflection_V2_Embeddings.e_env FStar_Reflection_V2_Embeddings.e_term - FStar_Reflection_V2_Embeddings.e_term uu___167 - FStar_Tactics_V2_Basic.refl_check_subtyping + FStar_Tactics_V2_Basic.refl_is_non_informative FStar_Reflection_V2_NBEEmbeddings.e_env FStar_Reflection_V2_NBEEmbeddings.e_term - FStar_Reflection_V2_NBEEmbeddings.e_term uu___168 in let uu___167 = @@ -1833,13 +1831,13 @@ let (uu___193 : unit) = uu___172 in FStar_Tactics_V2_InterpFuns.mk_tac_step_3 Prims.int_zero - "check_equiv" - FStar_Tactics_V2_Basic.refl_check_equiv + "check_subtyping" + FStar_Tactics_V2_Basic.refl_check_subtyping FStar_Reflection_V2_Embeddings.e_env FStar_Reflection_V2_Embeddings.e_term FStar_Reflection_V2_Embeddings.e_term uu___169 - FStar_Tactics_V2_Basic.refl_check_equiv + FStar_Tactics_V2_Basic.refl_check_subtyping FStar_Reflection_V2_NBEEmbeddings.e_env FStar_Reflection_V2_NBEEmbeddings.e_term FStar_Reflection_V2_NBEEmbeddings.e_term @@ -1853,7 +1851,7 @@ let (uu___193 : unit) = let uu___172 = FStar_Syntax_Embeddings.e_option - FStar_Reflection_V2_Embeddings.e_term in + FStar_Syntax_Embeddings.e_unit in let uu___173 = FStar_Syntax_Embeddings.e_list @@ -1866,7 +1864,7 @@ let (uu___193 : unit) = let uu___173 = FStar_TypeChecker_NBETerm.e_option - FStar_Reflection_V2_NBEEmbeddings.e_term in + FStar_TypeChecker_NBETerm.e_unit in let uu___174 = FStar_TypeChecker_NBETerm.e_list @@ -1876,16 +1874,16 @@ let (uu___193 : unit) = uu___174 in FStar_Tactics_V2_InterpFuns.mk_tac_step_3 Prims.int_zero - "core_compute_term_type" - FStar_Tactics_V2_Basic.refl_core_compute_term_type + "check_equiv" + FStar_Tactics_V2_Basic.refl_check_equiv FStar_Reflection_V2_Embeddings.e_env FStar_Reflection_V2_Embeddings.e_term - FStar_Tactics_Embedding.e_tot_or_ghost + FStar_Reflection_V2_Embeddings.e_term uu___171 - FStar_Tactics_V2_Basic.refl_core_compute_term_type + FStar_Tactics_V2_Basic.refl_check_equiv FStar_Reflection_V2_NBEEmbeddings.e_env FStar_Reflection_V2_NBEEmbeddings.e_term - FStar_Tactics_Embedding.e_tot_or_ghost_nbe + FStar_Reflection_V2_NBEEmbeddings.e_term uu___172 in let uu___171 = @@ -1895,8 +1893,13 @@ let (uu___193 : unit) = = let uu___174 = + let uu___175 + = + FStar_Syntax_Embeddings.e_tuple2 + FStar_Tactics_Embedding.e_tot_or_ghost + FStar_Reflection_V2_Embeddings.e_term in FStar_Syntax_Embeddings.e_option - FStar_Syntax_Embeddings.e_unit in + uu___175 in let uu___175 = FStar_Syntax_Embeddings.e_list @@ -1908,8 +1911,13 @@ let (uu___193 : unit) = = let uu___175 = + let uu___176 + = + FStar_TypeChecker_NBETerm.e_tuple2 + FStar_Tactics_Embedding.e_tot_or_ghost_nbe + FStar_Reflection_V2_NBEEmbeddings.e_term in FStar_TypeChecker_NBETerm.e_option - FStar_TypeChecker_NBETerm.e_unit in + uu___176 in let uu___176 = FStar_TypeChecker_NBETerm.e_list @@ -1917,20 +1925,16 @@ let (uu___193 : unit) = FStar_TypeChecker_NBETerm.e_tuple2 uu___175 uu___176 in - FStar_Tactics_V2_InterpFuns.mk_tac_step_4 + FStar_Tactics_V2_InterpFuns.mk_tac_step_2 Prims.int_zero - "core_check_term" - FStar_Tactics_V2_Basic.refl_core_check_term + "core_compute_term_type" + FStar_Tactics_V2_Basic.refl_core_compute_term_type FStar_Reflection_V2_Embeddings.e_env FStar_Reflection_V2_Embeddings.e_term - FStar_Reflection_V2_Embeddings.e_term - FStar_Tactics_Embedding.e_tot_or_ghost uu___173 - FStar_Tactics_V2_Basic.refl_core_check_term + FStar_Tactics_V2_Basic.refl_core_compute_term_type FStar_Reflection_V2_NBEEmbeddings.e_env FStar_Reflection_V2_NBEEmbeddings.e_term - FStar_Reflection_V2_NBEEmbeddings.e_term - FStar_Tactics_Embedding.e_tot_or_ghost_nbe uu___174 in let uu___173 = @@ -1940,13 +1944,8 @@ let (uu___193 : unit) = = let uu___176 = - let uu___177 - = - FStar_Syntax_Embeddings.e_tuple2 - FStar_Reflection_V2_Embeddings.e_term - FStar_Reflection_V2_Embeddings.e_term in FStar_Syntax_Embeddings.e_option - uu___177 in + FStar_Syntax_Embeddings.e_unit in let uu___177 = FStar_Syntax_Embeddings.e_list @@ -1958,13 +1957,8 @@ let (uu___193 : unit) = = let uu___177 = - let uu___178 - = - FStar_TypeChecker_NBETerm.e_tuple2 - FStar_Reflection_V2_NBEEmbeddings.e_term - FStar_Reflection_V2_NBEEmbeddings.e_term in FStar_TypeChecker_NBETerm.e_option - uu___178 in + FStar_TypeChecker_NBETerm.e_unit in let uu___178 = FStar_TypeChecker_NBETerm.e_list @@ -1972,17 +1966,19 @@ let (uu___193 : unit) = FStar_TypeChecker_NBETerm.e_tuple2 uu___177 uu___178 in - FStar_Tactics_V2_InterpFuns.mk_tac_step_3 + FStar_Tactics_V2_InterpFuns.mk_tac_step_4 Prims.int_zero - "tc_term" - FStar_Tactics_V2_Basic.refl_tc_term + "core_check_term" + FStar_Tactics_V2_Basic.refl_core_check_term FStar_Reflection_V2_Embeddings.e_env FStar_Reflection_V2_Embeddings.e_term + FStar_Reflection_V2_Embeddings.e_term FStar_Tactics_Embedding.e_tot_or_ghost uu___175 - FStar_Tactics_V2_Basic.refl_tc_term + FStar_Tactics_V2_Basic.refl_core_check_term FStar_Reflection_V2_NBEEmbeddings.e_env FStar_Reflection_V2_NBEEmbeddings.e_term + FStar_Reflection_V2_NBEEmbeddings.e_term FStar_Tactics_Embedding.e_tot_or_ghost_nbe uu___176 in let uu___175 @@ -1993,8 +1989,18 @@ let (uu___193 : unit) = = let uu___178 = + let uu___179 + = + let uu___180 + = + FStar_Syntax_Embeddings.e_tuple2 + FStar_Tactics_Embedding.e_tot_or_ghost + FStar_Reflection_V2_Embeddings.e_term in + FStar_Syntax_Embeddings.e_tuple2 + FStar_Reflection_V2_Embeddings.e_term + uu___180 in FStar_Syntax_Embeddings.e_option - FStar_Reflection_V2_Embeddings.e_universe in + uu___179 in let uu___179 = FStar_Syntax_Embeddings.e_list @@ -2006,8 +2012,18 @@ let (uu___193 : unit) = = let uu___179 = + let uu___180 + = + let uu___181 + = + FStar_TypeChecker_NBETerm.e_tuple2 + FStar_Tactics_Embedding.e_tot_or_ghost_nbe + FStar_Reflection_V2_NBEEmbeddings.e_term in + FStar_TypeChecker_NBETerm.e_tuple2 + FStar_Reflection_V2_NBEEmbeddings.e_term + uu___181 in FStar_TypeChecker_NBETerm.e_option - FStar_Reflection_V2_NBEEmbeddings.e_universe in + uu___180 in let uu___180 = FStar_TypeChecker_NBETerm.e_list @@ -2017,12 +2033,12 @@ let (uu___193 : unit) = uu___180 in FStar_Tactics_V2_InterpFuns.mk_tac_step_2 Prims.int_zero - "universe_of" - FStar_Tactics_V2_Basic.refl_universe_of + "tc_term" + FStar_Tactics_V2_Basic.refl_tc_term FStar_Reflection_V2_Embeddings.e_env FStar_Reflection_V2_Embeddings.e_term uu___177 - FStar_Tactics_V2_Basic.refl_universe_of + FStar_Tactics_V2_Basic.refl_tc_term FStar_Reflection_V2_NBEEmbeddings.e_env FStar_Reflection_V2_NBEEmbeddings.e_term uu___178 in @@ -2035,7 +2051,7 @@ let (uu___193 : unit) = let uu___180 = FStar_Syntax_Embeddings.e_option - FStar_Syntax_Embeddings.e_unit in + FStar_Reflection_V2_Embeddings.e_universe in let uu___181 = FStar_Syntax_Embeddings.e_list @@ -2048,7 +2064,7 @@ let (uu___193 : unit) = let uu___181 = FStar_TypeChecker_NBETerm.e_option - FStar_TypeChecker_NBETerm.e_unit in + FStar_Reflection_V2_NBEEmbeddings.e_universe in let uu___182 = FStar_TypeChecker_NBETerm.e_list @@ -2058,12 +2074,12 @@ let (uu___193 : unit) = uu___182 in FStar_Tactics_V2_InterpFuns.mk_tac_step_2 Prims.int_zero - "check_prop_validity" - FStar_Tactics_V2_Basic.refl_check_prop_validity + "universe_of" + FStar_Tactics_V2_Basic.refl_universe_of FStar_Reflection_V2_Embeddings.e_env FStar_Reflection_V2_Embeddings.e_term uu___179 - FStar_Tactics_V2_Basic.refl_check_prop_validity + FStar_Tactics_V2_Basic.refl_universe_of FStar_Reflection_V2_NBEEmbeddings.e_env FStar_Reflection_V2_NBEEmbeddings.e_term uu___180 in @@ -2073,54 +2089,95 @@ let (uu___193 : unit) = = let uu___181 = + let uu___182 + = + FStar_Syntax_Embeddings.e_option + FStar_Syntax_Embeddings.e_unit in + let uu___183 + = FStar_Syntax_Embeddings.e_list - FStar_Reflection_V2_Embeddings.e_pattern in + FStar_Syntax_Embeddings.e_issue in + FStar_Syntax_Embeddings.e_tuple2 + uu___182 + uu___183 in let uu___182 = let uu___183 = + FStar_TypeChecker_NBETerm.e_option + FStar_TypeChecker_NBETerm.e_unit in let uu___184 = + FStar_TypeChecker_NBETerm.e_list + FStar_TypeChecker_NBETerm.e_issue in + FStar_TypeChecker_NBETerm.e_tuple2 + uu___183 + uu___184 in + FStar_Tactics_V2_InterpFuns.mk_tac_step_2 + Prims.int_zero + "check_prop_validity" + FStar_Tactics_V2_Basic.refl_check_prop_validity + FStar_Reflection_V2_Embeddings.e_env + FStar_Reflection_V2_Embeddings.e_term + uu___181 + FStar_Tactics_V2_Basic.refl_check_prop_validity + FStar_Reflection_V2_NBEEmbeddings.e_env + FStar_Reflection_V2_NBEEmbeddings.e_term + uu___182 in + let uu___181 + = + let uu___182 + = + let uu___183 + = FStar_Syntax_Embeddings.e_list FStar_Reflection_V2_Embeddings.e_pattern in + let uu___184 + = let uu___185 = let uu___186 = FStar_Syntax_Embeddings.e_list + FStar_Reflection_V2_Embeddings.e_pattern in + let uu___187 + = + let uu___188 + = + FStar_Syntax_Embeddings.e_list FStar_Reflection_V2_Embeddings.e_binding in FStar_Syntax_Embeddings.e_list - uu___186 in + uu___188 in FStar_Syntax_Embeddings.e_tuple2 - uu___184 - uu___185 in + uu___186 + uu___187 in FStar_Syntax_Embeddings.e_option - uu___183 in - let uu___183 + uu___185 in + let uu___185 = FStar_TypeChecker_NBETerm.e_list FStar_Reflection_V2_NBEEmbeddings.e_pattern in - let uu___184 + let uu___186 = - let uu___185 + let uu___187 = - let uu___186 + let uu___188 = FStar_TypeChecker_NBETerm.e_list FStar_Reflection_V2_NBEEmbeddings.e_pattern in - let uu___187 + let uu___189 = - let uu___188 + let uu___190 = FStar_TypeChecker_NBETerm.e_list FStar_Reflection_V2_NBEEmbeddings.e_binding in FStar_TypeChecker_NBETerm.e_list - uu___188 in + uu___190 in FStar_TypeChecker_NBETerm.e_tuple2 - uu___186 - uu___187 in + uu___188 + uu___189 in FStar_TypeChecker_NBETerm.e_option - uu___185 in + uu___187 in FStar_Tactics_V2_InterpFuns.mk_tac_step_4 Prims.int_zero "check_match_complete" @@ -2128,95 +2185,95 @@ let (uu___193 : unit) = FStar_Reflection_V2_Embeddings.e_env FStar_Reflection_V2_Embeddings.e_term FStar_Reflection_V2_Embeddings.e_term - uu___181 - uu___182 + uu___183 + uu___184 FStar_Tactics_V2_Basic.refl_check_match_complete FStar_Reflection_V2_NBEEmbeddings.e_env FStar_Reflection_V2_NBEEmbeddings.e_term FStar_Reflection_V2_NBEEmbeddings.e_term - uu___183 - uu___184 in - let uu___181 - = - let uu___182 - = + uu___185 + uu___186 in let uu___183 = let uu___184 = let uu___185 = + let uu___186 + = + let uu___187 + = FStar_Syntax_Embeddings.e_tuple2 FStar_Reflection_V2_Embeddings.e_term FStar_Reflection_V2_Embeddings.e_term in FStar_Syntax_Embeddings.e_option - uu___185 in - let uu___185 + uu___187 in + let uu___187 = FStar_Syntax_Embeddings.e_list FStar_Syntax_Embeddings.e_issue in FStar_Syntax_Embeddings.e_tuple2 - uu___184 - uu___185 in - let uu___184 + uu___186 + uu___187 in + let uu___186 = - let uu___185 + let uu___187 = - let uu___186 + let uu___188 = FStar_TypeChecker_NBETerm.e_tuple2 FStar_Reflection_V2_NBEEmbeddings.e_term FStar_Reflection_V2_NBEEmbeddings.e_term in FStar_TypeChecker_NBETerm.e_option - uu___186 in - let uu___186 + uu___188 in + let uu___188 = FStar_TypeChecker_NBETerm.e_list FStar_TypeChecker_NBETerm.e_issue in FStar_TypeChecker_NBETerm.e_tuple2 - uu___185 - uu___186 in + uu___187 + uu___188 in FStar_Tactics_V2_InterpFuns.mk_tac_step_2 Prims.int_zero "instantiate_implicits" FStar_Tactics_V2_Basic.refl_instantiate_implicits FStar_Reflection_V2_Embeddings.e_env FStar_Reflection_V2_Embeddings.e_term - uu___183 + uu___185 FStar_Tactics_V2_Basic.refl_instantiate_implicits FStar_Reflection_V2_NBEEmbeddings.e_env FStar_Reflection_V2_NBEEmbeddings.e_term - uu___184 in - let uu___183 - = - let uu___184 - = + uu___186 in let uu___185 = let uu___186 = + let uu___187 + = + let uu___188 + = FStar_Syntax_Embeddings.e_option FStar_Tactics_Embedding.e_unfold_side in - let uu___187 + let uu___189 = FStar_Syntax_Embeddings.e_list FStar_Syntax_Embeddings.e_issue in FStar_Syntax_Embeddings.e_tuple2 - uu___186 - uu___187 in - let uu___186 + uu___188 + uu___189 in + let uu___188 = - let uu___187 + let uu___189 = FStar_TypeChecker_NBETerm.e_option FStar_Tactics_Embedding.e_unfold_side_nbe in - let uu___188 + let uu___190 = FStar_TypeChecker_NBETerm.e_list FStar_TypeChecker_NBETerm.e_issue in FStar_TypeChecker_NBETerm.e_tuple2 - uu___187 - uu___188 in + uu___189 + uu___190 in FStar_Tactics_V2_InterpFuns.mk_tac_step_3 Prims.int_zero "maybe_relate_after_unfolding" @@ -2224,62 +2281,62 @@ let (uu___193 : unit) = FStar_Reflection_V2_Embeddings.e_env FStar_Reflection_V2_Embeddings.e_term FStar_Reflection_V2_Embeddings.e_term - uu___185 + uu___187 FStar_Tactics_V2_Basic.refl_maybe_relate_after_unfolding FStar_Reflection_V2_NBEEmbeddings.e_env FStar_Reflection_V2_NBEEmbeddings.e_term FStar_Reflection_V2_NBEEmbeddings.e_term - uu___186 in - let uu___185 - = - let uu___186 - = + uu___188 in let uu___187 = let uu___188 = + let uu___189 + = + let uu___190 + = FStar_Syntax_Embeddings.e_option FStar_Reflection_V2_Embeddings.e_term in - let uu___189 + let uu___191 = FStar_Syntax_Embeddings.e_list FStar_Syntax_Embeddings.e_issue in FStar_Syntax_Embeddings.e_tuple2 - uu___188 - uu___189 in - let uu___188 + uu___190 + uu___191 in + let uu___190 = - let uu___189 + let uu___191 = FStar_TypeChecker_NBETerm.e_option FStar_Reflection_V2_NBEEmbeddings.e_term in - let uu___190 + let uu___192 = FStar_TypeChecker_NBETerm.e_list FStar_TypeChecker_NBETerm.e_issue in FStar_TypeChecker_NBETerm.e_tuple2 - uu___189 - uu___190 in + uu___191 + uu___192 in FStar_Tactics_V2_InterpFuns.mk_tac_step_2 Prims.int_zero "maybe_unfold_head" FStar_Tactics_V2_Basic.refl_maybe_unfold_head FStar_Reflection_V2_Embeddings.e_env FStar_Reflection_V2_Embeddings.e_term - uu___187 + uu___189 FStar_Tactics_V2_Basic.refl_maybe_unfold_head FStar_Reflection_V2_NBEEmbeddings.e_env FStar_Reflection_V2_NBEEmbeddings.e_term - uu___188 in - let uu___187 + uu___190 in + let uu___189 = - let uu___188 + let uu___190 = - let uu___189 + let uu___191 = FStar_Syntax_Embeddings.e_list FStar_Syntax_Embeddings.e_string in - let uu___190 + let uu___192 = FStar_TypeChecker_NBETerm.e_list FStar_TypeChecker_NBETerm.e_string in @@ -2288,21 +2345,21 @@ let (uu___193 : unit) = "push_open_namespace" FStar_Tactics_V2_Basic.push_open_namespace FStar_Reflection_V2_Embeddings.e_env - uu___189 + uu___191 FStar_Reflection_V2_Embeddings.e_env FStar_Tactics_V2_Basic.push_open_namespace FStar_Reflection_V2_NBEEmbeddings.e_env - uu___190 + uu___192 FStar_Reflection_V2_NBEEmbeddings.e_env in - let uu___189 + let uu___191 = - let uu___190 + let uu___192 = - let uu___191 + let uu___194 = FStar_Syntax_Embeddings.e_list FStar_Syntax_Embeddings.e_string in - let uu___192 + let uu___195 = FStar_TypeChecker_NBETerm.e_list FStar_TypeChecker_NBETerm.e_string in @@ -2312,63 +2369,63 @@ let (uu___193 : unit) = FStar_Tactics_V2_Basic.push_module_abbrev FStar_Reflection_V2_Embeddings.e_env FStar_Syntax_Embeddings.e_string - uu___191 + uu___194 FStar_Reflection_V2_Embeddings.e_env FStar_Tactics_V2_Basic.push_module_abbrev FStar_Reflection_V2_NBEEmbeddings.e_env FStar_TypeChecker_NBETerm.e_string - uu___192 + uu___195 FStar_Reflection_V2_NBEEmbeddings.e_env in - let uu___191 + let uu___194 = - let uu___192 + let uu___195 = - let uu___194 + let uu___196 = FStar_Syntax_Embeddings.e_list FStar_Syntax_Embeddings.e_string in - let uu___195 + let uu___197 = - let uu___196 + let uu___198 = FStar_Syntax_Embeddings.e_either FStar_Reflection_V2_Embeddings.e_bv FStar_Reflection_V2_Embeddings.e_fv in FStar_Syntax_Embeddings.e_option - uu___196 in - let uu___196 + uu___198 in + let uu___198 = FStar_TypeChecker_NBETerm.e_list FStar_TypeChecker_NBETerm.e_string in - let uu___197 + let uu___199 = - let uu___198 + let uu___200 = FStar_TypeChecker_NBETerm.e_either FStar_Reflection_V2_NBEEmbeddings.e_bv FStar_Reflection_V2_NBEEmbeddings.e_fv in FStar_TypeChecker_NBETerm.e_option - uu___198 in + uu___200 in FStar_Tactics_V2_InterpFuns.mk_tac_step_2 Prims.int_zero "resolve_name" FStar_Tactics_V2_Basic.resolve_name FStar_Reflection_V2_Embeddings.e_env - uu___194 - uu___195 + uu___196 + uu___197 FStar_Tactics_V2_Basic.resolve_name FStar_Reflection_V2_NBEEmbeddings.e_env - uu___196 - uu___197 in - let uu___194 + uu___198 + uu___199 in + let uu___196 = - let uu___195 + let uu___197 = - let uu___196 + let uu___198 = FStar_Syntax_Embeddings.e_list FStar_Syntax_Embeddings.e_issue in - let uu___197 + let uu___199 = FStar_TypeChecker_NBETerm.e_list FStar_TypeChecker_NBETerm.e_issue in @@ -2381,7 +2438,7 @@ let (uu___193 : unit) = is; FStar_Tactics_Monad.ret ()) - uu___196 + uu___198 FStar_Syntax_Embeddings.e_unit (fun is -> @@ -2389,9 +2446,12 @@ let (uu___193 : unit) = is; FStar_Tactics_Monad.ret ()) - uu___197 + uu___199 FStar_TypeChecker_NBETerm.e_unit in - [uu___195] in + [uu___197] in + uu___195 + :: + uu___196 in uu___192 :: uu___194 in diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml index 53eaa89d736..7f6bbbea0fc 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml @@ -1,4 +1,11 @@ open Prims +type tot_or_ghost = + | E_Total + | E_Ghost +let (uu___is_E_Total : tot_or_ghost -> Prims.bool) = + fun projectee -> match projectee with | E_Total -> true | uu___ -> false +let (uu___is_E_Ghost : tot_or_ghost -> Prims.bool) = + fun projectee -> match projectee with | E_Ghost -> true | uu___ -> false let (goal_ctr : Prims.int FStar_Compiler_Effect.ref) = FStar_Compiler_Util.mk_ref Prims.int_zero let (get_goal_ctr : unit -> Prims.int) = @@ -420,18 +427,11 @@ let (print_error : error -> Prims.string) = let (print_error_short : error -> Prims.string) = fun err -> FStar_Pervasives_Native.snd err type 'a result = context -> ('a success, error) FStar_Pervasives.either -type effect_label = - | E_TOTAL - | E_GHOST -let (uu___is_E_TOTAL : effect_label -> Prims.bool) = - fun projectee -> match projectee with | E_TOTAL -> true | uu___ -> false -let (uu___is_E_GHOST : effect_label -> Prims.bool) = - fun projectee -> match projectee with | E_GHOST -> true | uu___ -> false type hash_entry = { he_term: FStar_Syntax_Syntax.term ; he_gamma: FStar_Syntax_Syntax.binding Prims.list ; - he_res: (effect_label * FStar_Syntax_Syntax.typ) success } + he_res: (tot_or_ghost * FStar_Syntax_Syntax.typ) success } let (__proj__Mkhash_entry__item__he_term : hash_entry -> FStar_Syntax_Syntax.term) = fun projectee -> @@ -441,7 +441,7 @@ let (__proj__Mkhash_entry__item__he_gamma : fun projectee -> match projectee with | { he_term; he_gamma; he_res;_} -> he_gamma let (__proj__Mkhash_entry__item__he_res : - hash_entry -> (effect_label * FStar_Syntax_Syntax.typ) success) = + hash_entry -> (tot_or_ghost * FStar_Syntax_Syntax.typ) success) = fun projectee -> match projectee with | { he_term; he_gamma; he_res;_} -> he_res type tc_table = hash_entry FStar_Syntax_TermHashTable.hashtable @@ -506,7 +506,7 @@ let (uu___is_Neither : side -> Prims.bool) = let (insert : env -> FStar_Syntax_Syntax.term -> - (effect_label * FStar_Syntax_Syntax.typ) success -> unit) + (tot_or_ghost * FStar_Syntax_Syntax.typ) success -> unit) = fun g -> fun e -> @@ -634,7 +634,7 @@ let (is_type : let rec (is_arrow : env -> FStar_Syntax_Syntax.term -> - (FStar_Syntax_Syntax.binder * effect_label * FStar_Syntax_Syntax.typ) + (FStar_Syntax_Syntax.binder * tot_or_ghost * FStar_Syntax_Syntax.typ) result) = fun g -> @@ -656,7 +656,7 @@ let rec (is_arrow : | (g1, x1, c1) -> let eff = let uu___3 = FStar_Syntax_Util.is_total_comp c1 in - if uu___3 then E_TOTAL else E_GHOST in + if uu___3 then E_Total else E_Ghost in return (x1, eff, (FStar_Syntax_Util.comp_result c1))) else (let e_tag = @@ -672,14 +672,14 @@ let rec (is_arrow : ct.FStar_Syntax_Syntax.effect_name FStar_Parser_Const.effect_Lemma_lid) in if uu___4 - then FStar_Pervasives_Native.Some E_TOTAL + then FStar_Pervasives_Native.Some E_Total else (let uu___6 = FStar_Ident.lid_equals ct.FStar_Syntax_Syntax.effect_name FStar_Parser_Const.effect_Ghost_lid in if uu___6 - then FStar_Pervasives_Native.Some E_GHOST + then FStar_Pervasives_Native.Some E_Ghost else FStar_Pervasives_Native.None) in match e_tag with | FStar_Pervasives_Native.None -> @@ -747,7 +747,7 @@ let rec (is_arrow : FStar_Syntax_Syntax.comp = c }) t1.FStar_Syntax_Syntax.pos in let uu___1 = open_term g x t2 in - (match uu___1 with | (g1, x1, t3) -> return (x1, E_TOTAL, t3)) + (match uu___1 with | (g1, x1, t3) -> return (x1, E_Total, t3)) | FStar_Syntax_Syntax.Tm_refine { FStar_Syntax_Syntax.b = x; FStar_Syntax_Syntax.phi = uu___1;_} -> is_arrow g x.FStar_Syntax_Syntax.sort @@ -1186,7 +1186,7 @@ let (curry_application : let (lookup : env -> FStar_Syntax_Syntax.term -> - (effect_label * FStar_Syntax_Syntax.typ) result) + (tot_or_ghost * FStar_Syntax_Syntax.typ) result) = fun g -> fun e -> @@ -1297,46 +1297,49 @@ let rec iter2 : let uu___ = f x y b1 in op_let_Bang uu___ (fun b2 -> iter2 xs1 ys1 f b2) | uu___ -> fail "Lists of differing length" -let (non_informative : env -> FStar_Syntax_Syntax.term -> Prims.bool) = - fun g -> fun t -> FStar_TypeChecker_Normalize.non_info_norm g.tcenv t +let (is_non_informative : + FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.typ -> Prims.bool) = + fun g -> fun t -> FStar_TypeChecker_Normalize.non_info_norm g t +let (non_informative : env -> FStar_Syntax_Syntax.typ -> Prims.bool) = + fun g -> fun t -> is_non_informative g.tcenv t let (as_comp : - env -> (effect_label * FStar_Syntax_Syntax.typ) -> FStar_Syntax_Syntax.comp) + env -> (tot_or_ghost * FStar_Syntax_Syntax.typ) -> FStar_Syntax_Syntax.comp) = fun g -> fun et -> match et with - | (E_TOTAL, t) -> FStar_Syntax_Syntax.mk_Total t - | (E_GHOST, t) -> + | (E_Total, t) -> FStar_Syntax_Syntax.mk_Total t + | (E_Ghost, t) -> let uu___ = non_informative g t in if uu___ then FStar_Syntax_Syntax.mk_Total t else FStar_Syntax_Syntax.mk_GTotal t -let (comp_as_effect_label_and_type : +let (comp_as_tot_or_ghost_and_type : FStar_Syntax_Syntax.comp -> - (effect_label * FStar_Syntax_Syntax.typ) FStar_Pervasives_Native.option) + (tot_or_ghost * FStar_Syntax_Syntax.typ) FStar_Pervasives_Native.option) = fun c -> let uu___ = FStar_Syntax_Util.is_total_comp c in if uu___ then FStar_Pervasives_Native.Some - (E_TOTAL, (FStar_Syntax_Util.comp_result c)) + (E_Total, (FStar_Syntax_Util.comp_result c)) else (let uu___2 = FStar_Syntax_Util.is_tot_or_gtot_comp c in if uu___2 then FStar_Pervasives_Native.Some - (E_GHOST, (FStar_Syntax_Util.comp_result c)) + (E_Ghost, (FStar_Syntax_Util.comp_result c)) else FStar_Pervasives_Native.None) -let (join_eff : effect_label -> effect_label -> effect_label) = +let (join_eff : tot_or_ghost -> tot_or_ghost -> tot_or_ghost) = fun e0 -> fun e1 -> match (e0, e1) with - | (E_GHOST, uu___) -> E_GHOST - | (uu___, E_GHOST) -> E_GHOST - | uu___ -> E_TOTAL -let (join_eff_l : effect_label Prims.list -> effect_label) = - fun es -> FStar_List_Tot_Base.fold_right join_eff es E_TOTAL + | (E_Ghost, uu___) -> E_Ghost + | (uu___, E_Ghost) -> E_Ghost + | uu___ -> E_Total +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 -> FStar_Pervasives.Inl ((ctx.no_guard), FStar_Pervasives_Native.None) @@ -2449,13 +2452,13 @@ and (check_relation_comp : if uu___ then FStar_Pervasives_Native.Some - (E_TOTAL, (FStar_Syntax_Util.comp_result c)) + (E_Total, (FStar_Syntax_Util.comp_result c)) else (let uu___2 = FStar_Syntax_Util.is_tot_or_gtot_comp c in if uu___2 then FStar_Pervasives_Native.Some - (E_GHOST, (FStar_Syntax_Util.comp_result c)) + (E_Ghost, (FStar_Syntax_Util.comp_result c)) else FStar_Pervasives_Native.None) in let uu___ = let uu___1 = destruct_comp c0 in @@ -2563,14 +2566,14 @@ and (check_relation_comp : "Subcomp failed: Unequal computation types %s and %s" uu___11 uu___12 in fail uu___10)))) - | (FStar_Pervasives_Native.Some (E_TOTAL, t0), + | (FStar_Pervasives_Native.Some (E_Total, t0), FStar_Pervasives_Native.Some (uu___1, t1)) -> check_relation g rel t0 t1 - | (FStar_Pervasives_Native.Some (E_GHOST, t0), - FStar_Pervasives_Native.Some (E_GHOST, t1)) -> + | (FStar_Pervasives_Native.Some (E_Ghost, t0), + FStar_Pervasives_Native.Some (E_Ghost, t1)) -> check_relation g rel t0 t1 - | (FStar_Pervasives_Native.Some (E_GHOST, t0), - FStar_Pervasives_Native.Some (E_TOTAL, t1)) -> + | (FStar_Pervasives_Native.Some (E_Ghost, t0), + FStar_Pervasives_Native.Some (E_Total, t1)) -> let uu___1 = non_informative g t1 in if uu___1 then check_relation g rel t0 t1 @@ -2602,7 +2605,7 @@ and (check_subtype : and (memo_check : env -> FStar_Syntax_Syntax.term -> - (effect_label * FStar_Syntax_Syntax.typ) result) + (tot_or_ghost * FStar_Syntax_Syntax.typ) result) = fun g -> fun e -> @@ -2653,7 +2656,7 @@ and (check : Prims.string -> env -> FStar_Syntax_Syntax.term -> - (effect_label * FStar_Syntax_Syntax.typ) result) + (tot_or_ghost * FStar_Syntax_Syntax.typ) result) = fun msg -> fun g -> @@ -2663,7 +2666,7 @@ and (check : and (do_check_and_promote : env -> FStar_Syntax_Syntax.term -> - (effect_label * FStar_Syntax_Syntax.typ) result) + (tot_or_ghost * FStar_Syntax_Syntax.typ) result) = fun g -> fun e -> @@ -2674,15 +2677,15 @@ and (do_check_and_promote : | (eff, t) -> let eff1 = match eff with - | E_TOTAL -> E_TOTAL - | E_GHOST -> + | E_Total -> E_Total + | E_Ghost -> let uu___2 = non_informative g t in - if uu___2 then E_TOTAL else E_GHOST in + if uu___2 then E_Total else E_Ghost in return (eff1, t)) and (do_check : env -> FStar_Syntax_Syntax.term -> - (effect_label * FStar_Syntax_Syntax.typ) result) + (tot_or_ghost * FStar_Syntax_Syntax.typ) result) = fun g -> fun e -> @@ -2696,7 +2699,7 @@ and (do_check : FStar_Syntax_Syntax.rng = uu___3;_} -> let uu___4 = FStar_Syntax_Util.unlazy e1 in do_check g uu___4 | FStar_Syntax_Syntax.Tm_lazy i -> - return (E_TOTAL, (i.FStar_Syntax_Syntax.ltyp)) + return (E_Total, (i.FStar_Syntax_Syntax.ltyp)) | FStar_Syntax_Syntax.Tm_meta { FStar_Syntax_Syntax.tm2 = t; FStar_Syntax_Syntax.meta = uu___;_} -> memo_check g t @@ -2705,7 +2708,7 @@ and (do_check : let uu___1 = let uu___2 = FStar_Syntax_Util.ctx_uvar_typ uv in FStar_Syntax_Subst.subst' s uu___2 in - (E_TOTAL, uu___1) in + (E_Total, uu___1) in return uu___ | FStar_Syntax_Syntax.Tm_name x -> let uu___ = FStar_TypeChecker_Env.try_lookup_bv g.tcenv x in @@ -2715,14 +2718,14 @@ and (do_check : let uu___2 = FStar_Syntax_Print.bv_to_string x in FStar_Compiler_Util.format1 "Variable not found: %s" uu___2 in fail uu___1 - | FStar_Pervasives_Native.Some (t, uu___1) -> return (E_TOTAL, t)) + | FStar_Pervasives_Native.Some (t, uu___1) -> return (E_Total, t)) | FStar_Syntax_Syntax.Tm_fvar f -> let uu___ = FStar_TypeChecker_Env.try_lookup_lid g.tcenv (f.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v in (match uu___ with | FStar_Pervasives_Native.Some (([], t), uu___1) -> - return (E_TOTAL, t) + return (E_Total, t) | uu___1 -> fail "Missing universes instantiation") | FStar_Syntax_Syntax.Tm_uinst ({ FStar_Syntax_Syntax.n = FStar_Syntax_Syntax.Tm_fvar f; @@ -2743,7 +2746,7 @@ and (do_check : FStar_Compiler_Util.format1 "Top-level name not found: %s" uu___5 in fail uu___4 - | FStar_Pervasives_Native.Some (t, uu___4) -> return (E_TOTAL, t)) + | FStar_Pervasives_Native.Some (t, uu___4) -> return (E_Total, t)) | FStar_Syntax_Syntax.Tm_constant c -> (match c with | FStar_Const.Const_range_of -> fail "Unhandled constant" @@ -2754,11 +2757,11 @@ and (do_check : let t = FStar_TypeChecker_TcTerm.tc_constant g.tcenv e1.FStar_Syntax_Syntax.pos c in - return (E_TOTAL, t)) + return (E_Total, t)) | FStar_Syntax_Syntax.Tm_type u -> let uu___ = let uu___1 = mk_type (FStar_Syntax_Syntax.U_succ u) in - (E_TOTAL, uu___1) in + (E_Total, uu___1) in return uu___ | FStar_Syntax_Syntax.Tm_refine { FStar_Syntax_Syntax.b = x; FStar_Syntax_Syntax.phi = phi;_} -> @@ -2783,7 +2786,7 @@ and (do_check : | (uu___8, t') -> let uu___9 = is_type g' t' in op_let_Bang uu___9 - (fun uu___10 -> return (E_TOTAL, t))) in + (fun uu___10 -> return (E_Total, t))) in with_binders [x1] [u] uu___5)) | FStar_Syntax_Syntax.Tm_abs { FStar_Syntax_Syntax.bs = xs; FStar_Syntax_Syntax.body = body; @@ -2805,7 +2808,7 @@ and (do_check : let uu___6 = let uu___7 = as_comp g t in FStar_Syntax_Util.arrow xs1 uu___7 in - (E_TOTAL, uu___6) in + (E_Total, uu___6) in return uu___5) in with_binders xs1 us uu___3)) | FStar_Syntax_Syntax.Tm_arrow @@ -2828,7 +2831,7 @@ and (do_check : let uu___4 = let uu___5 = mk_type (FStar_Syntax_Syntax.U_max (u :: us)) in - (E_TOTAL, uu___5) in + (E_Total, uu___5) in return uu___4) in with_binders xs1 us uu___2)) | FStar_Syntax_Syntax.Tm_app uu___ -> @@ -3044,7 +3047,7 @@ and (do_check : c_e c in op_let_Bang uu___8 (fun uu___9 -> - let uu___10 = comp_as_effect_label_and_type c in + let uu___10 = comp_as_tot_or_ghost_and_type c in match uu___10 with | FStar_Pervasives_Native.Some (eff1, t) -> return (eff1, t)))) @@ -3327,7 +3330,7 @@ and (do_check : (fun uu___7 -> return (FStar_Pervasives_Native.Some - (E_TOTAL, t))) + (E_Total, t))) | uu___4 -> return FStar_Pervasives_Native.None in op_let_Bang uu___3 (fun branch_typ_opt -> @@ -3589,7 +3592,7 @@ and (do_check : let uu___7 = check_branches FStar_Syntax_Util.exp_true_bool - branches E_TOTAL in + branches E_Total in op_let_Bang uu___7 (fun eff -> let ty = @@ -4286,7 +4289,7 @@ let (check_term_top : FStar_Syntax_Syntax.typ FStar_Pervasives_Native.option -> Prims.bool -> guard_handler_t FStar_Pervasives_Native.option -> - (effect_label * FStar_Syntax_Syntax.typ) + (tot_or_ghost * FStar_Syntax_Syntax.typ) FStar_Pervasives_Native.option result) = fun g -> @@ -4306,20 +4309,20 @@ let (check_term_top : (match uu___1 with | (eff, t) -> let uu___2 = - (eff = E_GHOST) && + (eff = E_Ghost) && (let uu___3 = non_informative g1 t in Prims.op_Negation uu___3) in if uu___2 then fail "expected total effect, found ghost" else return - (FStar_Pervasives_Native.Some (E_TOTAL, t))) + (FStar_Pervasives_Native.Some (E_Total, t))) else return (FStar_Pervasives_Native.Some eff_te) | FStar_Pervasives_Native.Some t -> let target_comp = if must_tot || - ((FStar_Pervasives_Native.fst eff_te) = E_TOTAL) + ((FStar_Pervasives_Native.fst eff_te) = E_Total) then FStar_Syntax_Syntax.mk_Total t else FStar_Syntax_Syntax.mk_GTotal t in let uu___1 = @@ -4354,7 +4357,7 @@ let (check_term_top_gh : FStar_Syntax_Syntax.typ FStar_Pervasives_Native.option -> Prims.bool -> guard_handler_t FStar_Pervasives_Native.option -> - (((effect_label * FStar_Syntax_Syntax.typ) + (((tot_or_ghost * FStar_Syntax_Syntax.typ) FStar_Pervasives_Native.option * precondition), error) FStar_Pervasives.either) = @@ -4533,30 +4536,29 @@ let (check_term : let (compute_term_type_handle_guards : FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.term -> - Prims.bool -> - (FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.typ -> Prims.bool) - -> (FStar_Syntax_Syntax.typ, error) FStar_Pervasives.either) + (FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.typ -> Prims.bool) -> + ((tot_or_ghost * FStar_Syntax_Syntax.typ), error) + FStar_Pervasives.either) = fun g -> fun e -> - fun must_tot -> - fun gh -> - let e1 = FStar_Syntax_Compress.deep_compress true e in - let uu___ = - check_term_top_gh g e1 FStar_Pervasives_Native.None must_tot - (FStar_Pervasives_Native.Some gh) in - match uu___ with - | FStar_Pervasives.Inl - (FStar_Pervasives_Native.Some (uu___1, t), - FStar_Pervasives_Native.None) - -> FStar_Pervasives.Inl t - | FStar_Pervasives.Inl (FStar_Pervasives_Native.None, uu___1) -> - failwith "Impossible: Success must return some effect and type" - | FStar_Pervasives.Inl - (uu___1, FStar_Pervasives_Native.Some uu___2) -> - failwith - "Impossible: All guards should have been handled already" - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err + fun gh -> + let e1 = FStar_Syntax_Compress.deep_compress true e in + let must_tot = false in + let uu___ = + check_term_top_gh g e1 FStar_Pervasives_Native.None must_tot + (FStar_Pervasives_Native.Some gh) in + match uu___ with + | FStar_Pervasives.Inl + (FStar_Pervasives_Native.Some r, FStar_Pervasives_Native.None) -> + FStar_Pervasives.Inl r + | FStar_Pervasives.Inl (FStar_Pervasives_Native.None, uu___1) -> + failwith "Impossible: Success must return some effect and type" + | FStar_Pervasives.Inl (uu___1, FStar_Pervasives_Native.Some uu___2) + -> + failwith + "Impossible: All guards should have been handled already" + | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err let (open_binders_in_term : FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.binders -> diff --git a/src/tactics/FStar.Tactics.Embedding.fst b/src/tactics/FStar.Tactics.Embedding.fst index 2a37858d4f6..1a04cf956c0 100644 --- a/src/tactics/FStar.Tactics.Embedding.fst +++ b/src/tactics/FStar.Tactics.Embedding.fst @@ -23,6 +23,7 @@ open FStar.Compiler.Effect open FStar.Syntax.Syntax open FStar.Syntax.Embeddings open FStar.Compiler.Util +open FStar.Compiler.List open FStar.Tactics.Common open FStar.Tactics.Types @@ -66,6 +67,20 @@ let fstar_tactics_const ns = fv = S.fvconst lid; t = S.tconst lid } +let fstar_tc_core_lid s : lid = + FStar.Ident.lid_of_path (["FStar"; "Stubs"; "TypeChecker"; "Core"]@[s]) Range.dummyRange + +let fstar_tc_core_data s = + let lid = fstar_tc_core_lid s in + { lid = lid; + fv = lid_as_data_fv lid; + t = lid_as_data_tm lid } + +let fstar_tc_core_const s = + let lid = fstar_tc_core_lid s in + { lid = lid; + fv = S.fvconst lid; + t = S.tconst lid } let fstar_tactics_proofstate = fstar_tactics_const ["Types"; "proofstate"] @@ -86,15 +101,15 @@ let fstar_tactics_Continue = fstar_tactics_data ["Types"; "Continue"] let fstar_tactics_Skip = fstar_tactics_data ["Types"; "Skip"] let fstar_tactics_Abort = fstar_tactics_data ["Types"; "Abort"] -let fstar_tactics_unfold_side = fstar_tactics_const ["Types"; "unfold_side"] -let fstar_tactics_unfold_side_Left = fstar_tactics_data ["Types"; "Left"] -let fstar_tactics_unfold_side_Right = fstar_tactics_data ["Types"; "Right"] -let fstar_tactics_unfold_side_Both = fstar_tactics_data ["Types"; "Both"] -let fstar_tactics_unfold_side_Neither = fstar_tactics_data ["Types"; "Neither"] +let fstar_tc_core_unfold_side = fstar_tc_core_const "unfold_side" +let fstar_tc_core_unfold_side_Left = fstar_tc_core_data "Left" +let fstar_tc_core_unfold_side_Right = fstar_tc_core_data "Right" +let fstar_tc_core_unfold_side_Both = fstar_tc_core_data "Both" +let fstar_tc_core_unfold_side_Neither = fstar_tc_core_data "Neither" -let fstar_tactics_tot_or_ghost = fstar_tactics_const ["Types"; "tot_or_ghost"] -let fstar_tactics_tot_or_ghost_ETotal = fstar_tactics_data ["Types"; "E_Total"] -let fstar_tactics_tot_or_ghost_EGhost = fstar_tactics_data ["Types"; "E_Ghost"] +let fstar_tc_core_tot_or_ghost = fstar_tc_core_const "tot_or_ghost" +let fstar_tc_core_tot_or_ghost_ETotal = fstar_tc_core_data "E_Total" +let fstar_tc_core_tot_or_ghost_EGhost = fstar_tc_core_data "E_Ghost" let fstar_tactics_guard_policy = fstar_tactics_const ["Types"; "guard_policy"] let fstar_tactics_SMT = fstar_tactics_data ["Types"; "SMT"] @@ -396,37 +411,41 @@ let e_unfold_side = let open FStar.TypeChecker.Core in let embed_unfold_side (rng:Range.range) (s:side) : term = match s with - | Left -> fstar_tactics_unfold_side_Left.t - | Right -> fstar_tactics_unfold_side_Right.t - | Both -> fstar_tactics_unfold_side_Both.t - | Neither -> fstar_tactics_unfold_side_Neither.t + | Left -> fstar_tc_core_unfold_side_Left.t + | Right -> fstar_tc_core_unfold_side_Right.t + | Both -> fstar_tc_core_unfold_side_Both.t + | Neither -> fstar_tc_core_unfold_side_Neither.t in let unembed_unfold_side (t : term) : option side = match (SS.compress t).n with - | Tm_fvar fv when S.fv_eq_lid fv fstar_tactics_unfold_side_Left.lid -> Some Left - | Tm_fvar fv when S.fv_eq_lid fv fstar_tactics_unfold_side_Right.lid -> Some Right - | Tm_fvar fv when S.fv_eq_lid fv fstar_tactics_unfold_side_Both.lid -> Some Both - | Tm_fvar fv when S.fv_eq_lid fv fstar_tactics_unfold_side_Neither.lid -> Some Neither + | Tm_fvar fv when S.fv_eq_lid fv fstar_tc_core_unfold_side_Left.lid -> Some Left + | Tm_fvar fv when S.fv_eq_lid fv fstar_tc_core_unfold_side_Right.lid -> Some Right + | Tm_fvar fv when S.fv_eq_lid fv fstar_tc_core_unfold_side_Both.lid -> Some Both + | Tm_fvar fv when S.fv_eq_lid fv fstar_tc_core_unfold_side_Neither.lid -> Some Neither | _ -> None in - mk_emb embed_unfold_side unembed_unfold_side fstar_tactics_unfold_side.t + mk_emb embed_unfold_side unembed_unfold_side fstar_tc_core_unfold_side.t let e_unfold_side_nbe = let open FStar.TypeChecker.Core in let embed_unfold_side cb (res:side) : NBET.t = match res with - | Left -> mkConstruct fstar_tactics_unfold_side_Left.fv [] [] - | Right -> mkConstruct fstar_tactics_unfold_side_Right.fv [] [] - | Both -> mkConstruct fstar_tactics_unfold_side_Both.fv [] [] - | Neither -> mkConstruct fstar_tactics_unfold_side_Neither.fv [] [] + | Left -> mkConstruct fstar_tc_core_unfold_side_Left.fv [] [] + | Right -> mkConstruct fstar_tc_core_unfold_side_Right.fv [] [] + | Both -> mkConstruct fstar_tc_core_unfold_side_Both.fv [] [] + | Neither -> mkConstruct fstar_tc_core_unfold_side_Neither.fv [] [] in let unembed_unfold_side cb (t:NBET.t) : option side = match NBETerm.nbe_t_of_t t with - | NBETerm.Construct (fv, _, []) when S.fv_eq_lid fv fstar_tactics_unfold_side_Left.lid -> Some Left - | NBETerm.Construct (fv, _, []) when S.fv_eq_lid fv fstar_tactics_unfold_side_Right.lid -> Some Right - | NBETerm.Construct (fv, _, []) when S.fv_eq_lid fv fstar_tactics_unfold_side_Both.lid -> Some Both - | NBETerm.Construct (fv, _, []) when S.fv_eq_lid fv fstar_tactics_unfold_side_Neither.lid -> Some Neither + | NBETerm.Construct (fv, _, []) when S.fv_eq_lid fv fstar_tc_core_unfold_side_Left.lid -> + Some Left + | NBETerm.Construct (fv, _, []) when S.fv_eq_lid fv fstar_tc_core_unfold_side_Right.lid -> + Some Right + | NBETerm.Construct (fv, _, []) when S.fv_eq_lid fv fstar_tc_core_unfold_side_Both.lid -> + Some Both + | NBETerm.Construct (fv, _, []) when S.fv_eq_lid fv fstar_tc_core_unfold_side_Neither.lid -> + Some Neither | _ -> if !Options.debug_embedding then Err.log_issue Range.dummyRange (Err.Warning_NotEmbedded, @@ -435,33 +454,39 @@ let e_unfold_side_nbe = in { NBETerm.em = embed_unfold_side ; NBETerm.un = unembed_unfold_side - ; NBETerm.typ = mkFV fstar_tactics_unfold_side.fv [] [] - ; NBETerm.emb_typ = fv_as_emb_typ fstar_tactics_unfold_side.fv } + ; NBETerm.typ = mkFV fstar_tc_core_unfold_side.fv [] [] + ; NBETerm.emb_typ = fv_as_emb_typ fstar_tc_core_unfold_side.fv } let e_tot_or_ghost = + let open FStar.TypeChecker.Core in let embed_tot_or_ghost (rng:Range.range) (s:tot_or_ghost) : term = match s with - | E_Total -> fstar_tactics_tot_or_ghost_ETotal.t - | E_Ghost -> fstar_tactics_tot_or_ghost_EGhost.t + | E_Total -> fstar_tc_core_tot_or_ghost_ETotal.t + | E_Ghost -> fstar_tc_core_tot_or_ghost_EGhost.t in let unembed_tot_or_ghost (t : term) : option tot_or_ghost = match (SS.compress t).n with - | Tm_fvar fv when S.fv_eq_lid fv fstar_tactics_tot_or_ghost_ETotal.lid -> Some E_Total - | Tm_fvar fv when S.fv_eq_lid fv fstar_tactics_tot_or_ghost_EGhost.lid -> Some E_Ghost + | Tm_fvar fv when S.fv_eq_lid fv fstar_tc_core_tot_or_ghost_ETotal.lid -> + Some E_Total + | Tm_fvar fv when S.fv_eq_lid fv fstar_tc_core_tot_or_ghost_EGhost.lid -> + Some E_Ghost | _ -> None in - mk_emb embed_tot_or_ghost unembed_tot_or_ghost fstar_tactics_tot_or_ghost.t + mk_emb embed_tot_or_ghost unembed_tot_or_ghost fstar_tc_core_tot_or_ghost.t let e_tot_or_ghost_nbe = + let open FStar.TypeChecker.Core in let embed_tot_or_ghost cb (res:tot_or_ghost) : NBET.t = match res with - | E_Total -> mkConstruct fstar_tactics_tot_or_ghost_ETotal.fv [] [] - | E_Ghost -> mkConstruct fstar_tactics_tot_or_ghost_EGhost.fv [] [] + | E_Total -> mkConstruct fstar_tc_core_tot_or_ghost_ETotal.fv [] [] + | E_Ghost -> mkConstruct fstar_tc_core_tot_or_ghost_EGhost.fv [] [] in let unembed_tot_or_ghost cb (t:NBET.t) : option tot_or_ghost = match NBETerm.nbe_t_of_t t with - | NBETerm.Construct (fv, _, []) when S.fv_eq_lid fv fstar_tactics_tot_or_ghost_ETotal.lid -> Some E_Total - | NBETerm.Construct (fv, _, []) when S.fv_eq_lid fv fstar_tactics_tot_or_ghost_EGhost.lid -> Some E_Ghost + | NBETerm.Construct (fv, _, []) when S.fv_eq_lid fv fstar_tc_core_tot_or_ghost_ETotal.lid -> + Some E_Total + | NBETerm.Construct (fv, _, []) when S.fv_eq_lid fv fstar_tc_core_tot_or_ghost_EGhost.lid -> + Some E_Ghost | _ -> if !Options.debug_embedding then Err.log_issue Range.dummyRange (Err.Warning_NotEmbedded, @@ -470,8 +495,8 @@ let e_tot_or_ghost_nbe = in { NBETerm.em = embed_tot_or_ghost ; NBETerm.un = unembed_tot_or_ghost - ; NBETerm.typ = mkFV fstar_tactics_tot_or_ghost.fv [] [] - ; NBETerm.emb_typ = fv_as_emb_typ fstar_tactics_tot_or_ghost.fv } + ; NBETerm.typ = mkFV fstar_tc_core_tot_or_ghost.fv [] [] + ; NBETerm.emb_typ = fv_as_emb_typ fstar_tc_core_tot_or_ghost.fv } let e_guard_policy = let embed_guard_policy (rng:Range.range) (p : guard_policy) : term = diff --git a/src/tactics/FStar.Tactics.Embedding.fsti b/src/tactics/FStar.Tactics.Embedding.fsti index bf06449e401..5c343f7a482 100644 --- a/src/tactics/FStar.Tactics.Embedding.fsti +++ b/src/tactics/FStar.Tactics.Embedding.fsti @@ -34,7 +34,7 @@ val e_direction : embedding direction val e_ctrl_flag : embedding ctrl_flag val e_guard_policy : embedding guard_policy val e_unfold_side : embedding Core.side -val e_tot_or_ghost : embedding tot_or_ghost +val e_tot_or_ghost : embedding Core.tot_or_ghost val e_exn_nbe : NBETerm.embedding exn val e_proofstate_nbe : NBETerm.embedding proofstate @@ -44,7 +44,7 @@ val e_direction_nbe : NBETerm.embedding direction val e_ctrl_flag_nbe : NBETerm.embedding ctrl_flag val e_guard_policy_nbe : NBETerm.embedding guard_policy val e_unfold_side_nbe : NBETerm.embedding Core.side -val e_tot_or_ghost_nbe : NBETerm.embedding tot_or_ghost +val e_tot_or_ghost_nbe : NBETerm.embedding Core.tot_or_ghost val unfold_lazy_proofstate : lazyinfo -> term val unfold_lazy_goal : lazyinfo -> term diff --git a/src/tactics/FStar.Tactics.Monad.fst b/src/tactics/FStar.Tactics.Monad.fst index b454218968b..054b7e37412 100644 --- a/src/tactics/FStar.Tactics.Monad.fst +++ b/src/tactics/FStar.Tactics.Monad.fst @@ -84,9 +84,9 @@ let register_goal (g:goal) = (BU.string_of_int i) (Print.ctx_uvar_to_string uv); let goal_ty = U.ctx_uvar_typ uv in - match FStar.TypeChecker.Core.compute_term_type_handle_guards env goal_ty false (fun _ _ -> true) + match FStar.TypeChecker.Core.compute_term_type_handle_guards env goal_ty (fun _ _ -> true) with - | Inl _ -> () + | Inl _ -> () // ghost is ok | Inr err -> let msg = BU.format2 "Failed to check initial tactic goal %s because %s" diff --git a/src/tactics/FStar.Tactics.Types.fst b/src/tactics/FStar.Tactics.Types.fst index 8360b40a30e..166e14a8868 100644 --- a/src/tactics/FStar.Tactics.Types.fst +++ b/src/tactics/FStar.Tactics.Types.fst @@ -112,8 +112,9 @@ let get_phi (g:goal) : option term = let is_irrelevant (g:goal) : bool = Option.isSome (get_phi g) +let non_informative_token (g:env) (t:typ) = unit let subtyping_token (g:env) (t0 t1:typ) = unit let equiv_token (g:env) (t0 t1:typ) = unit -let typing_token (g:env) (e:term) (c:tot_or_ghost & typ) = unit +let typing_token (g:env) (e:term) (c:Core.tot_or_ghost & typ) = unit let match_complete_token (g:env) (sc:term) (t:typ) (pats:list pattern) = unit let issues = list FStar.Issue.issue diff --git a/src/tactics/FStar.Tactics.Types.fsti b/src/tactics/FStar.Tactics.Types.fsti index ccb7f969229..77e4318ebe1 100644 --- a/src/tactics/FStar.Tactics.Types.fsti +++ b/src/tactics/FStar.Tactics.Types.fsti @@ -120,21 +120,11 @@ val check_goal_solved : goal -> bool val get_phi : goal -> option term val is_irrelevant : goal -> bool -type unfold_side = - | Left - | Right - | Both - | Neither - -type tot_or_ghost = - | E_Total - | E_Ghost - - (*** These are here for userspace, the library has an interface into this module. *) (* Typing reflection *) +val non_informative_token (g:env) (t:typ) : Type0 val subtyping_token (g:env) (t0 t1:typ) : Type0 val equiv_token (g:env) (t0 t1:typ) : Type0 -val typing_token (g:env) (e:term) (c:tot_or_ghost & typ) : Type0 +val typing_token (g:env) (e:term) (c:Core.tot_or_ghost & typ) : Type0 val match_complete_token (g:env) (sc:term) (t:typ) (pats:list pattern) : Type0 let issues = list FStar.Issue.issue diff --git a/src/tactics/FStar.Tactics.V1.Basic.fst b/src/tactics/FStar.Tactics.V1.Basic.fst index 7d09ca74b06..4d66b854149 100644 --- a/src/tactics/FStar.Tactics.V1.Basic.fst +++ b/src/tactics/FStar.Tactics.V1.Basic.fst @@ -1404,10 +1404,10 @@ let _t_trefl (allow_guards:bool) (l : term) (r : term) : tac unit = // Note, from well-typedness of the goal, we already know ?u.ty <: ty let check_uvar_subtype u t = let env = { goal_env g with gamma = g.goal_ctx_uvar.ctx_uvar_gamma } in - match Core.compute_term_type_handle_guards env t false (fun _ _ -> true) + match Core.compute_term_type_handle_guards env t (fun _ _ -> true) with | Inr _ -> false - | Inl t_ty -> ( + | Inl (_, t_ty) -> ( // ignoring the effect, ghost is ok match Core.check_term_subtyping env ty t_ty with | Inl None -> //unconditional subtype mark_uvar_as_already_checked u; diff --git a/src/tactics/FStar.Tactics.V2.Basic.fst b/src/tactics/FStar.Tactics.V2.Basic.fst index a479715b971..ae9910533f6 100644 --- a/src/tactics/FStar.Tactics.V2.Basic.fst +++ b/src/tactics/FStar.Tactics.V2.Basic.fst @@ -1440,10 +1440,10 @@ let _t_trefl (allow_guards:bool) (l : term) (r : term) : tac unit = // Note, from well-typedness of the goal, we already know ?u.ty <: ty let check_uvar_subtype u t = let env = { goal_env g with gamma = g.goal_ctx_uvar.ctx_uvar_gamma } in - match Core.compute_term_type_handle_guards env t false (fun _ _ -> true) + match Core.compute_term_type_handle_guards env t (fun _ _ -> true) with | Inr _ -> false - | Inl t_ty -> ( + | Inl (_, t_ty) -> ( // ignoring effect, ghost is ok match Core.check_term_subtyping env ty t_ty with | Inl None -> //unconditional subtype mark_uvar_as_already_checked u; @@ -2203,6 +2203,23 @@ let unexpected_uvars_issue r = } in i +let refl_is_non_informative (g:env) (t:typ) : tac (option unit & issues) = + if no_uvars_in_g g && + no_uvars_in_term t + then refl_typing_builtin_wrapper (fun _ -> + dbg_refl g (fun _ -> + BU.format1 "refl_is_non_informative: %s\n" + (Print.term_to_string t)); + let b = Core.is_non_informative g t in + dbg_refl g (fun _ -> BU.format1 "refl_is_non_informative: returned %s" + (string_of_bool b)); + if b then ((), []) + else Errors.raise_error (Errors.Fatal_UnexpectedTerm, + "is_non_informative returned false ") Range.dummyRange) + else ( + ret (None, [unexpected_uvars_issue (Env.get_range g)]) + ) + let refl_check_relation (g:env) (t0 t1:typ) (rel:relation) : tac (option unit * issues) = @@ -2239,21 +2256,20 @@ let refl_check_subtyping (g:env) (t0 t1:typ) : tac (option unit & issues) = let refl_check_equiv (g:env) (t0 t1:typ) : tac (option unit & issues) = refl_check_relation g t0 t1 Equality -let to_must_tot (eff:tot_or_ghost) : bool = +let to_must_tot (eff:Core.tot_or_ghost) : bool = match eff with - | E_Total -> true - | E_Ghost -> false + | Core.E_Total -> true + | Core.E_Ghost -> false let refl_norm_type (g:env) (t:typ) : typ = N.normalize [Env.Beta; Env.Exclude Zeta] g t -let refl_core_compute_term_type (g:env) (e:term) (eff:tot_or_ghost) : tac (option typ & issues) = +let refl_core_compute_term_type (g:env) (e:term) : tac (option (Core.tot_or_ghost & typ) & issues) = if no_uvars_in_g g && no_uvars_in_term e then refl_typing_builtin_wrapper (fun _ -> dbg_refl g (fun _ -> BU.format1 "refl_core_compute_term_type: %s\n" (Print.term_to_string e)); - let must_tot = to_must_tot eff in let guards : ref (list (env & typ)) = BU.mk_ref [] in let gh = fun g guard -> (* FIXME: this is kinda ugly, we store all the guards @@ -2261,20 +2277,20 @@ let refl_core_compute_term_type (g:env) (e:term) (eff:tot_or_ghost) : tac (optio guards := (g, guard) :: !guards; true in - match Core.compute_term_type_handle_guards g e must_tot gh with - | Inl t -> + match Core.compute_term_type_handle_guards g e gh with + | Inl (eff, t) -> let t = refl_norm_type g t in dbg_refl g (fun _ -> BU.format2 "refl_core_compute_term_type for %s computed type %s\n" (Print.term_to_string e) (Print.term_to_string t)); - (t, !guards) + ((eff, t), !guards) | Inr err -> dbg_refl g (fun _ -> BU.format1 "refl_core_compute_term_type: %s\n" (Core.print_error err)); Errors.raise_error (Errors.Fatal_IllTyped, "core_compute_term_type failed: " ^ (Core.print_error err)) Range.dummyRange) else ret (None, [unexpected_uvars_issue (Env.get_range g)]) -let refl_core_check_term (g:env) (e:term) (t:typ) (eff:tot_or_ghost) +let refl_core_check_term (g:env) (e:term) (t:typ) (eff:Core.tot_or_ghost) : tac (option unit & issues) = if no_uvars_in_g g && @@ -2297,14 +2313,13 @@ let refl_core_check_term (g:env) (e:term) (t:typ) (eff:tot_or_ghost) Errors.raise_error (Errors.Fatal_IllTyped, "refl_core_check_term failed: " ^ (Core.print_error err)) Range.dummyRange) else ret (None, [unexpected_uvars_issue (Env.get_range g)]) -let refl_tc_term (g:env) (e:term) (eff:tot_or_ghost) : tac (option (term & typ) & issues) = +let refl_tc_term (g:env) (e:term) : tac (option (term & (Core.tot_or_ghost & typ)) & issues) = if no_uvars_in_g g && no_uvars_in_term e then refl_typing_builtin_wrapper (fun _ -> dbg_refl g (fun _ -> BU.format1 "refl_tc_term: %s\n" (Print.term_to_string e)); dbg_refl g (fun _ -> "refl_tc_term: starting tc {\n"); - let must_tot = to_must_tot eff in // // we don't instantiate implicits at the end of e // it is unlikely that we will be able to resolve them, @@ -2319,6 +2334,11 @@ let refl_tc_term (g:env) (e:term) (eff:tot_or_ghost) : tac (option (term & typ) // let e = let g = {g with phase1 = true; lax = true} in + // + // AR: we are lax checking to infer implicits, + // ghost is ok + // + let must_tot = false in let e, _, guard = g.typeof_tot_or_gtot_term g e must_tot in Rel.force_trivial_guard g guard; e in @@ -2335,17 +2355,17 @@ let refl_tc_term (g:env) (e:term) (eff:tot_or_ghost) : tac (option (term & typ) guards := (g, guard) :: !guards; true in - match Core.compute_term_type_handle_guards g e must_tot gh with - | Inl t -> + match Core.compute_term_type_handle_guards g e gh with + | Inl (eff, t) -> let t = refl_norm_type g t in dbg_refl g (fun _ -> BU.format2 "refl_tc_term for %s computed type %s\n" (Print.term_to_string e) (Print.term_to_string t)); - ((e, t), !guards) + ((e, (eff, t)), !guards) | Inr err -> - dbg_refl g (fun _ -> BU.format1 "refl_tc_term failed: %s\n" (Core.print_error err)); - Errors.raise_error (Errors.Fatal_IllTyped, "tc_term callback failed: " ^ Core.print_error err) e.pos + dbg_refl g (fun _ -> BU.format1 "refl_tc_term failed: %s\n" (Core.print_error err)); + Errors.raise_error (Errors.Fatal_IllTyped, "tc_term callback failed: " ^ Core.print_error err) e.pos end with | Errors.Error (Errors.Error_UnexpectedUnresolvedUvar, _, _, _) -> @@ -2436,7 +2456,8 @@ let refl_instantiate_implicits (g:env) (e:term) : tac (option (term & typ) & iss dbg_refl g (fun _ -> BU.format1 "refl_instantiate_implicits: %s\n" (Print.term_to_string e)); dbg_refl g (fun _ -> "refl_instantiate_implicits: starting tc {\n"); - let must_tot = true in + // AR: ghost is ok for instantiating implicits + let must_tot = false in let g = {g with instantiate_imp=false; phase1=true; lax=true} in let e, t, guard = g.typeof_tot_or_gtot_term g e must_tot in (* We force this guard here, and do not delay it, since we diff --git a/src/tactics/FStar.Tactics.V2.Basic.fsti b/src/tactics/FStar.Tactics.V2.Basic.fsti index 7053eb4534d..fab4c0a616e 100644 --- a/src/tactics/FStar.Tactics.V2.Basic.fsti +++ b/src/tactics/FStar.Tactics.V2.Basic.fsti @@ -125,11 +125,12 @@ val free_uvars : term -> tac (list Z.t) (***** Callbacks for the meta DSL framework *****) 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 refl_core_compute_term_type : env -> term -> tot_or_ghost -> tac (option typ & issues) -val refl_core_check_term : env -> term -> typ -> tot_or_ghost -> tac (option unit & issues) -val refl_tc_term : env -> term -> tot_or_ghost -> tac (option (term & typ) & 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_tc_term : env -> term -> tac (option (term & (Core.tot_or_ghost & typ)) & issues) val refl_universe_of : env -> term -> tac (option universe & issues) val refl_check_prop_validity : env -> term -> tac (option unit & issues) val refl_check_match_complete : env -> term -> term -> list pattern -> tac (option (list pattern & list (list RD.binding))) diff --git a/src/tactics/FStar.Tactics.V2.Interpreter.fst b/src/tactics/FStar.Tactics.V2.Interpreter.fst index 27248b61232..cc04f4dd8cf 100644 --- a/src/tactics/FStar.Tactics.V2.Interpreter.fst +++ b/src/tactics/FStar.Tactics.V2.Interpreter.fst @@ -603,6 +603,10 @@ let () = // reflection typechecker callbacks (part of the DSL framework) + mk_tac_step_2 0 "is_non_informative" + refl_is_non_informative RE.e_env RE.e_term (e_tuple2 (e_option e_unit) (e_list e_issue)) + refl_is_non_informative NRE.e_env NRE.e_term NBET.(e_tuple2 (e_option e_unit) (e_list e_issue)); + mk_tac_step_3 0 "check_subtyping" refl_check_subtyping RE.e_env RE.e_term RE.e_term (e_tuple2 (e_option e_unit) (e_list e_issue)) refl_check_subtyping NRE.e_env NRE.e_term NRE.e_term NBET.(e_tuple2 (e_option e_unit) (e_list e_issue)); @@ -611,17 +615,17 @@ let () = refl_check_equiv RE.e_env RE.e_term RE.e_term (e_tuple2 (e_option e_unit) (e_list e_issue)) refl_check_equiv NRE.e_env NRE.e_term NRE.e_term NBET.(e_tuple2 (e_option e_unit) (e_list e_issue)); - mk_tac_step_3 0 "core_compute_term_type" - refl_core_compute_term_type RE.e_env RE.e_term E.e_tot_or_ghost (e_tuple2 (e_option RE.e_term) (e_list e_issue)) - refl_core_compute_term_type NRE.e_env NRE.e_term E.e_tot_or_ghost_nbe NBET.(e_tuple2 (e_option NRE.e_term) (e_list e_issue)); + mk_tac_step_2 0 "core_compute_term_type" + refl_core_compute_term_type RE.e_env RE.e_term (e_tuple2 (e_option (e_tuple2 E.e_tot_or_ghost RE.e_term)) (e_list e_issue)) + refl_core_compute_term_type NRE.e_env NRE.e_term NBET.(e_tuple2 (e_option (e_tuple2 E.e_tot_or_ghost_nbe NRE.e_term)) (e_list e_issue)); mk_tac_step_4 0 "core_check_term" refl_core_check_term RE.e_env RE.e_term RE.e_term E.e_tot_or_ghost (e_tuple2 (e_option e_unit) (e_list e_issue)) refl_core_check_term NRE.e_env NRE.e_term NRE.e_term E.e_tot_or_ghost_nbe NBET.(e_tuple2 (e_option e_unit) (e_list e_issue)); - mk_tac_step_3 0 "tc_term" - refl_tc_term RE.e_env RE.e_term E.e_tot_or_ghost (e_tuple2 (e_option (e_tuple2 RE.e_term RE.e_term)) (e_list e_issue)) - refl_tc_term NRE.e_env NRE.e_term E.e_tot_or_ghost_nbe NBET.(e_tuple2 (e_option (e_tuple2 NRE.e_term NRE.e_term)) (e_list e_issue)); + mk_tac_step_2 0 "tc_term" + refl_tc_term RE.e_env RE.e_term (e_tuple2 (e_option (e_tuple2 RE.e_term (e_tuple2 E.e_tot_or_ghost RE.e_term))) (e_list e_issue)) + refl_tc_term NRE.e_env NRE.e_term NBET.(e_tuple2 (e_option (e_tuple2 NRE.e_term (e_tuple2 E.e_tot_or_ghost_nbe NRE.e_term))) (e_list e_issue)); mk_tac_step_2 0 "universe_of" refl_universe_of RE.e_env RE.e_term (e_tuple2 (e_option RE.e_universe) (e_list e_issue)) diff --git a/src/typechecker/FStar.TypeChecker.Core.fst b/src/typechecker/FStar.TypeChecker.Core.fst index 25d856860ed..e4c079d32ca 100644 --- a/src/typechecker/FStar.TypeChecker.Core.fst +++ b/src/typechecker/FStar.TypeChecker.Core.fst @@ -193,14 +193,10 @@ let print_error_short (err:error) = snd err let result a = context -> either (success a) error -type effect_label = - | E_TOTAL - | E_GHOST - type hash_entry = { he_term:term; he_gamma:list binding; - he_res:success (effect_label & typ); + he_res:success (tot_or_ghost & typ); } module THT = FStar.Syntax.TermHashTable type tc_table = THT.hashtable hash_entry @@ -221,7 +217,7 @@ let reset_cache_stats () = cache_stats := { hits = 0; misses = 0 } let report_cache_stats () = !cache_stats let clear_memo_table () = THT.clear table -let insert (g:env) (e:term) (res:success (effect_label & typ)) = +let insert (g:env) (e:term) (res:success (tot_or_ghost & typ)) = let entry = { he_term = e; he_gamma = g.tcenv.gamma; @@ -305,7 +301,7 @@ let is_type (g:env) (t:term) (fun _ -> aux (U.unrefine (N.unfold_whnf g.tcenv t)))) let rec is_arrow (g:env) (t:term) - : result (binder & effect_label & typ) + : result (binder & tot_or_ghost & typ) = let rec aux t = match (Subst.compress t).n with | Tm_arrow {bs=[x]; comp=c} -> @@ -314,8 +310,8 @@ let rec is_arrow (g:env) (t:term) let g, x, c = open_comp g x c in let eff = if U.is_total_comp c - then E_TOTAL - else E_GHOST + then E_Total + else E_Ghost in return (x, eff, U.comp_result c) else ( @@ -323,9 +319,9 @@ let rec is_arrow (g:env) (t:term) let Comp ct = c.n in if Ident.lid_equals ct.effect_name PC.effect_Pure_lid || Ident.lid_equals ct.effect_name PC.effect_Lemma_lid - then Some E_TOTAL + then Some E_Total else if Ident.lid_equals ct.effect_name PC.effect_Ghost_lid - then Some E_GHOST + then Some E_Ghost else None in (* Turn x:t -> Pure/Ghost t' pre post @@ -355,7 +351,7 @@ let rec is_arrow (g:env) (t:term) | Tm_arrow {bs=x::xs; comp=c} -> let t = S.mk (Tm_arrow {bs=xs; comp=c}) t.pos in let g, x, t = open_term g x t in - return (x, E_TOTAL, t) + return (x, E_Total, t) | Tm_refine {b=x} -> is_arrow g x.sort @@ -564,7 +560,7 @@ let curry_application hd arg args p = t -let lookup (g:env) (e:term) : result (effect_label & typ) = +let lookup (g:env) (e:term) : result (tot_or_ghost & typ) = match THT.lookup e table with | None -> record_cache_miss (); @@ -641,34 +637,36 @@ let rec iter2 (xs ys:list 'a) (f: 'a -> 'a -> 'b -> result 'b) (b:'b) iter2 xs ys f b | _ -> fail "Lists of differing length" +let is_non_informative g t = N.non_info_norm g t + let non_informative g t : bool - = N.non_info_norm g.tcenv t + = is_non_informative g.tcenv t -let as_comp (g:env) (et: (effect_label & typ)) +let as_comp (g:env) (et: (tot_or_ghost & typ)) : comp = match et with - | E_TOTAL, t -> S.mk_Total t - | E_GHOST, t -> + | E_Total, t -> S.mk_Total t + | E_Ghost, t -> if non_informative g t then S.mk_Total t else S.mk_GTotal t -let comp_as_effect_label_and_type (c:comp) - : option (effect_label & typ) +let comp_as_tot_or_ghost_and_type (c:comp) + : option (tot_or_ghost & typ) = if U.is_total_comp c - then Some (E_TOTAL, U.comp_result c) + then Some (E_Total, U.comp_result c) else if U.is_tot_or_gtot_comp c - then Some (E_GHOST, U.comp_result c) + then Some (E_Ghost, U.comp_result c) else None let join_eff e0 e1 = match e0, e1 with - | E_GHOST, _ - | _, E_GHOST -> E_GHOST - | _ -> E_TOTAL + | E_Ghost, _ + | _, E_Ghost -> E_Ghost + | _ -> E_Total -let join_eff_l es = List.Tot.fold_right join_eff es E_TOTAL +let join_eff_l es = List.Tot.fold_right join_eff es E_Total let guard_not_allowed : result bool @@ -1122,9 +1120,9 @@ and check_relation_comp (g:env) rel (c0 c1:comp) : result unit = let destruct_comp c = if U.is_total_comp c - then Some (E_TOTAL, U.comp_result c) + then Some (E_Total, U.comp_result c) else if U.is_tot_or_gtot_comp c - then Some (E_GHOST, U.comp_result c) + then Some (E_Ghost, U.comp_result c) else None in match destruct_comp c0, destruct_comp c1 with @@ -1152,11 +1150,11 @@ and check_relation_comp (g:env) rel (c0 c1:comp) ) ) - | Some (E_TOTAL, t0), Some (_, t1) - | Some (E_GHOST, t0), Some (E_GHOST, t1) -> + | Some (E_Total, t0), Some (_, t1) + | Some (E_Ghost, t0), Some (E_Ghost, t1) -> check_relation g rel t0 t1 - | Some (E_GHOST, t0), Some (E_TOTAL, t1) -> + | Some (E_Ghost, t0), Some (E_Total, t1) -> if non_informative g t1 then check_relation g rel t0 t1 else fail "Expected a Total computation, but got Ghost" @@ -1175,7 +1173,7 @@ and check_subtype (g:env) (e:option term) (t0 t1:typ) "FStar.TypeChecker.Core.check_subtype" and memo_check (g:env) (e:term) - : result (effect_label & typ) + : result (tot_or_ghost & typ) = let check_then_memo g e ctx = let r = do_check_and_promote g e ctx in match r with @@ -1217,34 +1215,34 @@ and memo_check (g:env) (e:term) ) and check (msg:string) (g:env) (e:term) - : result (effect_label & typ) + : result (tot_or_ghost & typ) = with_context msg (Some (CtxTerm e)) (fun _ -> memo_check g e) and do_check_and_promote (g:env) (e:term) - : result (effect_label & typ) + : result (tot_or_ghost & typ) = let! (eff, t) = do_check g e in let eff = match eff with - | E_TOTAL -> E_TOTAL - | E_GHOST -> if non_informative g t then E_TOTAL else E_GHOST in + | E_Total -> E_Total + | E_Ghost -> if non_informative g t then E_Total else E_Ghost in return (eff, t) (* G |- e : Tot t | pre *) and do_check (g:env) (e:term) - : result (effect_label & typ) = + : result (tot_or_ghost & typ) = let e = Subst.compress e in match e.n with | Tm_lazy ({lkind=Lazy_embedding _}) -> do_check g (U.unlazy e) | Tm_lazy i -> - return (E_TOTAL, i.ltyp) + return (E_Total, i.ltyp) | Tm_meta {tm=t} -> memo_check g t | Tm_uvar (uv, s) -> - return (E_TOTAL, Subst.subst' s (U.ctx_uvar_typ uv)) + return (E_Total, Subst.subst' s (U.ctx_uvar_typ uv)) | Tm_name x -> begin @@ -1252,14 +1250,14 @@ and do_check (g:env) (e:term) | None -> fail (BU.format1 "Variable not found: %s" (P.bv_to_string x)) | Some (t, _) -> - return (E_TOTAL, t) + return (E_Total, t) end | Tm_fvar f -> begin match Env.try_lookup_lid g.tcenv f.fv_name.v with | Some (([], t), _) -> - return (E_TOTAL, t) + return (E_Total, t) | _ -> //no implicit universe instantiation allowed fail "Missing universes instantiation" @@ -1272,7 +1270,7 @@ and do_check (g:env) (e:term) fail (BU.format1 "Top-level name not found: %s" (Ident.string_of_lid f.fv_name.v)) | Some (t, _) -> - return (E_TOTAL, t) + return (E_Total, t) end | Tm_constant c -> @@ -1287,11 +1285,11 @@ and do_check (g:env) (e:term) | _ -> let t = FStar.TypeChecker.TcTerm.tc_constant g.tcenv e.pos c in - return (E_TOTAL, t) + return (E_Total, t) end | Tm_type u -> - return (E_TOTAL, mk_type (U_succ u)) + return (E_Total, mk_type (U_succ u)) | Tm_refine {b=x; phi} -> let! _, t = check "refinement head" g x.sort in @@ -1300,7 +1298,7 @@ and do_check (g:env) (e:term) with_binders [x] [u] ( let! _, t' = check "refinement formula" g' phi in is_type g' t';! - return (E_TOTAL, t) + return (E_Total, t) ) | Tm_abs {bs=xs; body} -> @@ -1308,7 +1306,7 @@ and do_check (g:env) (e:term) let! us = with_context "abs binders" None (fun _ -> check_binders g xs) in with_binders xs us ( let! t = check "abs body" g' body in - return (E_TOTAL, U.arrow xs (as_comp g t)) + return (E_Total, U.arrow xs (as_comp g t)) ) | Tm_arrow {bs=xs; comp=c} -> @@ -1316,7 +1314,7 @@ and do_check (g:env) (e:term) let! us = with_context "arrow binders" None (fun _ -> check_binders g xs) in with_binders xs us ( let! u = with_context "arrow comp" None (fun _ -> check_comp g' c) in - return (E_TOTAL, mk_type (S.U_max (u::us))) + return (E_Total, mk_type (S.U_max (u::us))) ) | Tm_app _ -> ( @@ -1367,7 +1365,7 @@ and do_check (g:env) (e:term) 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;! - let Some (eff, t) = comp_as_effect_label_and_type c in + let Some (eff, t) = comp_as_tot_or_ghost_and_type c in return (eff, t) ) else fail (BU.format1 "Effect ascriptions are not fully handled yet: %s" (P.comp_to_string c)) @@ -1397,7 +1395,7 @@ and do_check (g:env) (e:term) let rec check_branches path_condition branch_typ_opt branches - : result (effect_label & typ) + : result (tot_or_ghost & typ) = match branches with | [] -> (match branch_typ_opt with @@ -1454,7 +1452,7 @@ and do_check (g:env) (e:term) match rc_opt with | Some ({ residual_typ = Some t }) -> with_context "residual type" (Some (CtxTerm t)) (fun _ -> universe_of g t) ;! - return (Some (E_TOTAL, t)) + return (Some (E_Total, t)) | _ -> return None @@ -1479,8 +1477,8 @@ and do_check (g:env) (e:term) let! _u_ty = is_type g_as_x returns_ty_t in let rec check_branches (path_condition: S.term) (branches: list S.branch) - (acc_eff: effect_label) - : result effect_label + (acc_eff: tot_or_ghost) + : result tot_or_ghost = match branches with | [] -> (match boolean_negation_simp path_condition with @@ -1526,7 +1524,7 @@ and do_check (g:env) (e:term) | _ -> check_branches next_path_condition rest eff_br in - let! eff = check_branches U.exp_true_bool branches E_TOTAL in + let! eff = check_branches U.exp_true_bool branches E_Total in let ty = Subst.subst [NT(as_x.binder_bv, sc)] returns_ty in return (eff, ty) @@ -1791,7 +1789,7 @@ let initial_env g gh = should_read_cache = true } let check_term_top g e topt (must_tot:bool) (gh:option guard_handler_t) - : result (option (effect_label & typ)) + : result (option (tot_or_ghost & typ)) = let g = initial_env g gh in let! eff_te = check "top" g e in match topt with @@ -1799,14 +1797,14 @@ let check_term_top g e topt (must_tot:bool) (gh:option guard_handler_t) // check expected effect if must_tot then let eff, t = eff_te in - if eff = E_GHOST && + if eff = E_Ghost && not (non_informative g t) then fail "expected total effect, found ghost" - else return (Some (E_TOTAL, t)) + else return (Some (E_Total, t)) else return (Some eff_te) | Some t -> let target_comp = - if must_tot || fst eff_te = E_TOTAL + if must_tot || fst eff_te = E_Total then S.mk_Total t else S.mk_GTotal t in @@ -1909,10 +1907,11 @@ let check_term g e t must_tot = | Inl (_, g) -> Inl g | Inr err -> Inr err -let compute_term_type_handle_guards g e must_tot gh = +let compute_term_type_handle_guards g e gh = let e = FStar.Syntax.Compress.deep_compress true e in + let must_tot = false in match check_term_top_gh g e None must_tot (Some gh) with - | Inl (Some (_, t), None) -> Inl t + | Inl (Some r, None) -> Inl r | Inl (None, _) -> failwith "Impossible: Success must return some effect and type" | Inl (_, Some _) -> failwith "Impossible: All guards should have been handled already" | Inr err -> Inr err diff --git a/src/typechecker/FStar.TypeChecker.Core.fsti b/src/typechecker/FStar.TypeChecker.Core.fsti index 0fcb3e030c1..328ea81dc72 100644 --- a/src/typechecker/FStar.TypeChecker.Core.fsti +++ b/src/typechecker/FStar.TypeChecker.Core.fsti @@ -6,6 +6,10 @@ module S = FStar.Syntax.Syntax module R = FStar.Compiler.Range module U = FStar.Syntax.Util +type tot_or_ghost = + | E_Total + | E_Ghost + val clear_memo_table (_:unit) : unit @@ -21,12 +25,14 @@ val side_to_string : side -> string val maybe_relate_after_unfolding (g:Env.env) (t0 t1:term) : side +val is_non_informative (g:Env.env) (t:typ) : bool + val check_term (g:Env.env) (e:term) (t:typ) (must_tot:bool) : either (option typ) error -val compute_term_type_handle_guards (g:Env.env) (e:term) (must_tot:bool) +val compute_term_type_handle_guards (g:Env.env) (e:term) (discharge_guard: Env.env -> typ -> bool) - : either typ error + : either (tot_or_ghost & typ) error val open_binders_in_term (g:Env.env) (bs:binders) (t:term) : Env.env & binders & term diff --git a/ulib/FStar.Stubs.TypeChecker.Core.fsti b/ulib/FStar.Stubs.TypeChecker.Core.fsti new file mode 100644 index 00000000000..e9e96aa1a8e --- /dev/null +++ b/ulib/FStar.Stubs.TypeChecker.Core.fsti @@ -0,0 +1,30 @@ +(* + Copyright 2008-2023 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) +module FStar.Stubs.TypeChecker.Core + +// +// A stub for using some type definition from FStar.TypeChecker.Core +// + +type tot_or_ghost = + | E_Total + | E_Ghost + +type unfold_side = + | Left + | Right + | Both + | Neither diff --git a/ulib/FStar.Tactics.Types.fsti b/ulib/FStar.Tactics.Types.fsti index 410d6ab4b00..22a896bb445 100644 --- a/ulib/FStar.Tactics.Types.fsti +++ b/ulib/FStar.Tactics.Types.fsti @@ -17,6 +17,7 @@ module FStar.Tactics.Types open FStar.Reflection.Types include FStar.Tactics.Common +include FStar.Stubs.TypeChecker.Core assume new type proofstate assume new type goal @@ -59,20 +60,8 @@ type guard_policy = | Force // Force guards without SMT | Drop // Drop guards, clearly unsound! careful! -type unfold_side = - | Left - | Right - | Both - | Neither - -// -// Used in the reflection typing judgment -// -type tot_or_ghost = - | E_Total - | E_Ghost - (* Typing reflection *) +val non_informative_token (g:env) (t:typ) : Type0 val subtyping_token (g:env) (t0 t1:typ) : Type0 val equiv_token (g:env) (t0 t1:typ) : Type0 val typing_token (g:env) (e:term) (c:tot_or_ghost & typ) : Type0 diff --git a/ulib/FStar.Tactics.V2.Builtins.fsti b/ulib/FStar.Tactics.V2.Builtins.fsti index 3afc3ae9c3d..6bfcc042812 100644 --- a/ulib/FStar.Tactics.V2.Builtins.fsti +++ b/ulib/FStar.Tactics.V2.Builtins.fsti @@ -448,39 +448,45 @@ val free_uvars : term -> Tac (list int) (** TODO: maybe the equiv APIs should require typing of the arguments? *) +unfold +let ret_t (a:Type) = option a & issues + +val is_non_informative (g:env) (t:typ) + : Tac (ret_t (non_informative_token g t)) + val check_subtyping (g:env) (t0 t1:typ) - : Tac (option (subtyping_token g t0 t1) & issues) + : Tac (ret_t (subtyping_token g t0 t1)) val check_equiv (g:env) (t0 t1:typ) - : Tac (option (equiv_token g t0 t1) & issues) + : Tac (ret_t (equiv_token g t0 t1)) // // Compute the type of e using the core typechecker // -val core_compute_term_type (g:env) (e:term) (eff:tot_or_ghost) - : Tac (option (t:typ{typing_token g e (eff, t)}) & issues) +val core_compute_term_type (g:env) (e:term) + : Tac (ret_t (r:(tot_or_ghost & typ){typing_token g e r})) // // Check that e:t using the core typechecker // val core_check_term (g:env) (e:term) (t:typ) (eff:tot_or_ghost) - : Tac (option (typing_token g e (eff, t)) & issues) + : Tac (ret_t (typing_token g e (eff, t))) // // Instantiate the implicits in e and compute its type // -val tc_term (g:env) (e:term) (eff:tot_or_ghost) - : Tac (option (r:(term & typ){typing_token g (fst r) (eff, snd r)}) & issues) +val tc_term (g:env) (e:term) + : Tac (ret_t (r:(term & (tot_or_ghost & typ)){typing_token g (fst r) (snd r)})) val universe_of (g:env) (e:term) - : Tac (option (u:universe{typing_token g e (E_Total, pack_ln (Tv_Type u))}) & issues) + : Tac (ret_t (u:universe{typing_token g e (E_Total, pack_ln (Tv_Type u))})) type prop_validity_token (g:env) (t:term) = e:term{typing_token g t (E_Total, pack_ln (Tv_FVar (pack_fv prop_qn))) /\ typing_token g e (E_Total, t)} val check_prop_validity (g:env) (t:term) - : Tac (option (prop_validity_token g t) & issues) + : Tac (ret_t (prop_validity_token g t)) // Can't immediately move to FStar.Tactics.Types since pattern is not in scope there val match_complete_token (g:env) (sc:term) (t:typ) (pats:list pattern) (bnds:list (list binding)) @@ -503,13 +509,13 @@ val check_match_complete (g:env) (sc:term) (t:typ) (pats:list pattern) // The client may follow it up with another call to core_check_term get the proof // val instantiate_implicits (g:env) (t:term) - : Tac (option (term & typ) & issues) + : Tac (ret_t (term & typ)) val maybe_relate_after_unfolding (g:env) (t1 t2:term) - : Tac (option unfold_side & issues) + : Tac (ret_t unfold_side) val maybe_unfold_head (g:env) (t0:term) - : Tac (option (t1:term{equiv_token g t0 t1}) & issues) + : Tac (ret_t (t1:term{equiv_token g t0 t1})) val push_open_namespace (g:env) (ns:name) : Tac env diff --git a/ulib/experimental/FStar.Reflection.Typing.fst b/ulib/experimental/FStar.Reflection.Typing.fst index 5dbc9ec66c7..a87de669f5a 100644 --- a/ulib/experimental/FStar.Reflection.Typing.fst +++ b/ulib/experimental/FStar.Reflection.Typing.fst @@ -930,3 +930,36 @@ and open_with_gt_ln_pats (l:list (pattern & bool)) (i:nat) (t:term) (j:nat) open_with_gt_ln_pats tl (i + k) t (j + k) let if_complete_match (g:env) (t:term) = magic() + +let mkif + (g:fstar_env) + (scrutinee:term) + (then_:term) + (else_:term) + (ty:term) + (u_ty:universe) + (hyp:var { None? (lookup_bvar g hyp) /\ ~(hyp `Set.mem` (freevars then_ `Set.union` freevars else_)) }) + (eff:T.tot_or_ghost) + (ty_eff:T.tot_or_ghost) + (ts : typing g scrutinee (eff, bool_ty)) + (tt : typing (extend_env g hyp (eq2 (pack_universe Uv_Zero) bool_ty scrutinee true_bool)) then_ (eff, ty)) + (te : typing (extend_env g hyp (eq2 (pack_universe Uv_Zero) bool_ty scrutinee false_bool)) else_ (eff, ty)) + (tr : typing g ty (ty_eff, tm_type u_ty)) +: typing g (mk_if scrutinee then_ else_) (eff, ty) += let brt = (Pat_Constant C_True, then_) in + let bre = (Pat_Constant C_False, else_) in + bindings_ok_pat_constant g C_True; + bindings_ok_pat_constant g C_False; + let brty () : branches_typing g u_zero bool_ty scrutinee (eff,ty) [brt; bre] [[]; []] = + BT_S (Pat_Constant C_True, then_) [] + (BO (Pat_Constant C_True) [] hyp then_ () tt) + _ _ ( + BT_S (Pat_Constant C_False, else_) [] + (BO (Pat_Constant C_False) [] hyp else_ () te) + _ _ + BT_Nil) + in + T_Match g u_zero bool_ty scrutinee T.E_Total (T_FVar g bool_fv) eff ts [brt; bre] (eff, ty) + [[]; []] + (MC_Tok g scrutinee bool_ty _ _ (Squash.return_squash (if_complete_match g scrutinee))) + (brty ()) diff --git a/ulib/experimental/FStar.Reflection.Typing.fsti b/ulib/experimental/FStar.Reflection.Typing.fsti index 42801c55a48..41fbdcb490e 100644 --- a/ulib/experimental/FStar.Reflection.Typing.fsti +++ b/ulib/experimental/FStar.Reflection.Typing.fsti @@ -1055,38 +1055,50 @@ let refl_bindings_to_bindings (bs : list R.binding) : list binding = [@@ no_auto_projectors] noeq -type non_informative : term -> Type0 = +type non_informative : env -> term -> Type0 = | Non_informative_type: + g:env -> u:universe -> - non_informative (pack_ln (Tv_Type u)) + non_informative g (pack_ln (Tv_Type u)) | Non_informative_fv: + g:env -> x:fv{is_non_informative_fv x} -> - non_informative (pack_ln (Tv_FVar x)) + non_informative g (pack_ln (Tv_FVar x)) | Non_informative_uinst: - x:fv -> + g:env -> + x:fv{is_non_informative_fv x} -> us:list universe -> - non_informative (pack_ln (Tv_UInst x us)) + non_informative g (pack_ln (Tv_UInst x us)) | Non_informative_app: + g:env -> t:term -> arg:argv -> - non_informative t -> - non_informative (pack_ln (Tv_App t arg)) + non_informative g t -> + non_informative g (pack_ln (Tv_App t arg)) | Non_informative_total_arrow: + g:env -> t0:term -> q:aqualv -> t1:term -> - non_informative t1 -> - non_informative (mk_arrow_ct t0 q (T.E_Total, t1)) + non_informative g t1 -> + non_informative g (mk_arrow_ct t0 q (T.E_Total, t1)) | Non_informative_ghost_arrow: + g:env -> t0:term -> q:aqualv -> t1:term -> - non_informative (mk_arrow_ct t0 q (T.E_Ghost, t1)) + non_informative g (mk_arrow_ct t0 q (T.E_Ghost, t1)) + + | Non_informative_token: + g:env -> + t:typ -> + squash (T.non_informative_token g t) -> + non_informative g t val bindings_ok_for_pat : env -> list R.binding -> pattern -> Type0 @@ -1410,7 +1422,7 @@ and related_comp : env -> comp_typ -> relation -> comp_typ -> Type0 = | Relc_ghost_total: g:env -> t:term -> - non_informative t -> + non_informative g t -> related_comp g (T.E_Ghost, t) R_Sub (T.E_Total, t) and branches_typing (g:env) (sc_u:universe) (sc_ty:typ) (sc:term) (rty:comp_typ) @@ -1754,8 +1766,7 @@ val if_complete_match (g:env) (t:term) // Derived rule for if - -let mkif +val mkif (g:fstar_env) (scrutinee:term) (then_:term) @@ -1770,20 +1781,3 @@ let mkif (te : typing (extend_env g hyp (eq2 (pack_universe Uv_Zero) bool_ty scrutinee false_bool)) else_ (eff, ty)) (tr : typing g ty (ty_eff, tm_type u_ty)) : typing g (mk_if scrutinee then_ else_) (eff, ty) -= let brt = (Pat_Constant C_True, then_) in - let bre = (Pat_Constant C_False, else_) in - bindings_ok_pat_constant g C_True; - bindings_ok_pat_constant g C_False; - let brty () : branches_typing g u_zero bool_ty scrutinee (eff,ty) [brt; bre] [[]; []] = - BT_S (Pat_Constant C_True, then_) [] - (BO (Pat_Constant C_True) [] hyp then_ () tt) - _ _ ( - BT_S (Pat_Constant C_False, else_) [] - (BO (Pat_Constant C_False) [] hyp else_ () te) - _ _ - BT_Nil) - in - T_Match g u_zero bool_ty scrutinee T.E_Total (T_FVar g bool_fv) eff ts [brt; bre] (eff, ty) - [[]; []] - (MC_Tok g scrutinee bool_ty _ _ (Squash.return_squash (if_complete_match g scrutinee))) - (brty ())