mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-21 10:41:59 +03:00
32e26c5bd1
Instead of having UN & RF (& Hole in the near future & maybe even more later e.g. operator names) we have a single UN constructor that takes a UserName instead of a String. UserName is (for now) ```idris data UserName : Type where Basic : String -> UserName -- default name constructor e.g. map Field : String -> UserName -- field accessor e.g. .fst Underscore : UserName -- no name e.g. _ ``` This is extracted from the draft PR #1852 which is too big to easily debug. Once this is working, I can go back to it.
52 lines
1.7 KiB
Idris
52 lines
1.7 KiB
Idris
module DerivingEq
|
|
|
|
import Language.Reflection
|
|
|
|
%language ElabReflection
|
|
|
|
public export
|
|
countArgs : (ty : TTImp) -> Nat
|
|
countArgs (IPi _ _ ExplicitArg _ _ retTy) = 1 + countArgs retTy
|
|
countArgs (IPi _ _ _ _ _ retTy) = countArgs retTy
|
|
countArgs _ = 0
|
|
|
|
-- %logging 5
|
|
public export
|
|
genEq : {t : _} -> Name -> Elab (t -> t -> Bool)
|
|
genEq typeName = do
|
|
let pos : FC = MkFC (Virtual Interactive) (0,0) (0,0)
|
|
[(n, _)] <- getType typeName
|
|
| _ => fail "Ambiguous name"
|
|
constrs <- getCons n
|
|
let and : TTImp -> TTImp -> TTImp
|
|
and x y = `(~(x) && ~(y))
|
|
compareEq : String -> String -> TTImp
|
|
compareEq x y = `(~(IVar pos $ UN (Basic x)) == ~(IVar pos $ UN (Basic y)))
|
|
makeClause : Name -> Elab Clause
|
|
makeClause constr = do
|
|
[(_, ty)] <- getType constr
|
|
| _ => fail "ambiguous name for constr"
|
|
let nArgs = countArgs ty
|
|
let xs = map (\i => "x_" ++ show i) $ take nArgs [1..]
|
|
let ys = map (\i => "y_" ++ show i) $ take nArgs [1..]
|
|
let px = foldl (IApp pos) (IVar pos constr) $ map (IBindVar pos) xs
|
|
let py = foldl (IApp pos) (IVar pos constr) $ map (IBindVar pos) ys
|
|
pure $ PatClause pos `(MkPair ~(px) ~(py))
|
|
$ foldl and `(True) $ zipWith compareEq xs ys
|
|
finalClause : Clause
|
|
finalClause = PatClause pos `(_) `(False)
|
|
clauses <- traverse makeClause constrs
|
|
let allClauses = clauses ++ [finalClause]
|
|
caseExpr = ICase pos `(MkPair x y) (Implicit pos True) allClauses
|
|
result = `(\x, y => ~(caseExpr))
|
|
check result
|
|
%logging 0
|
|
|
|
-- This tree works
|
|
|
|
data TreeOne a = BranchOne (TreeOne a) a (TreeOne a)
|
|
| Leaf
|
|
|
|
Eq a => Eq (TreeOne a) where
|
|
(==) = %runElab genEq `{ TreeOne }
|