git.iko.soy/Idris-dev
on master help sign in
Add disjointness and injectivity automation
9f9be2eDavid Raymond Christiansen
libs/pruviloj/Pruviloj.idr+5
compare with master
unifiedsplit
@@ -1,3 +1,8 @@
1+||| Provides the whole public interface of the proof tools. Import
2+||| `Pruviloj.Core` for just the simplest tactics.
1module Pruviloj
3module Pruviloj
2
4
3import public Pruviloj.Core
5import public Pruviloj.Core
6+import public Pruviloj.Disjoint
7+import public Pruviloj.Induction
8+import public Pruviloj.Injective
libs/pruviloj/Pruviloj/Disjoint.idrnew file+85
@@ -0,0 +1,85 @@
1+||| Provides a tactic for solving constructor disjointness goals.
2+module Pruviloj.Disjoint
3+
4+import Language.Reflection.Utils
5+
6+import Pruviloj.Core
7+import Pruviloj.Internals
8+import Pruviloj.Renamers
9+
10+%default total
11+%access private
12+
13+-------------------
14+-- PRIVATE GUTS --
15+-------------------
16+
17+||| Compute the name to use for a disjointness lemma.
18+disjointName : TTName -> TTName -> TTName
19+disjointName l r = NS (SN (MetaN (UN "disjoint") (SN (MetaN l r))))
20+ ["Disjoint", "Pruviloj"]
21+
22+||| Return the name of the disjointness lemma for two constructors,
23+||| defining it if necessary.
24+|||
25+||| @ l one of the constructor names
26+||| @ r the other constructor name
27+covering
28+getDisjointness : (l, r : TTName) -> Elab TTName
29+getDisjointness l r = exists <|> declare
30+
31+ where exists : Elab TTName
32+ exists = do (yep, _, _) <- lookupTyExact (disjointName l r)
33+ return yep
34+
35+ notConstructor : TTName -> Elab a
36+ notConstructor c = fail [NamePart c, TextPart "is not a constructor"]
37+
38+ covering
39+ 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 !(forgetTypes lty) noRenames
50+ (argsr, resr) <- stealBindings !(forgetTypes 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)
60+ defineFunction $ DefineFun fn []
61+ return fn
62+
63+----------------------
64+-- PUBLIC INTERFACE --
65+----------------------
66+
67+
68+||| Solve a goal of the form `(C1 x1 x2 ... xn = C2 x1 x2 ... xn) ->
69+||| Void` for disjoint constructors `C1` and `C2`.
70+public covering
71+disjoint : Elab ()
72+disjoint =
73+ do compute
74+ g <- snd <$> getGoal
75+ case g of
76+ `(((=) {A=~A} {B=~B} ~a ~b) -> Void) =>
77+ do Just lHead <- headName <$> forgetTypes a
78+ | Nothing => fail [TermPart a, TextPart "doesn't have a name at the head"]
79+ Just rHead <- headName <$> forgetTypes b
80+ | Nothing => fail [TermPart b, TextPart "doesn't have a name at the head"]
81+ [] <- refine (Var !(getDisjointness lHead rHead))
82+ | _ => fail [TextPart "Didn't solve argument to disjointness lemma"]
83+ skip
84+ ty =>
85+ fail [NamePart `{disjoint}, TextPart "is not applicable to goal", TermPart ty]
libs/pruviloj/Pruviloj/Injective.idrnew file+122
@@ -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"]
libs/pruviloj/Pruviloj/Renamers.idr+5−1
@@ -6,6 +6,10 @@ import Language.Reflection.Utils
6Renamer : Type
6Renamer : Type
7Renamer = TTName -> Maybe TTName
7Renamer = TTName -> Maybe TTName
8
8
9+||| A renamer that renames nothing
10+noRenames : Renamer
11+noRenames = const Nothing
12+
9||| Cause a renamer to forget a renaming
13||| Cause a renamer to forget a renaming
10restrict : Renamer -> TTName -> Renamer
14restrict : Renamer -> TTName -> Renamer
11restrict f n n' = if n == n' then Nothing else f n'
15restrict f n n' = if n == n' then Nothing else f n'
@@ -19,7 +23,7 @@ extend f n n' n'' = if n'' == n then Just n' else f n''
19||| @ from the old name
23||| @ from the old name
20||| @ to the new name
24||| @ to the new name
21rename : (from, to : TTName) -> Renamer
25rename : (from, to : TTName) -> Renamer
22−rename from to = extend (const Nothing) from to
26+rename from to = extend noRenames from to
23
27
24||| Alpha-convert `Raw` terms
28||| Alpha-convert `Raw` terms
25||| @ subst a renamer
29||| @ subst a renamer
libs/pruviloj/pruviloj.ipkg+2
@@ -4,7 +4,9 @@ opts = "--nobasepkgs -i ../prelude -i ../base"
4modules = Pruviloj
4modules = Pruviloj
5 , Pruviloj.Core
5 , Pruviloj.Core
6 , Pruviloj.Derive.Eliminators
6 , Pruviloj.Derive.Eliminators
7+ , Pruviloj.Disjoint
7 , Pruviloj.Induction
8 , Pruviloj.Induction
9+ , Pruviloj.Injective
8 , Pruviloj.Internals
10 , Pruviloj.Internals
9 , Pruviloj.Internals.TyConInfo
11 , Pruviloj.Internals.TyConInfo
10 , Pruviloj.Renamers
12 , Pruviloj.Renamers