@@ -0,0 +1,198 @@
1+||| Derive implementations of decidable equality.
2+module Pruviloj.Derive.DecEq
3+
4+import Data.Fin
5+import Data.Vect
6+
7+import Language.Reflection.Utils
8+
9+import Pruviloj.Core
10+
11+import Pruviloj.Renamers
12+import Pruviloj.Internals
13+
14+import Pruviloj.Derive.Eliminators
15+
16+import Pruviloj.Disjoint
17+import Pruviloj.Induction
18+import Pruviloj.Injective
19+
20+%default total
21+%access private
22+
23+
24+covering
25+noCase : TTName -> Elab ()
26+noCase contra =
27+ do [_, nope] <- apply (Var `{No}) [True, False]
28+ | _ => fail [TextPart "Bad holes from", NamePart `{Tactics.apply}]
29+ solve
30+ focus nope
31+
32+ -- Construct a lambda binding an assumption from which we can
33+ -- derive the contradiction
34+ h <- gensym "h"
35+ inj <- gensym "inj"
36+ attack
37+ intro h
38+ injective (Var h) inj
39+ unproduct (Var inj)
40+ ignore $ refine (Var contra) `andThen` hypothesis
41+ solve -- attack
42+
43+partial -- TODO make covering/total
44+matchCase : List Raw -> Elab ()
45+matchCase [] = search
46+matchCase (tm :: tms) =
47+ do hs <- induction tm
48+ y <- unsafeNth 0 hs
49+ n <- unsafeNth 1 hs
50+
51+ focus n; compute
52+ contra <- gensym "contra"
53+ attack; intro contra
54+ noCase contra; solve
55+
56+ focus y; compute
57+ prf <- gensym "prf"
58+ attack; intro prf
59+ rewriteWith (Var prf)
60+ matchCase tms
61+ solve
62+
63+spanM : (Monad m) => (a -> m Bool) -> List a -> m (List a, List a)
64+spanM p [] = pure ([], [])
65+spanM p (x::xs) =
66+ if !(p x)
67+ then do (yes, no) <- spanM p xs
68+ pure (x :: yes, no)
69+ else pure ([], x::xs)
70+
71+partitionM : Monad m => (a -> m Bool) -> List a -> m (List a, List a)
72+partitionM p [] = pure ([], [])
73+partitionM p (x :: xs) =
74+ do (y, n) <- partitionM p xs
75+ if !(p x) then pure (x :: y, n) else pure (y, x :: n)
76+
77+perhaps : (Alternative f) => (f a) -> (f (Maybe a))
78+perhaps x = (Just <$> x) <|> pure Nothing
79+
80+headIs : Raw -> TTName -> Bool
81+headIs tm n = maybe False (==n) (headName tm)
82+
83+partial
84+mkRhs : (fn, fam : TTName) -> Nat -> Elab ()
85+mkRhs fn fam k =
86+ case snd !getGoal of
87+ `(Dec ((=) {A=~A} {B=~_} ~x ~y)) =>
88+ let (c1, args1) = unApply x
89+ (c2, args2) = unApply y
90+ in if c1 /= c2
91+ then do (h :: _) <- refine (Var `{No})
92+ | _ => empty
93+ focus h
94+ disjoint
95+ else do let toMakeEqual = List.filter (uncurry (/=)) (zip args1 args2)
96+ tms <- for {b=Raw} toMakeEqual $ \(tm1, tm2) =>
97+ do env <- getEnv
98+ (tm1', ty1') <- forget tm1 >>= check env
99+ (tm2', ty2') <- forget tm2 >>= check env
100+ -- assume they have the same type here -
101+ -- reasonable due to same constructor, but
102+ -- this means order is important when
103+ -- traversing
104+ eq <- gensym "eq"
105+ rTy <- forget ty1'
106+ rTm1 <- forget tm1'
107+ rTm2 <- forget tm2'
108+ remember eq `(Dec ((=) {A=~rTy} {B=~rTy} ~rTm1 ~rTm2))
109+ simple $
110+ if headIs rTy fam
111+ then do (a2::a1::hs) <- reverse <$> apply (Var fn) (replicate k True ++ [False, False])
112+ solve
113+ focus a1; fill rTm1; solve
114+ focus a2; fill rTm2; solve
115+ for_ hs $ \h => inHole h (resolveTC fn)
116+ else do [_, dH, a1, a2] <- apply (Var `{decEq}) [True, False, False, False]
117+ solve
118+ focus a1; fill rTm1; solve
119+ focus a2; fill rTm2; solve
120+ focus dH; resolveTC fn
121+ return (Var eq)
122+ matchCase tms
123+ _ => fail [TextPart "Inapplicable"]
124+
125+||| Attempt to derive the body of an implementation of decidable
126+||| equality based on an existing type signature.
127+|||
128+||| The function signature must provide enough information for the
129+||| deriving to occur. It must consist of zero or more non-constraint
130+||| arguments followed by zero or more constraint arguments, followed
131+||| by the two values to compare. The constraint arguments must
132+||| provide sufficient instances of `DecEq` to decide the equality of
133+||| each constructor field. The final two arguments to the function
134+||| declaration must be the two values that will be compared for
135+||| equality.
136+|||
137+||| @ fn the name of the function whose type has been declared
138+abstract partial -- because of mkRhs
139+deriveDecEq : (fn : TTName) -> Elab ()
140+deriveDecEq fn =
141+ do (_, Ref, sig') <- lookupTyExact fn
142+ sig <- forget sig'
143+ (args, `(Dec ((=) {A=~A} {B=~_} ~(Var x) ~(Var y)))) <- stealBindings sig noRenames
144+ | other => fail [ TextPart "Return type"
145+ , RawPart (snd other)
146+ , TextPart "isn't decidable equality"
147+ ]
148+
149+ datatype <- maybe (fail [ RawPart A
150+ , TextPart "is not an application of a TC"
151+ ])
152+ lookupDatatypeExact
153+ (headName A)
154+
155+ -- the signature must be like this:
156+ -- 1. a collection of variable bindings (will be implicit)
157+ -- 2. a collection of constraints
158+ -- 3. the arguments x and y from the return type
159+ (bindings, constrs, arg1, arg2) <-
160+ the (Elab (List (TTName, Binder Raw),
161+ List (TTName, Binder Raw),
162+ (TTName, Binder Raw),
163+ (TTName, Binder Raw))) $
164+ case reverse args of
165+ [] => fail [TextPart "Invalid signature"]
166+ [_] => fail [TextPart "Invalid signaure"]
167+ (a2 :: a1 :: rest) =>
168+ do (constrs, bindings) <- partitionM (\x => isConstr (binderTy (snd x)))
169+ (reverse rest)
170+ return (bindings, constrs, a1, a2)
171+ let todo = [(c1, c2) | c1 <- constructors datatype
172+ , c2 <- constructors datatype]
173+ clauses <- for todo
174+ (uncurry $ mkCase (length bindings + length constrs)
175+ (name datatype))
176+ defineFunction $ DefineFun fn (catMaybes clauses)
177+ skip
178+
179+ where
180+ isConstr : Raw -> Elab Bool
181+ isConstr tm = case headName tm of
182+ Just n => isTCName n
183+ Nothing => return False
184+
185+ partial -- mkRhs
186+ mkCase : Nat -> TTName -> (x, y : (TTName, List CtorArg, Raw)) -> Elab (Maybe FunClause)
187+ mkCase k fam (cn1, args1, _) (cn2, args2, _) =
188+ perhaps $ elabPatternClause
189+ (do (h2 :: h1 :: _) <- reverse <$>
190+ apply (Var fn) (replicate k True ++ [False, False])
191+ solve
192+ focus h1
193+ apply (Var cn1) (replicate (length args1) True)
194+ solve
195+ focus h2
196+ apply (Var cn2) (replicate (length args2) True)
197+ solve)
198+ (mkRhs fn fam k)