Skip to content

Commit cfceb2b

Browse files
KaptchKaptch
committed
refactor
1 parent df4874f commit cfceb2b

12 files changed

Lines changed: 60 additions & 153 deletions

File tree

‎_CoqProject‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,8 @@
11
-Q theories gitrees
22
-Q vendor/Binding Binding
3+
-arg -w -arg -notation-overridden
4+
-arg -w -arg -notation-incompatible-prefix
5+
-arg -w -arg -redundant-canonical-projection
36
-arg -w -arg -ssr-search-moved
47

58
vendor/Binding/Properties.v

‎theories/examples/except_lang/lang.v‎

Lines changed: 14 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -34,9 +34,9 @@ Module Lang (Errors : ExcSig).
3434
| ThrowK (err : exc) : cont → cont
3535
| CatchK (err : exc) (h : @expr (inc X)) : cont → cont.
3636

37-
Arguments val X%bind : clear implicits.
38-
Arguments expr X%bind : clear implicits.
39-
Arguments cont X%bind : clear implicits.
37+
Arguments val X%_bind : clear implicits.
38+
Arguments expr X%_bind : clear implicits.
39+
Arguments cont X%_bind : clear implicits.
4040

4141

4242
Local Open Scope bind_scope.
@@ -55,18 +55,18 @@ Module Lang (Errors : ExcSig).
5555
match v with
5656
| LitV n => LitV n
5757
| RecV e => RecV (emap ((f ↑) ↑) e)
58-
end
59-
with kmap {A B : Set} (f : A [→] B) (K : cont A) : cont B :=
60-
match K with
61-
| END => END
62-
| IfK e₁ e₂ K => IfK (emap f e₁) (emap f e₂) (kmap f K)
63-
| AppLK v K => AppLK (vmap f v) (kmap f K)
64-
| AppRK e K => AppRK (emap f e) (kmap f K)
65-
| NatOpLK op v K => NatOpLK op (vmap f v) (kmap f K)
66-
| NatOpRK op e K => NatOpRK op (emap f e) (kmap f K)
67-
| ThrowK err K => ThrowK err (kmap f K)
68-
| CatchK err h K => CatchK err (emap (f ↑) h) (kmap f K)
6958
end.
59+
Fixpoint kmap {A B : Set} (f : A [→] B) (K : cont A) : cont B :=
60+
match K with
61+
| END => END
62+
| IfK e₁ e₂ K => IfK (emap f e₁) (emap f e₂) (kmap f K)
63+
| AppLK v K => AppLK (vmap f v) (kmap f K)
64+
| AppRK e K => AppRK (emap f e) (kmap f K)
65+
| NatOpLK op v K => NatOpLK op (vmap f v) (kmap f K)
66+
| NatOpRK op e K => NatOpRK op (emap f e) (kmap f K)
67+
| ThrowK err K => ThrowK err (kmap f K)
68+
| CatchK err h K => CatchK err (emap (f ↑) h) (kmap f K)
69+
end.
7070

7171
#[export] Instance FMap_expr : FunctorCore expr := @emap.
7272
#[export] Instance FMap_val : FunctorCore val := @vmap.

‎theories/examples/heap_lang/lang.v‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -376,7 +376,7 @@ Inductive ectx_item :=
376376
| FaaLCtx (v2 : val)
377377
| FaaRCtx (e1 : expr).
378378

379-
Fixpoint fill_item (Ki : ectx_item) (e : expr) : expr :=
379+
Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
380380
match Ki with
381381
| AppLCtx v2 => App e (of_val v2)
382382
| AppRCtx e1 => App e1 e
@@ -560,7 +560,7 @@ Definition state_init_heap (l : loc) (n : Z) (v : val) (σ : state) : state :=
560560
Lemma state_init_heap_singleton l v σ :
561561
state_init_heap l 1 v σ = state_upd_heap <[l:=Some v]> σ.
562562
Proof.
563-
destruct σ as [h p]. rewrite /state_init_heap /=. f_equiv.
563+
destruct σ as [h _]. rewrite /state_init_heap /=. f_equiv.
564564
rewrite right_id insert_union_singleton_l. done.
565565
Qed.
566566

‎theories/examples/input_lang/interp.v‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -158,17 +158,17 @@ Section interp.
158158
| If e e1 e2 => interp_if (interp_expr e) (interp_expr e1) (interp_expr e2)
159159
| Input => interp_input
160160
| Output e => interp_output (interp_expr e)
161-
end
162-
with interp_ectx {S} (K : ectx S) : interp_scope S -n> (IT -n> IT) :=
163-
match K with
164-
| EmptyK => λne env, idfun
165-
| AppRK e1 K => interp_apprk (interp_expr e1) (interp_ectx K)
166-
| AppLK K v2 => interp_applk (interp_ectx K) (interp_val v2)
167-
| NatOpRK op e1 K => interp_natoprk op (interp_expr e1) (interp_ectx K)
168-
| NatOpLK op K v2 => interp_natoplk op (interp_ectx K) (interp_val v2)
169-
| IfK K e1 e2 => interp_ifk (interp_ectx K) (interp_expr e1) (interp_expr e2)
170-
| OutputK K => interp_outputk (interp_ectx K)
171161
end.
162+
Fixpoint interp_ectx {S} (K : ectx S) : interp_scope S -n> (IT -n> IT) :=
163+
match K with
164+
| EmptyK => λne env, idfun
165+
| AppRK e1 K => interp_apprk (interp_expr e1) (interp_ectx K)
166+
| AppLK K v2 => interp_applk (interp_ectx K) (interp_val v2)
167+
| NatOpRK op e1 K => interp_natoprk op (interp_expr e1) (interp_ectx K)
168+
| NatOpLK op K v2 => interp_natoplk op (interp_ectx K) (interp_val v2)
169+
| IfK K e1 e2 => interp_ifk (interp_ectx K) (interp_expr e1) (interp_expr e2)
170+
| OutputK K => interp_outputk (interp_ectx K)
171+
end.
172172
Solve All Obligations with first [ solve_proper | solve_proper_please ].
173173

174174
Global Instance interp_val_asval {S} {D : interp_scope S} (v : val S)

‎theories/examples/input_lang/lang.v‎

Lines changed: 20 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -48,17 +48,17 @@ with vmap {A B : Set} (f : A [→] B) (v : val A) : val B :=
4848
match v with
4949
| LitV n => LitV n
5050
| RecV e => RecV (emap ((f ↑) ↑) e)
51-
end
52-
with kmap {A B : Set} (f : A [→] B) (K : ectx A) : ectx B :=
53-
match K with
54-
| EmptyK => EmptyK
55-
| OutputK K => OutputK (kmap f K)
56-
| IfK K e₁ e₂ => IfK (kmap f K) (emap f e₁) (emap f e₂)
57-
| AppLK K v => AppLK (kmap f K) (vmap f v)
58-
| AppRK e K => AppRK (emap f e) (kmap f K)
59-
| NatOpRK op e K => NatOpRK op (emap f e) (kmap f K)
60-
| NatOpLK op K v => NatOpLK op (kmap f K) (vmap f v)
6151
end.
52+
Fixpoint kmap {A B : Set} (f : A [→] B) (K : ectx A) : ectx B :=
53+
match K with
54+
| EmptyK => EmptyK
55+
| OutputK K => OutputK (kmap f K)
56+
| IfK K e₁ e₂ => IfK (kmap f K) (emap f e₁) (emap f e₂)
57+
| AppLK K v => AppLK (kmap f K) (vmap f v)
58+
| AppRK e K => AppRK (emap f e) (kmap f K)
59+
| NatOpRK op e K => NatOpRK op (emap f e) (kmap f K)
60+
| NatOpLK op K v => NatOpLK op (kmap f K) (vmap f v)
61+
end.
6262
#[export] Instance FMap_expr : FunctorCore expr := @emap.
6363
#[export] Instance FMap_val : FunctorCore val := @vmap.
6464
#[export] Instance FMap_ectx : FunctorCore ectx := @kmap.
@@ -79,17 +79,17 @@ with vbind {A B : Set} (f : A [⇒] B) (v : val A) : val B :=
7979
match v with
8080
| LitV n => LitV n
8181
| RecV e => RecV (ebind ((f ↑) ↑) e)
82-
end
83-
with kbind {A B : Set} (f : A [⇒] B) (K : ectx A) : ectx B :=
84-
match K with
85-
| EmptyK => EmptyK
86-
| OutputK K => OutputK (kbind f K)
87-
| IfK K e₁ e₂ => IfK (kbind f K) (ebind f e₁) (ebind f e₂)
88-
| AppLK K v => AppLK (kbind f K) (vbind f v)
89-
| AppRK e K => AppRK (ebind f e) (kbind f K)
90-
| NatOpRK op e K => NatOpRK op (ebind f e) (kbind f K)
91-
| NatOpLK op K v => NatOpLK op (kbind f K) (vbind f v)
9282
end.
83+
Fixpoint kbind {A B : Set} (f : A [⇒] B) (K : ectx A) : ectx B :=
84+
match K with
85+
| EmptyK => EmptyK
86+
| OutputK K => OutputK (kbind f K)
87+
| IfK K e₁ e₂ => IfK (kbind f K) (ebind f e₁) (ebind f e₂)
88+
| AppLK K v => AppLK (kbind f K) (vbind f v)
89+
| AppRK e K => AppRK (ebind f e) (kbind f K)
90+
| NatOpRK op e K => NatOpRK op (ebind f e) (kbind f K)
91+
| NatOpLK op K v => NatOpLK op (kbind f K) (vbind f v)
92+
end.
9393

9494
#[export] Instance BindCore_expr : BindCore expr := @ebind.
9595
#[export] Instance BindCore_val : BindCore val := @vbind.

‎theories/gitree/reductions.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -495,7 +495,7 @@ Section internal_step.
495495
- rewrite app_comm_cons.
496496
by rewrite -app_assoc.
497497
- iRewrite "H1".
498-
rewrite !app_length //.
498+
rewrite !length_app //.
499499
Qed.
500500

501501
Lemma external_step_internal_step α β σ σ' en :

‎theories/gitree/weakestpre.v‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -501,11 +501,11 @@ Section weakestpre.
501501
(at level 20, α, s, Φ at level 200, only parsing) : bi_scope.
502502

503503
Notation "'WP' α @ s ; E {{ v , Q } }" := (wp α s E (λ v, Q))
504-
(at level 20, α, s, Q at level 200,
504+
(at level 20, α, s, Q at level 200, v at level 200 as pattern,
505505
format "'[hv' 'WP' α '/' @ s ; E '/' {{ '[' v , '/' Q ']' } } ']'") : bi_scope.
506506

507507
Notation "'WP' α @ s {{ β , Φ } }" := (wp α s ⊤ (λ β, Φ))
508-
(at level 20, α, Φ at level 200,
508+
(at level 20, α, Φ at level 200, β at level 200 as pattern,
509509
format "'WP' α @ s {{ β , Φ } }") : bi_scope.
510510

511511
Notation "'WP' α @ s {{ Φ } }" := (wp α s ⊤ Φ)

‎theories/utils/clwp.v‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -175,8 +175,6 @@ Section clwp.
175175

176176
End clwp.
177177

178-
Check clwp.
179-
180178
Notation "'CLWP@{' re } e @ s ; E {{ Φ } }" :=
181179
(clwp re s E e Φ)
182180
(at level 20, e, Φ at level 200, only parsing) : bi_scope.

‎vendor/Binding/Core.v‎

Lines changed: 0 additions & 47 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,5 @@
11
Require Import Utf8.
22
Require Import RelationClasses Morphisms.
3-
Require Vector.
43

54
Declare Scope bind_scope.
65
Delimit Scope bind_scope with bind.
@@ -49,10 +48,6 @@ Section Arrows.
4948
Class FunctorCore (F : Obj → Type) :=
5049
fmap : ∀ {A B}, (Arr A B) → F A → F B.
5150

52-
(*Definition fmap {F : Obj → Type}
53-
{FunCore : FunctorCore F} {A B : Obj}
54-
(f : Arr A B) : F A → F B := fmap_core _ _ f.*)
55-
5651
Class Functor (F : Obj → Type) {FunCore : FunctorCore F} : Prop :=
5752
{ map_id {A} (f : Arr A A) (t : F A) (EQ : f ≡ ı) :
5853
fmap f t = t;
@@ -81,8 +76,6 @@ Section Substitutions.
8176
Definition sub {Arr Sub} {ASC : SubstCore Arr Sub} := Sub.
8277
Definition subarr {Arr Sub} {ASC : SubstCore Arr Sub} := Arr.
8378

84-
(*Notation " 'η' " := (subst_pure _) : bind_scope.
85-
Notation " σ • ρ " := (subst_comp σ%bind ρ%bind) (at level 40, left associativity) : bind_scope.*)
8679
Notation " f '̂' " := (subst_of_arr f%bind) (at level 30) : bind_scope.
8780

8881
Class Subst
@@ -103,10 +96,6 @@ Section Substitutions.
10396
Class BindCore (F : Obj → Type) :=
10497
bind : ∀ {A B}, (Sub A B) → F A → F B.
10598

106-
(*Definition bind {F : Obj → Type}
107-
{BindF : BindCore F} {A B : Obj}
108-
(f : Sub A B) : F A → F B := bind_core _ _ f.*)
109-
11099
Class BindMapPure (F : Obj → Type) {MapF : FunctorCore F} {BindF : BindCore F} : Prop :=
111100
{ bind_map {A B} (f : Arr A B) g t
112101
(EQ : f ̂ ≡ g) :
@@ -200,21 +189,6 @@ Section Shifting.
200189
{A : Obj}
201190
(a : F A) : F (Inc A) := fmap mk_shift a.
202191

203-
(*Fixpoint mk_shiftn
204-
{Arr : Obj → Obj → Type}
205-
{F : Obj → Type} {map} {MapF : FunctorCore (F:=F) (Arr:=Arr) map}
206-
{Inc : Obj → Obj} {AC : ArrowCore Arr} {ALC : ALiftableCore Arr Inc} {Sh : ShiftableCore Arr Inc}
207-
{A : Obj} n : Arr A (Nat.iter n Inc A) :=
208-
match n with
209-
| O => ı
210-
| S n' => (liftA (G := Inc) (mk_shiftn (Inc := Inc) n')) ∘ mk_shift
211-
end.
212-
213-
Definition shiftn {Arr : Obj → Obj → Type}
214-
{F : Obj → Type} {map} {MapF : FunctorCore (F:=F) (Arr:=Arr) map}
215-
{Inc : Obj → Obj} {AC : ArrowCore Arr} {ALC : ALiftableCore Arr Inc} {Sh : ShiftableCore Arr Inc}
216-
n {A : Obj} (a : F A) := fmap (mk_shiftn n) a.*)
217-
218192
Context (Arr : Obj → Obj → Type) {EqArr : EqIndCore Arr} {AC : ArrowCore Arr}.
219193
Context (Sub : Obj → Obj → Type) {EqSub : EqIndCore Sub} {SC : ArrowCore Sub}.
220194
Context {ASC : SubstCore Arr Sub}.
@@ -247,27 +221,6 @@ Section Substituting.
247221
{F : Obj → Type} {Inc : Obj → Obj} {Sb : SubstitutableCore Sub F Inc}
248222
{A : Obj}
249223
(a : G (Inc A)) (v : F A) : G A := bind (mk_subst v) a.
250-
251-
(*
252-
Fixpoint mk_substV
253-
{Sub : Obj → Obj → Type} {Arr : Obj → Obj → Type}
254-
{G : Obj → Type} {bnd} {BindG : BindCore (F:=G) (Sub:=Sub) bnd}
255-
{F : Obj → Type} {Inc : Obj → Obj} {PSC : PreSubstCore Sub} {AC : ArrowCore Arr}
256-
{SC : SubstCore Arr Sub} {SLC : SLiftableCore Sub Inc} {Sb : SubstitutableCore Sub F Inc}
257-
{A : Obj} {n} (xs : Vector.t (F A) n) : Sub (Nat.iter n Inc A) A :=
258-
match xs with
259-
| Vector.nil _ => η
260-
| Vector.cons _ x _ xs => (mk_subst (Inc := Inc) x) • (mk_substV (Inc := Inc) xs) ⇑
261-
end.
262-
263-
Definition substV
264-
{Sub : Obj → Obj → Type} {Arr : Obj → Obj → Type} {AC : ArrowCore Arr}
265-
{G : Obj → Type} {bnd} {BindG : BindCore (F:=G) (Sub:=Sub) bnd}
266-
{F : Obj → Type} {Inc : Obj → Obj} {PSC : PreSubstCore Sub} {SC : SubstCore Arr Sub}
267-
{SLC : SLiftableCore Sub Inc} {Sb : SubstitutableCore Sub F Inc}
268-
{A : Obj} {n} (xs : Vector.t (F A) n) (a : G (Nat.iter n Inc A)) : G A :=
269-
bind (mk_substV xs) a.
270-
*)
271224

272225
Context (Arr : Obj → Obj → Type) {EqArr : EqIndCore Arr} {AC : ArrowCore Arr}.
273226
Context (Sub : Obj → Obj → Type) {EqSub : EqIndCore Sub} {SC : ArrowCore Sub}.

‎vendor/Binding/Env.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,7 @@ Proof.
6969
solve_equiv.
7070
Qed.
7171

72-
Global Hint Extern 4 (_ ≡ _) => solve_equiv.
72+
Global Hint Extern 4 (_ ≡ _) => solve_equiv : core.
7373

7474
Ltac simpl_HFInd :=
7575
subst; try discriminate;

0 commit comments

Comments
 (0)