Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
RefinedC
Commits
e730d221
Commit
e730d221
authored
Nov 24, 2021
by
Michael Sammler
Browse files
less let bindings
parent
d7218553
Pipeline
#57820
passed with stage
in 11 minutes and 20 seconds
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
theories/typing/automation.v
View file @
e730d221
...
...
@@ -57,22 +57,19 @@ Ltac record_destruct_hint hint info ::= add_case_distinction_info hint info.
Ltac
convert_to_i2p_tac
P
bind
cont
::
=
lazymatch
P
with
|
typed_value
?v
?T
=>
bind
T
ltac
:
(
fun
H
=>
uconstr
:
(
typed_value
v
H
))
;
(* One could introduce more let-bindings as follows, but too
many let-bindings seem to hurt performance. *)
(* bind T ltac:(fun H => uconstr:(typed_value v H)); *)
cont
uconstr
:
(((
_
:
TypedValue
_
)
_
))
|
typed_bin_op
?v1
?ty1
?v2
?ty2
?o
?ot1
?ot2
?T
=>
bind
T
ltac
:
(
fun
H
=>
uconstr
:
(
typed_bin_op
v1
ty1
v2
ty2
o
ot1
ot2
H
))
;
cont
uconstr
:
(((
_
:
TypedBinOp
_
_
_
_
_
_
_
)
_
))
|
typed_un_op
?v
?ty
?o
?ot
?T
=>
bind
T
ltac
:
(
fun
H
=>
uconstr
:
(
typed_un_op
?v
?ty
?o
?ot
H
))
;
cont
uconstr
:
(((
_
:
TypedUnOp
_
_
_
_
)
_
))
|
typed_call
?v
?P
?vl
?tys
?T
=>
bind
T
ltac
:
(
fun
H
=>
uconstr
:
(
typed_call
v
P
vl
tys
H
))
;
cont
uconstr
:
(((
_
:
TypedCall
_
_
_
_
)
_
))
|
typed_copy_alloc_id
?v1
?ty1
?v2
?ty2
?ot
?T
=>
bind
T
ltac
:
(
fun
H
=>
uconstr
:
(
typed_copy_alloc_id
v1
ty1
v2
ty2
ot
H
))
;
cont
uconstr
:
(((
_
:
TypedCopyAllocId
_
_
_
_
_
)
_
))
|
typed_place
?P
?l1
?
β
1
?ty1
?T
=>
bind
T
ltac
:
(
fun
H
=>
uconstr
:
(
typed_place
P
l1
β
1
ty1
H
))
;
cont
uconstr
:
(((
_
:
TypedPlace
_
_
_
_
)
_
))
|
typed_if
?ot
?v
?P
?T1
?T2
=>
cont
uconstr
:
(((
_
:
TypedIf
_
_
_
)
_
_
))
...
...
@@ -81,25 +78,18 @@ Ltac convert_to_i2p_tac P bind cont ::=
|
typed_assert
?ot
?v
?ty
?s
?fn
?ls
?fr
?Q
=>
cont
uconstr
:
(((
_
:
TypedAssert
_
_
_
)
_
_
_
_
_
))
|
typed_read_end
?a
?E
?l
?
β
?ty
?ly
?T
=>
bind
T
ltac
:
(
fun
H
=>
uconstr
:
(
typed_read_end
a
E
l
β
ty
ly
H
))
;
cont
uconstr
:
(((
_
:
TypedReadEnd
_
_
_
_
_
_
)
_
))
|
typed_write_end
?a
?E
?ot
?v1
?ty1
?l2
?
β
2
?ty2
?T
=>
bind
T
ltac
:
(
fun
H
=>
uconstr
:
(
typed_write_end
a
E
ot
v1
ty1
l2
β
2
ty2
H
))
;
cont
uconstr
:
(((
_
:
TypedWriteEnd
_
_
_
_
_
_
_
_
)
_
))
|
typed_addr_of_end
?l
?
β
?ty
?T
=>
bind
T
ltac
:
(
fun
H
=>
uconstr
:
(
typed_addr_of_end
l
β
ty
H
))
;
cont
uconstr
:
(((
_
:
TypedAddrOfEnd
_
_
_
)
_
))
|
typed_cas
?ot
?v1
?P1
?v2
?P2
?v3
?P3
?T
=>
bind
T
ltac
:
(
fun
H
=>
uconstr
:
(
typed_cas
ot
v1
P1
v2
P2
v3
P3
H
))
;
cont
uconstr
:
(((
_
:
TypedCas
_
_
_
_
_
_
_
)
_
))
|
typed_annot_expr
?n
?a
?v
?P
?T
=>
bind
T
ltac
:
(
fun
H
=>
uconstr
:
(
typed_annot_expr
n
a
v
P
H
))
;
cont
uconstr
:
(((
_
:
TypedAnnotExpr
_
_
_
_
)
_
)
)
|
typed_annot_stmt
?a
?l
?P
?T
=>
bind
T
ltac
:
(
fun
H
=>
uconstr
:
(
typed_annot_stmt
a
l
P
H
))
;
cont
uconstr
:
(((
_
:
TypedAnnotStmt
_
_
_
)
_
))
|
typed_macro_expr
?m
?es
?T
=>
bind
T
ltac
:
(
fun
H
=>
uconstr
:
(
typed_macro_expr
m
es
H
))
;
cont
uconstr
:
(((
_
:
TypedMacroExpr
_
_
)
_
))
end
.
...
...
@@ -128,16 +118,14 @@ Ltac liRIntroduceLetInGoal :=
lazymatch
goal
with
|
|-
@
envs_entails
?PROP
?
Δ
?P
=>
lazymatch
P
with
(* | @bi_wand ?PROP ?Q ?T => *)
(* li_let_bind T (fun H => constr:(@envs_entails PROP Δ (@bi_wand PROP Q H))) *)
|
@
typed_val_expr
?
Σ
?tG
?e
?T
=>
li_let_bind
T
(
fun
H
=>
constr
:
(@
envs_entails
PROP
Δ
(@
typed_val_expr
Σ
tG
e
H
)))
|
@
typed_write
?
Σ
?tG
?b
?e
?ot
?v
?ty
?Mov
?T
=>
li_let_bind
T
(
fun
H
=>
constr
:
(@
envs_entails
PROP
Δ
(@
typed_write
Σ
tG
b
e
ot
v
ty
Mov
H
)))
(*
| @typed_place ?Σ ?tG ?P ?l1 ?β1 ?ty1 ?T =>
*)
(*
li_let_bind T (fun H => constr:(@envs_entails PROP Δ (@typed_place Σ tG P l1 β1 ty1 H)))
*)
(*
| @typed_bin_op ?Σ ?tG ?v1 ?P1 ?v2 ?P2 ?op ?ot1 ?ot2 ?T =>
*)
(*
li_let_bind T (fun H => constr:(@envs_entails PROP Δ (@typed_bin_op Σ tG v1 P1 v2 P2 op ot1 ot2 H)))
*)
|
@
typed_place
?
Σ
?tG
?P
?l1
?
β
1
?ty1
?T
=>
li_let_bind
T
(
fun
H
=>
constr
:
(@
envs_entails
PROP
Δ
(@
typed_place
Σ
tG
P
l1
β
1
ty1
H
)))
|
@
typed_bin_op
?
Σ
?tG
?v1
?P1
?v2
?P2
?op
?ot1
?ot2
?T
=>
li_let_bind
T
(
fun
H
=>
constr
:
(@
envs_entails
PROP
Δ
(@
typed_bin_op
Σ
tG
v1
P1
v2
P2
op
ot1
ot2
H
)))
end
end
.
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment