Extract Name to a new module.

3 files changed, 84 insertions, 25 deletions

diff --git a/obs.ipkg b/obs.ipkg
index 45b99c3..2de477f 100644
--- a/obs.ipkg
+++ b/obs.ipkg
@@ -10,4 +10,5 @@ executable = "cc-eval"
 main = Main
 
 modules
-  = Main
+  = CC.Name
+  , Main
diff --git a/src/CC/Name.idr b/src/CC/Name.idr
new file mode 100644
index 0000000..f1a66db
--- /dev/null
+++ b/src/CC/Name.idr
@@ -0,0 +1,67 @@
+module CC.Name
+
+import Control.Relation
+
+import Decidable.Equality
+
+import Text.Bounded
+import Text.PrettyPrint.Prettyprinter
+
+infix 4 ~~
+
+-- Definitions -----------------------------------------------------------------
+
+||| Names of variables.
+export
+Name : Type
+Name = WithBounds String
+
+%name Name n, m
+
+||| Equivalence relation on names.
+export
+(~~) : Rel Name
+m ~~ n = m.val = n.val
+
+%name (~~) prf
+
+-- Interfaces ------------------------------------------------------------------
+
+export
+Interpolation Name where
+  interpolate n = n.val
+
+export
+Pretty Name where
+  pretty n = pretty n.val
+
+export
+Reflexive Name (~~) where
+  reflexive = Refl
+
+export
+Symmetric Name (~~) where
+  symmetric prf = sym prf
+
+export
+Transitive Name (~~) where
+  transitive prf1 prf2 = trans prf1 prf2
+
+export Equivalence Name (~~) where
+
+-- Operations ------------------------------------------------------------------
+
+||| Constructs a new name from a bounded String.
+export
+MkName : WithBounds String -> Name
+MkName = id
+
+||| Decides if two names are equivalent
+export
+decEquiv : (m, n : Name) -> Dec (m ~~ n)
+decEquiv m n = decEq m.val n.val
+
+||| Returns the bounds of `name`, if any.
+export
+bounds : (name : Name) -> Maybe Bounds
+bounds name = if name.isIrrelevant then Nothing else Just name.bounds
diff --git a/src/Main.idr b/src/Main.idr
index 04f9839..9f4caf8 100644
--- a/src/Main.idr
+++ b/src/Main.idr
@@ -1,5 +1,7 @@
 module Main
 
+import CC.Name
+
 import Data.DPair
 import Data.List
 import Data.Nat
@@ -17,14 +19,6 @@ import Text.Parser
 import Text.PrettyPrint.Prettyprinter
 import Text.PrettyPrint.Prettyprinter.Render.Terminal
 
-infix 4 ~~
-
-Name : Type
-Name = WithBounds String
-
-(~~) : Name -> Name -> Type
-m ~~ n = m.val = n.val
-
 Context : Type
 Context = SnocList Name
 
@@ -144,7 +138,7 @@ quote (VAbs close@(Close n _ _)) =
   Abs n $
   assert_total $
   quote $
-  app (wknClose close (Drop id)) (Ntrl $ VVar 0 n (Here Refl))
+  app (wknClose close (Drop id)) (Ntrl $ VVar 0 n $ Here $ reflexive {rel = (~~)})
 
 quoteNtrl (VVar k n prf) = Var k n prf
 quoteNtrl (VApp n v) = App (quoteNtrl n) (quote v)
@@ -181,7 +175,7 @@ Applicative NameError where
 lookup : (ctx : Context) -> (n : Name) -> NameError $ Subset Nat (\k => IsVar k n ctx)
 lookup [<] n = Err (n ::: [])
 lookup (ctx :< m) n =
-  case decEq n.val m.val of
+  case decEquiv n m of
     Yes eq => Ok (Element 0 (Here eq))
     No _ => map (\p => Element (S p.fst) (There p.snd)) (lookup ctx n)
 
@@ -296,7 +290,7 @@ parseTerm = parseLambda <|> parseLet <|> parseSpine
 parseLambda = do
   match TLambda
   commit
-  names <- sepBy1 (match TComma >> commit) (bounds $ match TIdent)
+  names <- sepBy1 (match TComma >> commit) (MkName <$> (bounds $ match TIdent))
   commit
   match TFatArrow
   commit
@@ -314,12 +308,12 @@ parseLet = do
   match TSemi
   commit
   u <- parseTerm
-  pure $ RLet n t u
+  pure $ RLet (MkName n) t u
 
 parseSpine = foldl1 RApp <$> some parseAtom
 
 parseAtom =
-  (RVar <$> (bounds $ match TIdent <* commit)) <|>
+  (RVar <$> MkName <$> (bounds $ match TIdent <* commit)) <|>
   (parens parseTerm)
 
 parseSrc : Grammar state CCToken True RawTerm
@@ -353,20 +347,17 @@ parseStdin = do
 
 --------------------------------------------------------------------------------
 
-recomputeName : {ctx : Context} -> (k : Nat) -> (0 _ : IsVar k n ctx) -> Singleton n.val
-recomputeName {ctx = _ :< n} 0 (Here eq) = rewrite eq in Val n.val
-recomputeName (S k) (There prf) = recomputeName k prf
-
 startPrec, leftAppPrec, appPrec : Prec
 startPrec = Open
 leftAppPrec = Backtick
 appPrec = App
 
-prettySingleton : Pretty a => Singleton {a} x -> Doc ann
-prettySingleton (Val x) = pretty x
+prettyVar : (ctx : Context) -> (k : Nat) -> (0 _ : IsVar k n ctx) -> Doc ann
+prettyVar (_ :< n) 0 (Here eq) = pretty n
+prettyVar (ctx :< _) (S k) (There prf) = prettyVar ctx k prf
 
 prettyTerm : {ctx : Context} -> Prec -> Term ctx -> Doc ann
-prettyTerm d (Var k _ prf) = prettySingleton $ recomputeName k prf
+prettyTerm d (Var k _ prf) = prettyVar ctx k prf
 prettyTerm d t@(Abs _ _) =
   let (names ** t) = getNames t in
   parenthesise (d > startPrec) $ group $
@@ -379,15 +370,15 @@ prettyTerm d t@(Abs _ _) =
 
   prettyNames : List Name -> Doc ann
   prettyNames [] = neutral
-  prettyNames [n] = pretty n.val
-  prettyNames (n :: ns) = pretty n.val <+> comma <+> line <+> prettyNames ns
+  prettyNames [n] = pretty n
+  prettyNames (n :: ns) = pretty n <+> comma <+> line <+> prettyNames ns
 prettyTerm d (App t u) =
   parenthesise (d >= appPrec) $ group $
   prettyTerm leftAppPrec t <++> prettyTerm appPrec u
 prettyTerm d (Let n t u) =
   parenthesise (d > startPrec) $ group $ align $
     pretty "let" <++>
-    (group $ align $ hang 2 $ pretty n.val <++> pretty "=" <+> line <+> prettyTerm startPrec t) <+>
+    (group $ align $ hang 2 $ pretty n <++> pretty "=" <+> line <+> prettyTerm startPrec t) <+>
     pretty ";" <+> line <+>
     prettyTerm startPrec u
 
@@ -425,7 +416,7 @@ mainWith getOpt getTerm = do
   putDoc (pretty nf)
   where
   putErr : Name -> IO ()
-  putErr n = putBoundErrLn (Just n.bounds) "undefined name: \{n.val}"
+  putErr n = putBoundErrLn (bounds n) "undefined name: \{n}"
 
 partial
 main : IO ()