git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2649 from david-christiansen/pruviloj

Library of tactics for proof automation with Elab

commitb9a7e941634847a4cbffeddec2ef20dbb7ecafac authorDavid Christiansen <david@davidchristiansen.dk> dateFri 25 Sep 2015, 16:38 (11 years ago) parent928aed4a6c5150
16 files changed+1064−1
compare with master
unifiedsplit
idris.cabal+11 libs/Makefile+6−1 libs/prelude/Prelude/Applicative.idr+4 libs/pruviloj/Makefile+21 libs/pruviloj/Pruviloj.idr+3 libs/pruviloj/Pruviloj/Core.idr+144 libs/pruviloj/Pruviloj/Derive/Eliminators.idr+274 libs/pruviloj/Pruviloj/Induction.idr+162 libs/pruviloj/Pruviloj/Internals.idr+158 libs/pruviloj/Pruviloj/Internals/TyConInfo.idr+108 libs/pruviloj/Pruviloj/Renamers.idr+39 libs/pruviloj/README.txt+44 libs/pruviloj/pruviloj.ipkg+10 test/pruviloj001/expected test/pruviloj001/pruviloj001.idr+77 test/pruviloj001/run+3
idris.cabal+11
@@ -143,6 +143,13 @@ Extra-source-files:
143143 libs/effects/Effect/Logging/*.idr
144144 libs/effects/*.idr
145145
146+ libs/pruviloj/Makefile
147+ libs/pruviloj/pruviloj.ipkg
148+ libs/pruviloj/*.idr
149+ libs/pruviloj/Pruviloj/*.idr
150+ libs/pruviloj/Pruviloj/Derive/*.idr
151+ libs/pruviloj/Pruviloj/Internals/*.idr
152+
146153 test/Makefile
147154 test/runtest.pl
148155 test/reg001/run
@@ -602,6 +609,10 @@ Extra-source-files:
602609 test/proofsearch003/*.idr
603610 test/proofsearch003/expected
604611
612+ test/pruviloj001/run
613+ test/pruviloj001/*.idr
614+ test/pruviloj001/expected
615+
605616 test/quasiquote001/run
606617 test/quasiquote001/*.idr
607618 test/quasiquote001/expected
libs/Makefile+6−1
@@ -3,6 +3,7 @@ build:
33 $(MAKE) -C base build
44 $(MAKE) -C contrib build
55 $(MAKE) -C effects build
6+ $(MAKE) -C pruviloj build
67
78
89install:
@@ -10,24 +11,28 @@ install:
1011 $(MAKE) -C base install
1112 $(MAKE) -C contrib install
1213 $(MAKE) -C effects install
14+ $(MAKE) -C pruviloj install
1315
1416clean:
1517 $(MAKE) -C prelude clean
1618 $(MAKE) -C base clean
1719 $(MAKE) -C contrib clean
1820 $(MAKE) -C effects clean
21+ $(MAKE) -C pruviloj clean
1922
2023doc:
2124 $(MAKE) -C prelude doc
2225 $(MAKE) -C base doc
2326 $(MAKE) -C contrib doc
2427 $(MAKE) -C effects doc
28+ $(MAKE) -C pruviloj doc
2529
2630doc_clean:
2731 $(MAKE) -C prelude doc_clean
2832 $(MAKE) -C base doc_clean
2933 $(MAKE) -C contrib doc_clean
30− $(MAKE) -C effects doc_clean
34+ $(MAKE) -C effects doc_clean
35+ $(MAKE) -C pruviloj doc_clean
3136
3237
3338.PHONY: build install clean doc doc_clean
libs/prelude/Prelude/Applicative.idr+4
@@ -72,3 +72,7 @@ when False f = pure ()
7272||| Note: In Haskell, `choice` is called `asum`.
7373choice : (Foldable t, Alternative f) => t (f a) -> f a
7474choice x = foldr (<|>) empty x
75+
76+||| A fused version of choice and map.
77+choiceMap : (Foldable t, Alternative f) => (a -> f b) -> t a -> f b
78+choiceMap f x = foldr (\elt, acc => f elt <|> acc) empty x
libs/pruviloj/Makefilenew file+21
@@ -0,0 +1,21 @@
1+IDRIS := idris
2+PKG := pruviloj
3+
4+build:
5+ $(IDRIS) --build ${PKG}.ipkg
6+
7+clean:
8+ $(IDRIS) --clean ${PKG}.ipkg
9+
10+install:
11+ $(IDRIS) --install ${PKG}.ipkg
12+
13+rebuild: clean build
14+
15+doc:
16+ $(IDRIS) --mkdoc ${PKG}.ipkg
17+
18+doc_clean:
19+ rm -rf ${PKG}_doc
20+
21+.PHONY: build clean install rebuild doc doc_clean
libs/pruviloj/Pruviloj.idrnew file+3
@@ -0,0 +1,3 @@
1+module Pruviloj
2+
3+import public Pruviloj.Core
libs/pruviloj/Pruviloj/Core.idrnew file+144
@@ -0,0 +1,144 @@
1+||| Core tactics for working with Elab reflection. These will be used
2+||| by most reasonable scripts, and they may be candidates for
3+||| eventual Prelude inclusion.
4+module Pruviloj.Core
5+
6+
7+import Language.Reflection.Elab
8+import Language.Reflection.Utils
9+
10+data Infer : Type where
11+ MkInfer : (a : Type) -> a -> Infer
12+
13+||| Run something for effects, throwing away the return value
14+ignore : Functor f => f a -> f ()
15+ignore x = map (const ()) x
16+
17+||| Do nothing
18+skip : Applicative f => f ()
19+skip = pure ()
20+
21+||| Attempt to apply a tactic. If it fails, do nothing.
22+try : Alternative f => f a -> f ()
23+try tac = ignore tac <|> pure ()
24+
25+||| Solve the goal using the most recent applicable hypothesis
26+hypothesis : Elab ()
27+hypothesis =
28+ do hyps <- map fst <$> getEnv
29+ flip choiceMap hyps $ \n =>
30+ do fill (Var n)
31+ solve
32+
33+
34+||| Generate a unique name (using `gensym`) that looks like some
35+||| previous name, for ease of debugging code generators.
36+nameFrom : TTName -> Elab TTName
37+nameFrom (UN x) =
38+ gensym $ if length x == 0 || ("_" `isPrefixOf` x)
39+ then "x"
40+ else x
41+nameFrom (NS n ns) =
42+ nameFrom n -- throw out namespaces here, because we want to
43+ -- generate bound var names
44+nameFrom (MN x n) =
45+ gensym $ if length n == 0 || ("_" `isPrefixOf` n)
46+ then "n"
47+ else n
48+nameFrom (SN x) = gensym "SN"
49+nameFrom NErased = gensym "wasErased"
50+
51+||| Get the name at the head of the term, if it exists.
52+headName : Raw -> Maybe TTName
53+headName (RApp f _) = headName f
54+headName (Var n) = Just n
55+headName x = Nothing
56+
57+||| Create a new hole with a given type without changing the
58+||| focus. Return the name of the hole.
59+|||
60+||| @ hint the hint to pass to `gensym`
61+||| @ ty the type of the new hole
62+newHole : (hint : String) -> (ty : Raw) -> Elab TTName
63+newHole hint ty =
64+ do hn <- gensym hint
65+ claim hn ty
66+ return hn
67+
68+||| Use a term to solve a hole
69+|||
70+||| @ tm the term that has the right type for the hole
71+exact : (tm : Raw) -> Elab ()
72+exact tm = do apply tm []
73+ solve
74+
75+||| Introduce as many names as possible, returning them.
76+intros : Elab (List TTName)
77+intros = do g <- snd <$> getGoal
78+ go g
79+ where go : TT -> Elab (List TTName)
80+ go (Bind n (Pi _ _) body) =
81+ do n' <- nameFrom n
82+ intro n'
83+ (n' ::) <$> go body
84+ go _ = return []
85+
86+||| Run a tactic inside of a particular hole, if it still exists. If
87+||| it has been solved, do nothing.
88+inHole : TTName -> Elab () -> Elab ()
89+inHole h todo =
90+ when (h `elem` !getHoles) $
91+ do focus h
92+ todo
93+
94+||| Restrict a polymorphic type to () for contexts where it doesn't
95+||| matter. This is nice for sticking `debug` in a context where
96+||| Idris can't solve the type.
97+simple : {m : Type -> Type} -> m () -> m ()
98+simple x = x
99+
100+||| Replace the current goal with one that's definitionally
101+||| equal. Return the name of the new goal, and ensure that it's
102+||| focused.
103+|||
104+||| @ newGoal A type that is equivalent to the current goal
105+equiv : (newGoal : Raw) -> Elab TTName
106+equiv newGoal =
107+ do h <- gensym "goal"
108+ claim h newGoal
109+ fill (Var h); solve
110+ focus h
111+ return h
112+
113+||| Remember a term built with elaboration for later use. If the
114+||| current goal is `h`, then `remember n ty` puts a fresh hole at
115+||| the front of the queue, with the old goal `h` second. The
116+||| contents of this hole end up let-bound in the scope of
117+||| `h`. Return the name of the new hole, in case it will be used
118+||| later.
119+|||
120+||| @ n the name to be used to save the term
121+||| @ ty the type to inhabit
122+remember : (n : TTName) -> (ty : Raw) -> Elab TTName
123+remember n ty =
124+ do todo <- gensym "rememberThis"
125+ claim todo ty
126+ letbind n ty (Var todo)
127+ focus todo
128+ return todo
129+
130+||| Repeat a given tactic until it fails. Fails if the tactic fails on
131+||| the first attempt; succeeds otherwise.
132+repeatUntilFail : Elab () -> Elab ()
133+repeatUntilFail tac =
134+ do tac
135+ repeatUntilFail tac <|> return ()
136+
137+||| If the current goal is a pattern-bound variable, bind it with the
138+||| expected name. Otherwise fail.
139+bindPat : Elab ()
140+bindPat = do compute
141+ g <- snd <$> getGoal
142+ case g of
143+ Bind n (PVTy _) _ => patbind n
144+ _ => fail [TermPart g, TextPart "isn't looking for a pattern."]
libs/pruviloj/Pruviloj/Derive/Eliminators.idrnew file+274
@@ -0,0 +1,274 @@
1+module Pruviloj.Derive.Eliminators
2+
3+import Language.Reflection.Utils
4+import Data.Vect
5+
6+import Pruviloj.Core
7+import Pruviloj.Internals.TyConInfo
8+import Pruviloj.Internals
9+import Pruviloj.Renamers
10+
11+
12+%access private
13+
14+bindParams : TyConInfo -> Elab ()
15+bindParams info = traverse_ (uncurry forall) (getParams info)
16+
17+||| Bind indices at new names and return a renamer that's used to
18+||| rewrite an application of something to their designated global
19+||| names
20+bindIndices : TyConInfo -> Elab Renamer
21+bindIndices info = bind' (getIndices info) (const Nothing)
22+ where bind' : List (TTName, Raw) -> Renamer -> Elab Renamer
23+ bind' [] ren = return ren
24+ bind' ((n, t) :: ixs) ren = do n' <- nameFrom n
25+ forall n' (alphaRaw ren t)
26+ bind' ixs (extend ren n n')
27+
28+||| Return the renaming required to use the result type for this
29+||| binding of the indices
30+bindTarget : TyConInfo -> Elab (TTName, Renamer)
31+bindTarget info = do ren <- bindIndices info
32+ tn <- gensym "target"
33+ forall tn (alphaRaw ren $ result info)
34+ return (tn, ren)
35+
36+elabMotive : TyConInfo -> Elab ()
37+elabMotive info = do attack
38+ ren <- bindIndices info
39+ x <- gensym "scrutinee"
40+ forall x (alphaRaw ren $ result info)
41+ fill `(Type)
42+ solve -- the attack
43+ solve -- the motive type hole
44+
45+
46+
47+
48+headsMatch : Raw -> Raw -> Bool
49+headsMatch x y =
50+ case (headName x, headName y) of
51+ (Just n1, Just n2) => n1 == n2
52+ _ => False
53+
54+||| Make an induction hypothesis if one is called for
55+mkIh : TyConInfo -> (motiveName : TTName) -> (recArg : TTName) -> (argty, fam : Raw) -> Elab ()
56+mkIh info motiveName recArg argty fam =
57+ case !(stealBindings argty (const Nothing)) of
58+ (argArgs, argRes) =>
59+ if headsMatch argRes fam
60+ then do ih <- gensym "ih"
61+ ihT <- newHole "ihT" `(Type)
62+ forall ih (Var ihT)
63+ focus ihT
64+ attack
65+ for_ {b=()} argArgs $ \(n, b) =>
66+ forall n (getBinderTy b)
67+ let argTm : Raw = mkApp (Var recArg) (map (Var . fst) argArgs)
68+ argTmTy <- forgetTypes (snd !(check argTm))
69+ argHoles <- apply (Var motiveName)
70+ (replicate (length (getIndices info))
71+ (True, 0) ++
72+ [(False,1)])
73+ argH <- snd <$> last argHoles
74+ focus argH
75+ fill argTm; solve
76+ solve -- attack
77+ solve -- ihT
78+ else return ()
79+
80+elabMethodTy : TyConInfo -> TTName -> List CtorArg -> Raw -> Raw -> Elab ()
81+elabMethodTy info motiveName [] res ctorApp =
82+ do argHoles <- apply (Var motiveName)
83+ (replicate (length (getIndices info)) (True, 0) ++
84+ [(False, 1)])
85+ argH <- snd <$> last argHoles
86+ focus argH; fill ctorApp; solve
87+ solve
88+elabMethodTy info motiveName (CtorParameter arg :: args) res ctorApp =
89+ elabMethodTy info motiveName args res (RApp ctorApp (Var (argName arg)))
90+elabMethodTy info motiveName (CtorField arg :: args) res ctorApp =
91+ do let n = argName arg
92+ let t = argTy arg
93+ attack; forall n t
94+ mkIh info motiveName n t (result info)
95+ elabMethodTy info motiveName args res (RApp ctorApp (Var n))
96+ solve
97+
98+
99+
100+elabMethod : TyConInfo -> (motiveName, ctorN : TTName) -> List CtorArg -> Raw -> Elab ()
101+elabMethod info motiveName ctorN ctorArgs resTy =
102+ do elabMethodTy info motiveName ctorArgs resTy (Var ctorN)
103+
104+
105+||| Bind a method for a constructor
106+bindMethod : TyConInfo -> (motiveName, cn : TTName) -> List CtorArg -> Raw -> Elab ()
107+bindMethod info motiveName cn cargs cty =
108+ do n <- nameFrom cn
109+ h <- newHole "methTy" `(Type)
110+ forall n (Var h)
111+ focus h; elabMethod info motiveName cn cargs cty
112+
113+getElimTy : TyConInfo -> List (TTName, List CtorArg, Raw) -> Elab Raw
114+getElimTy info ctors =
115+ do ty <- runElab `(Type) $
116+ do bindParams info
117+ (scrut, iren) <- bindTarget info
118+ motiveN <- gensym "P"
119+ motiveH <- newHole "motive" `(Type)
120+ forall motiveN (Var motiveH)
121+ focus motiveH
122+ elabMotive info
123+
124+ for_ {b=()} ctors $ \(cn, cargs, cresty) =>
125+ bindMethod info motiveN cn cargs cresty
126+ let ret = mkApp (Var motiveN)
127+ (map (Var . fst)
128+ (getIndices info) ++
129+ [Var scrut])
130+ apply (alphaRaw iren ret) []
131+ solve
132+ forgetTypes (fst ty)
133+
134+
135+
136+data ElimArg = IHArgument TTName | NormalArgument TTName
137+
138+instance Show ElimArg where
139+ show (IHArgument x) = "IHArgument " ++ show x
140+ show (NormalArgument x) = "NormalArgument " ++ show x
141+
142+getElimClause : TyConInfo -> (elimn : TTName) -> (methCount : Nat) ->
143+ (TTName, List CtorArg, Raw) -> Nat -> Elab FunClause
144+getElimClause info elimn methCount (cn, args, resTy) whichCon =
145+ elabPatternClause
146+ (do -- Establish a hole for each parameter
147+ for (getParams info) {b=()} $ \(n, ty) =>
148+ do claim n ty
149+ unfocus n
150+
151+
152+ -- Establish a hole for each argument to the constructor
153+ for {b=()} args $ \arg =>
154+ case arg of
155+ CtorParameter _ => return ()
156+ CtorField arg => do claim (argName arg) (argTy arg)
157+ unfocus (argName arg)
158+
159+ -- Establish a hole for the scrutinee (infer type)
160+ scrutinee <- newHole "scrutinee" resTy
161+
162+
163+ -- Apply the eliminator to the proper holes
164+ let paramApp : Raw = mkApp (Var elimn) $
165+ map (Var . fst) (getParams info)
166+
167+ -- We leave the RHS with a function type: motive -> method* -> res
168+ -- to make it easier to map methods to constructors
169+ holes <- apply paramApp (replicate (length (getIndices info))
170+ (True, 0) ++
171+ [(False, 1)])
172+ scr <- snd <$> last holes
173+ focus scr; fill (Var scrutinee); solve
174+ solve
175+
176+ -- Fill the scrutinee with the concrete constructor pattern
177+ focus scrutinee
178+ apply (mkApp (Var cn) $
179+ map (\x => case x of
180+ CtorParameter param => Var (argName param)
181+ CtorField arg => Var (argName arg))
182+ args)
183+ []
184+ solve)
185+ (do motiveN <- gensym "motive"
186+ intro motiveN
187+ prevMethods <- doTimes whichCon intro1
188+ methN <- gensym "useThisMethod"
189+ intro methN
190+ nextMethods <- intros
191+
192+ argSpec <- Foldable.concat <$>
193+ for args
194+ (\x =>
195+ case x of
196+ CtorParameter _ => return List.Nil
197+ CtorField arg =>
198+ do let n = argName arg
199+ let t = argTy arg
200+ (argArgs, argRes) <- stealBindings t (const Nothing)
201+ if headsMatch argRes (result info) --recursive
202+ then return [ NormalArgument n
203+ , IHArgument n
204+ ]
205+ else return [NormalArgument n])
206+
207+ argHs <- apply (Var methN) (replicate (List.length argSpec) (True, 0))
208+ solve
209+
210+ -- Now build the recursive calls for the induction hypotheses
211+ for_ {a=(ElimArg, TTName)} {b=()}
212+ !(zipH argSpec (map snd argHs))
213+ (\(spec, nh) =>
214+ case spec of
215+ NormalArgument n => do focus nh
216+ apply (Var n) []
217+ solve
218+ IHArgument n =>
219+ do focus nh
220+ attack
221+ local <- intros
222+ ihHs <- apply (Var elimn) $
223+ replicate (length (TyConInfo.args info)) (True, 0) ++
224+ [(False, 1)] ++
225+ replicate (S methCount) (True, 0)
226+ solve -- application
227+
228+ let (arg::motive::methods) = map snd $ drop (length (TyConInfo.args info)) ihHs
229+ focus arg
230+
231+ apply (mkApp (Var n) (map Var local)) []; solve
232+ solve -- attack
233+
234+
235+ focus motive; fill (Var motiveN); solve
236+ let methodArgs : List TTName = toList prevMethods ++ [methN] ++ nextMethods
237+ remaining <- zipH methods methodArgs
238+
239+ for_ {b=()} remaining $ \todo =>
240+ do focus (fst todo)
241+ fill (Var (snd todo))
242+ solve))
243+
244+
245+
246+ where bindLam : List (TTName, Binder Raw) -> Raw -> Raw
247+ bindLam [] x = x
248+ bindLam ((n, b)::rest) x = RBind n (Lam (getBinderTy b)) $ bindLam rest x
249+
250+getElimClauses : TyConInfo -> (elimn : TTName) ->
251+ List (TTName, List CtorArg, Raw) -> Elab (List FunClause)
252+getElimClauses info elimn ctors =
253+ let methodCount = length ctors
254+ in traverse (\(i, con) => getElimClause info elimn methodCount con i)
255+ (enumerate ctors)
256+
257+instance Show FunClause where
258+ show (MkFunClause x y) = "(MkFunClause " ++ show x ++ " " ++ show y ++ ")"
259+
260+abstract
261+deriveElim : (tyn, elimn : TTName) -> Elab ()
262+deriveElim tyn elimn =
263+ do -- Begin with some basic sanity checking: the type name uniquely
264+ -- determines a datatype
265+ (MkDatatype tyn tyconArgs tyconRes ctors') <- lookupDatatypeExact tyn
266+
267+ info <- getTyConInfo tyconArgs (Var tyn)
268+ ctors <- traverse (processCtorArgs info) ctors'
269+ declareType $ Declare elimn [] !(getElimTy info ctors)
270+ clauses <- getElimClauses info elimn ctors
271+
272+ defineFunction $ DefineFun elimn clauses
273+ return ()
274+
libs/pruviloj/Pruviloj/Induction.idrnew file+162
@@ -0,0 +1,162 @@
1+module Pruviloj.Induction
2+
3+import Language.Reflection.Utils
4+
5+import Pruviloj.Core
6+import Pruviloj.Derive.Eliminators
7+import Pruviloj.Internals.TyConInfo
8+import Pruviloj.Internals
9+import Pruviloj.Renamers
10+
11+
12+%access private
13+
14+-- To perform induction:
15+-- 1. Type check the thing to do induction on
16+-- 2. If its type is not an inductive family, error
17+-- 3. Ensure that there exists an eliminator for the family
18+-- 4. Abstract the goal over the scrutinee to get the motive
19+-- 5. Apply the eliminator to the scrutinee and motive, with holes for methods
20+-- 6. Return these holes
21+
22+
23+elimN : TTName -> TTName
24+elimN n = NS (SN $ MetaN (UN "elim") n) ["Eliminators", "Induction", "Pruviloj"]
25+
26+mutual
27+ alphaEqual : (subst : TTName -> Maybe TTName) -> Raw -> Raw -> Bool
28+ alphaEqual subst (Var n) (Var m) =
29+ case subst n of
30+ Just n' => n' == m -- both are bound if this has been put in the subst
31+ Nothing => n == m -- free
32+ alphaEqual subst (RBind n b tm) (RBind m b' tm') =
33+ alphaEqualBinders subst b b' &&
34+ alphaEqual (extend subst n m) tm tm'
35+ alphaEqual subst (RApp f x) (RApp g y) =
36+ alphaEqual subst f g && alphaEqual subst x y
37+ alphaEqual subst RType RType = True
38+ alphaEqual subst (RUType u) (RUType u') = u == u'
39+ alphaEqual subst (RForce tm) (RForce tm') = alphaEqual subst tm tm'
40+ alphaEqual subst (RConstant c) (RConstant c') = c == c'
41+ alphaEqual subst _ _ = False
42+
43+ alphaEqualBinders : (subst : TTName -> Maybe TTName) -> Binder Raw -> Binder Raw -> Bool
44+ alphaEqualBinders subst (Lam tm) (Lam tm') =
45+ alphaEqual subst tm tm'
46+ alphaEqualBinders subst (Pi tm1 tm2) (Pi tm1' tm2') =
47+ alphaEqual subst tm1 tm1' &&
48+ alphaEqual subst tm2 tm2'
49+ alphaEqualBinders subst (Let tm1 tm2) (Let tm1' tm2') =
50+ alphaEqual subst tm1 tm1' &&
51+ alphaEqual subst tm2 tm2'
52+ alphaEqualBinders subst (NLet tm1 tm2) (NLet tm1' tm2') =
53+ alphaEqual subst tm1 tm1' &&
54+ alphaEqual subst tm2 tm2'
55+ alphaEqualBinders subst (Hole tm) (Hole tm') =
56+ alphaEqual subst tm tm'
57+ alphaEqualBinders subst (GHole tm) (GHole tm') =
58+ alphaEqual subst tm tm'
59+ alphaEqualBinders subst (Guess tm1 tm2) (Guess tm1' tm2') =
60+ alphaEqual subst tm1 tm1' &&
61+ alphaEqual subst tm2 tm2'
62+ alphaEqualBinders subst (PVar tm) (PVar tm') =
63+ alphaEqual subst tm tm'
64+ alphaEqualBinders subst (PVTy tm) (PVTy tm') =
65+ alphaEqual subst tm tm'
66+ alphaEqualBinders subst _ _ = False
67+
68+generalize : (hint : String) -> (ctxt, subject : Raw) -> Elab (TTName, Raw)
69+generalize hint ctxt subj = do n <- gensym hint
70+ return (n, !(gen' n ctxt subj))
71+ where
72+ mutual
73+ gen' : TTName -> Raw -> Raw -> Elab Raw
74+ gen' var outer inner = if alphaEqual (const Nothing) outer inner
75+ then return (Var var)
76+ else breakAndRecurse var outer inner
77+
78+ genB : TTName -> Binder Raw -> Raw -> Elab (Binder Raw)
79+ genB n (Lam ty) inner = [| Lam (gen' n ty inner) |]
80+ genB n (Pi ty ty') inner = [| Pi (gen' n ty inner) (gen' n ty' inner) |]
81+ genB n (Let ty val) inner = [| Let (gen' n ty inner) (gen' n val inner) |]
82+ genB n (NLet ty val) inner = [| NLet (gen' n ty inner) (gen' n val inner) |]
83+ genB n (Hole ty) inner = [| Hole (gen' n ty inner) |]
84+ genB n (GHole ty) inner = [| GHole (gen' n ty inner) |]
85+ genB n (Guess ty val) inner = [| Guess (gen' n ty inner) (gen' n val inner) |]
86+ genB n (PVar ty) inner = [| PVar (gen' n ty inner) |]
87+ genB n (PVTy ty) inner = [| PVTy (gen' n ty inner) |]
88+
89+ breakAndRecurse : TTName -> Raw -> Raw -> Elab Raw
90+ breakAndRecurse var (RBind n b tm) inner =
91+ -- Prevent variable capture by alpha-converting to a unique name
92+ do n' <- nameFrom n
93+ b' <- genB var b inner
94+ body' <- gen' var (alphaRaw (rename n n') tm) inner
95+ return $ RBind n' b' body'
96+ breakAndRecurse var (RApp tm tm') inner =
97+ [| RApp (gen' var tm inner) (gen' var tm' inner) |]
98+ breakAndRecurse var other inner = return other
99+
100+
101+countBinders : TT -> Nat
102+countBinders (Bind _ _ tm) = S (countBinders tm)
103+countBinders _ = Z
104+
105+
106+
107+indexVals : Raw -> TyConInfo -> List Raw
108+indexVals tm info =
109+ do let (var, tyArgs) = unApply tm
110+ let argsTogether = zip tyArgs (args info)
111+ (argVal, TyConIndex _) <- argsTogether
112+ | _ => empty
113+ return argVal
114+
115+makeMotive : (info : TyConInfo) -> (subj, subjTy, goal : Raw) -> Elab ()
116+makeMotive info sub subjTy goal =
117+ makeMotive' (indexVals subjTy info) goal
118+ where
119+ makeMotive' : List Raw -> Raw -> Elab ()
120+ makeMotive' [] r = do (n, r') <- generalize "subj" r sub
121+ attack
122+ intro n
123+ exact r'
124+ solve -- attack
125+ makeMotive' (i :: is) r = do (n, r') <- generalize "i" r i
126+ attack
127+ intro n
128+ makeMotive' is r'
129+ solve --attack
130+
131+||| Perform induction on some expression to solve the current
132+||| goal. Return a list of new holes to be solved.
133+public
134+induction : Raw -> Elab (List TTName)
135+induction subj =
136+ do g <- goalType
137+ (_, ty) <- check subj
138+ ty' <- forgetTypes ty
139+ case headName ty' of
140+ Nothing => fail [TermPart ty, TextPart "is not an inductive family"]
141+ Just fam =>
142+ do let elim = elimN fam
143+ (_,_,elimTy) <- (lookupTyExact elim) <|> (do deriveElim fam elim
144+ lookupTyExact elim)
145+ tydef <- lookupDatatypeExact fam
146+ info <- getTyConInfo (tyConArgs tydef) (tyConRes tydef)
147+ argHoles <- apply (Var elim)
148+ (replicate (length (args info)) (True, 0) ++
149+ [(False, 0), (False, 0)] ++ -- scrutinee, motive
150+ replicate (length (constructors tydef)) (False, 1))
151+ solve
152+
153+ -- Apply the eliminator to our scrutinee
154+ scrutH <- snd <$> unsafeNth (length (args info)) argHoles
155+ focus scrutH
156+ apply subj []
157+ solve
158+
159+ motiveH <- snd <$> unsafeNth (length (args info) + 1) argHoles
160+ focus motiveH; makeMotive info subj ty' g
161+
162+ return (map snd (drop (2 + length (tyConArgs tydef)) argHoles))
libs/pruviloj/Pruviloj/Internals.idrnew file+158
@@ -0,0 +1,158 @@
1+||| Internal details of the library, not for public consumption.
2+module Pruviloj.Internals
3+
4+
5+import Pruviloj.Core
6+import Pruviloj.Renamers
7+
8+import Data.Vect
9+
10+||| Get the name of a reflected type constructor argument.
11+tyConArgName : TyConArg -> TTName
12+tyConArgName (TyConParameter a) = argName a
13+tyConArgName (TyConIndex a) = argName a
14+
15+||| Modify the name of a reflected type constructor argument.
16+setTyConArgName : TyConArg -> TTName -> TyConArg
17+setTyConArgName (TyConParameter a) n = TyConParameter (record {argName = n} a)
18+setTyConArgName (TyConIndex a) n = TyConIndex (record {argName = n} a)
19+
20+||| Modify the type of a reflected type constructor argument using some function.
21+updateTyConArgTy : (Raw -> Raw) -> TyConArg -> TyConArg
22+updateTyConArgTy f (TyConParameter a) =
23+ TyConParameter (record {argTy = f (argTy a) } a)
24+updateTyConArgTy f (TyConIndex a) =
25+ TyConIndex (record {argTy = f (argTy a) } a)
26+
27+unApply : Raw -> (Raw, List Raw)
28+unApply tm = unApply' tm []
29+ where unApply' : Raw -> List Raw -> (Raw, List Raw)
30+ unApply' (RApp f x) xs = unApply' f (x::xs)
31+ unApply' notApp xs = (notApp, xs)
32+
33+mkApp : Raw -> List Raw -> Raw
34+mkApp f [] = f
35+mkApp f (x :: xs) = mkApp (RApp f x) xs
36+
37+||| Grab the binders from around a term, alpha-converting to make
38+||| their names unique
39+partial
40+stealBindings : Raw -> (nsubst : TTName -> Maybe TTName) -> Elab (List (TTName, Binder Raw), Raw)
41+stealBindings (RBind n b tm) nsubst =
42+ do n' <- nameFrom n
43+ (bindings, result) <- stealBindings tm (extend nsubst n n')
44+ return ((n', map (alphaRaw nsubst) b) :: bindings, result)
45+stealBindings tm nsubst = return ([], alphaRaw nsubst tm)
46+
47+||| Get the last element of a list. Fail on empty lists.
48+last : List a -> Elab a
49+last [] = fail [TextPart "Unexpected empty list"]
50+last [x] = return x
51+last (_::x::xs) = last (x::xs)
52+
53+||| Grab the binders from around a term, assuming that they have been
54+||| previously uniquified
55+extractBinders : Raw -> (List (TTName, Binder Raw), Raw)
56+extractBinders (RBind n b tm) = let (bs, res) = extractBinders tm
57+ in ((n, b) :: bs, res)
58+extractBinders tm = ([], tm)
59+
60+
61+||| Get the type annotation from a binder
62+getBinderTy : Binder t -> t
63+getBinderTy (Lam t) = t
64+getBinderTy (Pi t _) = t
65+getBinderTy (Let t _) = t
66+getBinderTy (NLet t _) = t
67+getBinderTy (Hole t) = t
68+getBinderTy (GHole t) = t
69+getBinderTy (Guess t _) = t
70+getBinderTy (PVar t) = t
71+getBinderTy (PVTy t) = t
72+
73+||| Map a list `[x1, x2, ..., xn]` to `[(0, x1), (1, x2), ..., (n-1, xn)]`
74+enumerate : List a -> List (Nat, a)
75+enumerate xs = enumerate' xs 0
76+ where enumerate' : List a -> Nat -> List (Nat, a)
77+ enumerate' [] _ = []
78+ enumerate' (x::xs) n = (n, x) :: enumerate' xs (S n)
79+
80+getSigmaArgs : Raw -> Elab (Raw, Raw)
81+getSigmaArgs `(MkSigma {a=~_} {P=~_} ~rhsTy ~lhs) = return (rhsTy, lhs)
82+getSigmaArgs arg = fail [TextPart "Not a sigma constructor"]
83+
84+bindPats : List (TTName, Binder Raw) -> Raw -> Raw
85+bindPats [] res = res
86+bindPats ((n, b)::bs) res = RBind n (PVar (getBinderTy b)) $ bindPats bs res
87+
88+bindPatTys : List (TTName, Binder Raw) -> Raw -> Raw
89+bindPatTys [] res = res
90+bindPatTys ((n, b)::bs) res = RBind n (PVTy (getBinderTy b)) $ bindPatTys bs res
91+
92+
93+||| Helper for elaborating pattern clauses. This helper takes care of
94+||| inferring the type of the left-hand side and bringing that
95+||| information onward to the right-hand side.
96+|||
97+||| While elaborating the left-hand side, the proof term contains a
98+||| Sigma type. This is part of the type inference going on and will
99+||| be removed.
100+|||
101+||| @ lhs the tactic script to establish the left-hand side of the
102+||| clause. It should cause an application of the term being
103+||| defined. Any holes left behind will be converted to pattern
104+||| variables with the same name.
105+||| @ rhs the tactic script to establish the right side of the clause.
106+||| It will be run in a context where the pattern variables are
107+||| already bound, and should leave behind no holes.
108+partial
109+elabPatternClause : (lhs, rhs : Elab ()) -> Elab FunClause
110+elabPatternClause lhs rhs =
111+ do -- Elaborate the LHS in a context where its type will be solved via unification
112+ (pat, _) <- runElab `(Sigma Type id) $
113+ do th <- newHole "finalTy" `(Type)
114+ patH <- newHole "pattern" (Var th)
115+ fill `(MkSigma ~(Var th) ~(Var patH) : Sigma Type id)
116+ solve
117+ focus patH
118+ lhs
119+ -- Convert all remaining holes to pattern variables
120+ traverse_ {b=()} (\h => focus h *> patvar h) !getHoles
121+ let (pvars, sigma) = extractBinders !(forgetTypes pat)
122+ (rhsTy, lhsTm) <- getSigmaArgs sigma
123+ rhsTm <- runElab (bindPatTys pvars rhsTy) $
124+ do -- Introduce all the pattern variables from the LHS
125+ repeatUntilFail bindPat <|> return ()
126+ rhs
127+ realRhs <- forgetTypes (fst rhsTm)
128+ return $ MkFunClause (bindPats pvars lhsTm) realRhs
129+
130+||| Introduce a unique binder name, returning it
131+intro1 : Elab TTName
132+intro1 = do g <- snd <$> getGoal
133+ case g of
134+ Bind n (Pi _ _) _ => do n' <- nameFrom n
135+ intro n'
136+ return n'
137+ _ => fail [ TextPart "Can't intro1 because goal"
138+ , TermPart g
139+ , TextPart "isn't a function type."]
140+
141+
142+||| Repeat an action some number of times, saving the results.
143+doTimes : Applicative m => (n : Nat) -> m a -> m (Vect n a)
144+doTimes Z x = pure []
145+doTimes (S k) x = [| x :: (doTimes k x) |]
146+
147+||| Zip two lists, failing if their lengths don't match.
148+zipH : List a -> List b -> Elab (List (a, b))
149+zipH [] [] = return []
150+zipH (x::xs) (y::ys) = ((x, y) ::) <$> zipH xs ys
151+zipH _ _ = fail [TextPart "length mismatch"]
152+
153+unsafeNth : Nat -> List a -> Elab a
154+unsafeNth _ [] = fail [TextPart "Ran out of list elements"]
155+unsafeNth Z (x :: _) = return x
156+unsafeNth (S k) (_ :: xs) = unsafeNth k xs
157+
158+
libs/pruviloj/Pruviloj/Internals/TyConInfo.idrnew file+108
@@ -0,0 +1,108 @@
1+module Pruviloj.Derive.TyConInfo
2+
3+import Pruviloj.Core
4+import Pruviloj.Internals
5+import Pruviloj.Renamers
6+
7+import Language.Reflection.Utils
8+
9+
10+
11+||| A representation of a type constructor in which all argument names
12+||| are made unique and they are separated into params and then
13+||| indices.
14+record TyConInfo where
15+ constructor MkTyConInfo
16+ ||| Invariant: the names of the args have been made unique
17+ args : List TyConArg
18+ ||| The type constructor, applied to its arguments
19+ result : Raw
20+
21+%name TyConInfo info
22+
23+getParams : TyConInfo -> List (TTName, Raw)
24+getParams info = mapMaybe param (args info)
25+ where param : TyConArg -> Maybe (TTName, Raw)
26+ param (TyConParameter a) = Just (argName a, argTy a)
27+ param _ = Nothing
28+
29+getIndices : TyConInfo -> List (TTName, Raw)
30+getIndices info = mapMaybe index (args info)
31+ where index : TyConArg -> Maybe (TTName, Raw)
32+ index (TyConIndex a) = Just (argName a, argTy a)
33+ index _ = Nothing
34+
35+||| Rename a bound variable across a telescope
36+renameIn : (from, to : TTName) -> List (TTName, Raw) -> List (TTName, Raw)
37+renameIn from to [] = []
38+renameIn from to ((n, ty)::tele) =
39+ (n, alphaRaw (rename from to) ty) ::
40+ if from == n
41+ then tele
42+ else renameIn from to tele
43+
44+||| Rename a free variable in type constructor info (used to implement
45+||| alpha-conversion for unique binder names, hence the odd name)
46+alphaTyConInfo : (TTName -> Maybe TTName) -> TyConInfo -> TyConInfo
47+alphaTyConInfo ren (MkTyConInfo [] res) = MkTyConInfo [] (alphaRaw ren res)
48+alphaTyConInfo ren (MkTyConInfo (tcArg::tcArgs) res) =
49+ let MkTyConInfo tcArgs' res' = alphaTyConInfo (restrict ren (tyConArgName tcArg)) (MkTyConInfo tcArgs res)
50+ tcArg' = updateTyConArgTy (alphaRaw ren) tcArg
51+ in MkTyConInfo (tcArg'::tcArgs') res'
52+
53+getTyConInfo' : List TyConArg -> Raw -> (TTName -> Maybe TTName) -> Elab TyConInfo
54+getTyConInfo' [] res _ = return (MkTyConInfo [] res)
55+getTyConInfo' (tcArg::tcArgs) res ren =
56+ do let n = tyConArgName tcArg
57+ n' <- nameFrom n
58+ let ren' = extend ren n n'
59+ -- n' is globally unique so we don't worry about scope
60+ next <- getTyConInfo' tcArgs (RApp res (Var n')) ren'
61+ return $ alphaTyConInfo ren' $
62+ record {args = setTyConArgName tcArg n' :: args next} next
63+
64+getTyConInfo : List TyConArg -> Raw -> Elab TyConInfo
65+getTyConInfo args res = getTyConInfo' args res (const Nothing)
66+
67+||| Convert the parameter names in a constructor to their global unique versions
68+processCtorArgs : TyConInfo -> (TTName, List CtorArg, Raw) -> Elab (TTName, List CtorArg, Raw)
69+processCtorArgs info (cn, cargs, resTy) =
70+ do (args', ty') <- convert' (const Nothing) cargs resTy info
71+ return (cn, args', ty')
72+ where
73+ ||| Find the name that was assigned to a given parameter
74+ ||| by comparing positions in the TyConInfo
75+ findParam : TTName -> List Raw -> List TyConArg -> Elab TTName
76+ findParam paramN (Var n :: args) (TyConParameter a :: tcArgs) =
77+ if n == paramN
78+ then return (argName a)
79+ else findParam paramN args tcArgs
80+ findParam paramN (_ :: args) (_ :: tcArgs) =
81+ findParam paramN args tcArgs
82+ findParam paramN _ _ = fail [ TextPart "Parameter"
83+ , NamePart paramN
84+ , TextPart "not found."
85+ ]
86+
87+ convert' : (TTName -> Maybe TTName) ->
88+ List CtorArg -> Raw ->
89+ TyConInfo -> Elab (List CtorArg, Raw)
90+ convert' subst [] ty info = return ([], alphaRaw subst ty)
91+ convert' subst (CtorField a :: args) ty info =
92+ do n' <- nameFrom (argName a)
93+ let a' = record {
94+ argName = n'
95+ , argTy = alphaRaw subst (argTy a)
96+ } a
97+ let subst' = extend subst (argName a) n'
98+ (args', ty') <- convert' subst' args ty info
99+ return (CtorField a' :: args', ty')
100+ convert' subst (CtorParameter a :: ctorArgs) ty info =
101+ do n' <- findParam (argName a) (snd (unApply ty)) (args info)
102+ let a' = record {
103+ argName = n'
104+ , argTy = alphaRaw subst (argTy a)
105+ } a
106+ let subst' = extend subst (argName a) n'
107+ (args', ty') <- convert' subst' ctorArgs ty info
108+ return (CtorParameter a' :: args', ty')
libs/pruviloj/Pruviloj/Renamers.idrnew file+39
@@ -0,0 +1,39 @@
1+module Pruviloj.Renamers
2+
3+import Language.Reflection.Utils
4+
5+||| A renamer keeps track of names to be substituted
6+Renamer : Type
7+Renamer = TTName -> Maybe TTName
8+
9+||| Cause a renamer to forget a renaming
10+restrict : Renamer -> TTName -> Renamer
11+restrict f n n' = if n == n' then Nothing else f n'
12+
13+||| Extend a renamer with a new renaming
14+extend : Renamer -> TTName -> TTName -> Renamer
15+extend f n n' n'' = if n'' == n then Just n' else f n''
16+
17+||| Create a new renamer
18+|||
19+||| @ from the old name
20+||| @ to the new name
21+rename : (from, to : TTName) -> Renamer
22+rename from to = extend (const Nothing) from to
23+
24+||| Alpha-convert `Raw` terms
25+||| @ subst a renamer
26+partial
27+alphaRaw : (subst : Renamer) -> Raw -> Raw
28+alphaRaw subst (Var n) with (subst n)
29+ alphaRaw subst (Var n) | Nothing = Var n
30+ alphaRaw subst (Var n) | Just n' = Var n'
31+alphaRaw subst (RBind n b tm) =
32+ let subst' = restrict subst n
33+ b' = map (alphaRaw subst) b
34+ in RBind n b' (alphaRaw subst' tm)
35+alphaRaw subst (RApp tm tm') = RApp (alphaRaw subst tm) (alphaRaw subst tm')
36+alphaRaw subst RType = RType
37+alphaRaw subst (RUType x) = RUType x
38+alphaRaw subst (RForce tm) = RForce (alphaRaw subst tm)
39+alphaRaw subst (RConstant c) = RConstant c
libs/pruviloj/README.txtnew file+44
@@ -0,0 +1,44 @@
1+ ___ _
2+ / \ _ / \ _
3+| | | / \| | / \
4+| | | _ _ _ _ _ \_/| | ___ \_/
5+| ---/ \ \/ \ \/ \ \/ \| |/ \/ \
6+| | | -/| | || | || || || | || |
7+| | | | | | |\ | /| || || | || |
8+\_/ \_/ \___/ \_/ \_/\_/\___/| |
9+ _/ |
10+ |__/
11+ a proof automation and program construction toolkit
12+
13+
14+Pruviloj is a library of tactics that work with Idris's elaborator
15+reflection. In addition to a library of small tactics, it contains
16+code for generating eliminators for inductive datatypes and using
17+those eliminators to do induction.
18+
19+
20+Q: How do I use Pruviloj?
21+A: Call Idris with the "-p pruviloj" option and add:
22+ import Pruviloj
23+ to the top of your file. If you want to do induction, then
24+ add:
25+ import Pruviloj.Induction
26+ as well.
27+
28+
29+Q: How do I find out what's available?
30+A: Use ":browse Pruviloj.Core" after importing the library.
31+ Pruviloj.Induction exports only one name: "induction".
32+ Use ":doc" to read the built-in documentation.
33+
34+
35+Q: How do I use the tactics?
36+A: Please read the Idris documentation on elaborator reflection.
37+ The syntax to invoke a tactic script is "%runElab script". To
38+ interactively work with a hole, use ":elab holeName".
39+
40+
41+Q: Where does the name come from?
42+A: "Pruviloj" is Esperanto for "proof tools". Perhaps confusingly
43+ for Esperantists, the Pruviloj library also contains utilities
44+ for code generation.
libs/pruviloj/pruviloj.ipkgnew file+10
@@ -0,0 +1,10 @@
1+package pruviloj
2+
3+opts = "--nobasepkgs -i ../prelude -i ../base"
4+modules = Pruviloj
5+ , Pruviloj.Core
6+ , Pruviloj.Derive.Eliminators
7+ , Pruviloj.Induction
8+ , Pruviloj.Internals
9+ , Pruviloj.Internals.TyConInfo
10+ , Pruviloj.Renamers
test/pruviloj001/expectednew file

No changes to the content.

test/pruviloj001/pruviloj001.idrnew file+77
@@ -0,0 +1,77 @@
1+-- Demonstrate that partial tactics can produce total programs and
2+-- that the basic parts of Pruviloj are doing what they should.
3+
4+import Pruviloj
5+import Pruviloj.Induction
6+
7+%default total
8+
9+||| Try some simplification and rewriting heuristics, then attempt to
10+||| solve the goal
11+partial
12+auto : Elab ()
13+auto = do compute
14+ attack
15+ try $ repeatUntilFail intro'
16+ hs <- map fst <$> getEnv
17+ for_ hs $
18+ \ih => try (rewriteWith (Var ih))
19+ hypothesis <|> search
20+ solve
21+
22+
23+||| ; in Coq (roughly)
24+andThen : Elab (List TTName) -> Elab a -> Elab ()
25+andThen tac1 tac2 =
26+ do hs <- tac1
27+ for_ hs $ \h =>
28+ inHole h $ ignore tac2
29+
30+||| Common pattern of proofs by induction.
31+partial
32+mush : Elab ()
33+mush =
34+ do n <- gensym "j"
35+ intro n
36+ try intros
37+ induction (Var n) `andThen` auto
38+
39+plusAssoc : (j, k, l : Nat) -> plus (plus j k) l = plus j (plus k l)
40+plusAssoc = %runElab mush
41+
42+plusZeroR : (k : Nat) -> plus k Z = k
43+plusZeroR = %runElab mush
44+
45+plusSRightS : (left : Nat) -> (right : Nat) -> S (left + right) = left + (S right)
46+plusSRightS = %runElab mush
47+
48+multOneLNeutral : (right : Nat) -> 1 * right = right
49+multOneLNeutral = %runElab mush
50+
51+multOneRNeutral : (left : Nat) -> left * 1 = left
52+multOneRNeutral = %runElab mush
53+
54+plusMinusLeftCancel : (left : Nat) -> (right : Nat) -> (right' : Nat) ->
55+ minus (left + right) (left + right') = minus right right'
56+plusMinusLeftCancel = %runElab mush
57+
58+powerOneNeutral : (base : Nat) -> power base 1 = base
59+powerOneNeutral = %runElab mush
60+
61+-- this silly tactic is controllable by introducing the non-inductive arg first
62+mapPreservesLen : (f : a -> b) -> (l : List a) ->
63+ length (map f l) = length l
64+mapPreservesLen f = %runElab mush
65+
66+lenAppend : (left : List a) -> (right : List a) ->
67+ length (left ++ right) = length left + length right
68+lenAppend = %runElab mush
69+
70+appendNilRightId : (l : List a) ->
71+ l ++ [] = l
72+appendNilRightId = %runElab mush
73+
74+-- Local Variables:
75+-- idris-load-packages: ("pruviloj")
76+-- End:
77+
test/pruviloj001/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris $@ -p pruviloj --check --nocolour --consolewidth 70 pruviloj001.idr
3+rm -f *.ibc