@@ -19,6 +19,34 @@ disjointName : TTName -> TTName -> TTName
1919disjointName l r = NS (SN (MetaN (UN "disjoint") (SN (MetaN l r))))
2020 ["Disjoint", "Pruviloj"]
2121
22+||| Compute the type to use for a disjointness lemma.
23+covering
24+disjointnessType : (l, r : TTName) -> Elab (TTName, List FunArg, Raw)
25+disjointnessType l r =
26+ do (l', DCon _ _, lty) <- lookupTyExact l
27+ | _ => notConstructor l
28+ (r', DCon _ _, rty) <- lookupTyExact r
29+ | _ => notConstructor r
30+ let fn = disjointName l' r'
31+ when (l' == r') $
32+ fail [ NamePart l', TextPart "and"
33+ , NamePart r', TextPart "are clearly not disjoint!"
34+ ]
35+ (argsl, resl) <- stealBindings !(forget lty) noRenames
36+ (argsr, resr) <- stealBindings !(forget rty) noRenames
37+ let args = map {b=FunArg}
38+ (\(n, b) => MkFunArg n (binderTy b) Implicit NotErased)
39+ (argsl ++ argsr)
40+ let eq : Raw = `((=) {A=~resl}
41+ {B=~resr}
42+ ~(mkApp (Var l') (map (Var . fst) argsl))
43+ ~(mkApp (Var r') (map (Var . fst) argsr)))
44+ h <- gensym "h"
45+ pure (fn, args ++ [MkFunArg h eq Explicit NotErased], `(Void))
46+ where
47+ notConstructor : TTName -> Elab a
48+ notConstructor c = fail [NamePart c, TextPart "is not a constructor"]
49+
2250||| Return the name of the disjointness lemma for two constructors,
2351||| defining it if necessary.
2452|||
@@ -27,36 +55,13 @@ disjointName l r = NS (SN (MetaN (UN "disjoint") (SN (MetaN l r))))
2755covering
2856getDisjointness : (l, r : TTName) -> Elab TTName
2957getDisjointness l r = exists <|> declare
30−
3158 where exists : Elab TTName
3259 exists = do (yep, _, _) <- lookupTyExact (disjointName l r)
3360 pure yep
34−
35− notConstructor : TTName -> Elab a
36− notConstructor c = fail [NamePart c, TextPart "is not a constructor"]
37−
3861 covering
3962 declare : Elab TTName
40− declare = do (l', DCon _ _, lty) <- lookupTyExact l
41− | _ => notConstructor l
42− (r', DCon _ _, rty) <- lookupTyExact r
43− | _ => notConstructor r
44− let fn = disjointName l' r'
45− when (l' == r') $
46− fail [ NamePart l', TextPart "and"
47− , NamePart r', TextPart "are clearly not disjoint!"
48− ]
49− (argsl, resl) <- stealBindings !(forget lty) noRenames
50− (argsr, resr) <- stealBindings !(forget rty) noRenames
51− let args = map {b=FunArg}
52− (\(n, b) => MkFunArg n (binderTy b) Implicit NotErased)
53− (argsl ++ argsr)
54− let eq : Raw = `((=) {A=~resl}
55− {B=~resr}
56− ~(mkApp (Var l') (map (Var . fst) argsl))
57− ~(mkApp (Var r') (map (Var . fst) argsr)))
58− h <- gensym "h"
59− declareType $ Declare fn (args ++ [MkFunArg h eq Explicit NotErased]) `(Void)
63+ declare = do (fn, args, ret) <- disjointnessType l r
64+ declareType $ Declare fn args ret
6065 defineFunction $ DefineFun fn []
6166 pure fn
6267
@@ -83,3 +88,38 @@ disjoint =
8388 skip
8489 ty =>
8590 fail [NamePart `{disjoint}, TextPart "is not applicable to goal", TermPart ty]
91+
92+||| Solve a goal when there is an hypothesis of the form
93+||| `(C1 x1 x2 ... xn = C2 x1 x2 ... xn)`
94+||| for disjoint constructors `C1` and `C2`.
95+||| Similar to `discriminate` in Coq.
96+public export covering
97+discriminate : Elab ()
98+discriminate =
99+ do compute
100+ g <- goalType
101+ -- for each thing in the context, until we find one that succeeds
102+ flip choiceMap !getEnv $ \(n, b) =>
103+ do -- 1) check if it is an equality
104+ `(((=) {A=~A} {B=~B} ~a ~b)) <- forget (binderTy b)
105+ | _ => fail [TextPart "Not equality type"]
106+ -- 2) check if both sides of the equality have heads
107+ case (headName a, headName b) of
108+ (Just lHead, Just rHead) =>
109+ do lemma <- Var <$> getDisjointness lHead rHead
110+ -- 3) learn how many arguments the lemma takes
111+ (_, x :: xs, _) <- disjointnessType lHead rHead
112+ | _ => fail [TextPart "Disjointness type takes no argument"]
113+ -- 4) try to apply and focus on the last hole
114+ apply `(void {a=~g}) [False]
115+ solve
116+ -- 5) try to call the disjointness lemma
117+ -- We only want to pass the last arg explicitly to the lemma
118+ let bools = map (const True) xs ++ [False]
119+ (h :: hs) <- apply lemma bools
120+ | _ => fail [TextPart "Disjointness lemma produces no holes"]
121+ solve
122+ -- 6) try to pass the current equality as an argument
123+ focus (last (h :: hs))
124+ exact (Var n)
125+ _ => fail [TextPart "Equality sides don't have a name at the head"]