Skip to content

Commit 87cb117

Browse files
gebnergebner
authored
Merge pull request #484 from FStarLang/gebner_reftactic
Adapt to tactic monad change.
2 parents 8bf255f + bd9724c commit 87cb117

21 files changed

+53
-58
lines changed

‎src/checker/Pulse.Checker.Base.fst‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1179,8 +1179,8 @@ let infer_post #g #ctxt (r:checker_result_t g ctxt NoHint)
11791179
let bs0 = bindings g in
11801180
let dom_g = dom g in
11811181
let fvs_t = freevars t in
1182-
let fail_fv_typ #a (x:string)
1183-
: T.Tac a =
1182+
let fail_fv_typ (x:string)
1183+
: T.Tac unit =
11841184
fail_doc g (Some (T.range_of_term t))
11851185
[Pulse.PP.text "Could not infer a type for this block; the return type `";
11861186
Pulse.PP.text (T.term_to_string t);

‎src/checker/Pulse.Checker.Pure.fst‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -166,8 +166,8 @@ does not make sense, as that indicates a well-typed term with no particular
166166
expected type, which is fine. *)
167167
let ill_typed_term (t:term) (expected_typ got_typ : option term)
168168
: TacH (list document)
169-
(requires fun _ -> None? expected_typ ==> None? got_typ)
170-
(ensures fun _ _ -> True)
169+
(requires None? expected_typ ==> None? got_typ)
170+
(ensures fun _ -> True)
171171
=
172172
let open Pulse.PP in
173173
match expected_typ, got_typ with
@@ -192,7 +192,7 @@ let instantiate_term_implicits
192192
let rng = RU.range_of_term t0 in
193193
let f = RU.env_set_range f (Pulse.Typing.Env.get_range g (Some rng)) in
194194
let topt, issues = catch_all (fun _ -> rtb_instantiate_implicits g f t0 expected inst_extra) in
195-
let fail #a issues : Tac a =
195+
let fail issues : Tac _ =
196196
fail_doc_with_subissues g (Some rng) issues []
197197
in
198198
match topt with

‎src/checker/Pulse.Checker.WithLocal.fst‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ let with_local_pre_typing (#g:env) (#pre:term) (pre_typing:tot_typing g pre tm_s
4646
tm_slprop
4747
= admit()
4848

49-
#push-options "--z3rlimit_factor 8 --fuel 0 --ifuel 1 --split_queries no"
49+
#push-options "--z3rlimit_factor 10 --fuel 0 --ifuel 1 --split_queries no"
5050
let head_range (t:st_term {Tm_WithLocal? t.term}) : range =
5151
let Tm_WithLocal { initializer } = t.term in
5252
(RU.range_of_term initializer)

‎src/checker/Pulse.JoinComp.fst‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -285,7 +285,7 @@ let rec join_comps
285285
(c_else:comp_st)
286286
(e_else_typing:st_typing g_else e_else c_else)
287287
(post:post_hint_t)
288-
: TacS (c:comp_st &
288+
: T.TacH (c:comp_st &
289289
st_typing g_then e_then c &
290290
st_typing g_else e_else c)
291291
(requires

‎src/checker/Pulse.JoinComp.fsti‎

Lines changed: 1 addition & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -19,12 +19,6 @@ module Pulse.JoinComp
1919
open Pulse.Syntax
2020
open Pulse.Typing
2121
module T = FStar.Tactics.V2
22-
effect TacS (a:Type) (pre : Type0) (post : (_:a{pre}) -> Type0) =
23-
Tactics.TacH a (requires (fun _ -> pre))
24-
(ensures (fun _ r -> pre /\ (
25-
match r with
26-
| Tactics.Result.Success r _ -> post r
27-
| _ -> True))) // does not guarantee anything on failure
2822

2923
val join_post #g #hyp #b
3024
(p1:post_hint_for_env (g_with_eq g hyp b tm_true))
@@ -41,7 +35,7 @@ val join_comps
4135
(c_else:comp_st)
4236
(e_else_typing:st_typing g_else e_else c_else)
4337
(post:post_hint_t)
44-
: TacS (c:comp_st &
38+
: T.TacH (c:comp_st &
4539
st_typing g_then e_then c &
4640
st_typing g_else e_else c)
4741
(requires

‎src/checker/Pulse.Typing.Combinators.fst‎

Lines changed: 10 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -169,7 +169,6 @@ let rec slprop_equiv_typing (#g:_) (#t0 #t1:term) (v:slprop_equiv g t0 t1)
169169
let t0_typing = d1 t1_typing in
170170
construct_forall_typing #g #u #b #t0 x b_typing t0_typing)
171171

172-
#push-options "--z3rlimit_factor 8 --ifuel 1 --fuel 2"
173172
let bind_t (case_c1 case_c2:comp_st -> bool) =
174173
(g:env) ->
175174
(pre:term) ->
@@ -190,15 +189,14 @@ let bind_t (case_c1 case_c2:comp_st -> bool) =
190189
c:comp_st { st_comp_of_comp c == st_comp_with_pre (st_comp_of_comp c2) pre /\
191190
comp_post_matches_hint c post_hint } &
192191
st_typing g t c)
193-
(requires fun _ ->
194-
let _, x = px in
192+
(requires
193+
(let _, x = px in
195194
comp_pre c1 == pre /\
196195
None? (lookup g x) /\
197196
(~(x `Set.mem` freevars_st e2)) /\
198197
open_term (comp_post c1) x == comp_pre c2 /\
199-
(~ (x `Set.mem` freevars (comp_post c2))))
200-
(ensures fun _ _ -> True)
201-
#pop-options
198+
(~ (x `Set.mem` freevars (comp_post c2)))))
199+
(ensures fun _ -> True)
202200

203201
let mk_bind_st_st
204202
: bind_t C_ST? C_ST?
@@ -359,18 +357,18 @@ let rec mk_bind (g:env)
359357
st_comp_of_comp c == st_comp_with_pre (st_comp_of_comp c2) pre /\
360358
comp_post_matches_hint c post_hint } &
361359
st_typing g t c)
362-
(requires fun _ ->
363-
let _, x = px in
360+
(requires
361+
(let _, x = px in
364362
comp_pre c1 == pre /\
365363
None? (lookup g x) /\
366364
(~(x `Set.mem` freevars_st e2)) /\
367365
open_term (comp_post c1) x == comp_pre c2 /\
368-
(~ (x `Set.mem` freevars (comp_post c2))))
369-
(ensures fun _ _ -> True) =
366+
(~ (x `Set.mem` freevars (comp_post c2)))))
367+
(ensures fun _ -> True) =
370368
let _, x = px in
371369
let b = nvar_as_binder px (comp_res c1) in
372-
let fail_bias (#a:Type) tag
373-
: T.TacH a (requires fun _ -> True) (ensures fun _ r -> FStar.Tactics.Result.Failed? r)
370+
let fail_bias tag
371+
: T.TacH _ (requires True) (ensures fun _ -> False)
374372
= let open Pulse.PP in
375373
fail_doc g (Some e1.range)
376374
[text "Cannot compose computations in this " ^/^ text tag ^/^ text " block:";

‎src/checker/Pulse.Typing.Combinators.fsti‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -58,14 +58,14 @@ val mk_bind (g:env)
5858
c:comp_st { st_comp_of_comp c == st_comp_with_pre (st_comp_of_comp c2) pre /\
5959
comp_post_matches_hint c post_hint } &
6060
st_typing g t c)
61-
(requires fun _ ->
62-
let _, x = px in
61+
(requires
62+
(let _, x = px in
6363
comp_pre c1 == pre /\
6464
None? (lookup g x) /\
6565
(~(x `Set.mem` freevars_st e2)) /\
6666
open_term (comp_post c1) x == comp_pre c2 /\
67-
(~ (x `Set.mem` freevars (comp_post c2))))
68-
(ensures fun _ _ -> True)
67+
(~ (x `Set.mem` freevars (comp_post c2)))))
68+
(ensures fun _ -> True)
6969

7070

7171
val bind_res_and_post_typing (g:env) (s2:comp_st) (x:var { fresh_wrt x g (freevars (comp_post s2)) })

‎src/checker/Pulse.Typing.Env.fst‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -459,7 +459,6 @@ let info (g:env) (r:option range) (msg:string) =
459459
let fail_doc_with_subissues #a (g:env) (ro : option range)
460460
(sub : list Issue.issue)
461461
(msg : list document)
462-
: T.TacH a (requires fun _ -> True) (ensures fun _ r -> FStar.Tactics.Result.Failed? r)
463462
=
464463
(* If for whatever reason `sub` is empty, F* will handle it well
465464
and a generic error message will be displayed *)

‎src/checker/Pulse.Typing.Env.fsti‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -225,10 +225,10 @@ val get_range (g:env) (r:option range) : T.Tac range
225225

226226
val fail_doc_env (#a:Type) (with_env:bool)
227227
(g:env) (r:option range) (msg:list Pprint.document)
228-
: T.TacH a (requires fun _ -> True) (ensures fun _ r -> FStar.Tactics.Result.Failed? r)
228+
: T.TacH a (requires True) (ensures fun _ -> False)
229229

230230
let fail_doc (#a:Type) (g:env) (r:option range) (msg:list Pprint.document)
231-
: T.TacH a (requires fun _ -> True) (ensures fun _ r -> FStar.Tactics.Result.Failed? r)
231+
: T.TacH a (requires True) (ensures fun _ -> False)
232232
= fail_doc_env false g r msg
233233

234234
val warn_doc (g:env) (r:option range) (msg:list Pprint.document)
@@ -241,7 +241,7 @@ val info_doc_env (g:env) (r:option range) (msg:list Pprint.document)
241241
: T.Tac unit
242242

243243
val fail (#a:Type) (g:env) (r:option range) (msg:string)
244-
: T.TAC a (fun _ post -> forall ex ps. post FStar.Tactics.Result.(Failed ex ps))
244+
: T.TacH a (requires True) (ensures fun _ -> False)
245245

246246
val warn (g:env) (r:option range) (msg:string)
247247
: T.Tac unit
@@ -252,7 +252,7 @@ val info (g:env) (r:option range) (msg:string)
252252
val fail_doc_with_subissues #a (g:env) (ro : option range)
253253
(sub : list Issue.issue)
254254
(msg : list Pprint.document)
255-
: T.TacH a (requires fun _ -> True) (ensures fun _ r -> FStar.Tactics.Result.Failed? r)
255+
: T.TacH a (requires True) (ensures fun _ -> False)
256256

257257
val info_doc_with_subissues (g:env) (r:option range)
258258
(sub : list Issue.issue)

‎src/ml/PulseSyntaxExtension_SyntaxWrapper.ml‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -238,9 +238,7 @@ let tac_to_string (env:Env.env) f =
238238
[]
239239
[]
240240
in
241-
match f ps with
242-
| FStarC_Tactics_Result.Success (x, _) -> x
243-
| FStarC_Tactics_Result.Failed (exn, _) -> failwith (print_exn exn)
241+
f (ref ps)
244242

245243
let binder_to_string (env:Env.env) (b:binder)
246244
: string

0 commit comments

Comments
 (0)