From 192a138bf245da3b0ea6c56fcf3579437b691df7 Mon Sep 17 00:00:00 2001 From: Ian Voysey Date: Mon, 10 Oct 2016 17:41:38 -0400 Subject: [PATCH] upgrading hotdog bun notation to more closely match the paper and the implementation --- aasubsume-min.agda | 4 +- checks.agda | 8 ++-- constructability.agda | 8 ++-- core.agda | 88 +++++++++++++++++----------------- examples.agda | 16 +++---- judgemental-erase.agda | 14 +++--- judgemental-inconsistency.agda | 20 ++++---- keys.md | 7 +++ moveerase.agda | 2 +- structural.agda | 4 +- 10 files changed, 89 insertions(+), 82 deletions(-) diff --git a/aasubsume-min.agda b/aasubsume-min.agda index ff799ab..a45e6f8 100644 --- a/aasubsume-min.agda +++ b/aasubsume-min.agda @@ -163,7 +163,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-ana : ∀ {Γ e t α e' } → (d : Γ ⊢ e ~ α ~> e' ⇐ t) → @@ -199,7 +199,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 index 1790361..b1df329 100644 --- a/checks.agda +++ b/checks.agda @@ -119,13 +119,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) @@ -162,7 +162,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) @@ -171,7 +171,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) diff --git a/constructability.agda b/constructability.agda index b450a2b..a2c4691 100644 --- 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 @@ -31,7 +31,7 @@ module constructability where -- construction of expressions in synthetic positions construct-synth : {Γ : ·ctx} {t : τ̇} {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 @@ -71,7 +71,7 @@ module constructability where -- construction of expressions in analytic positions construct-ana : {Γ : ·ctx} {t : τ̇} {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) diff --git a/core.agda b/core.agda index d8ccb86..e3565c6 100644 --- a/core.agda +++ b/core.agda @@ -5,7 +5,7 @@ module core where -- types data τ̇ : Set where num : τ̇ - <||> : τ̇ + ⦇⦈ : τ̇ _==>_ : τ̇ → τ̇ → τ̇ -- expressions, prefixed with a · to distinguish name clashes with agda @@ -16,8 +16,8 @@ module core where ·λ : Nat → ė → ė N : Nat → ė _·+_ : ė → ė → ė - <||> : ė - <|_|> : ė → ė + ⦇⦈ : ė + ⦇_⦈ : ė → ė _∘_ : ė → ė → ė ---- contexts and some operations on them @@ -56,8 +56,8 @@ module core where -- the type consistency judgement data _~_ : (t1 : τ̇) → (t2 : τ̇) → Set where TCRefl : {t : τ̇} → t ~ t - TCHole1 : {t : τ̇} → t ~ <||> - TCHole2 : {t : τ̇} → <||> ~ t + TCHole1 : {t : τ̇} → t ~ ⦇⦈ + TCHole2 : {t : τ̇} → ⦇⦈ ~ t TCArr : {t1 t2 t1' t2' : τ̇} → t1 ~ t1' → t2 ~ t2' → @@ -72,7 +72,7 @@ module core where --- matching for arrows data _▸arr_ : τ̇ → τ̇ → Set where - MAHole : <||> ▸arr (<||> ==> <||>) + MAHole : ⦇⦈ ▸arr (⦇⦈ ==> ⦇⦈) MAArr : {t1 t2 : τ̇} → (t1 ==> t2) ▸arr (t1 ==> t2) -- matching produces unique answers @@ -87,7 +87,7 @@ module core where -- function type matchconsist : ∀{t t'} → t ▸arr t' → - t ~ (<||> ==> <||>) + t ~ (⦇⦈ ==> ⦇⦈) matchconsist MAHole = TCHole2 matchconsist MAArr = TCArr TCHole1 TCHole1 @@ -115,10 +115,10 @@ module core where Γ ⊢ e1 <= num → Γ ⊢ e2 <= num → Γ ⊢ (e1 ·+ e2) => num - SEHole : {Γ : ·ctx} → Γ ⊢ <||> => <||> + SEHole : {Γ : ·ctx} → Γ ⊢ ⦇⦈ => ⦇⦈ SNEHole : {Γ : ·ctx} {e : ė} {t : τ̇} → Γ ⊢ e => t → - Γ ⊢ <| e |> => <||> + Γ ⊢ ⦇ e ⦈ => ⦇⦈ -- analysis data _⊢_<=_ : (Γ : ·ctx) → (e : ė) → (t : τ̇) → Set where @@ -158,7 +158,7 @@ module core where -- type consistency isn't transitive not-trans : ((t1 t2 t3 : τ̇) → t1 ~ t2 → t2 ~ t3 → t1 ~ t3) → ⊥ - not-trans t with t (num ==> num) <||> num TCHole1 TCHole2 + not-trans t with t (num ==> num) ⦇⦈ num TCHole1 TCHole2 ... | () -- if the domain or codomain of a pair of arrows isn't consistent, the @@ -174,8 +174,8 @@ module core where -- every pair of types is either consistent or not consistent ~dec : (t1 t2 : τ̇) → ((t1 ~ t2) + (t1 ~̸ t2)) -- this takes care of all hole cases, so we don't consider them below - ~dec _ <||> = Inl TCHole1 - ~dec <||> _ = Inl TCHole2 + ~dec _ ⦇⦈ = Inl TCHole1 + ~dec ⦇⦈ _ = Inl TCHole2 -- num cases ~dec num num = Inl TCRefl ~dec num (t2 ==> t3) = Inr (λ ()) @@ -221,7 +221,7 @@ module core where -- those types without holes anywhere tcomplete : τ̇ → Set tcomplete num = ⊤ - tcomplete <||> = ⊥ + tcomplete ⦇⦈ = ⊥ tcomplete (t1 ==> t2) = (tcomplete t1) × (tcomplete t2) -- similarly to the complete types, the complete expressions @@ -231,8 +231,8 @@ module core where ecomplete (·λ _ e1) = ecomplete e1 ecomplete (N x) = ⊤ ecomplete (e1 ·+ e2) = ecomplete e1 × ecomplete e2 - ecomplete <||> = ⊥ - ecomplete <| e1 |> = ⊥ + ecomplete ⦇⦈ = ⊥ + ecomplete ⦇ e1 ⦈ = ⊥ ecomplete (e1 ∘ e2) = ecomplete e1 × ecomplete e2 -- zippered form of types @@ -251,7 +251,7 @@ module core where _∘₂_ : ė → ê → ê _·+₁_ : ê → ė → ê _·+₂_ : ė → ê → ê - <|_|> : ê → ê + ⦇_⦈ : ê → ê -- erasure of cursor for types and expressions, judgementally. see -- jugemental-erase for an argument that this defines an isomorphic @@ -270,7 +270,7 @@ module core where EEApR : ∀{e1 e2 e2'} → erase-e e2 e2' → erase-e (e1 ∘₂ e2) (e1 ∘ e2') EEPlusL : ∀{e1 e1' e2} → erase-e e1 e1' → erase-e (e1 ·+₁ e2) (e1' ·+ e2) EEPlusR : ∀{e1 e2 e2'} → erase-e e2 e2' → erase-e (e1 ·+₂ e2) (e1 ·+ e2') - EENEHole : ∀{e e'} → erase-e e e' → erase-e <| e |> <| e' |> + EENEHole : ∀{e e'} → erase-e e e' → erase-e ⦇ e ⦈ ⦇ e' ⦈ -- the three grammars that define actions data direction : Set where @@ -306,10 +306,10 @@ module core where TMArrParent2 : {t1 t2 : τ̇} → (t1 ==>₂ ▹ t2 ◃) + move parent +> ▹ t1 ==> t2 ◃ TMDel : {t : τ̇} → - (▹ t ◃) + del +> (▹ <||> ◃) + (▹ t ◃) + del +> (▹ ⦇⦈ ◃) TMConArrow : {t : τ̇} → - (▹ t ◃) + construct arrow +> (t ==>₂ ▹ <||> ◃) - TMConNum : (▹ <||> ◃) + construct num +> (▹ num ◃) + (▹ t ◃) + construct arrow +> (t ==>₂ ▹ ⦇⦈ ◃) + TMConNum : (▹ ⦇⦈ ◃) + construct num +> (▹ num ◃) TMArrZip1 : {t1 t1' : τ̂} {t2 : τ̇} {α : action} → (t1 + α +> t1') → ((t1 ==>₁ t2) + α +> (t1' ==>₁ t2)) @@ -354,9 +354,9 @@ module core where -- rules for non-empty holes EMNEHoleChild1 : {e : ė} → - (▹ <| e |> ◃) + move (child 1) +>e <| ▹ e ◃ |> + (▹ ⦇ e ⦈ ◃) + move (child 1) +>e ⦇ ▹ e ◃ ⦈ EMNEHoleParent : {e : ė} → - <| ▹ e ◃ |> + move parent +>e (▹ <| e |> ◃) + ⦇ ▹ e ◃ ⦈ + move parent +>e (▹ ⦇ e ⦈ ◃) mutual -- synthetic action expressions @@ -366,35 +366,35 @@ module core where (e + move δ +>e e') → Γ ⊢ e => t ~ move δ ~> e' => t SADel : {Γ : ·ctx} {e : ė} {t : τ̇} → - Γ ⊢ ▹ e ◃ => t ~ del ~> ▹ <||> ◃ => <||> + Γ ⊢ ▹ e ◃ => t ~ del ~> ▹ ⦇⦈ ◃ => ⦇⦈ SAConAsc : {Γ : ·ctx} {e : ė} {t : τ̇} → Γ ⊢ ▹ e ◃ => t ~ construct asc ~> (e ·:₂ ▹ t ◃ ) => t SAConVar : {Γ : ·ctx} {x : Nat} {t : τ̇} → (p : (x , t) ∈ Γ) → - Γ ⊢ ▹ <||> ◃ => <||> ~ construct (var x) ~> ▹ X x ◃ => t + Γ ⊢ ▹ ⦇⦈ ◃ => ⦇⦈ ~ construct (var x) ~> ▹ X x ◃ => t SAConLam : {Γ : ·ctx} {x : Nat} → (x # Γ) → - Γ ⊢ ▹ <||> ◃ => <||> ~ construct (lam x) ~> - ((·λ x <||>) ·:₂ (▹ <||> ◃ ==>₁ <||>)) => (<||> ==> <||>) + Γ ⊢ ▹ ⦇⦈ ◃ => ⦇⦈ ~ construct (lam x) ~> + ((·λ x ⦇⦈) ·:₂ (▹ ⦇⦈ ◃ ==>₁ ⦇⦈)) => (⦇⦈ ==> ⦇⦈) SAConApArr : {Γ : ·ctx} {t t1 t2 : τ̇} {e : ė} → t ▸arr (t1 ==> t2) → - Γ ⊢ ▹ e ◃ => t ~ construct ap ~> e ∘₂ ▹ <||> ◃ => t2 + Γ ⊢ ▹ e ◃ => t ~ construct ap ~> e ∘₂ ▹ ⦇⦈ ◃ => t2 SAConApOtw : {Γ : ·ctx} {t : τ̇} {e : ė} → - (t ~̸ (<||> ==> <||>)) → - Γ ⊢ ▹ e ◃ => t ~ construct ap ~> <| e |> ∘₂ ▹ <||> ◃ => <||> + (t ~̸ (⦇⦈ ==> ⦇⦈)) → + Γ ⊢ ▹ e ◃ => t ~ construct ap ~> ⦇ e ⦈ ∘₂ ▹ ⦇⦈ ◃ => ⦇⦈ SAConNumlit : {Γ : ·ctx} {n : Nat} → - Γ ⊢ ▹ <||> ◃ => <||> ~ construct (numlit n) ~> ▹ N n ◃ => num + Γ ⊢ ▹ ⦇⦈ ◃ => ⦇⦈ ~ construct (numlit n) ~> ▹ N n ◃ => num SAConPlus1 : {Γ : ·ctx} {e : ė} {t : τ̇} → (t ~ num) → - Γ ⊢ ▹ e ◃ => t ~ construct plus ~> e ·+₂ ▹ <||> ◃ => num + Γ ⊢ ▹ e ◃ => t ~ construct plus ~> e ·+₂ ▹ ⦇⦈ ◃ => num SAConPlus2 : {Γ : ·ctx} {e : ė} {t : τ̇} → (t ~̸ num) → - Γ ⊢ ▹ e ◃ => t ~ construct plus ~> <| e |> ·+₂ ▹ <||> ◃ => num + Γ ⊢ ▹ e ◃ => t ~ construct plus ~> ⦇ e ⦈ ·+₂ ▹ ⦇⦈ ◃ => num SAConNEHole : {Γ : ·ctx} {e : ė} {t : τ̇} → - Γ ⊢ ▹ e ◃ => t ~ construct nehole ~> <| ▹ e ◃ |> => <||> + Γ ⊢ ▹ e ◃ => t ~ construct nehole ~> ⦇ ▹ e ◃ ⦈ => ⦇⦈ SAFinish : {Γ : ·ctx} {e : ė} {t : τ̇} → (Γ ⊢ e => t) → - Γ ⊢ ▹ <| e |> ◃ => <||> ~ finish ~> ▹ e ◃ => t + Γ ⊢ ▹ ⦇ e ⦈ ◃ => ⦇⦈ ~ finish ~> ▹ e ◃ => t SAZipAsc1 : {Γ : ·ctx} {e e' : ê} {α : action} {t : τ̇} → (Γ ⊢ e ~ α ~> e' ⇐ t) → Γ ⊢ (e ·:₁ t) => t ~ α ~> (e' ·:₁ t) => t @@ -426,7 +426,7 @@ module core where (erase-e e e◆) → (Γ ⊢ e◆ => t) → (Γ ⊢ e => t ~ α ~> e' => t') → - Γ ⊢ <| e |> => <||> ~ α ~> <| e' |> => <||> + Γ ⊢ ⦇ e ⦈ => ⦇⦈ ~ α ~> ⦇ e' ⦈ => ⦇⦈ -- analytic action expressions data _⊢_~_~>_⇐_ : (Γ : ·ctx) → (e : ê) → (α : action) → @@ -441,29 +441,29 @@ module core where (e + move δ +>e e') → Γ ⊢ e ~ move δ ~> e' ⇐ t AADel : {e : ė} {Γ : ·ctx} {t : τ̇} → - Γ ⊢ ▹ e ◃ ~ del ~> ▹ <||> ◃ ⇐ t + Γ ⊢ ▹ e ◃ ~ del ~> ▹ ⦇⦈ ◃ ⇐ t AAConAsc : {Γ : ·ctx} {e : ė} {t : τ̇} → Γ ⊢ ▹ e ◃ ~ construct asc ~> (e ·:₂ ▹ t ◃) ⇐ t AAConVar : {Γ : ·ctx} {t t' : τ̇} {x : Nat} → (t ~̸ t') → (p : (x , t') ∈ Γ) → - Γ ⊢ ▹ <||> ◃ ~ construct (var x) ~> <| ▹ X x ◃ |> ⇐ t + Γ ⊢ ▹ ⦇⦈ ◃ ~ construct (var x) ~> ⦇ ▹ X x ◃ ⦈ ⇐ t AAConLam1 : {Γ : ·ctx} {x : Nat} {t t1 t2 : τ̇} → (x # Γ) → (t ▸arr (t1 ==> t2)) → - Γ ⊢ ▹ <||> ◃ ~ construct (lam x) ~> - ·λ x (▹ <||> ◃) ⇐ t + Γ ⊢ ▹ ⦇⦈ ◃ ~ construct (lam x) ~> + ·λ x (▹ ⦇⦈ ◃) ⇐ t AAConLam2 : {Γ : ·ctx} {x : Nat} {t : τ̇} → (x # Γ) → - (t ~̸ (<||> ==> <||>)) → - Γ ⊢ ▹ <||> ◃ ~ construct (lam x) ~> - <| ·λ x <||> ·:₂ (▹ <||> ◃ ==>₁ <||>) |> ⇐ t + (t ~̸ (⦇⦈ ==> ⦇⦈)) → + Γ ⊢ ▹ ⦇⦈ ◃ ~ construct (lam x) ~> + ⦇ ·λ x ⦇⦈ ·:₂ (▹ ⦇⦈ ◃ ==>₁ ⦇⦈) ⦈ ⇐ t AAConNumlit : {Γ : ·ctx} {t : τ̇} {n : Nat} → (t ~̸ num) → - Γ ⊢ ▹ <||> ◃ ~ construct (numlit n) ~> <| ▹ (N n) ◃ |> ⇐ t + Γ ⊢ ▹ ⦇⦈ ◃ ~ construct (numlit n) ~> ⦇ ▹ (N n) ◃ ⦈ ⇐ t AAFinish : {Γ : ·ctx} {e : ė} {t : τ̇} → (Γ ⊢ e <= t) → - Γ ⊢ ▹ <| e |> ◃ ~ finish ~> ▹ e ◃ ⇐ t + Γ ⊢ ▹ ⦇ e ⦈ ◃ ~ finish ~> ▹ e ◃ ⇐ t AAZipLam : {Γ : ·ctx} {x : Nat} {t t1 t2 : τ̇} {e e' : ê} {α : action} → x # Γ → (t ▸arr (t1 ==> t2)) → diff --git a/examples.agda b/examples.agda index c9f1f71..5b7f7db 100644 --- a/examples.agda +++ b/examples.agda @@ -39,7 +39,7 @@ module examples where -- applying three to four has type hole -- but there is no action that -- can fill the hole in the type so this term is forever incomplete. - ex4 : ∅ ⊢ ((N 3) ·: <||>) ∘ (N 4) => <||> + ex4 : ∅ ⊢ ((N 3) ·: ⦇⦈) ∘ (N 4) => ⦇⦈ ex4 = SAp (SAsc (ASubsume SNum TCHole2)) MAHole (ASubsume SNum TCHole2) -- this module contains small examples that demonstrate the judgements @@ -51,12 +51,12 @@ module examples where -- have to unzip down to the point of the structure where you want to -- apply an edit, do the local edit rule, and then put it back together -- around you - talk0 : ∅ ⊢ (▹ <||> ◃ ·+₁ <||>) => num ~ construct (numlit 7) ~> - (▹ N 7 ◃ ·+₁ <||>) => num + talk0 : ∅ ⊢ (▹ ⦇⦈ ◃ ·+₁ ⦇⦈) => num ~ construct (numlit 7) ~> + (▹ N 7 ◃ ·+₁ ⦇⦈) => num talk0 = SAZipPlus1 (AASubsume EETop SEHole SAConNumlit TCRefl) - talk1 : ∅ ⊢ (·λ 0 <||> ·:₂ (▹ <||> ◃ ==>₁ <||>)) => (<||> ==> <||>) ~ construct num ~> - (·λ 0 <||> ·:₂ (▹ num ◃ ==>₁ <||>)) => (num ==> <||>) + talk1 : ∅ ⊢ (·λ 0 ⦇⦈ ·:₂ (▹ ⦇⦈ ◃ ==>₁ ⦇⦈)) => (⦇⦈ ==> ⦇⦈) ~ construct num ~> + (·λ 0 ⦇⦈ ·:₂ (▹ num ◃ ==>₁ ⦇⦈)) => (num ==> ⦇⦈) talk1 = SAZipAsc2 (TMArrZip1 TMConNum) (ETArrL ETTop) (ETArrL ETTop) (ALam refl MAArr (ASubsume SEHole TCRefl)) @@ -78,7 +78,7 @@ module examples where :: [] - figure1 : runsynth ∅ ▹ <||> ◃ <||> fig1-l (·λ 0 (X 0 ·+₂ ▹ N 1 ◃) ·:₁ (num ==> num)) (num ==> num) + figure1 : runsynth ∅ ▹ ⦇⦈ ◃ ⦇⦈ fig1-l (·λ 0 (X 0 ·+₂ ▹ N 1 ◃) ·:₁ (num ==> num)) (num ==> num) figure1 = DoSynth (SAConLam refl) (DoSynth (SAZipAsc2 (TMArrZip1 TMConNum) (ETArrL ETTop) (ETArrL ETTop) (ALam refl MAArr (ASubsume SEHole TCRefl))) @@ -113,7 +113,7 @@ module examples where :: finish :: [] - figure2 : runsynth (∅ ,, (incr , num ==> num)) ▹ <||> ◃ <||> fig2-l (X incr ∘₂ ▹ X incr ∘ (N 3) ◃) num + figure2 : runsynth (∅ ,, (incr , num ==> num)) ▹ ⦇⦈ ◃ ⦇⦈ fig2-l (X incr ∘₂ ▹ X incr ∘ (N 3) ◃) num figure2 = DoSynth (SAConVar refl) (DoSynth (SAConApArr MAArr) (DoSynth (SAZipApAna MAArr (SVar refl) (AAConVar (λ ()) refl)) @@ -141,7 +141,7 @@ module examples where :: move parent :: [] - figure2alt : runsynth (∅ ,, (incr , num ==> num)) ▹ <||> ◃ <||> fig2alt-l (X incr ∘₂ ▹ X incr ∘ (N 3) ◃) num + figure2alt : runsynth (∅ ,, (incr , num ==> num)) ▹ ⦇⦈ ◃ ⦇⦈ fig2alt-l (X incr ∘₂ ▹ X incr ∘ (N 3) ◃) num figure2alt = DoSynth (SAConVar refl) (DoSynth (SAConApArr MAArr) (DoSynth (SAZipApAna MAArr (SVar refl) (AASubsume EETop SEHole (SAConApArr MAHole) TCHole1)) diff --git a/judgemental-erase.agda b/judgemental-erase.agda index ef89258..2b0aa3f 100644 --- a/judgemental-erase.agda +++ b/judgemental-erase.agda @@ -40,7 +40,7 @@ module judgemental-erase where (e1 ∘₂ e2) ◆e = e1 ∘ (e2 ◆e) (e1 ·+₁ e2) ◆e = (e1 ◆e) ·+ e2 (e1 ·+₂ e2) ◆e = e1 ·+ (e2 ◆e) - <| e |> ◆e = <| e ◆e |> + ⦇ e ⦈ ◆e = ⦇ e ◆e ⦈ -- this pair of theorems moves from the judgmental form to the function form erase-t◆ : {t : τ̂} {tr : τ̇} → (erase-t t tr) → (t ◆t == tr) @@ -57,12 +57,12 @@ module judgemental-erase where erase-e◆ (EEApR p) = ap1 (λ x → _ ∘ x) (erase-e◆ p) erase-e◆ (EEPlusL p) = ap1 (λ x → x ·+ _) (erase-e◆ p) erase-e◆ (EEPlusR p) = ap1 (λ x → _ ·+ x) (erase-e◆ p) - erase-e◆ (EENEHole p) = ap1 (λ x → <| x |>) (erase-e◆ p) + erase-e◆ (EENEHole p) = ap1 (λ x → ⦇ x ⦈) (erase-e◆ p) -- this pair of theorems moves back from judgmental form to the function form ◆erase-t : (t : τ̂) (tr : τ̇) → (t ◆t == tr) → (erase-t t tr) ◆erase-t ▹ .num ◃ num refl = ETTop - ◆erase-t ▹ .<||> ◃ <||> refl = ETTop + ◆erase-t ▹ .⦇⦈ ◃ ⦇⦈ refl = ETTop ◆erase-t ▹ .(tr ==> tr₁) ◃ (tr ==> tr₁) refl = ETTop ◆erase-t (t ==>₁ x) (.(t ◆t) ==> .x) refl = ETArrL (◆erase-t t (t ◆t) refl) ◆erase-t (x ==>₂ t) (.x ==> .(t ◆t)) refl = ETArrR (◆erase-t t (t ◆t) refl) @@ -76,7 +76,7 @@ module judgemental-erase where ◆erase-e (x ∘₂ e) .(x ∘ (e ◆e)) refl = EEApR (◆erase-e e (e ◆e) refl) ◆erase-e (e ·+₁ x) .((e ◆e) ·+ x) refl = EEPlusL (◆erase-e e (e ◆e) refl) ◆erase-e (x ·+₂ e) .(x ·+ (e ◆e)) refl = EEPlusR (◆erase-e e (e ◆e) refl) - ◆erase-e <| e |> .(<| e ◆e |>) refl = EENEHole (◆erase-e e (e ◆e) refl) + ◆erase-e ⦇ e ⦈ .(⦇ e ◆e ⦈) refl = EENEHole (◆erase-e e (e ◆e) refl) -- taken together, these two theorems demonstrate that the round-trip of -- one of the pairings above is stable. as a consequence of the @@ -84,7 +84,7 @@ module judgemental-erase where -- sufficient to show that the whole thing is an isomorphism. erase-trt : (t : τ̂) (tr : τ̇) → (x : t ◆t == tr) → (erase-t◆ (◆erase-t t tr x)) == x erase-trt ▹ .num ◃ num refl = refl - erase-trt ▹ .<||> ◃ <||> refl = refl + erase-trt ▹ .⦇⦈ ◃ ⦇⦈ refl = refl erase-trt ▹ .(tr ==> tr₁) ◃ (tr ==> tr₁) refl = refl erase-trt (t ==>₁ x) (.(t ◆t) ==> .x) refl = ap1 (λ a → ap1 (λ x₁ → x₁ ==> x) a) (erase-trt t _ refl) erase-trt (x ==>₂ t) (.x ==> .(t ◆t)) refl = ap1 (λ a → ap1 (_==>_ x) a) (erase-trt t _ refl) @@ -98,7 +98,7 @@ module judgemental-erase where erase-ert (x ∘₂ e) .(x ∘ (e ◆e)) refl = ap1 (λ a → ap1 (_∘_ x) a) (erase-ert e _ refl) erase-ert (e ·+₁ x) .((e ◆e) ·+ x) refl = ap1 (λ a → ap1 (λ x₁ → x₁ ·+ x) a) (erase-ert e _ refl) erase-ert (x ·+₂ e) .(x ·+ (e ◆e)) refl = ap1 (λ a → ap1 (_·+_ x) a) (erase-ert e _ refl) - erase-ert <| e |> .(<| e ◆e |>) refl = ap1 (λ a → ap1 <|_|> a) (erase-ert e _ refl) + erase-ert ⦇ e ⦈ .(⦇ e ◆e ⦈) refl = ap1 (λ a → ap1 ⦇_⦈ a) (erase-ert e _ refl) -- this isomorphism amounts to the argument that the judgement has mode -- (∀, !∃), where uniqueness comes from erase-e◆. @@ -135,7 +135,7 @@ module judgemental-erase where erasee-det e1 e2 with erase-e◆ e1 ... | refl = erase-e◆ e2 - erase-in-hole : ∀ {e e'} → erase-e e e' → erase-e <| e |> <| e' |> + erase-in-hole : ∀ {e e'} → erase-e e e' → erase-e ⦇ e ⦈ ⦇ e' ⦈ erase-in-hole (EENEHole er) = EENEHole (erase-in-hole er) erase-in-hole x = EENEHole x diff --git a/judgemental-inconsistency.agda b/judgemental-inconsistency.agda index 97506b3..7f16da1 100644 --- a/judgemental-inconsistency.agda +++ b/judgemental-inconsistency.agda @@ -53,11 +53,11 @@ module judgemental-inconsistency where ... | Inr qq = ICArr2 (from~̸ _ _ qq) -- the remaining consistent types all lead to absurdities from~̸ num num ncon = abort (ncon TCRefl) - from~̸ num <||> ncon = abort (ncon TCHole1) - from~̸ <||> num ncon = abort (ncon TCHole2) - from~̸ <||> <||> ncon = abort (ncon TCRefl) - from~̸ <||> (t2 ==> t3) ncon = abort (ncon TCHole2) - from~̸ (t1 ==> t2) <||> ncon = abort (ncon TCHole1) + from~̸ num ⦇⦈ ncon = abort (ncon TCHole1) + from~̸ ⦇⦈ num ncon = abort (ncon TCHole2) + from~̸ ⦇⦈ ⦇⦈ ncon = abort (ncon TCRefl) + from~̸ ⦇⦈ (t2 ==> t3) ncon = abort (ncon TCHole2) + from~̸ (t1 ==> t2) ⦇⦈ ncon = abort (ncon TCHole1) -- need to display that at least one of the round-trips above is stable -- for this to be structure preserving and really an iso. @@ -66,8 +66,8 @@ module judgemental-inconsistency where rt (t1 ==> t2) num x = funext (λ x₁ → abort (x x₁)) rt (t1 ==> t2) (t3 ==> t4) x = funext (λ x₁ → abort (x x₁)) rt num num x = abort (x TCRefl) - rt num <||> x = abort (x TCHole1) - rt <||> num x = abort (x TCHole2) - rt <||> <||> x = abort (x TCRefl) - rt <||> (t2 ==> t3) x = abort (x TCHole2) - rt (t1 ==> t2) <||> x = abort (x TCHole1) + rt num ⦇⦈ x = abort (x TCHole1) + rt ⦇⦈ num x = abort (x TCHole2) + rt ⦇⦈ ⦇⦈ x = abort (x TCRefl) + rt ⦇⦈ (t2 ==> t3) x = abort (x TCHole2) + rt (t1 ==> t2) ⦇⦈ x = abort (x TCHole1) diff --git a/keys.md b/keys.md index 4ae74ec..7d770de 100644 --- a/keys.md +++ b/keys.md @@ -10,6 +10,9 @@ This file describes how to use the emacs agda input mode to enter each of those special characters, in roughly the order that they appear in `core.agda` broken into categories that aren't quite disjoint. +http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.UnicodeInput is a +good resource for wrangling this sort of thing. + Agda built-ins or prelude-defined types ------------------------------ @@ -65,3 +68,7 @@ arrows - "▸" is `\t 5` - "◆" is `\di` + +holes +----- + - "⦇" "⦈" are `C-x 8 Z NOTATION LEFT IMAGE BRACKET` and `Z NOTATION RIGHT IMAGE BRACKET` respectively diff --git a/moveerase.agda b/moveerase.agda index 2c74f3f..3efb44a 100644 --- a/moveerase.agda +++ b/moveerase.agda @@ -79,7 +79,7 @@ module moveerase where ... | refl = ap1 (λ q → _ ∘ q) (moveerase-ana er x₁ x₄ ) , refl moveerase-synth (EEPlusL er) (SPlus x x₁) (SAZipPlus1 x₂) = ap1 (λ q → q ·+ _) (moveerase-ana er x x₂) , refl moveerase-synth (EEPlusR er) (SPlus x x₁) (SAZipPlus2 x₂) = ap1 (λ q → _ ·+ q) (moveerase-ana er x₁ x₂) , refl - moveerase-synth er wt (SAZipHole x x₁ d) = ap1 <|_|> (π1 (moveerase-synth x x₁ d)) , refl + moveerase-synth er wt (SAZipHole x x₁ d) = ap1 ⦇_⦈ (π1 (moveerase-synth x x₁ d)) , refl moveerase-ana : ∀{Γ e e' e◆ t δ } → (er : erase-e e e◆) → diff --git a/structural.agda b/structural.agda index 0c4a995..8d69aa6 100644 --- a/structural.agda +++ b/structural.agda @@ -47,8 +47,8 @@ module structural where fresh x (·λ y e) = natEQp x y × fresh x e fresh x (N n) = ⊤ fresh x (e1 ·+ e2) = fresh x e1 × fresh x e2 - fresh x <||> = ⊤ - fresh x <| e |> = fresh x e + fresh x ⦇⦈ = ⊤ + fresh x ⦇ e ⦈ = fresh x e fresh x (e1 ∘ e2) = fresh x e1 × fresh x e2 ---- lemmas