Add the True type.

6 files changed, 65 insertions, 10 deletions

diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index bac6d04..fe00621 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -38,6 +38,8 @@ abstractSyntax ctx (Var b str) = do
     | Nothing => report b "unbound variable: \{str}"
   pure (Var b i)
 abstractSyntax ctx (Sort b s)  = pure (Sort b s)
+abstractSyntax ctx (Top b)     = pure (Top b)
+abstractSyntax ctx (Point b)   = pure (Point b)
 
 export
 abstractDefinition : Context n -> Definition -> Error (Definition n)
diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index 97a0d48..f930176 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -18,6 +18,7 @@ data NormalForm  : Nat -> Type
 public export
 data Constructor : Nat -> Type where
   Sort : Sort -> Constructor n
+  Top  : Constructor n
 
 public export
 data Neutral : Nat -> Type where
@@ -27,6 +28,7 @@ public export
 data NormalForm : Nat -> Type where
   Ntrl  : Neutral n -> NormalForm n
   Cnstr : Constructor n -> NormalForm n
+  Irrel : NormalForm n
 
 public export
 record Definition (n : Nat) where
@@ -49,11 +51,14 @@ eqNtrl  : Neutral n -> Neutral n -> Bool
 eqWhnf  : NormalForm n -> NormalForm n -> Bool
 
 eqCnstr (Sort s) (Sort s') = s == s'
+eqCnstr Top      Top       = True
+eqCnstr _ _ = False
 
 eqNtrl (Var i) (Var j) = i == j
 
 eqWhnf (Ntrl t)  (Ntrl u)  = eqNtrl t u
 eqWhnf (Cnstr t) (Cnstr u) = eqCnstr t u
+eqWhnf Irrel     Irrel     = True
 eqWhnf _ _ = False
 
 export
@@ -75,11 +80,13 @@ prettyPrecNtrl  : Prec -> Neutral n -> Doc ann
 prettyPrecWhnf  : Prec -> NormalForm n -> Doc ann
 
 prettyPrecCnstr d (Sort s) = prettyPrec d s
+prettyPrecCnstr d Top = pretty "()"
 
 prettyPrecNtrl d (Var i) = pretty "$\{show i}"
 
 prettyPrecWhnf d (Ntrl t)  = prettyPrecNtrl d t
 prettyPrecWhnf d (Cnstr t) = prettyPrecCnstr d t
+prettyPrecWhnf d Irrel     = pretty "_"
 
 export
 Pretty (Constructor n) where
@@ -114,11 +121,13 @@ renameNtrl  : Neutral n -> (Fin n -> Fin m) -> Neutral m
 renameWhnf  : NormalForm n -> (Fin n -> Fin m) -> NormalForm m
 
 renameCnstr (Sort s) f = Sort s
+renameCnstr Top      f = Top
 
 renameNtrl (Var i) f = Var (f i)
 
 renameWhnf (Ntrl t)  f = Ntrl $ renameNtrl t f
 renameWhnf (Cnstr t) f = Cnstr $ renameCnstr t f
+renameWhnf Irrel     f = Irrel
 
 export
 Rename Constructor where
@@ -139,11 +148,13 @@ substNtrl  : Neutral n -> (Fin n -> NormalForm m) -> NormalForm m
 substWhnf  : NormalForm n -> (Fin n -> NormalForm m) -> NormalForm m
 
 substCnstr (Sort s) f = Sort s
+substCnstr Top      f = Top
 
 substNtrl (Var i) f = f i
 
 substWhnf (Ntrl t)  f = substNtrl t f
 substWhnf (Cnstr t) f = Cnstr $ substCnstr t f
+substWhnf Irrel     f = Irrel
 
 export
 Subst Constructor NormalForm Constructor where
diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
index 278ff0f..2dd7052 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -23,11 +23,17 @@ data ObsTokenKind
   = OTNewline
   | OTIgnore
   | OTIdent
-  | OTSet
+  -- Keywords
   | OTProp
+  | OTSet
   | OTNat
+  -- Special symbols
+  | OTUnit
+  | OTPoint
+  -- Grouping symbols
   | OTPOpen
   | OTPClose
+  -- Definition characters
   | OTEqual
   | OTColon
 
@@ -35,9 +41,11 @@ Eq ObsTokenKind where
   OTNewline == OTNewline = True
   OTIgnore  == OTIgnore  = True
   OTIdent   == OTIdent   = True
-  OTSet     == OTSet     = True
   OTProp    == OTProp    = True
+  OTSet     == OTSet     = True
   OTNat     == OTNat     = True
+  OTUnit    == OTUnit    = True
+  OTPoint   == OTPoint   = True
   OTPOpen   == OTPOpen   = True
   OTPClose  == OTPClose  = True
   OTEqual   == OTEqual   = True
@@ -52,9 +60,11 @@ TokenKind ObsTokenKind where
   tokValue OTNewline s = ()
   tokValue OTIgnore  s = ()
   tokValue OTIdent   s = s
-  tokValue OTSet     s = ()
   tokValue OTProp    s = ()
+  tokValue OTSet     s = ()
   tokValue OTNat     s = stringToNatOrZ s
+  tokValue OTUnit    s = ()
+  tokValue OTPoint   s = ()
   tokValue OTPOpen   s = ()
   tokValue OTPClose  s = ()
   tokValue OTEqual   s = ()
@@ -84,6 +94,7 @@ obsTokenMap = toTokenMap [(newline, OTNewline), (spaces, OTIgnore)] ++
           Nothing => Tok OTIdent s)
   ] ++ toTokenMap
   [ (digits, OTNat)
+  , (exact "_", OTPoint)
   , (exact "(", OTPOpen)
   , (exact ")", OTPClose)
   , (exact "=", OTEqual)
@@ -122,13 +133,19 @@ sort = do
   sort <- prop <|> set
   pure (Sort sort.bounds sort.val)
 
+top : Grammar state ObsToken True Syntax
+top = map (\v => Top v.bounds) $ bounds $ match OTUnit
+
+point : Grammar state ObsToken True Syntax
+point = map (\v => Point v.bounds) $ bounds $ match OTPoint
+
 partial
 exp  : Grammar state ObsToken True Syntax
 partial
 term : Grammar state ObsToken True Syntax
 
 exp = term
-term = var <|> sort <|> parens exp
+term = var <|> sort <|> top <|> point <|> parens exp
 
 partial
 decl : Grammar state ObsToken True (WithBounds String, Syntax)
@@ -152,13 +169,20 @@ partial
 file : Grammar state ObsToken False (List Definition)
 file = many (match OTNewline) *> sepEndBy (some (match OTNewline)) fullDef
 
+postprocess : List (WithBounds ObsToken) -> List (WithBounds ObsToken)
+postprocess [] = []
+postprocess [tok] = if ignored tok then [] else [tok]
+postprocess (tok :: tail@(tok' :: toks)) = case (tok.val.kind, tok'.val.kind) of
+  (OTPOpen, OTPClose) => map (\_ => Tok OTUnit "()") (mergeBounds tok tok') :: postprocess toks
+  _ => if ignored tok then postprocess tail else tok :: postprocess tail
+
 partial
 export
 parse : String -> Error ObsToken (List Definition)
 parse str = do
   let (toks, _, _, "") = lex obsTokenMap str
     | (_, l, c, rem) => report (Error "failed to lex input" (Just $ MkBounds { startLine = l, startCol = c, endLine = l, endCol = c }) ::: [])
-  (defs, []) <- parse file $ filter (not . ignored) toks
+  (defs, []) <- parse file $ postprocess toks
     | (_, (t :: _)) => report (Error "unparsed tokens" (Just t.bounds) ::: [])
   pure defs
 
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index 71d070f..da2f9e4 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -11,9 +11,12 @@ import Text.PrettyPrint.Prettyprinter
 
 public export
 data Syntax : Type where
-  Var  : Bounds -> String -> Syntax
+  Var   : Bounds -> String -> Syntax
   -- Sorts
-  Sort : Bounds -> Sort -> Syntax
+  Sort  : Bounds -> Sort -> Syntax
+  -- True
+  Top   : Bounds -> Syntax
+  Point : Bounds -> Syntax
 
 public export
 record Definition where
@@ -28,6 +31,8 @@ record Definition where
 fullBounds : Syntax -> Bounds
 fullBounds (Var x str) = x
 fullBounds (Sort x s)  = x
+fullBounds (Top x)     = x
+fullBounds (Point x)   = x
 
 -- Pretty Print ----------------------------------------------------------------
 
@@ -35,6 +40,8 @@ export
 Pretty Syntax where
   prettyPrec d (Var x str) = pretty str
   prettyPrec d (Sort x s)  = prettyPrec d s
+  prettyPrec d (Top x)     = pretty "()"
+  prettyPrec d (Point x)   = pretty "_"
 
 export
 Pretty Definition where
diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index d5213d2..2cc2f93 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -12,9 +12,12 @@ import Text.PrettyPrint.Prettyprinter
 
 public export
 data Term : Nat -> Type where
-  Var  : Bounds -> Fin n -> Term n
+  Var   : Bounds -> Fin n -> Term n
   -- Sorts
-  Sort : Bounds -> Sort -> Term n
+  Sort  : Bounds -> Sort -> Term n
+  -- True
+  Top   : Bounds -> Term n
+  Point : Bounds -> Term n
 
 public export
 record Definition (n : Nat) where
@@ -35,6 +38,8 @@ export
 fullBounds : Term n -> Bounds
 fullBounds (Var x i)  = x
 fullBounds (Sort x s) = x
+fullBounds (Top x)     = x
+fullBounds (Point x)   = x
 
 -- Pretty Print ----------------------------------------------------------------
 
@@ -42,6 +47,8 @@ export
 Pretty (Term n) where
   prettyPrec d (Var x i)  = pretty "$\{show i}"
   prettyPrec d (Sort x s) = prettyPrec d s
+  prettyPrec d (Top x)    = pretty "()"
+  prettyPrec d (Point x)  = pretty "_"
 
 export
 Pretty (Definition n) where
diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr
index 95ffc19..22994ec 100644
--- a/src/Obs/Typing.idr
+++ b/src/Obs/Typing.idr
@@ -20,11 +20,13 @@ import Text.PrettyPrint.Prettyprinter.Render.Terminal
 -- invariant: all definitions fully expanded
 -- invariant: m |- t, u <- a : s
 convert : (t, u, a : NormalForm n) -> Sort -> Bool
-convert t u a Prop = True
+convert Irrel Irrel a Prop = True
 convert t u (Ntrl _) (Set k) = t == u
+convert (Cnstr Top) (Cnstr Top) (Cnstr (Sort Prop)) (Set 0) = True
 convert (Ntrl t) u (Cnstr (Sort s)) (Set k) = Ntrl t == u
 convert t (Ntrl u) (Cnstr (Sort s)) (Set k) = t == Ntrl u
 convert (Cnstr (Sort s')) (Cnstr (Sort s'')) (Cnstr (Sort s)) (Set k) = s' == s''
+convert _ _ _ _ = False
 
 -- Typing Contexts -------------------------------------------------------------
 
@@ -71,6 +73,8 @@ check ctx tm ty s = do
 
 infer ctx (Var b i) = pure $ index ctx i
 infer ctx (Sort b s) = pure $ (Cnstr (Sort s), Cnstr (Sort (suc s)), suc (suc s))
+infer ctx (Top b) = pure $ (Cnstr Top, Cnstr (Sort Prop), Set 0)
+infer ctx (Point b) = pure $ (Irrel, Cnstr Top, Prop)
 
 -- Checking Definitions and Blocks ---------------------------------------------