add Constructor record for more convenience

fixup lovely changes made by Tim Engler to work with Constructor record

Makefile

@@ -0,0 +1,19 @@
+# literally just convenience
+
+PKGNAME = elab-deriving
+
+.PHONY: build
+
+install:
+	idris2 --install ${PKGNAME}.ipkg
+
+build:
+	idris2 --build ${PKGNAME}.ipkg
+
+test:
+	@${MAKE} -C tests only=$(only)
+
+clean:
+	@find . -type f -name '*.ttc' -exec rm -f {} \;
+	@find . -type f -name '*.ttm' -exec rm -f {} \;
+	@find . -type f -name '*.ibc' -exec rm -f {} \;

README.md

@@ -3,6 +3,10 @@ Elab Deriving (bad name, pick better)
 
 Very WIP!
 
+Resources:
+https://github.com/mb64/idris2-extras/blob/main/Extra/Language/Derive.idr
+https://github.com/david-christiansen/derive-all-the-instances
+
 This is a package for deriving implementations of common functions and interfaces in [Idris2](https://github.com/idris-lang/Idris2). It's intended to alleviate the tedium of writing your own instances, especially for things like newtypes which is just a whole lot of copypasting of wrapping.
 
 It's pretty basic just now but so is elaborator reflection.

elab-deriving.ipkg

@@ -1,7 +1,7 @@
 package elab-deriving
 
 authors    = "MarcelineVQ"
-version    = "0.8.2.0"
+version    = "0.10.2.0"
 readme     = "README.md"
 
 homepage   = "https://github.com/MarcelineVQ/idris2-elab-deriving"

src/Language/Elab/Deriving/DecEq.idr

@@ -171,16 +171,16 @@ decEqSameCon funName conName argInfos =
                   ]
 
 
-decEqDiffCon : (opname : Name) -> (Name, List ArgInfo, TTImp) -> (Name, List ArgInfo, TTImp) -> Elab Clause
-decEqDiffCon op (cn1, ca1, ct1) (cn2, ca2, ct3) = 
+decEqDiffCon : (opname : Name) -> Constructor -> Constructor -> Elab Clause
+decEqDiffCon op con1 con2 =
   do
     sym1 <- readableGenSym "a"
     sym2 <- readableGenSym "b"
-    logMsg "decEqCA1" 1 (show ca1)
-    logMsg "decEqCA2" 1 (show ca2)
+    logMsg "decEqCA1" 1 (show con1.args)
+    logMsg "decEqCA2" 1 (show con1.args)
     (let
-        pat1 = makePat cn1 sym1 ca1
-        pat2 = makePat cn2 sym2 ca2
+        pat1 = makePat con1.name sym1 con1.args
+        pat2 = makePat con2.name sym2 con2.args
         lhs = iVar op `iApp` pat1 `iApp` pat2
         rhs = makeRhs sym1 sym2
      in 
@@ -240,14 +240,14 @@ deriveDecEq vis decEqname = do
     -- The components of our decEq-ing function
     funclaim <- decEqClaim funn tyinfo Private -- NB private
 
-    traverse (\(cn,la,ct) => 
+    traverse (\con =>
       do
-        logMsg "deriveDecEq" 1 $ "con name : " ++ show cn
-        logMsg "deriveDecEq" 1 $ "con list args: " ++ show la
-        logTerm "deriveDecEq" 1 "contype: " ct
+        logMsg "deriveDecEq" 1 $ "con name : " ++ show con.name
+        logMsg "deriveDecEq" 1 $ "con list args: " ++ show con.args
+        logTerm "deriveDecEq" 1 "contype: " con.type
       ) tyinfo.cons
 
-    funSameClauses <- traverse (\(consName, argInfo, _) => decEqSameCon funn consName argInfo) tyinfo.cons
+    funSameClauses <- traverse (\con => decEqSameCon funn con.name con.args) tyinfo.cons
     let diffCons = filter (not . isSameCons) [ (a,b) | a <- tyinfo.cons, b <- tyinfo.cons ]
     funDiffClauses <- traverse (uncurry $ decEqDiffCon funn) diffCons
 
@@ -263,6 +263,6 @@ deriveDecEq vis decEqname = do
     declare [funclaim, objclaim]
     declare [fundecl, objclause]
  where
-   isSameCons : ((Name,b), (Name, b)) -> Bool
-   isSameCons ((n1,_),(n2,_)) = n1 == n2
+   isSameCons : (Constructor, Constructor) -> Bool
+   isSameCons (con1, con2) = con1.name == con2.name
 

src/Language/Elab/Deriving/Eq.idr

@@ -48,19 +48,19 @@ eqClaim op tyinfo vis = do
   -- NB: I can't think of a reason not to Inline here
   pure $ iClaim MW vis [Inline] (mkTy op (addEqAutoImps params tysig))
 
-eqCon : (opname : Name) -> (Name, List ArgInfo, TTImp) -> Elab Clause
-eqCon op (conname, args, contype) = do
-    let vars = filter (isExplicitPi . piInfo) args
+eqCon : (opname : Name) -> Constructor -> Elab Clause
+eqCon op con = do
+    let vars = filter (isExplicitPi . piInfo) con.args
         pats = makePatNames vars infVars
-        lhs = iVar op `iApp` (makePat conname (map (map fst) pats)) `iApp` (makePat conname (map (map snd) pats))
+        lhs = iVar op `iApp` (makePat con.name (map (map fst) pats))
+                      `iApp` (makePat con.name (map (map snd) pats))
         rhs = makeRhs (catMaybes pats)
     logTerm "eqconlhs" 1 "" lhs
     logTerm "eqconrhs" 1 "" rhs
     pure $ patClause lhs rhs 
   where
     -- Make our pat names, we use Just to flag the vars we want to use, we don't
-    -- compare indices since they're vacuously the same for the Eq interface.
-    -- It doesn't seem to matter if an index is M1 or not.
+    -- compare indices since they're vacuously the same for an Eq interface.
     makePatNames : List ArgInfo
                -> Stream String -> (List (Maybe (Name,Name)))
     makePatNames [] vs = []

src/Language/Elab/Deriving/Ord.idr

@@ -47,14 +47,14 @@ compareClaim op tyinfo vis = do
 
 
 compareClause : (opname : Name)
-             -> (Int, (Name, List ArgInfo, TTImp))
-             -> (Int, (Name, List ArgInfo, TTImp)) -> Elab Clause
-compareClause op (i1,(conname1,args1,imp1)) (i2,(conname2,args2,imp2)) = do
-    let vars1 = filter (isExplicitPi . piInfo) args1
-    let vars2 = filter (isExplicitPi . piInfo) args2
+             -> (Int, Constructor)
+             -> (Int, Constructor) -> Elab Clause
+compareClause op (i1,con1) (i2,con2) = do
+    let vars1 = filter (isExplicitPi . piInfo) con1.args
+    let vars2 = filter (isExplicitPi . piInfo) con2.args
     let pats1 = makePatNames vars1 infVars "_1"
     let pats2 = makePatNames vars2 infVars "_2"
-    let lhs = iVar op `iApp` (makePat conname1 pats1) `iApp` (makePat conname2 pats2)
+    let lhs = iVar op `iApp` (makePat con1.name pats1) `iApp` (makePat con2.name pats2)
     let rhs = case compare i1 i2 of
                 LT => `(LT)
                 GT => `(GT)

src/Language/Elab/Deriving/Selectors.idr

@@ -46,33 +46,59 @@ data Foo : Type where
   Waf : Int -> Foo
   (:::) : Bool -> Bool -> Foo -- not really doable with singular functions, is::: ?
 
-select : TTImp -> Visibility -> (Name, List ArgInfo, TTImp) -> Elab ()
-select dty vis (conn,args,imp) = do
-  let n = mapName ("is" ++) conn -- isWaf
+select : TTImp -> Visibility -> Constructor -> Elab ()
+select dty vis con = do
+  let n = mapName ("is" ++) con.name -- isWaf
       c = iClaim MW vis [] $ mkTy n `( ~dty -> Bool)
-      expargs = filter (isExplicitPi . piInfo) args
-      c1 = patClause (iVar n `iApp` foldl (\xs,_ => `(~xs _) ) (iVar conn) expargs)
+      expargs = filter (isExplicitPi . piInfo) con.args
+      c1 = patClause (iVar n `iApp` foldl (\xs,_ => `(~xs _) ) (iVar con.name) expargs)
                      `(True)
       catchall = patClause `(~(iVar n) _) `(False)
       d = iDef n [c1,catchall]
   declare [c,d]
   pure ()
 
+||| Derives a selector for any non-operator constructor
+||| Simply because I'm not sure how to let you type the letters: e.g. is:::
 export
 deriveSelectors : Visibility -> Name -> Elab ()
 deriveSelectors vis tn = do
   ti <- makeTypeInfo tn
-  traverse_ (select ti.type vis) ti.cons
+  let cons' = filter (not . isOpName . name) ti.cons
+  traverse_ (select ti.type vis) cons'
+
+fetchRoot : TTImp -> TTImp
+fetchRoot (IApp _ y _) = fetchRoot y
+fetchRoot ty = ty
+
+isCon : Name -> Constructor -> Elab Clause
+isCon cn con = ?isCon_rhs
+
+-- This is kind of tough, we don't have a good way to say
+-- isFooCon (:::)   isFooCon Waf at the same type.
+-- If we take a Name, e.g.:
+-- isFooCon `{{(:::)}}   isFooCon `{{Waf}}
+-- We don't have a good way to enforce it's valid to use
+-- adding Maybe is a bit too much work for the user to deal with
+deriveIsCon : Visibility -> Name -> Elab ()
+deriveIsCon vis cn = do
+  ti <- makeTypeInfo cn
+  let n = mapName (\n => "is" ++ n ++ "Con") ti.name -- isFooCon, need to get Foo from cn
+  let c = iClaim MW vis [] $ mkTy `{{Foo}} `( Name -> Bool)
+  let catchall = patClause `(~(iVar n) _) `(False)
+
+  defs <- traverse (isCon ti.name) ti.cons
+  pure ()
+
 
 %runElab deriveSelectors Private `{{Foo}}
+-- %runElab deriveIsCon Private `{{Foo}}
 
 foo1 : Foo -> Bool
 foo1 x = isWaf x
 
 foo2 : Foo -> Bool
 foo2 x = isBif x
 
-foo3 : Foo -> Bool
-foo3 x = ?fsd -- is::: x  not really gonna happen
--- ^ This is why a combined approach is probably best, e.g. isCon (:::) x
-
+-- foo3 : Foo -> Bool
+-- foo3 x = is::: x -- isn't generated

src/Language/Elab/Deriving/Show.idr

@@ -36,17 +36,17 @@ showClaim op tyinfo vis = do
   -- NB: I can't think of a reason not to Inline here
   pure $ iClaim MW vis [Inline] (mkTy op (addShowAutoImps varnames' tysig))
 
-showCon : (opname : Name) -> (Name, List ArgInfo, TTImp) -> Elab Clause
-showCon op (conname, args, contype) = do
-    let varnames = filter (isExplicitPi . piInfo) args
+showCon : (opname : Name) -> Constructor -> Elab Clause
+showCon op con = do
+    let varnames = filter (isExplicitPi . piInfo) con.args
         lhsvars = map (show . name) varnames
         rhsvars = map (\arg => if isUse0 (count arg)
                              then Nothing
                              else Just (show arg.name)) varnames
         lhs = iVar op `iApp`
-                foldl (\tt,v => `(~(tt) ~(iBindVar v))) (iVar conname) lhsvars
+                foldl (\tt,v => `(~(tt) ~(iBindVar v))) (iVar con.name) lhsvars
         rhs = foldl (\tt,v => `( ~(tt) ++ " " ++ ~(beShown v)))
-                (iPrimVal (Str !(showName conname))) rhsvars
+                (iPrimVal (Str !(showName con.name))) rhsvars
     pure $ patClause lhs rhs
   where
     beShown : Maybe String -> TTImp

src/Language/Elab/Syntax.idr

@@ -173,6 +173,7 @@ mapName f (NS ns n) = (NS ns (mapName f n))
 mapName f (DN n realn) = (DN (f n) realn)
 -- mapName f (Nested ix n) = Nested ix (mapName f n)
 -- mapName f (CaseBlock outer inner) = CaseBlock outer inner
+-- mapName f (WithBlock outer inner) = WithBlock outer inner
 
 export
 extractNameStr : Name -> String
@@ -181,12 +182,20 @@ extractNameStr (MN x y) = x
 extractNameStr (NS xs x) = extractNameStr x
 extractNameStr (DN x _) = x
 
+isOpChar : Char -> Bool
+isOpChar c = c `elem` (unpack ":!#$%&*+./<=>?@\\^|-~")
+
+export
+isOpName : Name -> Bool
+isOpName n = any isOpChar (unpack (extractNameStr n))
+
 export
 extractNameNo : Name -> Int
 extractNameNo (MN _ i) = i
 extractNameNo _ = 0
 
--- Change/remove this later, we really don't want to have it, or export it
+-- Change/remove this later, we really don't want to export it and we currently
+-- do due to the nature of needing to make things public for elaboration
 export
 implementation Eq Name where
   (==) (UN x) (UN y) = x == y
@@ -204,6 +213,11 @@ isImplicitPi : PiInfo t -> Bool
 isImplicitPi ImplicitArg = True
 isImplicitPi _ = False
 
+export
+isAutoImplicitPi : PiInfo t -> Bool
+isAutoImplicitPi AutoImplicit = True
+isAutoImplicitPi _ = False
+
 export
 logDecls : String -> Nat -> String -> List Decl -> Elab ()
 logDecls ty n s d = logTerm ty n s $ ILocal EmptyFC d `( () )
@@ -241,6 +255,8 @@ Show (PiInfo tt) where
   show AutoImplicit = "AutoImplicit"
   show (DefImplicit _) = "DefImplicit _"
 
+
+-- Don't do this yourself, use Selectors :>
 export
 isUse0 : Count -> Bool
 isUse0 M0 = True
@@ -273,3 +289,48 @@ printInterfaceCon n = do
     | _ => fail $ "showObject: error during " ++ nstr ++ " constructor lookup"
   (_, objimp) <- lookupName icon
   logTerm "printInterfaceCon" 1 (nstr ++ ": ") objimp
+
+alterTT : (TTImp -> Maybe TTImp) -> TTImp -> TTImp
+alterTT f tt = maybe tt id (f tt)
+
+
+Eq FC where
+  (MkFC x1 y1 z1) == (MkFC x2 y2 z2) = x1 == x2 && y1 == y2 && z1 == z2
+  EmptyFC == EmptyFC = True
+  _ == _ = False
+
+-- bleh, but if I can polish Eq enough to add the deriving to the compiler this can go away.
+Eq TTImp where
+  (IVar x1 y1) == (IVar x2 y2) = x1 == x2 && y1 == y2
+  (IPi x1 y1 z1 w1 argTy1 retTy1) == (IPi x2 y2 z2 w2 argTy2 retTy2) = ?holeEq_2
+  (ILam x1 y1 z1 w1 argTy1 lamTy1) == (ILam x2 y2 z2 w2 argTy2 lamTy2) = ?holeEq_3
+  (ILet x1 y1 z1 nTy1 nVal1 scope1) == (ILet x2 y2 z2 nTy2 nVal2 scope2) = ?holeEq_4
+  (ICase x1 y1 ty1 xs1) == (ICase x2 y2 ty2 xs2) = ?holeEq_5
+  (ILocal x1 xs1 y1) == (ILocal x2 xs2 y2) = ?holeEq_6
+  (IUpdate x1 xs1 y1) == (IUpdate x2 xs2 y2) = ?holeEq_7
+  (IApp x1 y1 z1) == (IApp x2 y2 z2) = x1 == x2 && y1 == y2 && z1 == z2
+  (IImplicitApp x1 y1 z1 w1) == (IImplicitApp x2 y2 z2 w2) = x1 == x2 && y1 == y2 && z1 == z2 && w1 == w2
+  (IWithApp x1 y1 z1) == (IWithApp x2 y2 z2) = x1 == x2 && y1 == y2 && z1 == z2
+  (ISearch x1 depth1) == (ISearch x2 depth2) = x1 == x2 && depth1 == depth2
+  (IAlternative x1 y1 xs1) == (IAlternative x2 y2 xs2) = ?holeEq_12
+  (IRewrite x1 y1 z1) == (IRewrite x2 y2 z2) = ?holeEq_13
+  (IBindHere x1 y1 z1) == (IBindHere x2 y2 z2) = ?holeEq_14
+  (IBindVar x1 y1) == (IBindVar x2 y2) = ?holeEq_15
+  (IAs x1 y1 z1 w1) == (IAs x2 y2 z2 w2) = ?holeEq_16
+  (IMustUnify x1 y1 z1) == (IMustUnify x2 y2 z2) = ?holeEq_17
+  (IDelayed x1 y1 z1) == (IDelayed x2 y2 z2) = ?holeEq_18
+  (IDelay x1 y1) == (IDelay x2 y2) = ?holeEq_19
+  (IForce x1 y1) == (IForce x2 y2) = ?holeEq_20
+  (IQuote x1 y1) == (IQuote x2 y2) = ?holeEq_21
+  (IQuoteName x1 y1) == (IQuoteName x2 y2) = ?holeEq_22
+  (IQuoteDecl x1 y1) == (IQuoteDecl x2 y2) = ?holeEq_23
+  (IUnquote x1 y1) == (IUnquote x2 y2) = ?holeEq_24
+  (IPrimVal x1 c1) == (IPrimVal x2 c2) = ?holeEq_25
+  (IType x1) == (IType x2) = ?holeEq_26
+  (IHole x1 y1) == (IHole x2 y2) = ?holeEq_27
+  (Implicit x1 bindIfUnsolved1) == (Implicit x2 bindIfUnsolved2) = ?holeEq_28
+  (IWithUnambigNames x1 xs1 y1) == (IWithUnambigNames x2 xs2 y2) = ?holeEq_29
+  _ == _ = False
+
+-- ||| target for mapping an exact given TTImp
+-- target : TTImp -> (TTImp -> TTImp) -> TTImp -> TTImp

src/Language/Elab/Types.idr

@@ -38,14 +38,24 @@ logArgInfo n (MkArgInfo count piInfo name type isIndex) = do
   logMsg "logArgInfo" n $ "MkArgInfo " ++ show count ++ " " ++ show piInfo ++ " " ++ showPrec App name
   logTerm "logArgInfo" n "argimp: " type
 
+
+-- Fully qualified Name
+-- `type` is our fully applied type, e.g. given args a,b,c: Foo a b c
+public export
+record Constructor where
+  constructor MkConstructor
+  name : Name
+  args : List ArgInfo
+  type : TTImp
+
 -- Fully qualified Name
 -- `type` is our fully applied type, e.g. given args a,b,c: Foo a b c
 public export
 record TypeInfo where
   constructor MkTypeInfo
   name : Name
   args : List ArgInfo
-  cons : List (Name, List ArgInfo, TTImp)
+  cons : List Constructor
   type : TTImp
 
 
@@ -73,8 +83,7 @@ getConType qn = go (snd !(lookupName qn))
       (xs,retTy1) <- go retTy0
       let n1 = maybe !(genSym "arg") id n0
       logMsg "getConType" 1 "compute"
-      let b = maybe False (`indexOf`retTy1) n0 -- TODO: ask why is "isType" in there???
-      --let b = not (isType argTy) && maybe False (`indexOf`retTy1) n0
+      let b = maybe False (`indexOf`retTy1) n0
       pure $ (MkArgInfo c i n1 argTy b :: xs, retTy1)
     go retTy = pure ([],retTy)
 
@@ -121,7 +130,8 @@ makeTypeInfo n = do
   logMsg "makeTypeInfo" 1 "I'm being computed"
   let tyargs = filter (isExplicitPi . piInfo) args
       ty = appTyCon (map (\arg => extractNameStr  arg.name) tyargs) tyname
-  pure $ MkTypeInfo tyname args (zip connames conlist) ty
+  pure $ MkTypeInfo tyname args
+           (zipWith (\x,(y,z) => MkConstructor x y z) connames conlist) ty
 
 
 

src/Util.idr

@@ -38,9 +38,10 @@ export
 zipLS : List a -> Stream b -> List (a,b)
 zipLS = zipWithLS MkPair
 
-export
-catMaybes : List (Maybe a) -> List a
-catMaybes z = foldr (\m,f => maybe f (\x => (x ::) . f) m) id z []
+-- provided by Data.List now
+-- export
+-- catMaybes : List (Maybe a) -> List a
+-- catMaybes z = foldr (\m,f => maybe f (\x => (x ::) . f) m) id z []
 
 export
 unzip : List (a,b) -> (List a, List b)