Annotate and colour pairs and () properly

Now, the delaborator remembers if a particular unit or pair is the type or the constructor, and colours them accordingly.
jljox · Feb 4, 2014 · e80f871 · e80f871
1 parent ef16e5a
commit e80f871
Show file tree

Hide file tree

Showing 9 changed files with 105 additions and 69 deletions.
diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs
@@ -848,7 +848,7 @@ expandParams dec ps ns infs tm = en tm
     en (PEq f l r) = PEq f (en l) (en r)
     en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
     en (PTyped l r) = PTyped (en l) (en r)
-    en (PPair f l r) = PPair f (en l) (en r)
+    en (PPair f p l r) = PPair f p (en l) (en r)
     en (PDPair f l t r) = PDPair f (en l) (en t) (en r)
     en (PAlternative a as) = PAlternative a (map en as)
     en (PHidden t) = PHidden (en t)
@@ -942,7 +942,7 @@ expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
 
     bnames (PRef _ n) = [n]
     bnames (PApp _ _ args) = concatMap bnames (map getTm args)
-    bnames (PPair _ l r) = bnames l ++ bnames r
+    bnames (PPair _ _ l r) = bnames l ++ bnames r
     bnames (PDPair _ l Placeholder r) = bnames l ++ bnames r
     bnames _ = []
 
@@ -998,7 +998,7 @@ getPriority i tm = 1 -- pri tm
             ((P Ref _ _):_) -> 1
             [] -> 0 -- must be locally bound, if it's not an error...
     pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))
-    pri (PTrue _) = 0
+    pri (PTrue _ _) = 0
     pri (PFalse _) = 0
     pri (PRefl _ _) = 1
     pri (PEq _ l r) = max 1 (max (pri l) (pri r))
@@ -1007,7 +1007,7 @@ getPriority i tm = 1 -- pri tm
     pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))
     pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))
     pri (PTyped l r) = pri l
-    pri (PPair _ l r) = max 1 (max (pri l) (pri r))
+    pri (PPair _ _ l r) = max 1 (max (pri l) (pri r))
     pri (PDPair _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))
     pri (PAlternative a as) = maximum (map pri as)
     pri (PConstant _) = 0
@@ -1182,7 +1182,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
              put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
     imps top env (PTyped l r)
         = imps top env l
-    imps top env (PPair _ l r)
+    imps top env (PPair _ _ l r)
         = do (decls, ns) <- get
              let isn = namesIn uvars ist l ++ namesIn uvars ist r
              put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
@@ -1252,10 +1252,10 @@ addImpl' inpat env infns ist ptm
       = let l' = ai env ds l
             r' = ai env ds r in
             PTyped l' r'
-    ai env ds (PPair fc l r) 
+    ai env ds (PPair fc p l r) 
       = let l' = ai env ds l
             r' = ai env ds r in
-            PPair fc l' r'
+            PPair fc p l' r'
     ai env ds (PDPair fc l t r)
          = let l' = ai env ds l
                t' = ai env ds t
@@ -1455,7 +1455,7 @@ stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where
        = let alts' = filter (/= Placeholder) (map su alts) in
              if null alts' then Placeholder
                            else PAlternative b alts'
-    su (PPair fc l r) = PPair fc (su l) (su r)
+    su (PPair fc p l r) = PPair fc p (su l) (su r)
     su (PDPair fc l t r) = PDPair fc (su l) (su t) (su r)
     su t = t
 stripUnmatchable i tm = tm
@@ -1564,9 +1564,9 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
                                            return (ml ++ mr)
     match (PTyped l r) x = match l x
     match x (PTyped l r) = match x l
-    match (PPair _ l r) (PPair _ l' r') = do ml <- match' l l'
-                                             mr <- match' r r'
-                                             return (ml ++ mr)
+    match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'
+                                                 mr <- match' r r'
+                                                 return (ml ++ mr)
     match (PDPair _ l t r) (PDPair _ l' t' r') = do ml <- match' l l'
                                                     mt <- match' t t'
                                                     mr <- match' r r'
@@ -1587,7 +1587,7 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
     match (PTactics _) _ = return []
     match (PRefl _ _) (PRefl _ _) = return []
     match (PResolveTC _) (PResolveTC _) = return []
-    match (PTrue _) (PTrue _) = return []
+    match (PTrue _ _) (PTrue _ _) = return []
     match (PFalse _) (PFalse _) = return []
     match (PReturn _) (PReturn _) = return []
     match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
@@ -1647,7 +1647,7 @@ substMatchShadow n shs tm t = sm shs t where
     sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)
                                            (fmap (sm xs) tm)
     sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)
-    sm xs (PPair f x y) = PPair f (sm xs x) (sm xs y)
+    sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)
     sm xs (PDPair f x t y) = PDPair f (sm xs x) (sm xs t) (sm xs y)
     sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)
     sm xs (PHidden x) = PHidden (sm xs x)
@@ -1670,7 +1670,7 @@ shadow n n' t = sm t where
     sm (PEq f x y) = PEq f (sm x) (sm y)
     sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)
     sm (PTyped x y) = PTyped (sm x) (sm y)
-    sm (PPair f x y) = PPair f (sm x) (sm y)
+    sm (PPair f p x y) = PPair f p (sm x) (sm y)
     sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)
     sm (PAlternative a as) = PAlternative a (map sm as)
     sm (PTactics ts) = PTactics (map (fmap sm) ts)
@@ -1692,13 +1692,13 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where
 
   -- FIXME: Probably ought to do this for completeness! It's fine as
   -- long as there are no bindings inside tactics though.
-  mkUniqT tac = return tac 
+  mkUniqT tac = return tac
 
   mkUniq :: PTerm -> State [Name] PTerm
   mkUniq (PLam n ty sc)
          = do env <- get
-              (n', sc') <- 
-                    if n `elem` env 
+              (n', sc') <-
+                    if n `elem` env
                        then do let n' = uniqueName n (env ++ inScope)
                                return (n', shadow n n' sc)
                        else return (n, sc)
@@ -1708,8 +1708,8 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where
               return $! PLam n' ty' sc''
   mkUniq (PPi p n ty sc)
          = do env <- get
-              (n', sc') <- 
-                    if n `elem` env 
+              (n', sc') <-
+                    if n `elem` env
                        then do let n' = uniqueName n (env ++ inScope)
                                return (n', shadow n n' sc)
                        else return (n, sc)
@@ -1719,35 +1719,35 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where
               return $! PPi p n' ty' sc''
   mkUniq (PLet n ty val sc)
          = do env <- get
-              (n', sc') <- 
-                    if n `elem` env 
+              (n', sc') <-
+                    if n `elem` env
                        then do let n' = uniqueName n (env ++ inScope)
                                return (n', shadow n n' sc)
                        else return (n, sc)
               put (n' : env)
               ty' <- mkUniq ty; val' <- mkUniq val
               sc'' <- mkUniq sc'
               return $! PLet n' ty' val' sc''
-  mkUniq (PApp fc t args) 
+  mkUniq (PApp fc t args)
          = do t' <- mkUniq t
               args' <- mapM mkUniqA args
               return $! PApp fc t' args'
-  mkUniq (PAppBind fc t args) 
+  mkUniq (PAppBind fc t args)
          = do t' <- mkUniq t
               args' <- mapM mkUniqA args
               return $! PAppBind fc t' args'
-  mkUniq (PCase fc t alts) 
+  mkUniq (PCase fc t alts)
          = do t' <- mkUniq t
               alts' <- mapM (\(x,y)-> do x' <- mkUniq x; y' <- mkUniq y
                                          return (x', y')) alts
               return $! PCase fc t' alts'
-  mkUniq (PPair fc l r) 
+  mkUniq (PPair fc p l r)
          = do l' <- mkUniq l; r' <- mkUniq r
-              return $! PPair fc l' r'                                                      
-  mkUniq (PDPair fc l t r) 
+              return $! PPair fc p l' r'
+  mkUniq (PDPair fc l t r)
          = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r
-              return $! PDPair fc l' t' r'                                                      
-  mkUniq (PAlternative b as) 
+              return $! PDPair fc l' t' r'
+  mkUniq (PAlternative b as)
          = liftM (PAlternative b) (mapM mkUniq as)
   mkUniq (PHidden t) = liftM PHidden (mkUniq t)
   mkUniq (PUnifyLog t) = liftM PUnifyLog (mkUniq t)

diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs
@@ -603,6 +603,8 @@ updateNs ns t = mapPT updateRef t
 --                                      (map (updateDNs ns) ds)
 -- updateDNs ns c = c
 
+data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show)
+
 -- | High level language terms
 data PTerm = PQuote Raw
            | PRef FC Name
@@ -616,13 +618,13 @@ data PTerm = PQuote Raw
            | PAppBind FC PTerm [PArg] -- ^ implicitly bound application
            | PMatchApp FC Name -- ^ Make an application by type matching
            | PCase FC PTerm [(PTerm, PTerm)]
-           | PTrue FC
+           | PTrue FC PunInfo
            | PFalse FC
            | PRefl FC PTerm
            | PResolveTC FC
            | PEq FC PTerm PTerm
            | PRewrite FC PTerm PTerm (Maybe PTerm)
-           | PPair FC PTerm PTerm
+           | PPair FC PunInfo PTerm PTerm
            | PDPair FC PTerm PTerm PTerm
            | PAlternative Bool [PTerm] -- True if only one may work
            | PHidden PTerm -- ^ Irrelevant or hidden pattern
@@ -662,7 +664,7 @@ mapPT f t = f (mpt t) where
   mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)
   mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)
   mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)
-  mpt (PPair fc l r) = PPair fc (mapPT f l) (mapPT f r)
+  mpt (PPair fc p l r) = PPair fc p (mapPT f l) (mapPT f r)
   mpt (PDPair fc l t r) = PDPair fc (mapPT f l) (mapPT f t) (mapPT f r)
   mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)
   mpt (PHidden t) = PHidden (mapPT f t)
@@ -1154,7 +1156,9 @@ pprintPTerm impl bnd = prettySe 10 bnd
     prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm
     prettySe p bnd (PRefl _ _) = annotate (AnnName eqCon Nothing Nothing) $ text "refl"
     prettySe p bnd (PResolveTC _) = text "resolvetc"
-    prettySe p bnd (PTrue _) = annotate (AnnName unitTy Nothing Nothing) $ text "()"
+    prettySe p bnd (PTrue _ IsType) = annotate (AnnName unitTy Nothing Nothing) $ text "()"
+    prettySe p bnd (PTrue _ IsTerm) = annotate (AnnName unitCon Nothing Nothing) $ text "()"
+    prettySe p bnd (PTrue _ TypeOrTerm) = text "()"
     prettySe p bnd (PFalse _) = annotate (AnnName falseTy Nothing Nothing) $ text "_|_"
     prettySe p bnd (PEq _ l r) =
       bracket p 2 . align . group $
@@ -1165,8 +1169,20 @@ pprintPTerm impl bnd = prettySe 10 bnd
       text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r
     prettySe p bnd (PTyped l r) =
       lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen
-    prettySe p bnd (PPair _ l r) =
+    prettySe p bnd (PPair _ TypeOrTerm l r) =
       lparen <> prettySe 10 bnd l <> text "," <+> prettySe 10 bnd r <> rparen
+    prettySe p bnd (PPair _ IsType l r) =
+      annotate (AnnName pairTy Nothing Nothing) lparen <>
+      prettySe 10 bnd l <>
+      annotate (AnnName pairTy Nothing Nothing) comma <+>
+      prettySe 10 bnd r <>
+      annotate (AnnName pairTy Nothing Nothing) rparen
+    prettySe p bnd (PPair _ IsTerm l r) =
+      annotate (AnnName pairCon Nothing Nothing) lparen <>
+      prettySe 10 bnd l <>
+      annotate (AnnName pairCon Nothing Nothing) comma <+>
+      prettySe 10 bnd r <>
+      annotate (AnnName pairCon Nothing Nothing) rparen
     prettySe p bnd (PDPair _ l t r) =
       lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen
     prettySe p bnd (PAlternative a as) =
@@ -1380,13 +1396,13 @@ instance Sized PTerm where
   size (PApp fc name args) = 1 + size args
   size (PAppBind fc name args) = 1 + size args
   size (PCase fc trm bdy) = 1 + size trm + size bdy
-  size (PTrue fc) = 1
+  size (PTrue fc _) = 1
   size (PFalse fc) = 1
   size (PRefl fc _) = 1
   size (PResolveTC fc) = 1
   size (PEq fc left right) = 1 + size left + size right
   size (PRewrite fc left right _) = 1 + size left + size right
-  size (PPair fc left right) = 1 + size left + size right
+  size (PPair fc _ left right) = 1 + size left + size right
   size (PDPair fs left ty right) = 1 + size left + size ty + size right
   size (PAlternative a alts) = 1 + size alts
   size (PHidden hidden) = size hidden
@@ -1425,7 +1441,7 @@ allNamesIn tm = nub $ ni [] tm
     ni env (PEq _ l r)     = ni env l ++ ni env r
     ni env (PRewrite _ l r _) = ni env l ++ ni env r
     ni env (PTyped l r)    = ni env l ++ ni env r
-    ni env (PPair _ l r)   = ni env l ++ ni env r
+    ni env (PPair _ _ l r)   = ni env l ++ ni env r
     ni env (PDPair _ (PRef _ n) t r)  = ni env t ++ ni (n:env) r
     ni env (PDPair _ l t r)  = ni env l ++ ni env t ++ ni env r
     ni env (PAlternative a ls) = concatMap (ni env) ls
@@ -1447,7 +1463,7 @@ boundNamesIn tm = nub $ ni tm
     ni (PEq _ l r)     = ni l ++ ni r
     ni (PRewrite _ l r _) = ni l ++ ni r
     ni (PTyped l r)    = ni l ++ ni r
-    ni (PPair _ l r)   = ni l ++ ni r
+    ni (PPair _ _ l r)   = ni l ++ ni r
     ni (PDPair _ (PRef _ n) t r) = ni t ++ ni r
     ni (PDPair _ l t r) = ni l ++ ni t ++ ni r
     ni (PAlternative a as) = concatMap (ni) as
@@ -1474,7 +1490,7 @@ namesIn uvars ist tm = nub $ ni [] tm
     ni env (PEq _ l r)     = ni env l ++ ni env r
     ni env (PRewrite _ l r _) = ni env l ++ ni env r
     ni env (PTyped l r)    = ni env l ++ ni env r
-    ni env (PPair _ l r)   = ni env l ++ ni env r
+    ni env (PPair _ _ l r)   = ni env l ++ ni env r
     ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
     ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
     ni env (PAlternative a as) = concatMap (ni env) as
@@ -1502,7 +1518,7 @@ usedNamesIn vars ist tm = nub $ ni [] tm
     ni env (PEq _ l r)     = ni env l ++ ni env r
     ni env (PRewrite _ l r _) = ni env l ++ ni env r
     ni env (PTyped l r)    = ni env l ++ ni env r
-    ni env (PPair _ l r)   = ni env l ++ ni env r
+    ni env (PPair _ _ l r)   = ni env l ++ ni env r
     ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r
     ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r
     ni env (PAlternative a as) = concatMap (ni env) as

diff --git a/src/Idris/Coverage.hs b/src/Idris/Coverage.hs
@@ -164,7 +164,7 @@ genAll i args
     otherPats :: PTerm -> [PTerm]
     otherPats o@(PRef fc n) = ops fc n [] o
     otherPats o@(PApp _ (PRef fc n) xs) = ops fc n xs o
-    otherPats o@(PPair fc l r)
+    otherPats o@(PPair fc _ l r)
         = ops fc pairCon
                 ([pimp (sUN "A") Placeholder True,
                   pimp (sUN "B") Placeholder True] ++
@@ -196,7 +196,7 @@ genAll i args
         = PDPair fc (getTm t) Placeholder (getTm v)
     resugar (PApp _ (PRef fc n) [_,_,l,r])
       | n == pairCon
-        = PPair fc (getTm l) (getTm r)
+        = PPair fc IsTerm (getTm l) (getTm r)
     resugar t = t
 
     dropForce force (x : xs) i | i `elem` force

diff --git a/src/Idris/DSL.hs b/src/Idris/DSL.hs
@@ -37,7 +37,7 @@ expandDo dsl (PAppBind fc t args) = PAppBind fc (expandDo dsl t)
 expandDo dsl (PCase fc s opts) = PCase fc (expandDo dsl s)
                                         (map (pmap (expandDo dsl)) opts)
 expandDo dsl (PEq fc l r) = PEq fc (expandDo dsl l) (expandDo dsl r)
-expandDo dsl (PPair fc l r) = PPair fc (expandDo dsl l) (expandDo dsl r)
+expandDo dsl (PPair fc p l r) = PPair fc p (expandDo dsl l) (expandDo dsl r)
 expandDo dsl (PDPair fc l t r) = PDPair fc (expandDo dsl l) (expandDo dsl t)
                                            (expandDo dsl r)
 expandDo dsl (PAlternative a as) = PAlternative a (map (expandDo dsl) as)
@@ -93,7 +93,7 @@ var dsl n t i = v' i t where
     v' i (PApp f x as)   = PApp f (v' i x) (fmap (fmap (v' i)) as)
     v' i (PCase f t as)  = PCase f (v' i t) (fmap (pmap (v' i)) as)
     v' i (PEq f l r)     = PEq f (v' i l) (v' i r)
-    v' i (PPair f l r)   = PPair f (v' i l) (v' i r)
+    v' i (PPair f p l r) = PPair f p (v' i l) (v' i r)
     v' i (PDPair f l t r) = PDPair f (v' i l) (v' i t) (v' i r)
     v' i (PAlternative a as) = PAlternative a $ map (v' i) as
     v' i (PHidden t)     = PHidden (v' i t)
@@ -144,9 +144,9 @@ debind b tm = let (tm', (bs, _)) = runState (db' tm) ([], 0) in
                               return (PLet n ty v' (debind b sc))
     db' (PCase fc s opts) = do s' <- db' s
                                return (PCase fc s' (map (pmap (debind b)) opts))
-    db' (PPair fc l r) = do l' <- db' l
-                            r' <- db' r
-                            return (PPair fc l' r')
+    db' (PPair fc p l r) = do l' <- db' l
+                              r' <- db' r
+                              return (PPair fc p l' r')
     db' (PDPair fc l t r) = do l' <- db' l
                                r' <- db' r
                                return (PDPair fc l' t r')

diff --git a/src/Idris/DeepSeq.hs b/src/Idris/DeepSeq.hs
@@ -122,6 +122,9 @@ instance (NFData t) => NFData (PDecl' t) where
         rnf (PTransform x1 x2 x3 x4)
           = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
 
+instance NFData PunInfo where
+        rnf x = x `seq` ()
+
 instance (NFData t) => NFData (PClause' t) where
         rnf (PClause x1 x2 x3 x4 x5 x6)
           = rnf x1 `seq`
@@ -154,14 +157,14 @@ instance NFData PTerm where
         rnf (PAppBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
         rnf (PMatchApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
         rnf (PCase x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
-        rnf (PTrue x1) = rnf x1 `seq` ()
+        rnf (PTrue x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
         rnf (PFalse x1) = rnf x1 `seq` ()
         rnf (PRefl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
         rnf (PResolveTC x1) = rnf x1 `seq` ()
         rnf (PEq x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
         rnf (PRewrite x1 x2 x3 x4)
           = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
-        rnf (PPair x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
+        rnf (PPair x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
         rnf (PDPair x1 x2 x3 x4)
           = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
         rnf (PAlternative x1 x2) = rnf x1 `seq` rnf x2 `seq` ()