diff options
Diffstat (limited to 'src/Main.idr')
| -rw-r--r-- | src/Main.idr | 39 |
1 files changed, 15 insertions, 24 deletions
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 () |