post merge mopup

hazelgrove · Oct 10, 2016 · f62c07d · f62c07d
2 parents 5e8bddb + 192a138
commit f62c07d
Show file tree

Hide file tree

Showing 11 changed files with 116 additions and 111 deletions.
diff --git a/aasubsume-min.agda b/aasubsume-min.agda
@@ -152,12 +152,12 @@ module aasubsume-min where
     min-ana (AAFinish x) = _ , AAFinish x , <>
     min-ana (AAZipLam x₁ x₂ d) with min-ana d
     ... | a , b , c = _ , AAZipLam x₁ x₂ b , c
-    min-ana (AASubsume x x₁ SAConInl TCRefl) = inl ▹ <||> ◃ , AAConInl1 MPPlus , <>
-    min-ana (AASubsume x x₁ SAConInl TCHole2) = inl ▹ <||> ◃ , AAConInl1 MPHole , <>
-    min-ana (AASubsume x x₁ SAConInl (TCPlus x₃ x₄)) = inl ▹ <||> ◃ , AAConInl1 MPPlus , <>
-    min-ana (AASubsume x x₁ SAConInr TCRefl) = inr ▹ <||> ◃ , AAConInr1 MPPlus , <>
-    min-ana (AASubsume x x₁ SAConInr TCHole2) = inr ▹ <||> ◃ , AAConInr1 MPHole , <>
-    min-ana (AASubsume x x₁ SAConInr (TCPlus x₃ x₄)) = inr ▹ <||> ◃ , AAConInr1 MPPlus , <>
+    min-ana (AASubsume x x₁ SAConInl TCRefl) = inl ▹ ⦇⦈ ◃ , AAConInl1 MPPlus , <>
+    min-ana (AASubsume x x₁ SAConInl TCHole2) = inl ▹ ⦇⦈ ◃ , AAConInl1 MPHole , <>
+    min-ana (AASubsume x x₁ SAConInl (TCPlus x₃ x₄)) = inl ▹ ⦇⦈ ◃ , AAConInl1 MPPlus , <>
+    min-ana (AASubsume x x₁ SAConInr TCRefl) = inr ▹ ⦇⦈ ◃ , AAConInr1 MPPlus , <>
+    min-ana (AASubsume x x₁ SAConInr TCHole2) = inr ▹ ⦇⦈ ◃ , AAConInr1 MPHole , <>
+    min-ana (AASubsume x x₁ SAConInr (TCPlus x₃ x₄)) = inr ▹ ⦇⦈ ◃ , AAConInr1 MPPlus , <>
     min-ana (AAConInl1 x) = _ , AAConInl1 x , <>
     min-ana (AAConInl2 x) = _ , AAConInl2 x , <>
     min-ana (AAConInr1 x) = _ , AAConInr1 x , <>
@@ -214,7 +214,7 @@ module aasubsume-min where
     ... | (e'' , _ , _) = ap1 (λ q → _ ·+₂ q) qq
     min-fixed-synth (SAZipHole x x₁ d) min with min-fixed-synth d min
     ... | qq with min-synth d
-    ... | (e'' , _ , _) = ap1 <|_|> qq
+    ... | (e'' , _ , _) = ap1 ⦇_⦈ qq
     min-fixed-synth SAConInl min = refl
     min-fixed-synth SAConInr min = refl
     min-fixed-synth (SAConCase1 x₁ x₂ x₃) min = refl
@@ -254,7 +254,7 @@ module aasubsume-min where
     ... | (e'' , _ , _) = ap1 (λ q → _ ·+₂ q) qq
     min-fixed-ana (AASubsume x x₁ (SAZipHole x₂ x₃ x₄) x₅) min with min-fixed-synth x₄ min
     ... | qq with min-synth x₄
-    ... | (e'' , _ , _) = ap1 <|_|> qq
+    ... | (e'' , _ , _) = ap1 ⦇_⦈ qq
     min-fixed-ana (AAMove x) min = refl
     min-fixed-ana AADel min = refl
     min-fixed-ana AAConAsc min = refl

diff --git a/checks.agda b/checks.agda
@@ -130,13 +130,13 @@ module checks where
                erase-t t t◆ →
                erase-t t' t'◆ →
                runtype t L t' →
-               runsynth Γ (<||> ·:₂ t) t◆ L (<||> ·:₂ t') t'◆
+               runsynth Γ (⦇⦈ ·:₂ t) t◆ L (⦇⦈ ·:₂ t') t'◆
   ziplem-asc2 {Γ} er er' rt with erase-t◆ er | erase-t◆ er'
   ... | refl | refl = ziplem-asc2' {Γ = Γ} rt
    where
      ziplem-asc2' : ∀{t L t' Γ } →
                runtype t L t' →
-               runsynth Γ (<||> ·:₂ t) (t ◆t) L (<||> ·:₂ t') (t' ◆t)
+               runsynth Γ (⦇⦈ ·:₂ t) (t ◆t) L (⦇⦈ ·:₂ t') (t' ◆t)
      ziplem-asc2' DoRefl = DoRefl
      ziplem-asc2' (DoType x rt) = DoSynth
                       (SAZipAsc2 x (◆erase-t _ _ refl) (◆erase-t _ _ refl)
@@ -173,7 +173,7 @@ module checks where
   ziplem-nehole-a : ∀{Γ e e' L t t'} →
                 (Γ ⊢ e ◆e => t) →
                 runsynth Γ e t L e' t' →
-                runsynth Γ <| e |> <||> L <| e' |> <||>
+                runsynth Γ ⦇ e ⦈ ⦇⦈ L ⦇ e' ⦈ ⦇⦈
   ziplem-nehole-a wt DoRefl = DoRefl
   ziplem-nehole-a wt (DoSynth {e = e} x d) =
     DoSynth (SAZipHole (rel◆ e) wt x) (ziplem-nehole-a (actsense-synth (rel◆ e) (rel◆ _) x wt) d)
@@ -182,7 +182,7 @@ module checks where
                 (Γ ⊢ e ◆e => t) →
                 (t'' ~ t') →
                 runsynth Γ e t L e' t' →
-                runana Γ <| e |> L <| e' |> t''
+                runana Γ ⦇ e ⦈ L ⦇ e' ⦈ t''
   ziplem-nehole-b wt c DoRefl = DoRefl
   ziplem-nehole-b wt c (DoSynth x rs) =
                      DoAna (AASubsume (erase-in-hole (rel◆ _)) (SNEHole wt) (SAZipHole (rel◆ _) wt x) TCHole1)
@@ -299,8 +299,8 @@ module checks where
                   erase-e e e◆ →
                   Γ ⊢ e◆ => t →
                   runsynth Γ e t L e' t' →
-                  runana Γ (case₁ <| e  |> x <||> y <||>) L
-                           (case₁ <| e' |> x <||> y <||>) t0
+                  runana Γ (case₁ ⦇ e ⦈ x ⦇⦈ y ⦇⦈) L
+                           (case₁ ⦇ e' ⦈ x ⦇⦈ y ⦇⦈) t0
   ziplem-case1b _ _ _ _ DoRefl = DoRefl
   ziplem-case1b x# y# er wt (DoSynth x₁ rs) =
                    DoAna (AAZipCase1 x# y# (erase-in-hole er) (SNEHole wt) (SAZipHole er wt x₁)

diff --git a/constructability.agda b/constructability.agda
@@ -17,9 +17,9 @@ module constructability where
   -- in the list in the current formation context into the list monoid.
 
   -- construction of types
-  construct-type : (t : τ̇) → Σ[ L ∈ List action ] runtype (▹ <||> ◃) L (▹ t ◃)
+  construct-type : (t : τ̇) → Σ[ L ∈ List action ] runtype (▹ ⦇⦈ ◃) L (▹ t ◃)
   construct-type num  = [ construct num ] , DoType TMConNum DoRefl
-  construct-type <||> = [ del ]           , DoType TMDel DoRefl
+  construct-type ⦇⦈ = [ del ]           , DoType TMDel DoRefl
   construct-type (t1 ==> t2) with construct-type t1 | construct-type t2
   ... | (l1 , ih1) | (l2 , ih2) = l1 ++ construct arrow :: l2 ++ [ move parent ] ,
                                  runtype++ ih1
@@ -37,7 +37,7 @@ module constructability where
     -- construction of expressions in synthetic positions
     construct-synth : {Γ : ·ctx} {t : τ̇} {e : ė} → (Γ ⊢ e => t) →
                                   Σ[ L ∈ List action ]
-                                     runsynth Γ ▹ <||> ◃ <||> L ▹ e ◃ t
+                                     runsynth Γ ▹ ⦇⦈ ◃ ⦇⦈ L ▹ e ◃ t
       -- the three base cases
     construct-synth (SVar x) = [ construct (var _) ]    , DoSynth (SAConVar x) DoRefl
     construct-synth SNum =     [ construct (numlit _) ] , DoSynth SAConNumlit DoRefl
@@ -77,7 +77,7 @@ module constructability where
     -- construction of expressions in analytic positions
     construct-ana : {Γ : ·ctx} {t : τ̇} {e : ė} → (Γ ⊢ e <= t) →
                                 Σ[ L ∈ List action ]
-                                   runana Γ ▹ <||> ◃ L ▹ e ◃ t
+                                   runana Γ ▹ ⦇⦈ ◃ L ▹ e ◃ t
     construct-ana (ASubsume x c) with construct-synth x
     ... | (l , ih) = construct nehole :: l ++ (move parent :: finish :: []) ,
                      DoAna (AASubsume EETop SEHole SAConNEHole TCHole1)