-
Notifications
You must be signed in to change notification settings - Fork 1
/
ex_utils.v
136 lines (100 loc) · 4.47 KB
/
ex_utils.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
(** * Infrastructure for examples of DOT programs. *)
From stdpp Require Import strings.
From D Require Import tactics.
From D.Dot Require Import syn path_repl lr_syn_aux.
Implicit Types (L T U : ty) (v : vl) (e : tm) (d : dm) (ds : dms) (Γ : list ty).
(*******************)
(** * NOTATIONS **)
(*******************)
Coercion tv : vl_ >-> tm.
Coercion pv : vl_ >-> path.
Coercion vlit : base_lit >-> vl_.
Coercion lint : Z >-> base_lit.
Coercion lbool : bool >-> base_lit.
Identity Coercion vl2vl_ : vl >-> vl_.
Coercion vl_2vl := id : vl_ -> vl.
Module Import DBNotation.
Bind Scope expr_scope with tm.
Delimit Scope expr_scope with E.
Notation "()" := (vobj []) : expr_scope.
Notation "e1 + e2" := (tbin bplus e1%E e2%E) : expr_scope.
Notation "e1 - e2" := (tbin bminus e1%E e2%E) : expr_scope.
Notation "e1 * e2" := (tbin btimes e1%E e2%E) : expr_scope.
Notation "e1 `div` e2" := (tbin bdiv e1%E e2%E) : expr_scope.
Notation "e1 ≤ e2" := (tbin ble e1%E e2%E) : expr_scope.
Notation "e1 < e2" := (tbin blt e1%E e2%E) : expr_scope.
Notation "e1 = e2" := (tbin beq e1%E e2%E) : expr_scope.
Notation "e1 ≠ e2" := (tun unot (tbin beq e1%E e2%E)) : expr_scope.
Notation "~ e" := (tun unot e%E) (at level 75, right associativity) : expr_scope.
Notation "e1 > e2" := (e2%E < e1%E)%E : expr_scope.
Notation "e1 ≥ e2" := (e2%E ≤ e1%E)%E : expr_scope.
(** ** Notation for object values. *)
Open Scope dms_scope.
Notation "{@ }" := (@nil (string * dm)) (format "{@ }") : dms_scope.
Notation "{@ x }" := ( x :: {@} ) (format "{@ x }") : dms_scope.
Notation "{@ x ; y ; .. ; z }" :=
(cons x (cons y .. (cons z nil) ..))
(format "'[v' {@ '[' x ']' ; '/' y ; '/' .. ; '/' z } ']'")
: dms_scope.
Close Scope dms_scope.
Arguments vobj _%dms_scope.
Notation "'ν' ds" := (vobj ds) (at level 60, ds at next level).
Notation "'val' l = v" := (l, dpt v) (at level 60, l at level 50).
Notation "'type' l = T" := (l, dtysyn T) (at level 60, l at level 50).
(** Notation for object types. *)
#[global] Instance : Top ty := TTop.
#[global] Instance : Bottom ty := TBot.
Open Scope ty_scope.
Notation "{@ T1 }" := ( TAnd T1 ⊤ ) (format "{@ T1 }") : ty_scope.
Notation "{@ T1 ; T2 ; .. ; Tn }" :=
(TAnd T1 (TAnd T2 .. (TAnd Tn ⊤)..))
(format "'[v' {@ '[' T1 ']' ; '/' T2 ; '/' .. ; '/' Tn } ']'") : ty_scope.
Close Scope ty_scope.
Notation "'𝐙'" := TInt : ty_scope.
Notation "▶:" := TLater : ty_scope.
(* Level taken from Iris. *)
Notation "▶: T" := (TLater T) (at level 49, right associativity) : ty_scope.
Notation "'∀:' T , U" := (TAll T U) (at level 48, T at level 98, U at level 98).
Notation "'μ' Ts" := (TMu Ts) (at level 50, Ts at next level).
Notation "'type' l >: L <: U" := (TTMemL l L U) (at level 60, l at level 50, L, U at level 70) : ty_scope.
Notation "'val' l : T" :=
(TVMem l T)
(at level 60, l, T at level 50, format "'[' 'val' l : T ']' '/'") : ty_scope.
Notation "S →: T" := (TAll S%ty (shift T%ty)) (at level 49, T at level 98, right associativity) : ty_scope.
Notation "p @; l" := (TSel p l) (at level 48).
Notation "v @ l1 @ .. @ l2" := (pself .. (pself v l1) .. l2)
(format "v @ l1 @ .. @ l2", at level 48, l1, l2 at level 40).
Notation "a @: b" := (tproj a b) (at level 59, b at next level).
Infix "$:" := tapp (at level 68, left associativity).
Notation tparam A := (type A >: ⊥ <: ⊤)%ty.
Definition typeEq l T : ty := type l >: T <: T.
Notation x0 := (vvar 0).
Notation x1 := (vvar 1).
Notation x2 := (vvar 2).
Notation x3 := (vvar 3).
Notation x4 := (vvar 4).
Notation x5 := (vvar 5).
Notation TUnit := (⊤%ty : ty).
Notation tUnit := (tv (vint 0) : tm).
End DBNotation.
(******************)
(** * AUTOMATION **)
(******************)
From D.Dot Require Import traversals.
Import Trav1.
Ltac stconstructor := match goal with
| |- forall_traversal_tm _ _ _ => constructor
| |- forall_traversal_vl _ _ _ => constructor
| |- forall_traversal_dm _ _ _ => constructor
| |- forall_traversal_path _ _ _ => constructor
| |- forall_traversal_ty _ _ _ => constructor
| |- forall_traversal_kind _ _ _ => constructor
| |- Forall _ _ => constructor
end.
Ltac stcrush := try ((progress repeat stconstructor); eauto).
#[global] Hint Extern 10 (_ ≤ _) => lia : core.
#[global] Hint Extern 0 (dms_hasnt _ _) => done : core.
#[global] Hint Resolve Nat.lt_0_succ : core.
Definition lett t u := tapp (vabs u) t.
(** Simplify substitution operations on concrete terms. *)
Ltac simplSubst := rewrite /= /up/= /ids/ids_vl/=.