git.iko.soy/Idris-dev
on 1b71663 help sign in
Idris-dev/src/Idris/Core/Elaborate.hs
998 lines 37 kB history raw
1{-|
2Module : Idris.Core.Elaborate
3Description : A high level language of tactic composition, for building elaborators from a high level language into the core theory.
5License : BSD3
6Maintainer : The Idris Community.
8This is our interface to proof construction, rather than ProofState,
9because this gives us a language to build derived tactics out of the
10primitives.
11-}
13{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, PatternGuards #-}
14module Idris.Core.Elaborate (
15 module Idris.Core.Elaborate
16 , module Idris.Core.ProofState
17 ) where
19import Idris.Core.Evaluate
20import Idris.Core.ProofState
21import Idris.Core.ProofTerm (bound_in, bound_in_term, getProofTerm, mkProofTerm,
22 refocus)
23import Idris.Core.TT
24import Idris.Core.Typecheck
25import Idris.Core.Unify
27import Control.Monad.State.Strict
28import Data.List
30data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))
31 deriving Show
33type Elab' aux a = StateT (ElabState aux) TC a
34type Elab a = Elab' () a
36proof :: ElabState aux -> ProofState
37proof (ES (p, _) _ _) = p
39-- Insert a 'proofSearchFail' error if necessary to shortcut any further
40-- fruitless searching
41proofFail :: Elab' aux a -> Elab' aux a
42proofFail e = do s <- get
43 case runStateT e s of
44 OK (a, s') -> do put s'
45 return $! a
46 Error err -> lift $ Error (ProofSearchFail err)
48explicit :: Name -> Elab' aux ()
49explicit n = do ES (p, a) s m <- get
50 let p' = p { dontunify = n : dontunify p }
51 put (ES (p', a) s m)
53-- Add a name that's okay to use in proof search (typically either because
54-- it was given explicitly on the lhs, or intrduced as an explicit lambda
55-- or let binding)
56addPSname :: Name -> Elab' aux ()
57addPSname n@(UN _)
58 = do ES (p, a) s m <- get
59 let p' = p { psnames = n : psnames p }
60 put (ES (p', a) s m)
61addPSname _ = return () -- can only use user given names
63getPSnames :: Elab' aux [Name]
64getPSnames = do ES (p, a) s m <- get
65 return (psnames p)
67saveState :: Elab' aux ()
68saveState = do e@(ES p s _) <- get
69 put (ES p s (Just e))
71loadState :: Elab' aux ()
72loadState = do (ES p s e) <- get
73 case e of
74 Just st -> put st
75 _ -> lift $ Error . Msg $ "Nothing to undo"
77getNameFrom :: Name -> Elab' aux Name
78getNameFrom n = do (ES (p, a) s e) <- get
79 let next = nextname p
80 let p' = p { nextname = next + 1 }
81 put (ES (p', a) s e)
82 let n' = case n of
83 UN x -> MN (next+100) x
84 MN i x -> if i == 99999
85 then MN (next+500) x
86 else MN (next+100) x
87 NS (UN x) s -> MN (next+100) x
88 _ -> n
89 return $! n'
91setNextName :: Elab' aux ()
92setNextName = do env <- get_env
93 ES (p, a) s e <- get
94 let pargs = map fst (getArgTys (ptype p))
95 initNextNameFrom (pargs ++ map fstEnv env)
97initNextNameFrom :: [Name] -> Elab' aux ()
98initNextNameFrom ns = do ES (p, a) s e <- get
99 let n' = maxName (nextname p) ns
100 put (ES (p { nextname = n' }, a) s e)
101 where
102 maxName m ((MN i _) : xs) = maxName (max m i) xs
103 maxName m (_ : xs) = maxName m xs
104 maxName m [] = m + 1
107-- | Transform the error returned by an elaboration script, preserving
108-- location information and proof search failure messages.
109transformErr :: (Err -> Err) -> Elab' aux a -> Elab' aux a
110transformErr f elab = do s <- get
111 case runStateT elab s of
112 OK (a, s') -> do put s'
113 return $! a
114 Error e -> lift $ Error (rewriteErr e)
116 where
117 rewriteErr (At f e) = At f (rewriteErr e)
118 rewriteErr (ProofSearchFail e) = ProofSearchFail (rewriteErr e)
119 rewriteErr e = f e
121errAt :: String -> Name -> Maybe Type -> Elab' aux a -> Elab' aux a
122errAt thing n ty = transformErr (Elaborating thing n ty)
125erunAux :: FC -> Elab' aux a -> Elab' aux (a, aux)
126erunAux f elab
127 = do s <- get
128 case runStateT elab s of
129 OK (a, s') -> do put s'
130 aux <- getAux
131 return $! (a, aux)
132 Error (ProofSearchFail (At f e))
133 -> lift $ Error (ProofSearchFail (At f e))
134 Error (At f e) -> lift $ Error (At f e)
135 Error e -> lift $ Error (At f e)
137erun :: FC -> Elab' aux a -> Elab' aux a
138erun f e = do (x, _) <- erunAux f e
139 return x
141runElab :: aux -> Elab' aux a -> ProofState -> TC (a, ElabState aux)
142runElab a e ps = runStateT e (ES (ps, a) "" Nothing)
144execElab :: aux -> Elab' aux a -> ProofState -> TC (ElabState aux)
145execElab a e ps = execStateT e (ES (ps, a) "" Nothing)
147initElaborator :: Name -- ^ the name of what's to be elaborated
148 -> String -- ^ the current source file
149 -> Context -- ^ the current global context
150 -> Ctxt TypeInfo -- ^ the value of the idris_datatypes field of IState
151 -> Int -- ^ the value of the idris_name field of IState
152 -> Type -- ^ the goal type
153 -> ProofState
154initElaborator = newProof
156elaborate :: String -> Context -> Ctxt TypeInfo -> Int -> Name -> Type -> aux -> Elab' aux a -> TC (a, String)
157elaborate tcns ctxt datatypes globalNames n ty d elab =
158 do let ps = initElaborator n tcns ctxt datatypes globalNames ty
159 (a, ES ps' str _) <- runElab d elab ps
160 return $! (a, str)
162-- | Modify the auxiliary state
163updateAux :: (aux -> aux) -> Elab' aux ()
164updateAux f = do ES (ps, a) l p <- get
165 put (ES (ps, f a) l p)
167-- | Get the auxiliary state
168getAux :: Elab' aux aux
169getAux = do ES (ps, a) _ _ <- get
170 return $! a
172-- | Set whether to show the unifier log
173unifyLog :: Bool -> Elab' aux ()
174unifyLog log = do ES (ps, a) l p <- get
175 put (ES (ps { unifylog = log }, a) l p)
177getUnifyLog :: Elab' aux Bool
178getUnifyLog = do ES (ps, a) l p <- get
179 return (unifylog ps)
181-- | Process a tactic within the current elaborator state
182processTactic' :: Tactic -> Elab' aux ()
183processTactic' t = do ES (p, a) logs prev <- get
184 (p', log) <- lift $ processTactic t p
185 put (ES (p', a) (logs ++ log) prev)
186 return $! ()
188updatePS :: (ProofState -> ProofState) -> Elab' aux ()
189updatePS f = do ES (ps, a) logs prev <- get
190 put $ ES (f ps, a) logs prev
192now_elaborating :: FC -> Name -> Name -> Elab' aux ()
193now_elaborating fc f a = updatePS (nowElaboratingPS fc f a)
194done_elaborating_app :: Name -> Elab' aux ()
195done_elaborating_app f = updatePS (doneElaboratingAppPS f)
196done_elaborating_arg :: Name -> Name -> Elab' aux ()
197done_elaborating_arg f a = updatePS (doneElaboratingArgPS f a)
198elaborating_app :: Elab' aux [(FC, Name, Name)]
199elaborating_app = do ES (ps, _) _ _ <- get
200 return $ map (\ (FailContext x y z) -> (x, y, z))
201 (while_elaborating ps)
203-- Some handy gadgets for pulling out bits of state
205-- | Get the global context
206get_context :: Elab' aux Context
207get_context = do ES p _ _ <- get
208 return $! (context (fst p))
210-- | Update the context.
211-- (should only be used for adding temporary definitions or all sorts of
212-- stuff could go wrong)
213set_context :: Context -> Elab' aux ()
214set_context ctxt = do ES (p, a) logs prev <- get
215 put (ES (p { context = ctxt }, a) logs prev)
217get_datatypes :: Elab' aux (Ctxt TypeInfo)
218get_datatypes = do ES p _ _ <- get
219 return $! (datatypes (fst p))
221set_datatypes :: Ctxt TypeInfo -> Elab' aux ()
222set_datatypes ds = do ES (p, a) logs prev <- get
223 put (ES (p { datatypes = ds }, a) logs prev)
225get_global_nextname :: Elab' aux Int
226get_global_nextname = do ES (ps, _) _ _ <- get
227 return (global_nextname ps)
229set_global_nextname :: Int -> Elab' aux ()
230set_global_nextname i = do ES (ps, a) logs prev <- get
231 put $ ES (ps { global_nextname = i}, a) logs prev
233-- | get the proof term
234get_term :: Elab' aux Term
235get_term = do ES p _ _ <- get
236 return $! (getProofTerm (pterm (fst p)))
238-- | modify the proof term
239update_term :: (Term -> Term) -> Elab' aux ()
240update_term f = do ES (p,a) logs prev <- get
241 let p' = p { pterm = mkProofTerm (f (getProofTerm (pterm p))) }
242 put (ES (p', a) logs prev)
244-- | get the local context at the currently in focus hole
245get_env :: Elab' aux Env
246get_env = do ES p _ _ <- get
247 lift $ envAtFocus (fst p)
249get_inj :: Elab' aux [Name]
250get_inj = do ES p _ _ <- get
251 return $! (injective (fst p))
253get_holes :: Elab' aux [Name]
254get_holes = do ES p _ _ <- get
255 return $! (holes (fst p))
257get_usedns :: Elab' aux [Name]
258get_usedns = do ES p _ _ <- get
259 let bs = bound_in (pterm (fst p)) ++
260 bound_in_term (ptype (fst p))
261 let nouse = holes (fst p) ++ bs ++ dontunify (fst p) ++ usedns (fst p)
262 return $! nouse
264get_probs :: Elab' aux Fails
265get_probs = do ES p _ _ <- get
266 return $! (problems (fst p))
268-- | Return recently solved names (that is, the names solved since the
269-- last call to get_recents)
270get_recents :: Elab' aux [Name]
271get_recents = do ES (p, a) l prev <- get
272 put (ES (p { recents = [] }, a) l prev)
273 return (recents p)
275-- | get the current goal type
276goal :: Elab' aux Type
277goal = do ES p _ _ <- get
278 b <- lift $ goalAtFocus (fst p)
279 return $! (binderTy b)
281is_guess :: Elab' aux Bool
282is_guess = do ES p _ _ <- get
283 b <- lift $ goalAtFocus (fst p)
284 case b of
285 Guess _ _ -> return True
286 _ -> return False
288-- | Get the guess at the current hole, if there is one
289get_guess :: Elab' aux Term
290get_guess = do ES p _ _ <- get
291 b <- lift $ goalAtFocus (fst p)
292 case b of
293 Guess t v -> return $! v
294 _ -> fail "Not a guess"
296-- | Typecheck locally
297get_type :: Raw -> Elab' aux Type
298get_type tm = do ctxt <- get_context
299 env <- get_env
300 (val, ty) <- lift $ check ctxt env tm
301 return $! (finalise ty)
303get_type_val :: Raw -> Elab' aux (Term, Type)
304get_type_val tm = do ctxt <- get_context
305 env <- get_env
306 (val, ty) <- lift $ check ctxt env tm
307 return $! (finalise val, finalise ty)
309-- | get holes we've deferred for later definition
310get_deferred :: Elab' aux [Name]
311get_deferred = do ES p _ _ <- get
312 return $! (deferred (fst p))
314checkInjective :: (Term, Term, Term) -> Elab' aux ()
315checkInjective (tm, l, r) = do ctxt <- get_context
316 if isInj ctxt tm then return $! ()
317 else lift $ tfail (NotInjective tm l r)
318 where isInj ctxt (P _ n _)
319 | isConName n ctxt = True
320 isInj ctxt (App _ f a) = isInj ctxt f
321 isInj ctxt (Constant _) = True
322 isInj ctxt (TType _) = True
323 isInj ctxt (Bind _ (Pi _ _ _ _) sc) = True
324 isInj ctxt _ = False
326-- | get implementation argument names
327get_implementations :: Elab' aux [Name]
328get_implementations = do ES p _ _ <- get
329 return $! (implementations (fst p))
331-- | get auto argument names
332get_autos :: Elab' aux [(Name, ([FailContext], [Name]))]
333get_autos = do ES p _ _ <- get
334 return $! (autos (fst p))
336-- | given a desired hole name, return a unique hole name
337unique_hole :: Name -> Elab' aux Name
338unique_hole = unique_hole' False
340unique_hole' :: Bool -> Name -> Elab' aux Name
341unique_hole' reusable n
342 = do ES p _ _ <- get
343 let bs = bound_in (pterm (fst p)) ++
344 bound_in_term (ptype (fst p))
345 let nouse = holes (fst p) ++ bs ++ dontunify (fst p) ++ usedns (fst p)
346 n' <- return $! uniqueNameCtxt (context (fst p)) n nouse
347 ES (p, a) s u <- get
348 case n' of
349 MN i _ -> when (i >= nextname p) $
350 put (ES (p { nextname = i + 1 }, a) s u)
351 _ -> return $! ()
352 return $! n'
354elog :: String -> Elab' aux ()
355elog str = do ES p logs prev <- get
356 put (ES p (logs ++ str ++ "\n") prev)
358getLog :: Elab' aux String
359getLog = do ES p logs _ <- get
360 return $! logs
362-- The primitives, from ProofState
364attack :: Elab' aux ()
365attack = processTactic' Attack
367claim :: Name -> Raw -> Elab' aux ()
368claim n t = processTactic' (Claim n t)
370claimFn :: Name -> Name -> Raw -> Elab' aux ()
371claimFn n bn t = processTactic' (ClaimFn n bn t)
373unifyGoal :: Raw -> Elab' aux ()
374unifyGoal t = processTactic' (UnifyGoal t)
376unifyTerms :: Raw -> Raw -> Elab' aux ()
377unifyTerms t1 t2 = processTactic' (UnifyTerms t1 t2)
379exact :: Raw -> Elab' aux ()
380exact t = processTactic' (Exact t)
382fill :: Raw -> Elab' aux ()
383fill t = processTactic' (Fill t)
385match_fill :: Raw -> Elab' aux ()
386match_fill t = processTactic' (MatchFill t)
388prep_fill :: Name -> [Name] -> Elab' aux ()
389prep_fill n ns = processTactic' (PrepFill n ns)
391complete_fill :: Elab' aux ()
392complete_fill = processTactic' CompleteFill
394solve :: Elab' aux ()
395solve = processTactic' Solve
397start_unify :: Name -> Elab' aux ()
398start_unify n = processTactic' (StartUnify n)
400end_unify :: Elab' aux ()
401end_unify = processTactic' EndUnify
403-- Clear the list of variables not to unify, and try to solve them
404unify_all :: Elab' aux ()
405unify_all = processTactic' UnifyAll
407regret :: Elab' aux ()
408regret = processTactic' Regret
410compute :: Elab' aux ()
411compute = processTactic' Compute
413computeLet :: Name -> Elab' aux ()
414computeLet n = processTactic' (ComputeLet n)
416simplify :: Elab' aux ()
417simplify = processTactic' Simplify
419whnf_compute :: Elab' aux ()
420whnf_compute = processTactic' WHNF_Compute
422whnf_compute_args :: Elab' aux ()
423whnf_compute_args = processTactic' WHNF_ComputeArgs
425eval_in :: Raw -> Elab' aux ()
426eval_in t = processTactic' (EvalIn t)
428check_in :: Raw -> Elab' aux ()
429check_in t = processTactic' (CheckIn t)
431intro :: Maybe Name -> Elab' aux ()
432intro n = processTactic' (Intro n)
434introTy :: Raw -> Maybe Name -> Elab' aux ()
435introTy ty n = processTactic' (IntroTy ty n)
437forall :: Name -> RigCount -> Maybe ImplicitInfo -> Raw -> Elab' aux ()
438forall n r i t = processTactic' (Forall n r i t)
440letbind :: Name -> RigCount -> Raw -> Raw -> Elab' aux ()
441letbind n rig t v = processTactic' (LetBind n rig t v)
443expandLet :: Name -> Term -> Elab' aux ()
444expandLet n v = processTactic' (ExpandLet n v)
446rewrite :: Raw -> Elab' aux ()
447rewrite tm = processTactic' (Rewrite tm)
449equiv :: Raw -> Elab' aux ()
450equiv tm = processTactic' (Equiv tm)
452-- | Turn the current hole into a pattern variable with the provided
453-- name, made unique if not the same as the head of the hole queue
454patvar :: Name -> Elab' aux ()
455patvar n@(SN _) = do apply (Var n) []; solve
456patvar n = do env <- get_env
457 hs <- get_holes
458 if (n `elem` map fstEnv env) then do apply (Var n) []; solve
459 else do n' <- case hs of
460 (h : hs) -> if n == h then return n
461 else unique_hole n
462 _ -> unique_hole n
463 processTactic' (PatVar n)
465-- | Turn the current hole into a pattern variable with the provided
466-- name, but don't make MNs unique.
467patvar' :: Name -> Elab' aux ()
468patvar' n@(SN _) = do apply (Var n) [] ; solve
469patvar' n = do env <- get_env
470 hs <- get_holes
471 if (n `elem` map fstEnv env) then do apply (Var n) [] ; solve
472 else processTactic' (PatVar n)
474patbind :: Name -> RigCount -> Elab' aux ()
475patbind n r = processTactic' (PatBind n r)
477focus :: Name -> Elab' aux ()
478focus n = processTactic' (Focus n)
480movelast :: Name -> Elab' aux ()
481movelast n = processTactic' (MoveLast n)
483dotterm :: Elab' aux ()
484dotterm = do ES (p, a) s m <- get
485 tm <- get_term
486 case holes p of
487 [] -> return ()
488 (h : hs) ->
489 do let outer = findOuter h [] tm
490 let p' = p { dotted = (h, outer) : dotted p }
491-- trace ("DOTTING " ++ show (h, outer) ++ "\n" ++
492-- show tm) $
493 put $ ES (p', a) s m
494 where
495 findOuter h env (P _ n _) | h == n = env
496 findOuter h env (Bind n b sc)
497 = union (foB b)
498 (findOuter h env (instantiate (P Bound n (binderTy b)) sc))
499 where foB (Guess t v) = union (findOuter h env t) (findOuter h (n:env) v)
500 foB (Let _ t v) = union (findOuter h env t) (findOuter h env v)
501 foB b = findOuter h env (binderTy b)
502 findOuter h env (App _ f a)
503 = union (findOuter h env f) (findOuter h env a)
504 findOuter h env _ = []
507get_dotterm :: Elab' aux [(Name, [Name])]
508get_dotterm = do ES (p, a) s m <- get
509 return (dotted p)
511-- | Set the zipper in the proof state to point at the current sub term
512-- (This currently happens automatically, so this will have no effect...)
513zipHere :: Elab' aux ()
514zipHere = do ES (ps, a) s m <- get
515 let pt' = refocus (Just (head (holes ps))) (pterm ps)
516 put (ES (ps { pterm = pt' }, a) s m)
518matchProblems :: Bool -> Elab' aux ()
519matchProblems all = processTactic' (MatchProblems all)
521unifyProblems :: Elab' aux ()
522unifyProblems = processTactic' UnifyProblems
524defer :: [Name] -> [Name] -> Name -> Elab' aux Name
525defer ds ls n
526 = do n' <- unique_hole n
527 processTactic' (Defer ds ls n')
528 return n'
530deferType :: Name -> Raw -> [Name] -> Elab' aux ()
531deferType n ty ns = processTactic' (DeferType n ty ns)
533implementationArg :: Name -> Elab' aux ()
534implementationArg n = processTactic' (Implementation n)
536autoArg :: Name -> Elab' aux ()
537autoArg n = processTactic' (AutoArg n)
539setinj :: Name -> Elab' aux ()
540setinj n = processTactic' (SetInjective n)
542proofstate :: Elab' aux ()
543proofstate = processTactic' ProofState
545reorder_claims :: Name -> Elab' aux ()
546reorder_claims n = processTactic' (Reorder n)
548qed :: Elab' aux Term
549qed = do processTactic' QED
550 ES p _ _ <- get
551 return $! (getProofTerm (pterm (fst p)))
553undo :: Elab' aux ()
554undo = processTactic' Undo
556-- | Prepare to apply a function by creating holes to be filled by the arguments
557prepare_apply :: Raw -- ^ The operation being applied
558 -> [Bool] -- ^ Whether arguments are implicit
559 -> Elab' aux [(Name, Name)] -- ^ The names of the arguments and their holes to be filled with elaborated argument values
560prepare_apply fn imps =
561 do ty <- get_type fn
562 ctxt <- get_context
563 env <- get_env
564 -- let claims = getArgs ty imps
565 -- claims <- mkClaims (normalise ctxt env ty) imps []
566 -- Count arguments to check if we need to normalise the type
567 let usety = if argsOK (finalise ty) imps
568 then finalise ty
569 else normalise ctxt env (finalise ty)
570 claims <- -- trace (show (fn, imps, ty, map fst env, normalise ctxt env (finalise ty))) $
571 mkClaims usety imps [] (map fstEnv env)
572 ES (p, a) s prev <- get
573 -- reverse the claims we made so that args go left to right
574 let n = length (filter not imps)
575 let (h : hs) = holes p
576 put (ES (p { holes = h : (reverse (take n hs) ++ drop n hs) }, a) s prev)
577 return $! claims
578 where
579 argsOK :: Type -> [a] -> Bool
580 argsOK (Bind n (Pi _ _ _ _) sc) (i : is) = argsOK sc is
581 argsOK _ (i : is) = False
582 argsOK _ [] = True
584 mkClaims :: Type -- ^ The type of the operation being applied
585 -> [Bool] -- ^ Whether the arguments are implicit
586 -> [(Name, Name)] -- ^ Accumulator for produced claims
587 -> [Name] -- ^ Hypotheses
588 -> Elab' aux [(Name, Name)] -- ^ The names of the arguments and their holes, resp.
589 mkClaims (Bind n' (Pi _ _ t_in _) sc) (i : is) claims hs =
590 do let t = rebind hs t_in
591 n <- getNameFrom (mkMN n')
592-- when (null claims) (start_unify n)
593 let sc' = instantiate (P Bound n t) sc
594 env <- get_env
595 claim n (forgetEnv (map fstEnv env) t)
596 when i (movelast n)
597 mkClaims sc' is ((n', n) : claims) hs
598 mkClaims t [] claims _ = return $! (reverse claims)
599 mkClaims _ _ _ _
600 | Var n <- fn
601 = do ctxt <- get_context
602 lift $ tfail $ TooManyArguments n
603 | otherwise = fail $ "Too many arguments for " ++ show fn
605 mkMN n@(MN i _) = n
606 mkMN n@(UN x) = MN 99999 x
607 mkMN n@(SN s) = sMN 99999 (show s)
608 mkMN (NS n xs) = NS (mkMN n) xs
610 rebind hs (Bind n t sc)
611 | n `elem` hs = let n' = uniqueName n hs in
612 Bind n' (fmap (rebind hs) t) (rebind (n':hs) sc)
613 | otherwise = Bind n (fmap (rebind hs) t) (rebind (n:hs) sc)
614 rebind hs (App s f a) = App s (rebind hs f) (rebind hs a)
615 rebind hs t = t
617-- | Apply an operator, solving some arguments by unification or matching.
618apply, match_apply :: Raw -- ^ The operator to apply
619 -> [(Bool, Int)] -- ^ For each argument, whether to
620 -- attempt to solve it and the
621 -- priority in which to do so
622 -> Elab' aux [(Name, Name)]
623apply = apply' fill
624match_apply = apply' match_fill
626apply' :: (Raw -> Elab' aux ()) -> Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]
627apply' fillt fn imps =
628 do args <- prepare_apply fn (map fst imps)
629 -- _Don't_ solve the arguments we're specifying by hand.
630 -- (remove from unified list before calling end_unify)
631 hs <- get_holes
632 ES (p, a) s prev <- get
633 let dont = if null imps
634 then head hs : dontunify p
635 else getNonUnify (head hs : dontunify p) imps args
636 let (n, hunis) = -- trace ("AVOID UNIFY: " ++ show (fn, dont)) $
637 unified p
638 let unify = -- trace ("Not done " ++ show hs) $
639 dropGiven dont hunis hs
640 let notunify = -- trace ("Not done " ++ show (hs, hunis)) $
641 keepGiven dont hunis hs
642 put (ES (p { dontunify = dont, unified = (n, unify),
643 notunified = notunify ++ notunified p }, a) s prev)
644 fillt (raw_apply fn (map (Var . snd) args))
645 ulog <- getUnifyLog
646 g <- goal
647 traceWhen ulog
648 ("Goal " ++ show g ++ " -- when elaborating " ++ show fn)
649 end_unify
650 return $! (map (\(argName, argHole) -> (argName, updateUnify unify argHole)) args)
651 where updateUnify us n = case lookup n us of
652 Just (P _ t _) -> t
653 _ -> n
655 getNonUnify acc [] _ = acc
656 getNonUnify acc _ [] = acc
657 getNonUnify acc ((i,_):is) ((a, t):as)
658 | i = getNonUnify acc is as
659 | otherwise = getNonUnify (t : acc) is as
662apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux ()
663apply2 fn elabs =
664 do args <- prepare_apply fn (map isJust elabs)
665 fill (raw_apply fn (map (Var . snd) args))
666 elabArgs (map snd args) elabs
667 ES (p, a) s prev <- get
668 end_unify
669 solve
670 where elabArgs [] [] = return $! ()
671 elabArgs (n:ns) (Just e:es) = do focus n; e
672 elabArgs ns es
673 elabArgs (n:ns) (_:es) = elabArgs ns es
675 isJust (Just _) = False
676 isJust _ = True
678apply_elab :: Name -> [Maybe (Int, Elab' aux ())] -> Elab' aux ()
679apply_elab n args =
680 do ty <- get_type (Var n)
681 ctxt <- get_context
682 env <- get_env
683 claims <- doClaims (normalise ctxt env ty) args []
684 prep_fill n (map fst claims)
685 elabClaims [] False claims
686 complete_fill
687 end_unify
688 where
689 doClaims (Bind n' (Pi _ _ t _) sc) (i : is) claims =
690 do n <- unique_hole (mkMN n')
691 when (null claims) (start_unify n)
692 let sc' = instantiate (P Bound n t) sc
693 claim n (forget t)
694 case i of
695 Nothing -> return $! ()
696 Just _ -> -- don't solve by unification as there is an explicit value
697 do ES (p, a) s prev <- get
698 put (ES (p { dontunify = n : dontunify p }, a) s prev)
699 doClaims sc' is ((n, i) : claims)
700 doClaims t [] claims = return $! (reverse claims)
701 doClaims _ _ _ = fail $ "Wrong number of arguments for " ++ show n
703 elabClaims failed r []
704 | null failed = return $! ()
705 | otherwise = if r then elabClaims [] False failed
706 else return $! ()
707 elabClaims failed r ((n, Nothing) : xs) = elabClaims failed r xs
708 elabClaims failed r (e@(n, Just (_, elaboration)) : xs)
709 | r = try (do ES p _ _ <- get
710 focus n; elaboration; elabClaims failed r xs)
711 (elabClaims (e : failed) r xs)
712 | otherwise = do ES p _ _ <- get
713 focus n; elaboration; elabClaims failed r xs
715 mkMN n@(MN _ _) = n
716 mkMN n@(UN x) = MN 0 x
717 mkMN (NS n ns) = NS (mkMN n) ns
719-- If the goal is not a Pi-type, invent some names and make it a pi type
720checkPiGoal :: Name -> Elab' aux ()
721checkPiGoal n
722 = do g <- goal
723 ctxt <- get_context
724 env <- get_env
725 case (normalise ctxt env g) of
726 Bind _ (Pi _ _ _ _) _ -> return ()
727 _ -> do a <- getNameFrom (sMN 0 "__pargTy")
728 b <- getNameFrom (sMN 0 "__pretTy")
729 f <- getNameFrom (sMN 0 "pf")
730 claim a RType
731 claim b RType
732 claim f (RBind n (Pi RigW Nothing (Var a) RType) (Var b))
733 movelast a
734 movelast b
735 fill (Var f)
736 solve
737 focus f
739simple_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
740simple_app infer fun arg str =
741 try (dep_app fun arg str)
742 (infer_app infer fun arg str)
744infer_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
745infer_app infer fun arg str =
746 do a <- getNameFrom (sMN 0 "__argTy")
747 b <- getNameFrom (sMN 0 "__retTy")
748 f <- getNameFrom (sMN 0 "f")
749 s <- getNameFrom (sMN 0 "is")
750 claim a RType
751 claim b RType
752 claim f (RBind (sMN 0 "_aX") (Pi RigW Nothing (Var a) RType) (Var b))
753 tm <- get_term
754 start_unify s
755 -- if 'infer' is set, we're assuming it's a simply typed application
756 -- so safe to unify with the goal type (as there'll be no dependencies)
757 when infer $ unifyGoal (Var b)
758 hs <- get_holes
759 claim s (Var a)
760 prep_fill f [s]
761 focus f; fun
762 focus s; arg
763 tm <- get_term
764 ps <- get_probs
765 ty <- goal
766 hs <- get_holes
767 complete_fill
768 env <- get_env
769 -- We don't need a and b in the hole queue any more since they were
770 -- just for checking f, so move them to the end. If they never end up
771 -- getting solved, we'll get an 'Incomplete term' error.
772 hs <- get_holes
773 when (a `elem` hs) $ do movelast a
774 when (b `elem` hs) $ do movelast b
775 end_unify
777dep_app :: Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
778dep_app fun arg str =
779 do a <- getNameFrom (sMN 0 "__argTy")
780 b <- getNameFrom (sMN 0 "__retTy")
781 fty <- getNameFrom (sMN 0 "__fnTy")
782 f <- getNameFrom (sMN 0 "f")
783 s <- getNameFrom (sMN 0 "ds")
784 claim a RType
785 claim fty RType
786 claim f (Var fty)
787 tm <- get_term
788 g <- goal
789 start_unify s
790 claim s (Var a)
792 prep_fill f [s]
793 focus f; attack; fun
794 end_unify
795 fty <- goal
796 solve
797 focus s; attack;
798 ctxt <- get_context
799 env <- get_env
800 case normalise ctxt env fty of
801 -- if f gives a function type, unify our argument type with
802 -- f's expected argument type
803 Bind _ (Pi _ _ argty _) _ -> unifyGoal (forget argty)
804 -- Can't infer a type for 'f', so fail here (and drop back to
805 -- simply typed application where we infer the type for f)
806 _ -> fail "Can't make type"
807 end_unify
808 arg
809 solve
810 complete_fill
812 -- We don't need a and b in the hole queue any more since they were
813 -- just for checking f, so move them to the end. If they never end up
814 -- getting solved, we'll get an 'Incomplete term' error.
815 hs <- get_holes
816 when (a `elem` hs) $ do movelast a
817 when (b `elem` hs) $ do movelast b
818 end_unify
820-- Abstract over an argument of unknown type, giving a name for the hole
821-- which we'll fill with the argument type too.
822arg :: Name -> RigCount -> Maybe ImplicitInfo -> Name -> Elab' aux ()
823arg n r i tyhole = do ty <- unique_hole tyhole
824 claim ty RType
825 movelast ty
826 forall n r i (Var ty)
828-- try a tactic, if it adds any unification problem, return an error
829no_errors :: Elab' aux () -> Maybe Err -> Elab' aux ()
830no_errors tac err
831 = do ps <- get_probs
832 s <- get
833 case err of
834 Nothing -> tac
835 Just e -> -- update the error, if there is one.
836 case runStateT tac s of
837 Error _ -> lift $ Error e
838 OK (a, s') -> do put s'
839 return a
840 unifyProblems
841 ps' <- get_probs
842 if (length ps' > length ps) then
843 case reverse ps' of
844 ((x, y, _, env, inerr, while, _) : _) ->
845 let (xp, yp) = getProvenance inerr
846 env' = map (\(x, rig, b) -> (x, binderTy b)) env in
847 lift $ tfail $
848 case err of
849 Nothing -> CantUnify False (x, xp) (y, yp) inerr env' 0
850 Just e -> e
851 else return $! ()
853-- Try a tactic, if it fails, try another
854try :: Elab' aux a -> Elab' aux a -> Elab' aux a
855try t1 t2 = try' t1 t2 False
857handleError :: (Err -> Bool) -> Elab' aux a -> Elab' aux a -> Elab' aux a
858handleError p t1 t2
859 = do s <- get
860 ps <- get_probs
861 case runStateT t1 s of
862 OK (v, s') -> do put s'
863 return $! v
864 Error e1 -> if p e1 then
865 do case runStateT t2 s of
866 OK (v, s') -> do put s'; return $! v
867 Error e2 -> lift (tfail e2)
868 else lift (tfail e1)
870try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a
871try' t1 t2 proofSearch
872 = do s <- get
873 ps <- get_probs
874 ulog <- getUnifyLog
875 ivs <- get_implementations
876 case prunStateT 999999 False ps Nothing t1 s of
877 OK ((v, _, _), s') -> do put s'
878 return $! v
879 Error e1 -> traceWhen ulog ("try failed " ++ show e1) $
880 if recoverableErr e1 then
881 do case runStateT t2 s of
882 OK (v, s') -> do put s'; return $! v
883 Error e2 -> lift (tfail e2)
884 else lift (tfail e1)
885 where recoverableErr err@(CantUnify r x y _ _ _)
886 = -- traceWhen r (show err) $
887 r || proofSearch
888 recoverableErr (CantSolveGoal _ _) = False
889 recoverableErr (CantResolveAlts _) = proofSearch
890 recoverableErr (ProofSearchFail (Msg _)) = True
891 recoverableErr (ProofSearchFail _) = False
892 recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e
893 recoverableErr (At _ e) = recoverableErr e
894 recoverableErr (ElabScriptDebug _ _ _) = False
895 recoverableErr _ = True
897tryCatch :: Elab' aux a -> (Err -> Elab' aux a) -> Elab' aux a
898tryCatch t1 t2
899 = do s <- get
900 ps <- get_probs
901 ulog <- getUnifyLog
902-- case prunStateT 999999 False ps t1 s of
903 case runStateT t1 s of
904 OK (v, s') -> do put s'
905 return $! v
906 Error e1 -> traceWhen ulog ("tryCatch failed " ++ show e1) $
907 case runStateT (t2 e1) s of
908 OK (v, s') -> do put s'
909 return $! v
910 Error e2 -> lift (tfail e2)
912tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a
913tryWhen True a b = try a b
914tryWhen False a b = a
916-- Bool says whether it's okay to create new unification problems. If set
917-- to False, then the whole tactic fails if there are any new problems
918tryAll :: [(Elab' aux a, Name)] -> Elab' aux a
919tryAll = tryAll' True
921tryAll' :: Bool -> [(Elab' aux a, Name)] -> Elab' aux a
922tryAll' _ [(x, _)] = x
923tryAll' constrok xs = doAll [] 999999 xs
924 where
925 cantResolve :: Elab' aux a
926 cantResolve = lift $ tfail $ CantResolveAlts (map snd xs)
928 noneValid :: Elab' aux a
929 noneValid = lift $ tfail $ NoValidAlts (map snd xs)
931 doAll :: [Elab' aux a] -> -- successes
932 Int -> -- most problems
933 [(Elab' aux a, Name)] -> -- still to try
934 Elab' aux a
935 doAll [res] pmax [] = res
936 doAll (_:_) pmax [] = cantResolve
937 doAll [] pmax [] = noneValid
938 doAll cs pmax ((x, msg):xs)
939 = do s <- get
940 ps <- get_probs
941 ivs <- get_implementations
942 g <- goal
943 case prunStateT pmax True ps (if constrok then Nothing
944 else Just ivs) x s of
945 OK ((v, newps, probs), s') ->
946 do let cs' = if (newps < pmax)
947 then [do put s'; return $! v]
948 else (do put s'; return $! v) : cs
949 put s
950 doAll cs' newps xs
951 Error err -> do put s
952 doAll cs pmax xs
954-- Run an elaborator, and fail if any problems or constraints are introduced
955prunStateT
956 :: Int
957 -> Bool
958 -> [a]
959 -> Maybe [b] -- constraints left, if we're interested
960 -> Control.Monad.State.Strict.StateT
961 (ElabState t) TC t1
962 -> ElabState t
963 -> TC ((t1, Int, Idris.Core.Unify.Fails), ElabState t)
964prunStateT pmax zok ps ivs x s
965 = case runStateT x s of
966 OK (v, s'@(ES (p, _) _ _)) ->
967 let newps = length (problems p) - length ps
968 ibad = badImplementations (implementations p) ivs
969 newpmax = if newps < 0 then 0 else newps in
970 if (newpmax > pmax || (not zok && newps > 0)) -- length ps == 0 && newpmax > 0))
971 then case reverse (problems p) of
972 ((_,_,_,_,e,_,_):_) -> Error e
973 else if ibad
974 then Error (InternalMsg "Constraint introduced in disambiguation")
975 else OK ((v, newpmax, problems p), s')
976 Error e -> Error e
977 where
978 badImplementations _ Nothing = False
979 badImplementations inow (Just ithen) = length inow > length ithen
981debugElaborator :: [ErrorReportPart] -> Elab' aux a
982debugElaborator msg = do ps <- fmap proof get
983 saveState -- so we don't need to remember the hole order
984 hs <- get_holes
985 holeInfo <- mapM getHoleInfo hs
986 loadState
987 lift . Error $ ElabScriptDebug msg (getProofTerm (pterm ps)) holeInfo
988 where getHoleInfo :: Name -> Elab' aux (Name, Type, [(Name, Binder Type)])
989 getHoleInfo h = do focus h
990 g <- goal
991 env <- get_env
992 return (h, g, envBinders env)
994qshow :: Fails -> String
995qshow fs = show (map (\ (x, y, _, _, _, _, _) -> (x, y)) fs)
997dumpprobs [] = ""
998dumpprobs ((_,_,_,e):es) = show e ++ "\n" ++ dumpprobs es