diff --git a/src/tactics/FStarC.Tactics.V2.Basic.fst b/src/tactics/FStarC.Tactics.V2.Basic.fst index 9497ba78047..b273c507de8 100644 --- a/src/tactics/FStarC.Tactics.V2.Basic.fst +++ b/src/tactics/FStarC.Tactics.V2.Basic.fst @@ -2635,9 +2635,9 @@ let refl_check_prop_validity (g:env) (e:term) : tac (option unit & issues) = else return (None, [unexpected_uvars_issue (Env.get_range g)]) let refl_check_match_complete (g:env) (sc:term) (scty:typ) (pats : list RD.pattern) -: tac (option (list RD.pattern & list (list RD.binding))) +: tac (option (list RD.pattern & list (list RD.binding)) & issues) = - return () ;! + refl_typing_builtin_wrapper "refl_check_match_complete" fun _ -> (* We just craft a match with the sc and patterns, using `1` in every branch, and check it against type int. *) let one = U.exp_int "1" in @@ -2645,26 +2645,24 @@ let refl_check_match_complete (g:env) (sc:term) (scty:typ) (pats : list RD.patte let mm = mk (Tm_match {scrutinee=sc; ret_opt=None; brs=brs; rc_opt=None}) sc.pos in let env = g in let env = Env.set_expected_typ env S.t_int in - let! mm, _, g = __tc env mm in - - let errs, b = Errors.catch_errors_and_ignore_rest (fun () -> Env.is_trivial <| Rel.discharge_guard env g) in - match errs, b with - | [], Some true -> - let get_pats t = - match (U.unmeta t).n with - | Tm_match {brs} -> List.map (fun (p,_,_) -> p) brs - | _ -> failwith "refl_check_match_complete: not a match?" - in - let pats = get_pats mm in - let rec bnds_for_pat (p:pat) : list RD.binding = - match p.v with - | Pat_constant _ -> [] - | Pat_cons (fv, _, pats) -> List.concatMap (fun (p, _) -> bnds_for_pat p) pats - | Pat_var bv -> [bv_to_binding bv] - | Pat_dot_term _ -> [] - in - return (Some (List.map inspect_pat pats, List.map bnds_for_pat pats)) - | _ -> return None + let mm, _, guard = TcTerm.typeof_tot_or_gtot_term env mm true in + + Rel.force_trivial_guard env guard; + let get_pats t = + match (U.unmeta t).n with + | Tm_match {brs} -> List.map (fun (p,_,_) -> p) brs + | _ -> failwith "refl_check_match_complete: not a match?" + in + let mm = SC.deep_compress false true mm in // important! we must return fully-compressed patterns + let pats = get_pats mm in + let rec bnds_for_pat (p:pat) : list RD.binding = + match p.v with + | Pat_constant _ -> [] + | Pat_cons (fv, _, pats) -> List.concatMap (fun (p, _) -> bnds_for_pat p) pats + | Pat_var bv -> [bv_to_binding bv] + | Pat_dot_term _ -> [] + in + (List.map inspect_pat pats, List.map bnds_for_pat pats), [] let refl_instantiate_implicits (g:env) (e:term) (expected_typ : option term) : tac (option (list (bv & typ) & term & typ) & issues) = diff --git a/src/tactics/FStarC.Tactics.V2.Basic.fsti b/src/tactics/FStarC.Tactics.V2.Basic.fsti index 474d268d08a..bc1fc779870 100644 --- a/src/tactics/FStarC.Tactics.V2.Basic.fsti +++ b/src/tactics/FStarC.Tactics.V2.Basic.fsti @@ -140,7 +140,7 @@ val refl_core_check_term_at_type : env -> term -> typ -> tac (option Core.t 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))) +val refl_check_match_complete : env -> term -> term -> list pattern -> tac (option (list pattern & list (list RD.binding)) & issues) val refl_instantiate_implicits : env -> term -> expected_typ:option term -> tac (option (list (bv & typ) & term & typ) & issues) val refl_try_unify : env -> list (bv & typ) -> term -> term -> tac (option (list (bv & term)) & issues) val refl_maybe_relate_after_unfolding : env -> term -> term -> tac (option Core.side & issues) diff --git a/tests/tactics/CheckMatchComplete.fst b/tests/tactics/CheckMatchComplete.fst index fb39c1c5c31..16c09c76bce 100644 --- a/tests/tactics/CheckMatchComplete.fst +++ b/tests/tactics/CheckMatchComplete.fst @@ -9,21 +9,21 @@ let guard (b:bool) = let test_wild () : Tac unit = let pat = Reflection.V2.Pat_Var (Sealed.seal (`int)) (Sealed.seal "x") in let e = cur_env () in - let r = check_match_complete e (`1) (`int) [pat] in + let (r, _) = check_match_complete e (`1) (`int) [pat] in guard (Some? r) let _ = assert True by (test_wild ()) let test_const_ok () : Tac unit = let pat = Reflection.V2.Pat_Constant (C_Int 1) in let e = cur_env () in - let r = check_match_complete e (`1) (`int) [pat] in + let (r, _) = check_match_complete e (`1) (`int) [pat] in guard (Some? r) let _ = assert True by (test_const_ok ()) let test_const_bad () : Tac unit = let pat = Reflection.V2.Pat_Constant (C_Int 2) in let e = cur_env () in - let r = check_match_complete e (`1) (`int) [pat] in + let (r, _) = check_match_complete e (`1) (`int) [pat] in guard (None? r) let _ = assert True by (test_const_bad ()) @@ -31,7 +31,7 @@ let test_const_two () : Tac unit = let pat1 = Reflection.V2.Pat_Constant (C_Int 1) in let pat2 = Reflection.V2.Pat_Var (Sealed.seal (`int)) (Sealed.seal "x") in let e = cur_env () in - let r = check_match_complete e (`1) (`int) [pat1; pat2] in + let (r, _) = check_match_complete e (`1) (`int) [pat1; pat2] in guard (Some? r) let _ = assert True by (test_const_two ()) @@ -39,6 +39,6 @@ let test_const_two' () : Tac unit = let pat1 = Reflection.V2.Pat_Constant (C_Int 2) in let pat2 = Reflection.V2.Pat_Var (Sealed.seal (`int)) (Sealed.seal "x") in let e = cur_env () in - let r = check_match_complete e (`1) (`int) [pat1; pat2] in + let (r, _) = check_match_complete e (`1) (`int) [pat1; pat2] in guard (Some? r) let _ = assert True by (test_const_two' ()) diff --git a/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti b/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti index c883d904e5c..f91f3e5f60b 100644 --- a/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti +++ b/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti @@ -555,9 +555,10 @@ val check_prop_validity (g:env) (t:term) val match_complete_token (g:env) (sc:term) (t:typ) (pats:list pattern) (bnds:list (list binding)) : Type0 -// Returns elaborated patterns, the bindings for each one, and a token +// Returns elaborated patterns, the bindings for each one, and a token. Possibly some issues +// too. val check_match_complete (g:env) (sc:term) (t:typ) (pats:list pattern) - : Tac (option (pats_bnds:(list pattern & list (list binding)) + : Tac (ret_t (pats_bnds:(list pattern & list (list binding)) {match_complete_token g sc t (fst pats_bnds) (snd pats_bnds) /\ List.Tot.length (fst pats_bnds) == List.Tot.length (snd pats_bnds) /\ List.Tot.length (fst pats_bnds) == List.Tot.length pats}))