Improve parsing.

1 files changed, 99 insertions, 116 deletions

diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index 578bf83..446fdcb 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -12,147 +12,130 @@ import Text.PrettyPrint.Prettyprinter
 
 public export
 data Term : Nat -> Type where
-  Var    : WithBounds String -> Fin n -> Term n
+  Var    : String -> Fin n -> Term n
   -- Sorts
-  Sort   : Bounds -> Sort -> Term n
+  Sort   : Sort -> Term n
   -- Dependent Product
-  Pi     : Bounds -> String -> Term n -> Term (S n) -> Term n
-  Lambda : Bounds -> String -> Term (S n) -> Term n
-  App    : Term n -> Term n -> Term n
+  Pi     : WithBounds String -> WithBounds (Term n) -> WithBounds (Term (S n)) -> Term n
+  Lambda : WithBounds String -> WithBounds (Term (S n)) -> Term n
+  App    : WithBounds (Term n) -> WithBounds (Term n) -> Term n
   -- Dependent Sums
-  Sigma  : Bounds -> String -> Term n -> Term (S n) -> Term n
-  Pair   : Bounds -> Term n -> Term n -> Term n
-  Fst    : Bounds -> Term n -> Term n
-  Snd    : Bounds -> Term n -> Term n
+  Sigma  : WithBounds String -> WithBounds (Term n) -> WithBounds (Term (S n)) -> Term n
+  Pair   : WithBounds (Term n) -> WithBounds (Term n) -> Term n
+  Fst    : WithBounds (Term n) -> Term n
+  Snd    : WithBounds (Term n) -> Term n
   -- True
-  Top    : Bounds -> Term n
-  Point  : Bounds -> Term n
+  Top    : Term n
+  Point  : Term n
   -- False
-  Bottom : Bounds -> Term n
-  Absurd : Bounds -> Term n -> Term n -> Term n
+  Bottom : Term n
+  Absurd : WithBounds (Term n) -> WithBounds (Term n) -> Term n
   -- Equality
-  Equal  : Bounds -> Term n -> Term n -> Term n
-  Refl   : Bounds -> Term n -> Term n
-  Transp : Bounds -> Term n -> Term n -> Term n -> Term n -> Term n -> Term n
-  Cast   : Bounds -> Term n -> Term n -> Term n -> Term n
-  CastId : Bounds -> Term n -> Term n
+  Equal  : WithBounds (Term n) -> WithBounds (Term n) -> Term n
+  Refl   : WithBounds (Term n) -> Term n
+  Transp : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n
+  Cast   : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n
+  CastId : WithBounds (Term n) -> Term n
 
 public export
 record Definition (n : Nat) where
   constructor MkDefinition
-  bounds : Bounds -- of the name
-  name   : String
-  ty     : Term n
-  tm     : Term n
+  name   : WithBounds String
+  ty     : WithBounds (Term n)
+  tm     : WithBounds (Term n)
 
 public export
 data Block : Nat -> Type where
   Nil  : Block 0
   (:<) : Block n -> Definition n -> Block (S n)
 
--- Operations ------------------------------------------------------------------
+-- Pretty Print ----------------------------------------------------------------
 
-export
-fullBounds : Term n -> WithBounds (Term n)
-fullBounds tm@(Var var i) = map (\_ => tm) var
-fullBounds tm@(Sort x s) = MkBounded tm False x
-fullBounds tm@(Pi x var a b) = mergeBounds (mergeBounds (fullBounds a) (fullBounds b)) (MkBounded tm False x)
-fullBounds tm@(Lambda x var t) = mergeBounds (fullBounds t) (MkBounded tm False x)
-fullBounds tm@(App t u) = map (\_ => tm) (mergeBounds (fullBounds t) (fullBounds u))
-fullBounds tm@(Sigma x var a b) = mergeBounds (mergeBounds (fullBounds a) (fullBounds b)) (MkBounded tm False x)
-fullBounds tm@(Pair x t u) = mergeBounds (mergeBounds (fullBounds t) (fullBounds u)) (MkBounded tm False x)
-fullBounds tm@(Fst x t) = mergeBounds (fullBounds t) (MkBounded tm False x)
-fullBounds tm@(Snd x t) = mergeBounds (fullBounds t) (MkBounded tm False x)
-fullBounds tm@(Top x) = MkBounded tm False x
-fullBounds tm@(Point x) = MkBounded tm False x
-fullBounds tm@(Bottom x) = MkBounded tm False x
-fullBounds tm@(Absurd x a t) = mergeBounds (mergeBounds (fullBounds a) (fullBounds t)) (MkBounded tm False x)
-fullBounds tm@(Equal x t u) = mergeBounds (mergeBounds (fullBounds t) (fullBounds u)) (MkBounded tm False x)
-fullBounds tm@(Refl x t) = mergeBounds (fullBounds t) (MkBounded tm False x)
-fullBounds tm@(Transp x t b u t' e) = mergeBounds (mergeBounds (mergeBounds (fullBounds t) (fullBounds b)) (mergeBounds (fullBounds u) (fullBounds t'))) (mergeBounds (fullBounds e) (MkBounded tm False x))
-fullBounds tm@(Cast x b e t) = mergeBounds (mergeBounds (fullBounds b) (fullBounds e)) (mergeBounds (fullBounds t) (MkBounded tm False x))
-fullBounds tm@(CastId x t) = mergeBounds (fullBounds t) (MkBounded tm False x)
+prettyPrec : Prec -> Term n -> Doc ann
+prettyPrecBounds : Prec -> WithBounds (Term n) -> Doc ann
 
--- Pretty Print ----------------------------------------------------------------
+prettyPrec d (Var var _) = pretty var
+prettyPrec d (Sort s) = prettyPrec d s
+prettyPrec d (Pi var a b) =
+  parenthesise (d > Open) $
+  group $
+  parens (pretty var.val <++> colon <+> softline <+> prettyPrecBounds Open a) <++>
+  pretty "->" <+> softline <+>
+  prettyPrecBounds Open b
+prettyPrec d (Lambda var t) =
+  parenthesise (d > Open) $
+  group $
+  backslash <+> pretty var.val <++>
+  pretty "=>" <+> softline <+>
+  prettyPrecBounds Open t
+prettyPrec d (App t u) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [prettyPrecBounds Open t, prettyPrecBounds App u]
+prettyPrec d (Sigma var a b) =
+  parenthesise (d >= App) $
+  group $
+  parens (pretty var.val <++> colon <+> softline <+> prettyPrecBounds Open a) <++>
+  pretty "**" <+> softline <+>
+  prettyPrecBounds Open b
+prettyPrec d (Pair t u) =
+  angles $
+  group $
+  neutral <++> prettyPrecBounds Open t <+> comma <+> softline <+> prettyPrecBounds Open u <++> neutral
+prettyPrec d (Fst t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "fst", prettyPrecBounds App t]
+prettyPrec d (Snd t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "snd", prettyPrecBounds App t]
+prettyPrec d Top = pretty "()"
+prettyPrec d Point = pretty "tt"
+prettyPrec d Bottom = pretty "Void"
+prettyPrec d (Absurd a t) =
+  parenthesise (d > Open) $
+  group $
+  fillSep [pretty "absurd", prettyPrecBounds App a, prettyPrecBounds App t]
+prettyPrec d (Equal t u) =
+  parenthesise (d >= Equal) $
+  group $
+  prettyPrecBounds Equal t <++> pretty "~" <+> softline <+> prettyPrecBounds Equal u
+prettyPrec d (Refl t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "refl", prettyPrecBounds App t]
+prettyPrec d (Transp t b u t' e) =
+  parenthesise (d >= App) $
+  group $
+  fillSep $
+  [ pretty "transp"
+  , prettyPrecBounds App t
+  , prettyPrecBounds App b
+  , prettyPrecBounds App u
+  , prettyPrecBounds App t'
+  , prettyPrecBounds App e
+  ]
+prettyPrec d (Cast b e t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "cast", prettyPrecBounds App b, prettyPrecBounds App e, prettyPrecBounds App t]
+prettyPrec d (CastId t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "castRefl", prettyPrecBounds App t]
+
+prettyPrecBounds d (MkBounded v _ _) = prettyPrec d v
 
 export
 Pretty (Term n) where
-  prettyPrec d (Var var _) = pretty var.val
-  prettyPrec d (Sort _ s) = prettyPrec d s
-  prettyPrec d (Pi _ var a b) =
-    parenthesise (d > Open) $
-    group $
-    parens (pretty var <++> colon <+> softline <+> prettyPrec Open a) <++>
-    pretty "->" <+> softline <+>
-    prettyPrec Open b
-  prettyPrec d (Lambda _ var t) =
-    parenthesise (d > Open) $
-    group $
-    backslash <+> pretty var <++>
-    pretty "=>" <+> softline <+>
-    prettyPrec Open t
-  prettyPrec d (App t u) =
-    parenthesise (d >= App) $
-    group $
-    fillSep [prettyPrec Open t, prettyPrec App u]
-  prettyPrec d (Sigma _ var a b) =
-    parenthesise (d >= App) $
-    group $
-    parens (pretty var <++> colon <+> softline <+> prettyPrec Open a) <++>
-    pretty "**" <+> softline <+>
-    prettyPrec Open b
-  prettyPrec d (Pair _ t u) =
-    angles $
-    group $
-    neutral <++> prettyPrec Open t <+> comma <+> softline <+> prettyPrec Open u <++> neutral
-  prettyPrec d (Fst _ t) =
-    parenthesise (d >= App) $
-    group $
-    fillSep [pretty "fst", prettyPrec App t]
-  prettyPrec d (Snd _ t) =
-    parenthesise (d >= App) $
-    group $
-    fillSep [pretty "snd", prettyPrec App t]
-  prettyPrec d (Top _) = pretty "()"
-  prettyPrec d (Point _) = pretty "tt"
-  prettyPrec d (Bottom _) = pretty "Void"
-  prettyPrec d (Absurd _ a t) =
-    parenthesise (d > Open) $
-    group $
-    fillSep [pretty "absurd", prettyPrec App a, prettyPrec App t]
-  prettyPrec d (Equal _ t u) =
-    parenthesise (d >= Equal) $
-    group $
-    prettyPrec Equal t <++> pretty "~" <+> softline <+> prettyPrec Equal u
-  prettyPrec d (Refl _ t) =
-    parenthesise (d >= App) $
-    group $
-    fillSep [pretty "refl", prettyPrec App t]
-  prettyPrec d (Transp _ t b u t' e) =
-    parenthesise (d >= App) $
-    group $
-    fillSep $
-    [ pretty "transp"
-    , prettyPrec App t
-    , prettyPrec App b
-    , prettyPrec App u
-    , prettyPrec App t'
-    , prettyPrec App e
-    ]
-  prettyPrec d (Cast _ b e t) =
-    parenthesise (d >= App) $
-    group $
-    fillSep [pretty "cast", prettyPrec App b, prettyPrec App e, prettyPrec App t]
-  prettyPrec d (CastId _ t) =
-    parenthesise (d >= App) $
-    group $
-    fillSep [pretty "castRefl", prettyPrec App t]
+  prettyPrec = Term.prettyPrec
 
 export
 Pretty (Definition n) where
   pretty def = group $
-    pretty def.name <++> colon <+> softline <+> pretty def.ty <+> hardline <+>
-    pretty def.name <++> equals <+> softline <+> pretty def.tm
+    pretty def.name.val <++> colon <+> softline <+> pretty def.ty.val <+> hardline <+>
+    pretty def.name.val <++> equals <+> softline <+> pretty def.tm.val
 
 export
 Pretty (Block n) where