[ new ] module specialised to 0ℓ (#27)

examples/Base.agda

@@ -31,6 +31,7 @@ open import Relation.Binary.PropositionalEquality.Decidable public
 open import Induction.Nat.Strong hiding (<-lower ; ≤-lower) public
 
 open import Data.Subset public
+open import Data.Singleton public
 
 open import Text.Parser.Types.Core                public
 open import Text.Parser.Types                     public
@@ -43,10 +44,6 @@ open import Text.Parser.Monad.Result hiding (map) public
 
 open Agdarsec′ public
 
-infix 0 _!
-data Singleton {a} {A : Set a} : A → Set a where
-  _! : (a : A) → Singleton a
-
 record Tokenizer (A : Set≤ l) : Set (level (level≤ A)) where
   constructor mkTokenizer
   field tokenize : List.List Char → List.List (theSet A)

examples/SExp.agda

@@ -1,5 +1,3 @@
-{-# OPTIONS --guardedness #-}
-
 module SExp where
 
 open import Level using (0ℓ)
@@ -19,17 +17,16 @@ open import Data.Product
 open import Data.Subset
 open import Function.Base
 open import Induction.Nat.Strong
-open import Relation.Unary using (IUniversal ; _⇒_)
 open import Relation.Binary.PropositionalEquality.Decidable
 
-open import Text.Parser 0ℓ
+open import Text.Parser
 
 module _ where
 
-  sexp : ∀[ Parser [ SExp ] ]
+  sexp : ∀[ Parser SExp ]
   sexp =
     -- SExp is an inductive type so we build the parser as a fixpoint
-    fix (Parser [ SExp ]) $ λ rec →
+    fix (Parser SExp) $ λ rec →
         -- First we have atoms. Assuming we have already consumed the leading space, an
         -- atom is just a non empty list of alphabetical characters.
 
@@ -49,7 +46,7 @@ module _ where
         -- I give a bit more details about `lift` and `box` below.
         -- As for the previous case we use `<$>` to massage the result into a `SExp`.
         sexp = (λ (a , mb) → maybe (Pair a) a mb)
-               <$> parens (lift2 (λ p q → (spaces ?&> p <&? box spaces) <&?> box (q <&? box spaces))
+               <$> parens (lift2 (λ p q → withSpaces p <&?> box (q <&? box spaces))
                                  rec
                                  rec)
      in
@@ -71,11 +68,9 @@ module _ where
 
 
   -- The full parser is obtained by disregarding spaces before & after the expression
-  SEXP : ∀[ Parser [ SExp ] ]
+  SEXP : ∀[ Parser SExp ]
   SEXP = spaces ?&> sexp <&? box spaces
 
-open import Base Level.zero
-
 -- And we can run the thing on a test (which is very convenient when refactoring grammars!..):
 _ : "((  this    is)
       ((a (  pair based))

src/Data/Singleton.agda

@@ -0,0 +1,30 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Singleton where
+
+open import Level using (Level; levelOfType)
+open import Data.Empty.Polymorphic using (⊥)
+open import Data.Maybe.Base using (Maybe; nothing; just)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+
+private
+  variable
+    a b : Level
+    A : Set a
+    B : Set b
+
+infix 0 _!
+data Singleton {A : Set a} : A → Set a where
+  _! : (a : A) → Singleton a
+
+fromJust : Maybe A → Set (levelOfType A)
+fromJust (just a) = Singleton a
+fromJust nothing  = ⊥
+
+fromInj₁ : A ⊎ B → Set (levelOfType A)
+fromInj₁ (inj₁ a) = Singleton a
+fromInj₁ (inj₂ _) = ⊥
+
+fromInj₂ : A ⊎ B → Set (levelOfType B)
+fromInj₂ (inj₁ _) = ⊥
+fromInj₂ (inj₂ b) = Singleton b