[ fix ] :printdef support for P(D)Pair & Equal (#2416)

idris2api.ipkg

@@ -123,6 +123,7 @@ modules =
     Idris.Resugar,
     Idris.SetOptions,
     Idris.Syntax,
+    Idris.Syntax.Builtin,
     Idris.Syntax.Traversals,
     Idris.Syntax.Views,
     Idris.Version,

src/Idris/Desugar.idr

@@ -19,6 +19,7 @@ import Idris.Error
 import Idris.Pretty
 import Idris.REPL.Opts
 import Idris.Syntax
+import Idris.Syntax.Builtin
 
 import Idris.Elab.Implementation
 import Idris.Elab.Interface
@@ -170,18 +171,6 @@ idiomise fc mns fn
         nm  = maybe pur (`NS` pur) mns
      in IApp fc (IVar fc nm) fn
 
-pairname : Name
-pairname = NS builtinNS (UN $ Basic "Pair")
-
-mkpairname : Name
-mkpairname = NS builtinNS (UN $ Basic "MkPair")
-
-dpairname : Name
-dpairname = NS dpairNS (UN $ Basic "DPair")
-
-mkdpairname : Name
-mkdpairname = NS dpairNS (UN $ Basic "MkDPair")
-
 data Bang : Type where
 
 mutual
@@ -532,11 +521,11 @@ mutual
 
       strInterpolate : List RawImp -> RawImp
       strInterpolate []
-        = IVar EmptyFC (NS preludeNS $ UN $ Basic "Nil")
+        = IVar EmptyFC nilName
       strInterpolate (x :: xs)
         = let xFC = virtualiseFC (getFC x) in
-          apply (IVar xFC (NS preludeNS $ UN $ Basic "::"))
-          [ IApp xFC (IVar EmptyFC (UN $ Basic "interpolate"))
+          apply (IVar xFC consName)
+          [ IApp xFC (IVar EmptyFC interpolateName)
                      x
           , strInterpolate xs
           ]
@@ -667,8 +656,8 @@ mutual
       = do l' <- desugarTree side ps l
            r' <- desugarTree side ps r
            pure (IAlternative loc FirstSuccess
-                     [apply (IVar eqFC (UN $ Basic "===")) [l', r'],
-                      apply (IVar eqFC (UN $ Basic "~=~")) [l', r']])
+                     [apply (IVar eqFC eqName) [l', r'],
+                      apply (IVar eqFC heqName) [l', r']])
   desugarTree side ps (Infix loc _ (UN $ Basic "$") l r) -- special case since '$' is special syntax
       = do l' <- desugarTree side ps l
            r' <- desugarTree side ps r

src/Idris/Doc/Display.idr

@@ -72,11 +72,11 @@ displayImpl defs (n, idx, gdef)
   = case definition gdef of
       PMDef _ _ ct _ [(vars ** (env,  _, rhs))] =>
         do rhstm <- resugar env !(normaliseHoles defs env rhs)
-           let (_, args) = getFnArgs rhstm
+           let (_, args) = getFnArgs defaultKindedName rhstm
            defs <- get Ctxt
            pds <- map catMaybes $ for args $ \ arg => do
              let (_, expr) = underLams (unArg arg)
-             let (PRef _ kn, _) = getFnArgs expr
+             let (PRef _ kn, _) = getFnArgs defaultKindedName expr
                | _ => pure Nothing
              log "doc.implementation" 20 $ "Got name \{show @{Raw} kn}"
              let (ns, DN dn nm) = splitNS (kn.fullName)

src/Idris/Doc/String.idr

@@ -469,7 +469,7 @@ getDocsForImplementation :
   PTerm -> Core (Maybe (Doc IdrisSyntax))
 getDocsForImplementation t = do
   -- the term better be of the shape (I e1 e2 e3) where I is a name
-  let (PRef fc intf, args) = getFnArgs t
+  let (PRef fc intf, args) = getFnArgs id t
     | _ => pure Nothing
   -- That name (I) better be the name of an interface
   syn <- get Syn
@@ -489,7 +489,7 @@ getDocsForImplementation t = do
     let (_, retTy) = underPis ty
     -- try to see whether it approximates what we are looking for
     -- we throw the head away because it'll be the interface name (I)
-    let (_, cargs) = getFnArgs retTy
+    let (_, cargs) = getFnArgs defaultKindedName retTy
     bs <- for (zip args cargs) $ \ (arg, carg) => do
       -- For now we only compare the heads of the arguments because we expect
       -- we are interested in implementations of the form
@@ -498,7 +498,7 @@ getDocsForImplementation t = do
       -- retain implementations whose type is fully compatible.
 
       -- TODO: check the Args have the same shape before unArgging?
-      let ((PRef fc hd, _), (PRef _ chd, _)) = (getFnArgs (unArg arg), getFnArgs (unArg carg))
+      let ((PRef fc hd, _), (PRef _ chd, _)) = ( getFnArgs id (unArg arg), getFnArgs defaultKindedName (unArg carg))
         | ((PPrimVal _ c, _), (PPrimVal _ c', _)) => pure (c == c')
         | ((PType _, _), (PType _, _)) => pure True
         | _ => pure False

src/Idris/Syntax/Builtin.idr

@@ -0,0 +1,41 @@
+module Idris.Syntax.Builtin
+
+import Core.Name
+
+%default total
+
+export
+pairname : Name
+pairname = NS builtinNS (UN $ Basic "Pair")
+
+export
+mkpairname : Name
+mkpairname = NS builtinNS (UN $ Basic "MkPair")
+
+export
+dpairname : Name
+dpairname = NS dpairNS (UN $ Basic "DPair")
+
+export
+mkdpairname : Name
+mkdpairname = NS dpairNS (UN $ Basic "MkDPair")
+
+export
+nilName : Name
+nilName = NS preludeNS (UN $ Basic "Nil")
+
+export
+consName : Name
+consName = NS preludeNS (UN $ Basic "::")
+
+export
+interpolateName : Name
+interpolateName = NS preludeNS (UN $ Basic "interpolate")
+
+export
+eqName : Name
+eqName = NS builtinNS (UN $ Basic "===")
+
+export
+heqName : Name
+heqName = NS builtinNS (UN $ Basic "~=~")

src/Idris/Syntax/Views.idr

@@ -1,6 +1,7 @@
 module Idris.Syntax.Views
 
 import Idris.Syntax
+import Idris.Syntax.Builtin
 
 %default total
 
@@ -17,8 +18,8 @@ unArg (Auto _ t) = t
 unArg (Named _ _ t) = t
 
 export
-getFnArgs : PTerm' nm -> (PTerm' nm, List (Arg' nm))
-getFnArgs fts = go fts [] where
+getFnArgs : (Name -> nm) -> PTerm' nm -> (PTerm' nm, List (Arg' nm))
+getFnArgs embed fts = go fts [] where
 
   go : PTerm' nm -> List (Arg' nm) -> (PTerm' nm, List (Arg' nm))
   go (PApp fc f t) = go f . (Explicit fc t ::)
@@ -26,6 +27,12 @@ getFnArgs fts = go fts [] where
   go (PNamedApp fc f n t) = go f . (Named fc n t ::)
   go (PBracketed fc f) = go f
   go (POp fc opFC op l r) = (PRef opFC op,) . (Explicit fc l ::) . (Explicit fc r ::)
+  go (PEq fc l r) = (PRef fc $ embed eqName,) . (Explicit fc l ::) . (Explicit fc r ::)
+  -- ambiguous, picking the type constructor here
+  go (PPair fc l r) = (PRef fc $ embed pairname,) . (Explicit fc l ::) . (Explicit fc r ::)
+  go (PDPair full fc l ty r)
+    = (PRef fc $ embed dpairname,)
+    . (Explicit fc l ::) . (Explicit fc ty ::) . (Explicit fc r ::)
   go f = (f,)
 
 export

tests/idris2/interface001/IFace.idr

@@ -47,10 +47,10 @@ test : ((Eq b, Eq b, Eq a), Eq b) => a -> a -> Bool
 test x y = x == y
 
 interface DecEq a where
-  decEq : (x : a) -> (y : a) -> Dec (x = y)
+  decEq : (x : a) -> (y : a) -> Dec (x === y)
 
 -- partial!
-eqNat : (x : Nat) -> (y : Nat) -> Dec (x = y)
+eqNat : (x : Nat) -> (y : Nat) -> Dec (x === y)
 eqNat (S x) (S y)
     = case eqNat x y of
            Yes Refl => Yes Refl

tests/idris2/interface001/IFace1.idr

@@ -47,10 +47,10 @@ test : ((Eq b, Eq b, Eq a), Eq b) => a -> a -> Bool
 test x y = x == y
 
 interface DecEq ty where
-  decEq : (x : ty) -> (y : ty) -> Dec (x = y)
+  decEq : (x : ty) -> (y : ty) -> Dec (x === y)
 
 -- partial!
-eqNat : (x : Nat) -> (y : Nat) -> Dec (x = y)
+eqNat : (x : Nat) -> (y : Nat) -> Dec (x === y)
 eqNat (S x) (S y)
     = case eqNat x y of
            Yes Refl => Yes Refl