remove language notation as a separate file

Katydid.lean

@@ -11,6 +11,5 @@ import Katydid.Expr.Desc
 import Katydid.Expr.Regex
 
 import Katydid.Conal.Language
-import Katydid.Conal.LanguageNotation
 import Katydid.Conal.Calculus
 import Katydid.Conal.Examples

Katydid/Conal/Calculus.lean

@@ -1,7 +1,7 @@
 -- A translation to Lean from Agda
 -- https://github.com/conal/paper-2021-language-derivatives/blob/main/Calculus.lagda
 
-import Katydid.Conal.LanguageNotation
+import Katydid.Conal.Language
 import Mathlib.Logic.Equiv.Defs -- ≃
 import Katydid.Std.Tipe
 open dLang
@@ -27,7 +27,7 @@ def example_of_proof_relevant_parse : (char 'a' ⋃ char 'b') (toList "a") -> Na
     | mk eq =>
       contradiction
 
-def example_of_proof_relevant_parse2 : (char 'a', (char 'b' ⋃ char 'c')) (toList "ab") -> Nat := by
+def example_of_proof_relevant_parse2 : (concat (char 'a') (char 'b' ⋃ char 'c')) (toList "ab") -> Nat := by
   intro x1
   simp at x1
   cases x1 with
@@ -178,7 +178,7 @@ def nullable_scalar:
 --   (λ { (([] , []) , refl , νP , νQ) → refl})
 def nullable_concat:
   ∀ (P Q: dLang α),
-    ν' (P, Q) ≃ (Prod (ν' Q) (ν' P)) := by
+    ν' (concat P Q) ≃ (Prod (ν' Q) (ν' P)) := by
   -- TODO
   sorry
 
@@ -301,7 +301,7 @@ def derivative_scalar:
 def derivative_concat:
   ∀ (a: α) (P Q: dLang α),
   -- TODO: Redo this definition to do extensional isomorphism: `⟷` properly
-    (δ' (P , Q) a) ≡ dLang.scalar (ν' P) ((δ' Q a) ⋃ ((δ' P a), Q)) := by
+    (δ' (concat P Q) a) ≡ dLang.scalar (ν' P) ((δ' Q a) ⋃ (concat (δ' P a) Q)) := by
   -- TODO
   sorry
 
@@ -341,6 +341,6 @@ def derivative_concat:
 def derivative_star:
   ∀ (a: α) (P: dLang α),
   -- TODO: Redo this definition to do extensional isomorphism: `⟷` properly
-    (δ' (P *) a) ≡ dLang.scalar (List (ν' P)) (δ' P a, P *) := by
+    (δ' (P *) a) ≡ dLang.scalar (List (ν' P)) (concat (δ' P a) (P *)) := by
   -- TODO
   sorry

Katydid/Conal/Examples.lean

@@ -1,7 +1,7 @@
 -- A translation to Lean from Agda
 -- https://github.com/conal/paper-2021-language-derivatives/blob/main/Examples.lagda
 
-import Katydid.Conal.LanguageNotation
+import Katydid.Conal.Language
 open dLang
 
 example: (dLang.char 'a') ['a'] := by
@@ -27,25 +27,25 @@ example : (char 'a' ⋃ char 'b') (String.toList "b") := by
 
 -- _ : a⋆b ('a' ∷ 'b' ∷ [])
 -- _ = ([ 'a' ] , [ 'b' ]) , refl , refl , refl
-example : (char 'a', char 'b') (String.toList "ab") := by
+example : (concat (char 'a') (char 'b')) (String.toList "ab") := by
   simp
   exists ['a']
   exists ['b']
   exists trfl
   exists trfl
 
-example : (char 'a', char 'b') (String.toList "ab") := by
+example : (concat (char 'a') (char 'b')) (String.toList "ab") := by
   simp
   refine PSigma.mk ['a'] ?a
   refine PSigma.mk ['b'] ?b
   refine PSigma.mk trfl ?c
   refine PSigma.mk trfl ?d
   rfl
 
-example : (char 'a', char 'b') (String.toList "ab") :=
+example : (concat (char 'a') (char 'b')) (String.toList "ab") :=
   PSigma.mk ['a'] (PSigma.mk ['b'] (PSigma.mk trfl (PSigma.mk trfl rfl)))
 
-example : (char 'a', char 'b') (String.toList "ab") :=
+example : (concat (char 'a') (char 'b')) (String.toList "ab") :=
   PSigma.mk ['a'] (PSigma.mk ['b'] (PSigma.mk trfl (PSigma.mk trfl rfl)))
 
 example : ((char 'a')*) (String.toList "a") := by sorry

Katydid/Conal/Language.lean

@@ -30,18 +30,25 @@ def emptySet : dLang α :=
   -- PEmpty is a Sort, which works for both Prop and Type
   fun _ => PEmpty
 
+-- `(priority := high)` is required to avoid the error: "ambiguous, possible interpretations"
+notation (priority := high) "∅" => dLang.emptySet -- backslash emptyset
+
 -- 𝒰 : Lang
 -- 𝒰 w = ⊤
 def universal : dLang α :=
   -- PUnit is Empty, but allows specifying the universe
   -- PUnit is a Sort, which works for both Prop and Type
   fun _ => PUnit
 
+notation "𝒰" => dLang.universal -- backslash McU
+
 -- 𝟏 : Lang
 -- 𝟏 w = w ≡ []
 def emptyStr : dLang α :=
   fun w => w ≡ []
 
+notation "ε" => dLang.emptyStr -- backslash epsilon
+
 -- ` : A → Lang
 -- ` c w = w ≡ [ c ]
 def char (a : α): dLang α :=
@@ -53,18 +60,24 @@ def char (a : α): dLang α :=
 def scalar (s : Type u) (P : dLang α) : dLang α :=
   fun w => s × P w
 
+infixl:4 " · " => dLang.scalar -- backslash .
+
 -- infixr 6 _∪_
 -- _∪_ : Op₂ Lang
 -- (P ∪ Q) w = P w ⊎ Q w
 def or (P : dLang α) (Q : dLang α) : dLang α :=
   fun w => P w ⊕ Q w
 
+infixl:5 (priority := high) " ⋃ " => dLang.or -- backslash U
+
 -- infixr 6 _∩_
 -- _∩_ : Op₂ Lang
 -- (P ∩ Q) w = P w × Q w
 def and (P : dLang α) (Q : dLang α) : dLang α :=
   fun w => P w × Q w
 
+infixl:4 " ⋂ " => dLang.and -- backslash I
+
 -- infixl 7 _⋆_
 -- _⋆_ : Op₂ Lang
 -- (P ⋆ Q) w = ∃⇃ λ (u ,  v) → (w ≡ u ⊙ v) × P u × Q v
@@ -83,6 +96,8 @@ def star (P : dLang α) : dLang α :=
   fun (w : List α) =>
     Σ' (ws : List (List α)), (_pws: All P ws) ×' w = (List.join ws)
 
+postfix:6 "*" => dLang.star
+
 -- TODO: What does proof relevance even mean for the `not` operator?
 def not (P: dLang α) : dLang α :=
   fun (w: List α) =>
@@ -91,6 +106,20 @@ def not (P: dLang α) : dLang α :=
 -- attribute [simp] allows these definitions to be unfolded when using the simp tactic.
 attribute [simp] universal emptySet emptyStr char scalar or and concat star
 
+example: dLang α := 𝒰
+example: dLang α := ε
+example: dLang α := (ε ⋃ 𝒰)
+example: dLang α := (ε ⋂ 𝒰)
+example: dLang α := ∅
+example: dLang α := (∅*)
+example: dLang Char := char 'a'
+example: dLang Char := char 'b'
+example: dLang Char := (char 'a' ⋂ ∅)
+example: dLang Char := (char 'a' ⋂ char 'b')
+example: dLang Nat := (char 1 ⋂ char 2)
+example: (_t: Type) -> dLang Nat := (PUnit · char 2)
+example: dLang Nat := (concat (char 1) (char 2))
+
 -- 𝜈 :(A✶ → B) → B -- “nullable”
 -- 𝜈 f = f []
 -- nullable