git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2687 from david-christiansen/pruviloj
a79463eDavid Christiansen
libs/prelude/Language/Reflection/Elab.idr+8−1
compare with master
unifiedsplit
@@ -144,6 +144,7 @@ data Elab : Type -> Type where
144 prim__DeclareType : TyDecl -> Elab ()
144 prim__DeclareType : TyDecl -> Elab ()
145 prim__DefineFunction : FunDefn -> Elab ()
145 prim__DefineFunction : FunDefn -> Elab ()
146 prim__AddInstance : TTName -> TTName -> Elab ()
146 prim__AddInstance : TTName -> TTName -> Elab ()
147+ prim__IsTCName : TTName -> Elab Bool
147
148
148 prim__ResolveTC : TTName -> Elab ()
149 prim__ResolveTC : TTName -> Elab ()
149 prim__Search : Int -> List TTName -> Elab ()
150 prim__Search : Int -> List TTName -> Elab ()
@@ -427,13 +428,19 @@ namespace Tactics
427 defineFunction : FunDefn -> Elab ()
428 defineFunction : FunDefn -> Elab ()
428 defineFunction defun = prim__DefineFunction defun
429 defineFunction defun = prim__DefineFunction defun
429
430
430− ||| Register a new instance for type class resolution
431+ ||| Register a new instance for type class resolution.
431 |||
432 |||
432 ||| @ className the name of the class for which an instance is being registered
433 ||| @ className the name of the class for which an instance is being registered
433 ||| @ instName the name of the definition to use in instance search
434 ||| @ instName the name of the definition to use in instance search
434 addInstance : (className, instName : TTName) -> Elab ()
435 addInstance : (className, instName : TTName) -> Elab ()
435 addInstance className instName = prim__AddInstance className instName
436 addInstance className instName = prim__AddInstance className instName
436
437
438+ ||| Determine whether a name denotes a class.
439+ |||
440+ ||| @ name a name that might denote a class.
441+ isTCName : (name : TTName) -> Elab Bool
442+ isTCName name = prim__IsTCName name
443+
437 ||| Attempt to solve the current goal with a type class dictionary
444 ||| Attempt to solve the current goal with a type class dictionary
438 |||
445 |||
439 ||| @ fn the name of the definition being elaborated (to prevent Idris
446 ||| @ fn the name of the definition being elaborated (to prevent Idris
libs/pruviloj/Pruviloj.idr+5
@@ -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/Core.idr+90−9
@@ -3,13 +3,8 @@
3||| eventual Prelude inclusion.
3||| eventual Prelude inclusion.
4module Pruviloj.Core
4module Pruviloj.Core
5
5
6−
7−import Language.Reflection.Elab
8import Language.Reflection.Utils
6import Language.Reflection.Utils
9
7
10−data Infer : Type where
11− MkInfer : (a : Type) -> a -> Infer
12−
13||| Run something for effects, throwing away the return value
8||| Run something for effects, throwing away the return value
14ignore : Functor f => f a -> f ()
9ignore : Functor f => f a -> f ()
15ignore x = map (const ()) x
10ignore x = map (const ()) x
@@ -85,11 +80,11 @@ intros = do g <- snd <$> getGoal
85
80
86||| Run a tactic inside of a particular hole, if it still exists. If
81||| Run a tactic inside of a particular hole, if it still exists. If
87||| it has been solved, do nothing.
82||| it has been solved, do nothing.
88−inHole : TTName -> Elab () -> Elab ()
83+inHole : TTName -> Elab a -> Elab (Maybe a)
89inHole h todo =
84inHole h todo =
90− when (h `elem` !getHoles) $
85+ if (h `elem` !getHoles)
91− do focus h
86+ then do focus h; Just <$> todo
92− todo
87+ else return Nothing
93
88
94||| Restrict a polymorphic type to () for contexts where it doesn't
89||| Restrict a polymorphic type to () for contexts where it doesn't
95||| matter. This is nice for sticking `debug` in a context where
90||| matter. This is nice for sticking `debug` in a context where
@@ -142,3 +137,89 @@ bindPat = do compute
142 case g of
137 case g of
143 Bind n (PVTy _) _ => patbind n
138 Bind n (PVTy _) _ => patbind n
144 _ => fail [TermPart g, TextPart "isn't looking for a pattern."]
139 _ => fail [TermPart g, TextPart "isn't looking for a pattern."]
140+
141+||| The underlying implementation type for the inferType operator.
142+data Infer : Type where
143+ MkInfer : (a : Type) -> a -> Infer
144+
145+||| Run a tactic script in a context where the type of the resulting
146+||| expression must be solvable via unification. Return the term and
147+||| its type.
148+|||
149+||| @ tac a tactic script that will be run with focus on the hole
150+||| whose type is to be inferred.
151+total
152+inferType : (tac : Elab ()) -> Elab (TT, TT)
153+inferType tac =
154+ case fst !(runElab `(Infer) (startInfer *> tac)) of
155+ `(MkInfer ~ty ~tm) => return (tm, ty)
156+ _ => fail [TextPart "Not infer"]
157+ where
158+ startInfer : Elab ()
159+ startInfer = do [_, (_, tmH)] <- apply (Var `{MkInfer}) [(True, 0), (False, 1)]
160+ | err => fail [TextPart "Type inference failure"]
161+ solve
162+ focus tmH
163+
164+||| Given one tactic that produces a list of subgoal names and another
165+||| that produces some result, run the second tactic in each hole
166+||| produced by the first and return the resulting values.
167+|||
168+||| Elab has no built-in notion of "subgoals", so this simulates the
169+||| Coq or JonPRL semicolon operators.
170+|||
171+||| @ first run this tactic to produce subgoals
172+||| @ after run this tactic in each subgoal
173+andThen : (first : Elab (List TTName)) -> (after : Elab a) -> Elab (List a)
174+andThen first after =
175+ do hs <- first
176+ catMaybes <$> for hs (flip inHole after)
177+
178+||| Refine the current goal using some term, constructing holes for
179+||| all arguments that can't be inferred. Return the list of generated
180+||| holes.
181+|||
182+||| @ tm the term to apply to some number of goals
183+refine : (tm : Raw) -> Elab (List TTName)
184+refine tm =
185+ do ty <- (snd <$> check tm) >>= forgetTypes
186+ g <- goalType
187+
188+ -- we don't care about negative results because it'll just fail anyway
189+ let argCount = minus (countPi ty) (countPi g)
190+ newHoles <- apply tm (replicate argCount (True, 0))
191+ solve
192+ actualHoles <- getHoles
193+ return (filter (flip elem actualHoles) (map snd newHoles))
194+
195+ where countPi : Raw -> Nat
196+ countPi (RBind _ (Pi _ _) body) = S (countPi body)
197+ countPi _ = Z
198+
199+
200+||| Split a pair into its projections, binding them in the context
201+||| with the supplied names. A special case of Coq's `inversion`.
202+both : Raw -> TTName -> TTName -> Elab ()
203+both tm n1 n2 =
204+ do -- We don't know that the term is canonical, so let-bind projections applied to it
205+ (A, B) <- isPairTy (snd !(check tm))
206+ remember n1 A; apply `(fst {a=~A} {b=~B} ~tm) []; solve
207+ remember n2 B; apply `(snd {a=~A} {b=~B} ~tm) []; solve
208+ where
209+ isPairTy : TT -> Elab (Raw, Raw)
210+ isPairTy `((~A, ~B) : Type) = [| MkPair (forgetTypes A) (forgetTypes B) |]
211+ isPairTy tm = fail [TermPart tm, TextPart "is not a pair"]
212+
213+||| Let-bind all results of completely destructuring nested tuples.
214+|||
215+||| This makes them available to the `hypothesis` tactic, among others.
216+|||
217+||| @ tm the nested tuple to destructure
218+covering
219+unproduct : (tm : Raw) -> Elab ()
220+unproduct tm =
221+ do n1 <- gensym "left"
222+ n2 <- gensym "right"
223+ both tm n1 n2
224+ try (unproduct (Var n1))
225+ try (unproduct (Var n2))
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/Internals.idr+5−9
@@ -77,10 +77,6 @@ enumerate xs = enumerate' xs 0
77 enumerate' [] _ = []
77 enumerate' [] _ = []
78 enumerate' (x::xs) n = (n, x) :: enumerate' xs (S n)
78 enumerate' (x::xs) n = (n, x) :: enumerate' xs (S n)
79
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−
84bindPats : List (TTName, Binder Raw) -> Raw -> Raw
80bindPats : List (TTName, Binder Raw) -> Raw -> Raw
85bindPats [] res = res
81bindPats [] res = res
86bindPats ((n, b)::bs) res = RBind n (PVar (getBinderTy b)) $ bindPats bs res
82bindPats ((n, b)::bs) res = RBind n (PVar (getBinderTy b)) $ bindPats bs res
@@ -109,19 +105,19 @@ partial
109elabPatternClause : (lhs, rhs : Elab ()) -> Elab FunClause
105elabPatternClause : (lhs, rhs : Elab ()) -> Elab FunClause
110elabPatternClause lhs rhs =
106elabPatternClause lhs rhs =
111 do -- Elaborate the LHS in a context where its type will be solved via unification
107 do -- Elaborate the LHS in a context where its type will be solved via unification
112− (pat, _) <- runElab `(Sigma Type id) $
108+ (pat, _) <- runElab `(Infer) $
113 do th <- newHole "finalTy" `(Type)
109 do th <- newHole "finalTy" `(Type)
114 patH <- newHole "pattern" (Var th)
110 patH <- newHole "pattern" (Var th)
115− fill `(MkSigma ~(Var th) ~(Var patH) : Sigma Type id)
111+ fill `(MkInfer ~(Var th) ~(Var patH))
116 solve
112 solve
117 focus patH
113 focus patH
118 lhs
114 lhs
119 -- Convert all remaining holes to pattern variables
115 -- Convert all remaining holes to pattern variables
120 traverse_ {b=()} (\h => focus h *> patvar h) !getHoles
116 traverse_ {b=()} (\h => focus h *> patvar h) !getHoles
121− let (pvars, sigma) = extractBinders !(forgetTypes pat)
117+ (pvars, `(MkInfer ~rhsTy ~lhsTm)) <- extractBinders <$> (forgetTypes pat)
122− (rhsTy, lhsTm) <- getSigmaArgs sigma
118+ | fail [TextPart "Couldn't infer type of left-hand pattern"]
123 rhsTm <- runElab (bindPatTys pvars rhsTy) $
119 rhsTm <- runElab (bindPatTys pvars rhsTy) $
124− do -- Introduce all the pattern variables from the LHS
120+ do -- Introduce all the pattern variables from the LHS
125 repeatUntilFail bindPat <|> return ()
121 repeatUntilFail bindPat <|> return ()
126 rhs
122 rhs
127 realRhs <- forgetTypes (fst rhsTm)
123 realRhs <- forgetTypes (fst rhsTm)
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
src/Idris/Elab/Term.hs+16−6
@@ -1990,7 +1990,6 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
1990 set_context ctxt'
1990 set_context ctxt'
1991 updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rFunArgToPArg args) checked) :
1991 updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rFunArgToPArg args) checked) :
1992 new_tyDecls e }
1992 new_tyDecls e }
1993− aux <- getAux
1994 returnUnit
1993 returnUnit
1995 | n == tacN "prim__DefineFunction", [decl] <- args
1994 | n == tacN "prim__DefineFunction", [decl] <- args
1996 = do defn <- reifyFunDefn decl
1995 = do defn <- reifyFunDefn decl
@@ -2002,6 +2001,11 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
2002 updateAux $ \e -> e { new_tyDecls = RAddInstance className instName :
2001 updateAux $ \e -> e { new_tyDecls = RAddInstance className instName :
2003 new_tyDecls e}
2002 new_tyDecls e}
2004 returnUnit
2003 returnUnit
2004+ | n == tacN "prim__IsTCName", [n] <- args
2005+ = do n' <- reifyTTName n
2006+ case lookupCtxtExact n' (idris_classes ist) of
2007+ Just _ -> fmap fst . checkClosed $ Var (sNS (sUN "True") ["Bool", "Prelude"])
2008+ Nothing -> fmap fst . checkClosed $ Var (sNS (sUN "False") ["Bool", "Prelude"])
2005 | n == tacN "prim__ResolveTC", [fn] <- args
2009 | n == tacN "prim__ResolveTC", [fn] <- args
2006 = do g <- goal
2010 = do g <- goal
2007 fn <- reifyTTName fn
2011 fn <- reifyTTName fn
@@ -2030,17 +2034,23 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
2030 aux <- getAux
2034 aux <- getAux
2031 datatypes <- get_datatypes
2035 datatypes <- get_datatypes
2032 env <- get_env
2036 env <- get_env
2037+
2033− (_, ES (p, aux') _ _) <-
2038+ (ctxt', ES (p, aux') _ _) <-
2034 do (ES (current_p, _) _ _) <- get
2039 do (ES (current_p, _) _ _) <- get
2040+ lift $ runElab aux
2035− lift $ runElab aux (runElabAction ist fc [] script ns)
2041+ (do runElabAction ist fc [] script ns
2042+ ctxt' <- get_context
2043+ return ctxt')
2036− ((newProof recH ctxt datatypes goalTT)
2044+ ((newProof recH ctxt datatypes goalTT)
2037− { nextname = nextname current_p})
2045+ { nextname = nextname current_p })
2046+ set_context ctxt'
2047+
2038 let tm_out = getProofTerm (pterm p)
2048 let tm_out = getProofTerm (pterm p)
2039 do (ES (prf, _) s e) <- get
2049 do (ES (prf, _) s e) <- get
2040 let p' = prf { nextname = nextname p }
2050 let p' = prf { nextname = nextname p }
2041 put (ES (p', aux') s e)
2051 put (ES (p', aux') s e)
2042 env' <- get_env
2052 env' <- get_env
2043− (tm, ty, _) <- lift $ recheck ctxt env (forget tm_out) tm_out
2053+ (tm, ty, _) <- lift $ recheck ctxt' env (forget tm_out) tm_out
2044 let (tm', ty') = (reflect tm, reflect ty)
2054 let (tm', ty') = (reflect tm, reflect ty)
2045 fmap fst . checkClosed $
2055 fmap fst . checkClosed $
2046 rawPair (Var $ reflm "TT", Var $ reflm "TT")
2056 rawPair (Var $ reflm "TT", Var $ reflm "TT")
src/Idris/REPL.hs+9−5
@@ -1225,12 +1225,16 @@ process fn (Pattelab t)
1225
1225
1226process fn (Missing n)
1226process fn (Missing n)
1227 = do i <- getIState
1227 = do i <- getIState
1228− let i' = i { idris_options = (idris_options i) { opt_showimp = True } }
1228+ ppOpts <- fmap ppOptionIst getIState
1229 case lookupCtxt n (idris_patdefs i) of
1229 case lookupCtxt n (idris_patdefs i) of
1230− [] -> iPrintError $ "Unknown operator " ++ show n
1230+ [] -> iPrintError $ "Unknown operator " ++ show n
1231− [(_, tms)] ->
1231+ [(_, tms)] ->
1232− iPrintResult (showSep "\n" (map (showTm i') tms))
1232+ iRenderResult (vsep (map (pprintPTerm ppOpts {ppopt_impl = True}
1233+ []
1234+ []
1235+ (idris_infixes i))
1236+ tms))
1233− _ -> iPrintError $ "Ambiguous name"
1237+ _ -> iPrintError $ "Ambiguous name"
1234process fn (DynamicLink l)
1238process fn (DynamicLink l)
1235 = do i <- getIState
1239 = do i <- getIState
1236 let importdirs = opt_importdirs (idris_options i)
1240 let importdirs = opt_importdirs (idris_options i)
test/meta002/Tacs.idr+3−2
@@ -11,7 +11,6 @@ import Data.Vect
11
11
12import Language.Reflection
12import Language.Reflection
13import Language.Reflection.Errors
13import Language.Reflection.Errors
14−import Language.Reflection.Elab
15import Language.Reflection.Utils
14import Language.Reflection.Utils
16
15
17%default total
16%default total
@@ -33,7 +32,9 @@ foo = %runElab (do intro (UN "fnord")
33 solve)
32 solve)
34
33
35
34
36−
35+%runElab (do n <- isTCName `{Nat}
36+ s <- isTCName `{Show}
37+ if n || not s then fail [TextPart "nope"] else return ())
37
38
38-- Note that <|> is equivalent to "try" in the old tactics.
39-- Note that <|> is equivalent to "try" in the old tactics.
39-- In these tactics, we use ordinary do notation and ordinary documentation strings!
40-- In these tactics, we use ordinary do notation and ordinary documentation strings!
test/meta002/expected+1−1
@@ -1,3 +1,3 @@
1−Tacs.idr:290:15:
1+Tacs.idr:291:15:
2When checking right hand side of testElab3:
2When checking right hand side of testElab3:
3Unifying ty and ARR ty t would lead to infinite value
3Unifying ty and ARR ty t would lead to infinite value
test/pruviloj001/pruviloj001.idr+1−9
@@ -19,14 +19,6 @@ auto = do compute
19 hypothesis <|> search
19 hypothesis <|> search
20 solve
20 solve
21
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.
22||| Common pattern of proofs by induction.
31partial
23partial
32mush : Elab ()
24mush : Elab ()
@@ -34,7 +26,7 @@ mush =
34 do n <- gensym "j"
26 do n <- gensym "j"
35 intro n
27 intro n
36 try intros
28 try intros
37− induction (Var n) `andThen` auto
29+ ignore $ induction (Var n) `andThen` auto
38
30
39plusAssoc : (j, k, l : Nat) -> plus (plus j k) l = plus j (plus k l)
31plusAssoc : (j, k, l : Nat) -> plus (plus j k) l = plus j (plus k l)
40plusAssoc = %runElab mush
32plusAssoc = %runElab mush