@@ -6,6 +6,7 @@ import Idris.AbsSyntax
66import Idris.Error
77import Idris.Delaborate
88import Idris.Imports
9+import Idris.ElabTerm
910import Paths_idris
1011
1112import Core.TT
@@ -19,22 +20,15 @@ import Control.Monad.State
1920import Data.List
2021import Debug.Trace
2122
22−-- Data to pass to recursively called elaborators; e.g. for where blocks,
23−-- paramaterised declarations, etc.
2423
25−data ElabInfo = EInfo { params :: [(Name, PTerm)],
26− inblock :: Ctxt [Name], -- names in the block, and their params
27− liftname :: Name -> Name }
24+recheckC ctxt fc env t
25+ = do (tm, ty, cs) <- tclift $ recheck ctxt env t
26+ addConstraints fc cs
27+ return (tm, ty)
2828
29−toplevel = EInfo [] emptyContext id
30−
31−recheckC ctxt env t = do (tm, ty, cs) <- tclift $ recheck ctxt env t
32− addConstraints cs
33− return (tm, ty)
34−
35−checkDef ns = do ctxt <- getContext
36− mapM (\(n, t) -> do (t', _) <- recheckC ctxt [] t
37− return (n, t')) ns
29+checkDef fc ns = do ctxt <- getContext
30+ mapM (\(n, t) -> do (t', _) <- recheckC ctxt fc [] t
31+ return (n, t')) ns
3832
3933elabType :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> Idris ()
4034elabType info syn fc n ty' = {- let ty' = piBind (params info) ty_in
@@ -47,10 +41,10 @@ elabType info syn fc n ty' = {- let ty' = piBind (params info) ty_in
4741 logLvl 2 $ show n ++ " type " ++ showImp True ty
4842 ((ty', defer), log) <- tclift $ elaborate ctxt n (Set (UVal 0))
4943 (erun fc (build i info False ty))
50− (cty, _) <- recheckC ctxt [] ty'
44+ (cty, _) <- recheckC ctxt fc [] ty'
5145 logLvl 2 $ "---> " ++ show cty
5246 let nty = normalise ctxt [] cty
53− ds <- checkDef ((n, nty):defer)
47+ ds <- checkDef fc ((n, nty):defer)
5448 addDeferred ds
5549
5650elabData :: ElabInfo -> SyntaxInfo -> FC -> PData -> Idris ()
@@ -63,9 +57,9 @@ elabData info syn fc (PDatadecl n t_in dcons)
6357 let t = addImpl i t_in
6458 ((t', defer), log) <- tclift $ elaborate ctxt n (Set (UVal 0))
6559 (erun fc (build i info False t))
66− def' <- checkDef defer
60+ def' <- checkDef fc defer
6761 addDeferred def'
68− (cty, _) <- recheckC ctxt [] t'
62+ (cty, _) <- recheckC ctxt fc [] t'
6963 logLvl 2 $ "---> " ++ show cty
7064 updateContext (addTyDecl n cty) -- temporary, to check cons
7165 cons <- mapM (elabCon info syn) dcons
@@ -83,10 +77,10 @@ elabCon info syn (n, t_in, fc)
8377 ((t', defer), log) <- tclift $ elaborate ctxt n (Set (UVal 0))
8478 (erun fc (build i info False t))
8579 logLvl 2 $ "Rechecking " ++ show t'
86− def' <- checkDef defer
80+ def' <- checkDef fc defer
8781 addDeferred def'
8882 ctxt <- getContext
89− (cty, _) <- recheckC ctxt [] t'
83+ (cty, _) <- recheckC ctxt fc [] t'
9084 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty
9185 return (n, cty)
9286
@@ -122,7 +116,7 @@ elabVal info aspat tm_in
122116 logLvl 3 ("Value: " ++ show tm')
123117 let vtm = getInferTerm tm'
124118 logLvl 2 (show vtm)
125− recheckC ctxt [] vtm
119+ recheckC ctxt (FC "prompt" 0) [] vtm
126120
127121elabClause :: ElabInfo -> FC -> PClause -> Idris (Term, Term)
128122elabClause info fc (PClause fname lhs_in withs rhs_in whereblock)
@@ -137,7 +131,7 @@ elabClause info fc (PClause fname lhs_in withs rhs_in whereblock)
137131 let lhs_tm = orderPats (getInferTerm lhs')
138132 let lhs_ty = getInferType lhs'
139133 logLvl 3 (show lhs_tm)
140− (clhs, clhsty) <- recheckC ctxt [] lhs_tm
134+ (clhs, clhsty) <- recheckC ctxt fc [] lhs_tm
141135 logLvl 5 ("Checked " ++ show clhs)
142136 -- Elaborate where block
143137 ist <- getIState
@@ -164,10 +158,10 @@ elabClause info fc (PClause fname lhs_in withs rhs_in whereblock)
164158 return $ runState (collectDeferred tt) [])
165159 logLvl 2 $ "---> " ++ show rhs'
166160 when (not (null defer)) $ iLOG $ "DEFERRED " ++ show defer
167− def' <- checkDef defer
161+ def' <- checkDef fc defer
168162 addDeferred def'
169163 ctxt <- getContext
170− (crhs, crhsty) <- recheckC ctxt [] rhs'
164+ (crhs, crhsty) <- recheckC ctxt fc [] rhs'
171165 return (clhs, crhs)
172166 where
173167 decorate x = UN (show fname ++ "#" ++ show x)
@@ -197,7 +191,7 @@ elabClause info fc (PWith fname lhs_in withs wval_in withblock)
197191 let lhs_ty = getInferType lhs'
198192 let ret_ty = getRetTy lhs_ty
199193 logLvl 3 (show lhs_tm)
200− (clhs, clhsty) <- recheckC ctxt [] lhs_tm
194+ (clhs, clhsty) <- recheckC ctxt fc [] lhs_tm
201195 logLvl 5 ("Checked " ++ show clhs)
202196 let bargs = getPBtys lhs_tm
203197 let wval = addImpl i wval_in
@@ -212,9 +206,9 @@ elabClause info fc (PWith fname lhs_in withs wval_in withblock)
212206 psolve lhs_tm
213207 tt <- get_term
214208 return (tt, d))
215− def' <- checkDef defer
209+ def' <- checkDef fc defer
216210 addDeferred def'
217− (cwval, cwvalty) <- recheckC ctxt [] (getInferTerm wval')
211+ (cwval, cwvalty) <- recheckC ctxt fc [] (getInferTerm wval')
218212 logLvl 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)
219213 windex <- getName
220214 -- build a type declaration for the new function:
@@ -224,7 +218,7 @@ elabClause info fc (PWith fname lhs_in withs wval_in withblock)
224218 let wname = MN windex (show fname)
225219 let imps = getImps wtype -- add to implicits context
226220 put (i { idris_implicits = addDef wname imps (idris_implicits i) })
227− def' <- checkDef [(wname, wtype)]
221+ def' <- checkDef fc [(wname, wtype)]
228222 addDeferred def'
229223
230224 -- in the subdecls, lhs becomes:
@@ -247,9 +241,9 @@ elabClause info fc (PWith fname lhs_in withs wval_in withblock)
247241 psolve lhs_tm
248242 tt <- get_term
249243 return (tt, d))
250− def' <- checkDef defer
244+ def' <- checkDef fc defer
251245 addDeferred def'
252− (crhs, crhsty) <- recheckC ctxt [] rhs'
246+ (crhs, crhsty) <- recheckC ctxt fc [] rhs'
253247 return (clhs, crhs)
254248 where
255249 getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t
@@ -485,304 +479,3 @@ elabDecl' info (PDirective i) = i
485479-- elabDecl' info (PImport i) = loadModule i
486480
487481
488−-- Using the elaborator, convert a term in raw syntax to a fully
489−-- elaborated, typechecked term.
490−--
491−-- If building a pattern match, we convert undeclared variables from
492−-- holes to pattern bindings.
493−
494−-- Also find deferred names in the term and their types
495−
496−build :: IState -> ElabInfo -> Bool -> PTerm -> Elab (Term, [(Name, Type)])
497−build ist info pattern tm
498− = do elab ist info pattern tm
499− tt <- get_term
500− return $ runState (collectDeferred tt) []
501−
502−elab :: IState -> ElabInfo -> Bool -> PTerm -> Elab ()
503−elab ist info pattern tm
504− = do elabE tm
505− when pattern -- convert remaining holes to pattern vars
506− mkPat
507− where
508− isph arg = case getTm arg of
509− Placeholder -> True
510− _ -> False
511−
512− toElab arg = case getTm arg of
513− Placeholder -> Nothing
514− v -> Just (priority arg, elabE v)
515−
516− mkPat = do hs <- get_holes
517− case hs of
518− (h: hs) -> do patvar h; mkPat
519− [] -> return ()
520−
521− elabE t = {- do g <- goal
522− tm <- get_term
523− trace ("Elaborating " ++ show t ++ " : " ++ show g ++ "\n\tin " ++ show tm)
524− $ -} elab' t
525−
526− local f = do e <- get_env
527− return (f `elem` map fst e)
528−
529− elab' PSet = do fill RSet; solve
530− elab' (PConstant c) = do apply (RConstant c) []; solve
531− elab' (PQuote r) = do fill r; solve
532− elab' (PTrue fc) = try (elab' (PRef fc unitCon))
533− (elab' (PRef fc unitTy))
534− elab' (PFalse fc) = elab' (PRef fc falseTy)
535− elab' (PResolveTC (FC "HACK" _))
536− = resolveTC 10 ist
537− elab' (PResolveTC fc) = do c <- unique_hole (MN 0 "c")
538− instanceArg c
539− elab' (PRefl fc) = elab' (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,
540− pimp (MN 0 "x") Placeholder])
541− elab' (PEq fc l r) = elab' (PApp fc (PRef fc eqTy) [pimp (MN 0 "a") Placeholder,
542− pimp (MN 0 "b") Placeholder,
543− pexp l, pexp r])
544− elab' (PPair fc l r) = try (elabE (PApp fc (PRef fc pairTy)
545− [pexp l,pexp r]))
546− (elabE (PApp fc (PRef fc pairCon)
547− [pimp (MN 0 "A") Placeholder,
548− pimp (MN 0 "B") Placeholder,
549− pexp l, pexp r]))
550− elab' (PDPair fc l@(PRef _ n) t r)
551− = case t of
552− Placeholder -> try asType asValue
553− _ -> asType
554− where asType = elab' (PApp fc (PRef fc sigmaTy)
555− [pexp t,
556− pexp (PLam n Placeholder r)])
557− asValue = elab' (PApp fc (PRef fc existsCon)
558− [pimp (MN 0 "a") t,
559− pimp (MN 0 "P") Placeholder,
560− pexp l, pexp r])
561− elab' (PDPair fc l t r) = elab' (PApp fc (PRef fc existsCon)
562− [pimp (MN 0 "a") t,
563− pimp (MN 0 "P") Placeholder,
564− pexp l, pexp r])
565− elab' (PRef fc n) | pattern && not (inparamBlock n)
566− = do ctxt <- get_context
567− let sc = case lookupTy n ctxt of
568− Nothing -> True
569− _ -> False
570− if sc
571− then erun fc $
572− try (do apply (Var n) []; solve)
573− (patvar n)
574− else do apply (Var n) []; solve
575− where inparamBlock n = case lookupCtxt n (inblock info) of
576− Nothing -> False
577− _ -> True
578− elab' (PRef fc n) = erun fc $ do apply (Var n) []; solve
579− elab' (PLam n Placeholder sc)
580− = do attack; intro (Just n); elabE sc; solve
581− elab' (PLam n ty sc)
582− = do tyn <- unique_hole (MN 0 "lamty")
583− claim tyn RSet
584− attack
585− introTy (Var tyn) (Just n)
586− -- end_unify
587− focus tyn
588− elabE ty
589− elabE sc
590− solve
591− elab' (PPi _ n Placeholder sc)
592− = do attack; arg n (MN 0 "ty"); elabE sc; solve
593− elab' (PPi _ n ty sc)
594− = do attack; tyn <- unique_hole (MN 0 "ty")
595− claim tyn RSet
596− n' <- case n of
597− MN _ _ -> unique_hole n
598− _ -> return n
599− forall n' (Var tyn)
600− focus tyn
601− elabE ty
602− elabE sc
603− solve
604− elab' (PLet n ty val sc)
605− = do attack;
606− tyn <- unique_hole (MN 0 "letty")
607− claim tyn RSet
608− valn <- unique_hole (MN 0 "letval")
609− claim valn (Var tyn)
610− letbind n (Var tyn) (Var valn)
611− case ty of
612− Placeholder -> return ()
613− _ -> do focus tyn
614− elabE ty
615− focus valn
616− elabE val
617− elabE sc
618− solve
619− elab' (PApp fc (PRef _ f) args')
620− = do let args = {- case lookupCtxt f (inblock info) of
621− Just ps -> (map (pexp . (PRef fc)) ps ++ args')
622− _ ->-} args'
623− ivs <- get_instances
624− try (do ns <- apply (Var f) (map isph args)
625− solve
626− let (ns', eargs)
627− = unzip $
628− sortBy (\(_,x) (_,y) -> compare (priority x) (priority y))
629− (zip ns args)
630− elabArgs [] False ns' (map (\x -> (lazyarg x, getTm x)) eargs))
631− (do apply_elab f (map toElab args)
632− solve)
633− ivs' <- get_instances
634− when (not pattern) $
635− mapM_ (\n -> do focus n
636− resolveTC 10 ist) (ivs' \\ ivs)
637−-- ivs <- get_instances
638−-- when (not (null ivs)) $
639−-- do t <- get_term
640−-- trace (show ivs ++ "\n" ++ show t) $
641−-- mapM_ (\n -> do focus n
642−-- resolveTC ist) ivs
643− where tcArg (n, PConstraint _ _ Placeholder) = True
644− tcArg _ = False
645−
646− elab' (PApp fc f [arg])
647− = erun fc $
648− do simple_app (elabE f) (elabE (getTm arg))
649− solve
650− elab' Placeholder = do (h : hs) <- get_holes
651− movelast h
652− elab' (PMetavar n) = do attack; defer n; solve
653− elab' (PProof ts) = do mapM_ (runTac True ist) ts
654− elab' (PTactics ts) = do mapM_ (runTac False ist) ts
655− elab' (PElabError e) = fail e
656− elab' x = fail $ "Not implemented " ++ show x
657−
658− elabArgs failed retry [] _
659− | retry = let (ns, ts) = unzip (reverse failed) in
660− elabArgs [] False ns ts
661− | otherwise = return ()
662− elabArgs failed r (n:ns) ((_, Placeholder) : args)
663− = elabArgs failed r ns args
664− elabArgs failed r (n:ns) ((lazy, t) : args)
665− | lazy && not pattern
666− = do elabArg n (PApp bi (PRef bi (UN "lazy"))
667− [pimp (UN "a") Placeholder,
668− pexp t]);
669− | otherwise = elabArg n t
670− where elabArg n t = if r
671− then try (do focus n; elabE t; elabArgs failed r ns args)
672− (elabArgs ((n,(lazy, t)):failed) r ns args)
673− else do focus n; elabE t; elabArgs failed r ns args
674−
675−trivial :: IState -> Elab ()
676−trivial ist = try (elab ist toplevel False (PRefl (FC "prf" 0)))
677− (do env <- get_env
678− tryAll (map fst env))
679− where
680− tryAll [] = fail "No trivial solution"
681− tryAll (x:xs) = try (elab ist toplevel False (PRef (FC "prf" 0) x))
682− (tryAll xs)
683−
684−resolveTC :: Int -> IState -> Elab ()
685−resolveTC depth ist
686− = do t <- goal
687− tm <- get_term
688− try (trivial ist)
689− (blunderbuss t (map fst (ctxtAlist (tt_ctxt ist))))
690− where
691− blunderbuss t [] = fail $ "Can't resolve type class " ++ show t
692− blunderbuss t (n:ns) | tcname n = try (resolve n depth)
693− (blunderbuss t ns)
694− | otherwise = blunderbuss t ns
695− tcname (UN ('@':_)) = True
696− tcname (NS _ n) = tcname n
697− tcname _ = False
698−
699− resolve n depth
700− | depth == 0 = fail $ "Can't resolve type class"
701− | otherwise
702− = do t <- goal
703− let imps = case lookupCtxt n (idris_implicits ist) of
704− Nothing -> []
705− Just args -> map isImp args
706− args <- apply (Var n) imps
707− mapM_ (\ (_,n) -> do focus n
708− resolveTC (depth - 1) ist)
709− (filter (\ (x, y) -> not x) (zip imps args))
710− solve
711− where isImp (PImp _ _ _ _) = True
712− isImp _ = False
713−
714−collectDeferred :: Term -> State [(Name, Type)] Term
715−collectDeferred (Bind n (GHole t) app) =
716− do ds <- get
717− put ((n, t) : ds)
718− return app
719−collectDeferred (Bind n b t) = do b' <- cdb b
720− t' <- collectDeferred t
721− return (Bind n b' t')
722− where
723− cdb (Let t v) = liftM2 Let (collectDeferred t) (collectDeferred v)
724− cdb (Guess t v) = liftM2 Guess (collectDeferred t) (collectDeferred v)
725− cdb b = do ty' <- collectDeferred (binderTy b)
726− return (b { binderTy = ty' })
727−collectDeferred (App f a) = liftM2 App (collectDeferred f) (collectDeferred a)
728−collectDeferred t = return t
729−
730−-- Running tactics directly
731−
732−runTac :: Bool -> IState -> PTactic -> Elab ()
733−runTac autoSolve ist tac = runT (fmap (addImpl ist) tac) where
734− runT (Intro []) = do g <- goal
735− attack; intro (bname g)
736− where
737− bname (Bind n _ _) = Just n
738− bname _ = Nothing
739− runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs
740− runT (Exact tm) = do elab ist toplevel False tm
741− when autoSolve solveAll
742− runT (Refine fn []) = do imps <- case lookupCtxt fn (idris_implicits ist) of
743− Nothing -> envArgs fn
744− Just args -> return $ map isImp args
745− ns <- apply (Var fn) imps
746− when autoSolve solveAll
747− where isImp (PImp _ _ _ _) = True
748− isImp _ = False
749− envArgs n = do e <- get_env
750− case lookup n e of
751− Just t -> return $ map (const False)
752− (getArgTys (binderTy t))
753− _ -> return []
754− runT (Refine fn imps) = do ns <- apply (Var fn) imps
755− when autoSolve solveAll
756− runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that
757− = do attack; -- (h:_) <- get_holes
758− tyn <- unique_hole (MN 0 "rty")
759− -- start_unify h
760− claim tyn RSet
761− valn <- unique_hole (MN 0 "rval")
762− claim valn (Var tyn)
763− letn <- unique_hole (MN 0 "rewrite_rule")
764− letbind letn (Var tyn) (Var valn)
765− focus valn
766− elab ist toplevel False tm
767− rewrite (Var letn)
768− when autoSolve solveAll
769− runT (LetTac n tm)
770− = do attack
771− tyn <- unique_hole (MN 0 "letty")
772− claim tyn RSet
773− valn <- unique_hole (MN 0 "letval")
774− claim valn (Var tyn)
775− letn <- unique_hole n
776− letbind letn (Var tyn) (Var valn)
777− focus valn
778− elab ist toplevel False tm
779− when autoSolve solveAll
780− runT Compute = compute
781− runT Trivial = do trivial ist; when autoSolve solveAll
782− runT (Focus n) = focus n
783− runT Solve = solve
784− runT (Try l r) = do try (runT l) (runT r)
785− runT (TSeq l r) = do runT l; runT r
786− runT x = fail $ "Not implemented " ++ show x
787−
788−solveAll = try (do solve; solveAll) (return ())