Skip to content

Commit

Permalink
fixing a range in stapp checker
Browse files Browse the repository at this point in the history
  • Loading branch information
@aseemr
aseemr committed Jul 25, 2023
1 parent ade170b commit 00ab198
Show file tree
Hide file tree
Showing 2 changed files with 31 additions and 16 deletions.
2 changes: 1 addition & 1 deletion lib/steel/pulse/Pulse.Checker.STApp.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -128,7 +128,7 @@ let check
let d : st_typing _ _ (open_comp_with comp_typ arg) =
T_STApp g head formal qual comp_typ arg (E dhead) (E darg) in
let d = canonicalize_st_typing d in
let t = wr (Tm_STApp {head; arg_qual=qual; arg}) in
let t = { term = Tm_STApp {head; arg_qual=qual; arg}; range } in
let c = (canon_comp (open_comp_with comp_typ arg)) in
let d : st_typing g t c = d in

Expand Down
45 changes: 30 additions & 15 deletions src/ocaml/plugin/generated/Pulse_Checker_STApp.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -976,21 +976,23 @@ let (check :
(FStar_Range.mk_range
"Pulse.Checker.STApp.fst"
(Prims.of_int (131))
(Prims.of_int (16))
(Prims.of_int (18))
(Prims.of_int (131))
(Prims.of_int (56)))))
(Prims.of_int (67)))))
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
"Pulse.Checker.STApp.fst"
(Prims.of_int (131))
(Prims.of_int (59))
(Prims.of_int (72))
(Prims.of_int (135))
(Prims.of_int (93)))))
(FStar_Tactics_Effect.lift_div_tac
(fun
uu___6 ->
Pulse_Typing.wr
{
Pulse_Syntax_Base.term1
=
(Pulse_Syntax_Base.Tm_STApp
{
Pulse_Syntax_Base.head
Expand All @@ -999,7 +1001,10 @@ let (check :
= qual;
Pulse_Syntax_Base.arg
= arg1
})))
});
Pulse_Syntax_Base.range2
= range
}))
(fun
uu___6 ->
(fun t2
Expand Down Expand Up @@ -1180,21 +1185,23 @@ let (check :
(FStar_Range.mk_range
"Pulse.Checker.STApp.fst"
(Prims.of_int (131))
(Prims.of_int (16))
(Prims.of_int (18))
(Prims.of_int (131))
(Prims.of_int (56)))))
(Prims.of_int (67)))))
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
"Pulse.Checker.STApp.fst"
(Prims.of_int (131))
(Prims.of_int (59))
(Prims.of_int (72))
(Prims.of_int (135))
(Prims.of_int (93)))))
(FStar_Tactics_Effect.lift_div_tac
(fun
uu___7 ->
Pulse_Typing.wr
{
Pulse_Syntax_Base.term1
=
(Pulse_Syntax_Base.Tm_STApp
{
Pulse_Syntax_Base.head
Expand All @@ -1203,7 +1210,10 @@ let (check :
= qual;
Pulse_Syntax_Base.arg
= arg1
})))
});
Pulse_Syntax_Base.range2
= range
}))
(fun
uu___7 ->
(fun t2
Expand Down Expand Up @@ -1384,21 +1394,23 @@ let (check :
(FStar_Range.mk_range
"Pulse.Checker.STApp.fst"
(Prims.of_int (131))
(Prims.of_int (16))
(Prims.of_int (18))
(Prims.of_int (131))
(Prims.of_int (56)))))
(Prims.of_int (67)))))
(FStar_Sealed.seal
(Obj.magic
(FStar_Range.mk_range
"Pulse.Checker.STApp.fst"
(Prims.of_int (131))
(Prims.of_int (59))
(Prims.of_int (72))
(Prims.of_int (135))
(Prims.of_int (93)))))
(FStar_Tactics_Effect.lift_div_tac
(fun
uu___7 ->
Pulse_Typing.wr
{
Pulse_Syntax_Base.term1
=
(Pulse_Syntax_Base.Tm_STApp
{
Pulse_Syntax_Base.head
Expand All @@ -1407,7 +1419,10 @@ let (check :
= qual;
Pulse_Syntax_Base.arg
= arg1
})))
});
Pulse_Syntax_Base.range2
= range
}))
(fun
uu___7 ->
(fun t2
Expand Down

0 comments on commit 00ab198

Please sign in to comment.