@@ -32,14 +32,25 @@ toplevel = EInfo [] emptyContext id Nothing
3232build :: IState -> ElabInfo -> Bool -> Name -> PTerm ->
3333 Elab (Term, [(Name, Type)])
3434build ist info pattern fn tm
35− = do elab ist info pattern fn tm
35+ = do elab ist info pattern False fn tm
3636 tt <- get_term
3737 return $ runState (collectDeferred tt) []
3838
39−elab :: IState -> ElabInfo -> Bool -> Name -> PTerm ->
39+-- Build a term autogenerated as a typeclass method definition
40+-- (Separate, so we don't go overboard resolving things that we don't
41+-- know about yet on the LHS of a pattern def)
42+
43+buildTC :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm ->
44+ Elab (Term, [(Name, Type)])
45+buildTC ist info pattern tcgen fn tm
46+ = do elab ist info pattern tcgen fn tm
47+ tt <- get_term
48+ return $ runState (collectDeferred tt) []
49+
50+elab :: IState -> ElabInfo -> Bool -> Bool -> Name -> PTerm ->
4051 Elab ()
41−elab ist info pattern fn tm
42− = do elabE tm
52+elab ist info pattern tcgen fn tm
53+ = do elabE False tm
4354 when pattern -- convert remaining holes to pattern vars
4455 mkPat
4556 where
@@ -47,66 +58,66 @@ elab ist info pattern fn tm
4758 Placeholder -> (True, priority arg)
4859 _ -> (False, priority arg)
4960
50− toElab arg = case getTm arg of
61+ toElab ina arg = case getTm arg of
5162 Placeholder -> Nothing
52− v -> Just (priority arg, elabE v)
63+ v -> Just (priority arg, elabE ina v)
5364
5465 mkPat = do hs <- get_holes
5566 case hs of
5667 (h: hs) -> do patvar h; mkPat
5768 [] -> return ()
5869
59− elabE t = {- do g <- goal
70+ elabE ina t = {- do g <- goal
6071 tm <- get_term
6172 trace ("Elaborating " ++ show t ++ " : " ++ show g ++ "\n\tin " ++ show tm)
62− $ -} elab' t
73+ $ -} elab' ina t
6374
6475 local f = do e <- get_env
6576 return (f `elem` map fst e)
6677
67− elab' PSet = do fill RSet; solve
68− elab' (PConstant c) = do apply (RConstant c) []; solve
69− elab' (PQuote r) = do fill r; solve
70− elab' (PTrue fc) = try (elab' (PRef fc unitCon))
71− (elab' (PRef fc unitTy))
72− elab' (PFalse fc) = elab' (PRef fc falseTy)
73− elab' (PResolveTC (FC "HACK" _)) -- for chasing parent classes
78+ elab' ina PSet = do fill RSet; solve
79+ elab' ina (PConstant c) = do apply (RConstant c) []; solve
80+ elab' ina (PQuote r) = do fill r; solve
81+ elab' ina (PTrue fc) = try (elab' ina (PRef fc unitCon))
82+ (elab' ina (PRef fc unitTy))
83+ elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)
84+ elab' ina (PResolveTC (FC "HACK" _)) -- for chasing parent classes
7485 = resolveTC 2 fn ist
75− elab' (PResolveTC fc) = do c <- unique_hole (MN 0 "c")
76− instanceArg c
77− elab' (PRefl fc) = elab' (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,
86+ elab' ina (PResolveTC fc) = do c <- unique_hole (MN 0 "c")
87+ instanceArg c
88+ elab' ina (PRefl fc) = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,
7889 pimp (MN 0 "x") Placeholder])
79− elab' (PEq fc l r) = elab' (PApp fc (PRef fc eqTy) [pimp (MN 0 "a") Placeholder,
90+ elab' ina (PEq fc l r) = elab' ina (PApp fc (PRef fc eqTy) [pimp (MN 0 "a") Placeholder,
8091 pimp (MN 0 "b") Placeholder,
8192 pexp l, pexp r])
82− elab' (PPair fc l r) = try (elabE (PApp fc (PRef fc pairTy)
93+ elab' ina (PPair fc l r) = try (elabE True (PApp fc (PRef fc pairTy)
8394 [pexp l,pexp r]))
84− (elabE (PApp fc (PRef fc pairCon)
95+ (elabE True (PApp fc (PRef fc pairCon)
8596 [pimp (MN 0 "A") Placeholder,
8697 pimp (MN 0 "B") Placeholder,
8798 pexp l, pexp r]))
88− elab' (PDPair fc l@(PRef _ n) t r)
99+ elab' ina (PDPair fc l@(PRef _ n) t r)
89100 = case t of
90101 Placeholder -> try asType asValue
91102 _ -> asType
92− where asType = elab' (PApp fc (PRef fc sigmaTy)
103+ where asType = elab' ina (PApp fc (PRef fc sigmaTy)
93104 [pexp t,
94105 pexp (PLam n Placeholder r)])
95− asValue = elab' (PApp fc (PRef fc existsCon)
106+ asValue = elab' ina (PApp fc (PRef fc existsCon)
96107 [pimp (MN 0 "a") t,
97108 pimp (MN 0 "P") Placeholder,
98109 pexp l, pexp r])
99− elab' (PDPair fc l t r) = elab' (PApp fc (PRef fc existsCon)
110+ elab' ina (PDPair fc l t r) = elab' ina (PApp fc (PRef fc existsCon)
100111 [pimp (MN 0 "a") t,
101112 pimp (MN 0 "P") Placeholder,
102113 pexp l, pexp r])
103− elab' (PAlternative as)
114+ elab' ina (PAlternative as)
104115 = let as' = pruneAlt as in
105− try (tryAll (zip (map elab' as') (map showHd as')))
106− (tryAll (zip (map elab' as) (map showHd as)))
116+ try (tryAll (zip (map (elab' ina) as') (map showHd as')))
117+ (tryAll (zip (map (elab' ina) as) (map showHd as)))
107118 where showHd (PApp _ h _) = show h
108119 showHd x = show x
109− elab' (PRef fc n) | pattern && not (inparamBlock n)
120+ elab' ina (PRef fc n) | pattern && not (inparamBlock n)
110121 = do ctxt <- get_context
111122 let sc = case lookupTy Nothing n ctxt of
112123 [] -> True
@@ -119,22 +130,22 @@ elab ist info pattern fn tm
119130 where inparamBlock n = case lookupCtxtName Nothing n (inblock info) of
120131 [] -> False
121132 _ -> True
122− elab' (PRef fc n) = erun fc $ do apply (Var n) []; solve
123− elab' (PLam n Placeholder sc)
124− = do attack; intro (Just n); elabE sc; solve
125− elab' (PLam n ty sc)
133+ elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve
134+ elab' ina (PLam n Placeholder sc)
135+ = do attack; intro (Just n); elabE True sc; solve
136+ elab' ina (PLam n ty sc)
126137 = do tyn <- unique_hole (MN 0 "lamty")
127138 claim tyn RSet
128139 attack
129140 introTy (Var tyn) (Just n)
130141 -- end_unify
131142 focus tyn
132− elabE ty
133− elabE sc
143+ elabE True ty
144+ elabE True sc
134145 solve
135− elab' (PPi _ n Placeholder sc)
136− = do attack; arg n (MN 0 "ty"); elabE sc; solve
137− elab' (PPi _ n ty sc)
146+ elab' ina (PPi _ n Placeholder sc)
147+ = do attack; arg n (MN 0 "ty"); elabE True sc; solve
148+ elab' ina (PPi _ n ty sc)
138149 = do attack; tyn <- unique_hole (MN 0 "ty")
139150 claim tyn RSet
140151 n' <- case n of
@@ -142,10 +153,10 @@ elab ist info pattern fn tm
142153 _ -> return n
143154 forall n' (Var tyn)
144155 focus tyn
145− elabE ty
146− elabE sc
156+ elabE True ty
157+ elabE True sc
147158 solve
148− elab' (PLet n ty val sc)
159+ elab' ina (PLet n ty val sc)
149160 = do attack;
150161 tyn <- unique_hole (MN 0 "letty")
151162 claim tyn RSet
@@ -155,27 +166,31 @@ elab ist info pattern fn tm
155166 case ty of
156167 Placeholder -> return ()
157168 _ -> do focus tyn
158− elabE ty
169+ elabE True ty
159170 focus valn
160− elabE val
161− elabE sc
171+ elabE True val
172+ elabE True sc
162173 solve
163− elab' (PApp fc (PRef _ f) args')
174+ elab' ina (PApp fc (PRef _ f) args')
164175 = do let args = {- case lookupCtxt f (inblock info) of
165176 Just ps -> (map (pexp . (PRef fc)) ps ++ args')
166177 _ ->-} args'
167178 ivs <- get_instances
179+ -- HACK: we shouldn't resolve type classes if we're defining an instance
180+ -- function or default defition.
181+ let isinf = f == inferCon || tcname f
168182 try (do ns <- apply (Var f) (map isph args)
169183 solve
170184 let (ns', eargs)
171185 = unzip $
172186 sortBy (\(_,x) (_,y) -> compare (priority x) (priority y))
173187 (zip ns args)
174− elabArgs [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs))
175− (do apply_elab f (map toElab args)
188+ elabArgs (ina || not isinf)
189+ [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs))
190+ (do apply_elab f (map (toElab (ina || not isinf)) args)
176191 solve)
177192 ivs' <- get_instances
178− when (not pattern) $
193+ when (not pattern || (ina && not tcgen)) $
179194 mapM_ (\n -> do focus n
180195 resolveTC 7 fn ist) (ivs' \\ ivs)
181196-- ivs <- get_instances
@@ -187,37 +202,37 @@ elab ist info pattern fn tm
187202 where tcArg (n, PConstraint _ _ Placeholder) = True
188203 tcArg _ = False
189204
190− elab' (PApp fc f [arg])
205+ elab' a (PApp fc f [arg])
191206 = erun fc $
192− do simple_app (elabE f) (elabE (getTm arg))
207+ do simple_app (elabE a f) (elabE True (getTm arg))
193208 solve
194− elab' Placeholder = do (h : hs) <- get_holes
195− movelast h
196− elab' (PMetavar n) = let n' = case namespace info of
209+ elab' ina Placeholder = do (h : hs) <- get_holes
210+ movelast h
211+ elab' ina (PMetavar n) = let n' = case namespace info of
197212 Just xs@(_:_) -> NS n xs
198213 _ -> n in
199− do attack; defer n'; solve
200− elab' (PProof ts) = do mapM_ (runTac True ist) ts
201− elab' (PTactics ts) = do mapM_ (runTac False ist) ts
202− elab' (PElabError e) = fail e
203− elab' x = fail $ "Something's gone wrong. Did you miss a semi-colon somewhere?"
214+ do attack; defer n'; solve
215+ elab' ina (PProof ts) = do mapM_ (runTac True ist) ts
216+ elab' ina (PTactics ts) = do mapM_ (runTac False ist) ts
217+ elab' ina (PElabError e) = fail e
218+ elab' ina x = fail $ "Something's gone wrong. Did you miss a semi-colon somewhere?"
204219
205− elabArgs failed retry [] _
220+ elabArgs ina failed retry [] _
206221 | retry = let (ns, ts) = unzip (reverse failed) in
207− elabArgs [] False ns ts
222+ elabArgs ina [] False ns ts
208223 | otherwise = return ()
209− elabArgs failed r (n:ns) ((_, Placeholder) : args)
210− = elabArgs failed r ns args
211− elabArgs failed r (n:ns) ((lazy, t) : args)
224+ elabArgs ina failed r (n:ns) ((_, Placeholder) : args)
225+ = elabArgs ina failed r ns args
226+ elabArgs ina failed r (n:ns) ((lazy, t) : args)
212227 | lazy && not pattern
213228 = do elabArg n (PApp bi (PRef bi (UN "lazy"))
214229 [pimp (UN "a") Placeholder,
215230 pexp t]);
216231 | otherwise = elabArg n t
217232 where elabArg n t = if r
218− then try (do focus n; elabE t; elabArgs failed r ns args)
219− (elabArgs ((n,(lazy, t)):failed) r ns args)
220− else do focus n; elabE t; elabArgs failed r ns args
233+ then try (do focus n; elabE ina t; elabArgs ina failed r ns args)
234+ (elabArgs ina ((n,(lazy, t)):failed) r ns args)
235+ else do focus n; elabE ina t; elabArgs ina failed r ns args
221236
222237pruneAlt :: [PTerm] -> [PTerm]
223238pruneAlt xs = map prune xs
@@ -233,12 +248,13 @@ pruneAlt xs = map prune xs
233248 headIs f _ = True -- keep if it's not an application
234249
235250trivial :: IState -> Elab ()
236−trivial ist = try (elab ist toplevel False (MN 0 "tac") (PRefl (FC "prf" 0)))
251+trivial ist = try (elab ist toplevel False False (MN 0 "tac") (PRefl (FC "prf" 0)))
237252 (do env <- get_env
238253 tryAll (map fst env))
239254 where
240255 tryAll [] = fail "No trivial solution"
241− tryAll (x:xs) = try (elab ist toplevel False (MN 0 "tac") (PRef (FC "prf" 0) x))
256+ tryAll (x:xs) = try (elab ist toplevel False False
257+ (MN 0 "tac") (PRef (FC "prf" 0) x))
242258 (tryAll xs)
243259
244260resolveTC :: Int -> Name -> IState -> Elab ()
@@ -271,9 +287,6 @@ resolveTC depth fn ist
271287 blunderbuss t (n:ns) | n /= fn && tcname n = try (resolve n depth)
272288 (blunderbuss t ns)
273289 | otherwise = blunderbuss t ns
274− tcname (UN ('@':_)) = True
275− tcname (NS n _) = tcname n
276− tcname _ = False
277290
278291 resolve n depth
279292 | depth == 0 = fail $ "Can't resolve type class"
@@ -316,7 +329,7 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where
316329 bname (Bind n _ _) = Just n
317330 bname _ = Nothing
318331 runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs
319− runT (Exact tm) = do elab ist toplevel False (MN 0 "tac") tm
332+ runT (Exact tm) = do elab ist toplevel False False (MN 0 "tac") tm
320333 when autoSolve solveAll
321334 runT (Refine fn [])
322335 = do (fn', imps) <- case lookupCtxtName Nothing fn (idris_implicits ist) of
@@ -345,7 +358,7 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where
345358 letn <- unique_hole (MN 0 "rewrite_rule")
346359 letbind letn (Var tyn) (Var valn)
347360 focus valn
348− elab ist toplevel False (MN 0 "tac") tm
361+ elab ist toplevel False False (MN 0 "tac") tm
349362 rewrite (Var letn)
350363 when autoSolve solveAll
351364 runT (LetTac n tm)
@@ -357,7 +370,7 @@ runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where
357370 letn <- unique_hole n
358371 letbind letn (Var tyn) (Var valn)
359372 focus valn
360− elab ist toplevel False (MN 0 "tac") tm
373+ elab ist toplevel False False (MN 0 "tac") tm
361374 when autoSolve solveAll
362375 runT Compute = compute
363376 runT Trivial = do trivial ist; when autoSolve solveAll