@@ -0,0 +1,122 @@
1+module Pruviloj.Injective
2+
3+import Language.Reflection.Utils
4+
5+import Pruviloj.Core
6+import Pruviloj.Internals
7+import Pruviloj.Renamers
8+
9+%default total
10+%access private
11+
12+-------------------
13+-- PRIVATE GUTS --
14+-------------------
15+
16+||| Compute the name for a constructor's injectivity lemma
17+injName : TTName -> TTName
18+injName cn = NS (SN (MetaN `{{injectivity}} cn)) ["Injective", "Pruviloj"]
19+
20+||| Provide an error message for when non-constructor names are passed
21+notConstructor : TTName -> Elab a
22+notConstructor c = fail [NamePart c, TextPart "is not a constructor"]
23+
24+covering
25+getInjectivity : (cn : TTName) -> Elab TTName
26+getInjectivity cn = exists <|> declare
27+ where exists : Elab TTName
28+ exists = do (fn, Ref, _) <- lookupTyExact (injName cn)
29+ | (fn, _, _) => fail [TextPart "Bad earlier declaration of", NamePart fn]
30+ return fn
31+
32+ covering
33+ declare : Elab TTName
34+ declare = do (cn', DCon _ _, cty) <- lookupTyExact cn
35+ | _ => notConstructor cn
36+ let fn = injName cn'
37+ (args1, res1) <- stealBindings !(forgetTypes cty) noRenames
38+ (args2, res2) <- stealBindings !(forgetTypes cty) noRenames
39+ let impls1 = map (\(n, b) => MkFunArg n (binderTy b) Implicit NotErased)
40+ args1
41+ let impls2 = map (\(n, b) => MkFunArg n (binderTy b) Implicit NotErased)
42+ args2
43+ let res = foldr (\t1, t2 => RApp (RApp (Var `{Pair}) t1) t2)
44+ `(() : Type)
45+ (map (\(a1, a2) =>
46+ `((=) {A=~(argTy a1)}
47+ {B=~(argTy a2)}
48+ ~(Var (argName a1))
49+ ~(Var (argName a2))))
50+ (zip impls1 impls2))
51+
52+ declareType $ Declare fn (impls1 ++ impls2 ++
53+ [ MkFunArg !(gensym "arg")
54+ `((=) {A=~res1}
55+ {B=~res2}
56+ ~(mkApp (Var cn)
57+ (map (Var . fst) args1))
58+ ~(mkApp (Var cn)
59+ (map (Var . fst) args2)))
60+ Explicit
61+ NotErased])
62+
63+ res
64+ clause <- elabPatternClause
65+ (do ((_, h)::_) <- reverse <$>
66+ apply (Var fn)
67+ (replicate (2 * length args1)
68+ (True, 0) ++
69+ [(False, 0)])
70+ | _ => fail [TextPart "Missing hole"]
71+ solve
72+ focus h; search)
73+ search -- rhs is conjunction of Refls
74+ defineFunction $
75+ DefineFun fn [clause]
76+ return fn
77+
78+countBinders : TT -> Nat
79+countBinders (Bind _ _ body) = S (countBinders body)
80+countBinders _ = Z
81+
82+
83+----------------------
84+-- PUBLIC INTERFACE --
85+----------------------
86+
87+
88+||| Given an equality of the form `(C x1 ... xn = C y1 ... yn)`,
89+||| generate an product of the equalities `(x1 = y1)` ... `(xn = yn)`.
90+|||
91+||| The equalities are let-bound to the provided name.
92+|||
93+||| @ tm the equality to exploit injectivity on
94+||| @ n the name at which to bind the result
95+covering public
96+injective : (tm : Raw) -> (n : TTName) -> Elab ()
97+injective tm n =
98+ do (_, ty) <- check tm
99+ case !(forgetTypes ty) of
100+ `((=) {A=~A} {B=~B} ~x ~y) =>
101+ case (headName x, headName y) of
102+ (Just xHd, Just yHd) =>
103+ if xHd /= yHd
104+ then fail [ TextPart "Mismatch between", NamePart xHd
105+ , TextPart "and", NamePart yHd
106+ ]
107+ else do fn <- getInjectivity xHd
108+ tyH <- newHole "ty" `(Type)
109+ tmH <- newHole "tm" (Var tyH)
110+
111+ letbind n (Var tyH) (Var tmH)
112+ focus tmH
113+ (_, _, fnTy) <- lookupTyExact fn
114+
115+ ((_, arg) :: _) <- reverse <$> apply (Var fn) (replicate (pred (countBinders fnTy)) (True, 0) ++ [(False,0)])
116+ | _ => fail [TextPart "No hole for argument"]
117+ solve
118+
119+ focus arg; apply tm []; solve
120+ _ => fail [TextPart "oops"]
121+
122+ _ => fail [TextPart "can't use injectivity on non-equality"]