{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor #-} module Idris.ElabDecls where import Idris.AbsSyntax import Idris.Error import Idris.Delaborate import Idris.Imports import Idris.ElabTerm import Idris.Coverage import Idris.DataOpts import Paths_idris import Core.TT import Core.Elaborate hiding (Tactic(..)) import Core.Evaluate import Core.Typecheck import Core.CaseTree import Control.Monad import Control.Monad.State import Data.List import Data.Maybe import Debug.Trace recheckC ctxt fc env t = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...) (tm, ty, cs) <- tclift $ recheck ctxt env (forget t) t addConstraints fc cs return (tm, ty) checkDef fc ns = do ctxt <- getContext mapM (\(n, t) -> do (t', _) <- recheckC ctxt fc [] t return (n, t')) ns elabType :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> Idris () elabType info syn fc n ty' = {- let ty' = piBind (params info) ty_in n = liftname info n_in in -} do checkUndefined fc n ctxt <- getContext i <- get ty' <- implicit syn n ty' let ty = addImpl i ty' logLvl 2 $ show n ++ " type " ++ showImp True ty ((ty', defer, is), log) <- tclift $ elaborate ctxt n (Set (UVal 0)) [] (erun fc (build i info False n ty)) (cty, _) <- recheckC ctxt fc [] ty' logLvl 2 $ "---> " ++ show cty let nty = normalise ctxt [] cty ds <- checkDef fc ((n, nty):defer) addIBC (IBCDef n) addDeferred ds mapM_ (elabCaseBlock info) is elabData :: ElabInfo -> SyntaxInfo -> FC -> PData -> Idris () elabData info syn fc (PDatadecl n t_in dcons) = do iLOG (show fc) checkUndefined fc n ctxt <- getContext i <- get t_in <- implicit syn n t_in let t = addImpl i t_in ((t', defer, is), log) <- tclift $ elaborate ctxt n (Set (UVal 0)) [] (erun fc (build i info False n t)) def' <- checkDef fc defer addDeferred def' mapM_ (elabCaseBlock info) is (cty, _) <- recheckC ctxt fc [] t' logLvl 2 $ "---> " ++ show cty updateContext (addTyDecl n cty) -- temporary, to check cons cons <- mapM (elabCon info syn) dcons ttag <- getName i <- get put (i { idris_datatypes = addDef n (TI (map fst cons)) (idris_datatypes i) }) addIBC (IBCDef n) addIBC (IBCData n) collapseCons n cons updateContext (addDatatype (Data n ttag cty cons)) elabCon :: ElabInfo -> SyntaxInfo -> (Name, PTerm, FC) -> Idris (Name, Type) elabCon info syn (n, t_in, fc) = do checkUndefined fc n ctxt <- getContext i <- get t_in <- implicit syn n t_in let t = addImpl i t_in logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ showImp True t ((t', defer, is), log) <- tclift $ elaborate ctxt n (Set (UVal 0)) [] (erun fc (build i info False n t)) logLvl 2 $ "Rechecking " ++ show t' def' <- checkDef fc defer addDeferred def' mapM_ (elabCaseBlock info) is ctxt <- getContext (cty, _) <- recheckC ctxt fc [] t' logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty addIBC (IBCDef n) forceArgs n cty return (n, cty) elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris () elabClauses info fc opts n_in cs = let n = liftname info n_in in do pats_in <- mapM (elabClause info fc (TCGen `elem` opts)) cs solveDeferred n let pats = mapMaybe id pats_in logLvl 3 (showSep "\n" (map (\ (l,r) -> show l ++ " = " ++ show r) pats)) ist <- get let tcase = opt_typecase (idris_options ist) let pdef = map debind (map (simpl (tt_ctxt ist)) pats) cov <- coverage pcover <- if cov then idrisCatch (do missing <- genClauses fc n (map fst pdef) cs mapM_ (elabClause info fc True) missing return True) (\c -> do -- iputStrLn $ "Warning: " ++ show c return False) else return False pdef' <- applyOpts pdef let tree = simpleCase tcase pcover pdef let tree' = simpleCase tcase pcover pdef' tclift $ sameLength pdef logLvl 3 (show tree) logLvl 3 $ "Optimised: " ++ show tree' ctxt <- getContext ist <- get put (ist { idris_patdefs = addDef n pdef' (idris_patdefs ist) }) case lookupTy (namespace info) n ctxt of [ty] -> do updateContext (addCasedef n (inlinable opts) tcase pcover pdef pdef' ty) addIBC (IBCDef n) [] -> return () where debind (x, y) = (depat x, depat y) depat (Bind n (PVar t) sc) = depat (instantiate (P Bound n t) sc) depat x = x simpl ctxt (x, y) = (x, simplify ctxt [] y) sameLength ((x, _) : xs) = do l <- sameLength xs let (f, as) = unApply x if (null xs || l == length as) then return (length as) else tfail (At fc (Msg "Clauses have differing numbers of arguments ")) sameLength [] = return 0 elabVal :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type) elabVal info aspat tm_in = do ctxt <- getContext i <- get let tm = addImpl i tm_in logLvl 10 (showImp True tm) ((tm', defer, is), _) <- tclift $ elaborate ctxt (MN 0 "val") infP [] (build i info aspat (MN 0 "val") (infTerm tm)) logLvl 3 ("Value: " ++ show tm') let vtm = getInferTerm tm' logLvl 2 (show vtm) recheckC ctxt (FC "prompt" 0) [] vtm elabClause :: ElabInfo -> FC -> Bool -> PClause -> Idris (Maybe (Term, Term)) elabClause info fc tcgen (PClause fname lhs_in [] PImpossible []) = do ctxt <- getContext i <- get let lhs = addImpl i lhs_in -- if the LHS type checks, it is possible, so report an error case elaborate ctxt (MN 0 "patLHS") infP [] (erun fc (buildTC i info True tcgen fname (infTerm lhs))) of OK ((lhs', _, _), _) -> do let lhs_tm = orderPats (getInferTerm lhs') checkInferred fc (delab' i lhs_tm True) lhs fail $ show fc ++ ":" ++ showImp True (delab' i lhs_tm True) ++ " is a possible case" ++ "\n" ++ showImp True lhs Error _ -> return () return Nothing elabClause info fc tcgen (PClause fname lhs_in withs rhs_in whereblock) = do ctxt <- getContext -- Build the LHS as an "Infer", and pull out its type and -- pattern bindings i <- get let lhs = addImpl i lhs_in logLvl 5 ("LHS: " ++ showImp True lhs) ((lhs', dlhs, []), _) <- tclift $ elaborate ctxt (MN 0 "patLHS") infP [] (erun fc (buildTC i info True tcgen fname (infTerm lhs))) let lhs_tm = orderPats (getInferTerm lhs') let lhs_ty = getInferType lhs' logLvl 3 (show lhs_tm) (clhs, clhsty) <- recheckC ctxt fc [] lhs_tm logLvl 5 ("Checked " ++ show clhs) -- Elaborate where block ist <- getIState windex <- getName let winfo = pinfo (pvars ist lhs_tm) whereblock windex let decls = concatMap declared whereblock let newargs = pvars ist lhs_tm let wb = map (expandParamsD ist decorate newargs decls) whereblock logLvl 5 $ show wb mapM_ (elabDecl' info) wb -- Now build the RHS, using the type of the LHS as the goal. i <- get -- new implicits from where block logLvl 5 (showImp True (expandParams decorate newargs decls rhs_in)) let rhs = addImpl i (expandParams decorate newargs decls rhs_in) -- TODO: but don't do names in scope logLvl 2 (showImp True rhs) ctxt <- getContext -- new context with where block added ((rhs', defer, is), _) <- tclift $ elaborate ctxt (MN 0 "patRHS") clhsty [] (do pbinds lhs_tm (_, _, is) <- erun fc (build i info False fname rhs) psolve lhs_tm tt <- get_term let (tm, ds) = runState (collectDeferred tt) [] return (tm, ds, is)) logLvl 2 $ "---> " ++ show rhs' when (not (null defer)) $ iLOG $ "DEFERRED " ++ show defer def' <- checkDef fc defer addDeferred def' mapM_ (elabCaseBlock info) is ctxt <- getContext logLvl 5 $ "Rechecking" (crhs, crhsty) <- recheckC ctxt fc [] rhs' i <- get checkInferred fc (delab' i crhs True) rhs return $ Just (clhs, crhs) where decorate x = UN (show fname ++ "#" ++ show x) pinfo ns ps i = let ds = concatMap declared ps newps = params info ++ ns dsParams = map (\n -> (n, map fst newps)) ds newb = addAlist dsParams (inblock info) l = liftname info in info { params = newps, inblock = newb, liftname = id -- (\n -> case lookupCtxt n newb of -- Nothing -> n -- _ -> MN i (show n)) . l } elabClause info fc tcgen (PWith fname lhs_in withs wval_in withblock) = do ctxt <- getContext -- Build the LHS as an "Infer", and pull out its type and -- pattern bindings i <- get let lhs = addImpl i lhs_in logLvl 5 ("LHS: " ++ showImp True lhs) ((lhs', dlhs, []), _) <- tclift $ elaborate ctxt (MN 0 "patLHS") infP [] (erun fc (buildTC i info True tcgen fname (infTerm lhs))) let lhs_tm = orderPats (getInferTerm lhs') let lhs_ty = getInferType lhs' let ret_ty = getRetTy lhs_ty logLvl 3 (show lhs_tm) (clhs, clhsty) <- recheckC ctxt fc [] lhs_tm logLvl 5 ("Checked " ++ show clhs) let bargs = getPBtys lhs_tm let wval = addImpl i wval_in logLvl 5 ("Checking " ++ showImp True wval) -- Elaborate wval in this context ((wval', defer, is), _) <- tclift $ elaborate ctxt (MN 0 "withRHS") (bindTyArgs PVTy bargs infP) [] (do pbinds lhs_tm -- TODO: may want where here - see winfo abpve (_', d, is) <- erun fc (build i info False fname (infTerm wval)) psolve lhs_tm tt <- get_term return (tt, d, is)) def' <- checkDef fc defer addDeferred def' mapM_ (elabCaseBlock info) is (cwval, cwvalty) <- recheckC ctxt fc [] (getInferTerm wval') logLvl 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty) windex <- getName -- build a type declaration for the new function: -- (ps : Xs) -> (withval : cwvalty) -> ret_ty let wtype = bindTyArgs Pi (bargs ++ [(MN 0 "warg", getRetTy cwvalty)]) ret_ty logLvl 3 ("New function type " ++ show wtype) let wname = MN windex (show fname) let imps = getImps wtype -- add to implicits context put (i { idris_implicits = addDef wname imps (idris_implicits i) }) addIBC (IBCDef wname) def' <- checkDef fc [(wname, wtype)] addDeferred def' -- in the subdecls, lhs becomes: -- fname pats | wpat [rest] -- ==> fname' ps wpat [rest], match pats against toplevel for ps wb <- mapM (mkAuxC wname lhs (map fst bargs)) withblock logLvl 5 ("with block " ++ show wb) mapM_ (elabDecl info) wb -- rhs becomes: fname' ps wval let rhs = PApp fc (PRef fc wname) (map (pexp . (PRef fc) . fst) bargs ++ [pexp wval]) logLvl 3 ("New RHS " ++ show rhs) ctxt <- getContext -- New context with block added i <- get ((rhs', defer, is), _) <- tclift $ elaborate ctxt (MN 0 "wpatRHS") clhsty [] (do pbinds lhs_tm (_, d, is) <- erun fc (build i info False fname rhs) psolve lhs_tm tt <- get_term return (tt, d, is)) def' <- checkDef fc defer addDeferred def' mapM_ (elabCaseBlock info) is (crhs, crhsty) <- recheckC ctxt fc [] rhs' return $ Just (clhs, crhs) where getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t getImps _ = [] mkAuxC wname lhs ns (PClauses fc o n cs) | True = do cs' <- mapM (mkAux wname lhs ns) cs return $ PClauses fc o wname cs' | otherwise = fail $ show fc ++ "with clause uses wrong function name " ++ show n mkAuxC wname lhs ns d = return $ d mkAux wname toplhs ns (PClause n tm_in (w:ws) rhs wheres) = do i <- get let tm = addImpl i tm_in logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++ showImp True toplhs) case matchClause toplhs tm of Left _ -> fail $ show fc ++ "with clause does not match top level" Right mvars -> do logLvl 3 ("Match vars : " ++ show mvars) lhs <- updateLHS n wname mvars ns (fullApp tm) w return $ PClause wname lhs ws rhs wheres mkAux wname toplhs ns (PWith n tm_in (w:ws) wval withs) = do i <- get let tm = addImpl i tm_in logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++ showImp True toplhs) withs' <- mapM (mkAuxC wname toplhs ns) withs case matchClause toplhs tm of Left _ -> fail $ show fc ++ "with clause does not match top level" Right mvars -> do lhs <- updateLHS n wname mvars ns (fullApp tm) w return $ PWith wname lhs ws wval withs' updateLHS n wname mvars ns (PApp fc (PRef fc' n') args) w = return $ substMatches mvars $ PApp fc (PRef fc' wname) (map (pexp . (PRef fc')) ns ++ [pexp w]) updateLHS n wname mvars ns tm w = fail $ "Not implemented match " ++ show tm fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs)) fullApp x = x data MArgTy = IA | EA | CA deriving Show elabClass :: ElabInfo -> SyntaxInfo -> FC -> [PTerm] -> Name -> [(Name, PTerm)] -> [PDecl] -> Idris () elabClass info syn fc constraints tn ps ds = do let cn = UN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn) let tty = pibind ps PSet let constraint = PApp fc (PRef fc tn) (map (pexp . PRef fc) (map fst ps)) -- build data declaration ims <- mapM tdecl (filter tydecl ds) defs <- mapM (defdecl (map (\ (x,y,z) -> z) ims) constraint) (filter clause ds) let (methods, imethods) = unzip (map (\ (x,y,z) -> (x, y)) ims) let cty = impbind ps $ conbind constraints $ pibind methods constraint let cons = [(cn, cty, fc)] let ddecl = PData syn fc (PDatadecl tn tty cons) elabDecl info ddecl -- for each constraint, build a top level function to chase it let usyn = syn { using = ps ++ using syn } fns <- mapM (cfun cn constraint usyn (map fst imethods)) constraints mapM_ (elabDecl info) (concat fns) -- for each method, build a top level function fns <- mapM (tfun cn constraint usyn (map fst imethods)) imethods mapM_ (elabDecl info) (concat fns) -- add the default definitions mapM_ (elabDecl info) (concat (map (snd.snd) defs)) i <- get let defaults = map (\ (x, (y, z)) -> (x,y)) defs put (i { idris_classes = addDef tn (CI cn imethods defaults (map fst ps)) (idris_classes i) }) addIBC (IBCClass tn) where pibind [] x = x pibind ((n, ty): ns) x = PPi expl n ty (pibind ns x) impbind [] x = x impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x) conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x) conbind [] x = x tdecl (PTy syn _ n t) = do t' <- implicit syn n t return ( (n, (toExp (map fst ps) Exp t')), (n, (toExp (map fst ps) Imp t')), (n, (syn, t) ) ) tdecl _ = fail "Not allowed in a class declaration" -- Create default definitions defdecl mtys c d@(PClauses fc opts n cs) = case lookup n mtys of Just (syn, ty) -> do let ty' = insertConstraint c ty let ds = map (decorateid defaultdec) [PTy syn fc n ty', PClauses fc (TCGen:opts) n cs] iLOG (show ds) return (n, (defaultdec n, ds)) _ -> fail $ show n ++ " is not a method" defdecl _ _ _ = fail "Can't happen (defdecl)" defaultdec (UN n) = UN ("default#" ++ n) defaultdec (NS n ns) = NS (defaultdec n) ns tydecl (PTy _ _ _ _) = True tydecl _ = False clause (PClauses _ _ _ _) = True clause _ = False cfun cn c syn all con = do let cfn = UN ('@':show cn ++ "#" ++ show con) let mnames = take (length all) $ map (\x -> MN x "meth") [0..] let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames) let lhs = PApp fc (PRef fc cfn) [pconst capp] let rhs = PResolveTC (FC "HACK" 0) let ty = PPi constraint (MN 0 "pc") c con iLOG (showImp True ty) iLOG (showImp True lhs ++ " = " ++ showImp True rhs) return [PTy syn fc cfn ty, PClauses fc [Inlinable,TCGen] cfn [PClause cfn lhs [] rhs []]] tfun cn c syn all (m, ty) = do let ty' = insertConstraint c ty let mnames = take (length all) $ map (\x -> MN x "meth") [0..] let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames) let margs = getMArgs ty let anames = map (\x -> MN x "arg") [0..] let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames) let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames) iLOG (showImp True ty) iLOG (show (m, ty', capp, margs)) iLOG (showImp True lhs ++ " = " ++ showImp True rhs) return [PTy syn fc m ty', PClauses fc [Inlinable,TCGen] m [PClause m lhs [] rhs []]] getMArgs (PPi (Imp _ _) n ty sc) = IA : getMArgs sc getMArgs (PPi (Exp _ _) n ty sc) = EA : getMArgs sc getMArgs (PPi (Constraint _ _) n ty sc) = CA : getMArgs sc getMArgs _ = [] getMeth (m:ms) (a:as) x | x == a = PRef fc m | otherwise = getMeth ms as x lhsArgs (EA : xs) (n : ns) = pexp (PRef fc n) : lhsArgs xs ns lhsArgs (IA : xs) ns = lhsArgs xs ns lhsArgs (CA : xs) ns = lhsArgs xs ns lhsArgs [] _ = [] rhsArgs (EA : xs) (n : ns) = pexp (PRef fc n) : rhsArgs xs ns rhsArgs (IA : xs) ns = pexp Placeholder : rhsArgs xs ns rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns rhsArgs [] _ = [] insertConstraint c (PPi p@(Imp _ _) n ty sc) = PPi p n ty (insertConstraint c sc) insertConstraint c sc = PPi constraint (MN 0 "c") c sc -- make arguments explicit and don't bind class parameters toExp ns e (PPi (Imp l s) n ty sc) | n `elem` ns = toExp ns e sc | otherwise = PPi (e l s) n ty (toExp ns e sc) toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc) toExp ns e sc = sc elabInstance :: ElabInfo -> SyntaxInfo -> FC -> [PTerm] -> Name -> [PTerm] -> PTerm -> [PDecl] -> Idris () elabInstance info syn fc cs n ps t ds = do i <- get (n, ci) <- case lookupCtxtName (namespace info) n (idris_classes i) of [c] -> return c _ -> fail $ show n ++ " is not a type class" let iname = UN ('@':show n ++ "$" ++ show ps) elabType info syn fc iname t let ips = zip (class_params ci) ps let ns = case n of NS n ns' -> ns' _ -> [] let mtys = map (\ (n, t) -> let t' = substMatches ips t in (decorate ns n, coninsert cs t', t')) (class_methods ci) logLvl 3 (show (mtys, ips)) let ds' = insertDefaults (class_defaults ci) ns ds iLOG ("Defaults inserted: " ++ show ds' ++ "\n" ++ show ci) mapM_ (warnMissing ds' ns) (map fst (class_methods ci)) let wb = map mkTyDecl mtys ++ map (decorateid (decorate ns)) ds' let lhs = PRef fc iname let rhs = PApp fc (PRef fc (instanceName ci)) (map (pexp . mkMethApp) mtys) let idecl = PClauses fc [Inlinable, TCGen] iname [PClause iname lhs [] rhs wb] iLOG (show idecl) elabDecl info idecl where mkMethApp (n, _, ty) = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty)) lamBind i (PPi (Constraint _ _) _ _ sc) sc' = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc') lamBind i (PPi _ n ty sc) sc' = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc') lamBind i _ sc = sc methArgs i (PPi (Imp _ _) n ty sc) = PImp 0 False n (PRef fc (MN i "meth")) : methArgs (i+1) sc methArgs i (PPi (Exp _ _) n ty sc) = PExp 0 False (PRef fc (MN i "meth")) : methArgs (i+1) sc methArgs i (PPi (Constraint _ _) n ty sc) = PConstraint 0 False (PResolveTC fc) : methArgs (i+1) sc methArgs i _ = [] papp fc f [] = f papp fc f as = PApp fc f as decorate ns (UN n) = NS (UN ('!':n)) ns decorate ns (NS (UN n) s) = NS (UN ('!':n)) ns mkTyDecl (n, t, _) = PTy syn fc n t conbind (ty : ns) x = PPi constraint (MN 0 "c") ty (conbind ns x) conbind [] x = x coninsert cs (PPi p@(Imp _ _) n t sc) = PPi p n t (coninsert cs sc) coninsert cs sc = conbind cs sc insertDefaults :: [(Name, Name)] -> [String] -> [PDecl] -> [PDecl] insertDefaults [] ns ds = ds insertDefaults ((n,dn) : defs) ns ds = insertDefaults defs ns (insertDef n dn ns ds) insertDef meth def ns decls | null $ filter (clauseFor meth ns) decls = decls ++ [PClauses fc [Inlinable,TCGen] meth [PClause meth (PApp fc (PRef fc meth) []) [] (PApp fc (PRef fc def) []) []]] | otherwise = decls warnMissing decls ns meth | null $ filter (clauseFor meth ns) decls = iWarn fc $ "method " ++ show meth ++ " not defined" | otherwise = return () clauseFor m ns (PClauses _ _ m' _) = decorate ns m == decorate ns m' clauseFor m ns _ = False decorateid decorate (PTy s f n t) = PTy s f (decorate n) t decorateid decorate (PClauses f o n cs) = PClauses f o (decorate n) (map dc cs) where dc (PClause n t as w ds) = PClause (decorate n) (dappname t) as w ds dc (PWith n t as w ds) = PWith (decorate n) (dappname t) as w (map (decorateid decorate) ds) dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as dappname t = t pbinds (Bind n (PVar t) sc) = do attack; patbind n pbinds sc pbinds tm = return () pbty (Bind n (PVar t) sc) tm = Bind n (PVTy t) (pbty sc tm) pbty _ tm = tm getPBtys (Bind n (PVar t) sc) = (n, t) : getPBtys sc getPBtys _ = [] psolve (Bind n (PVar t) sc) = do solve; psolve sc psolve tm = return () pvars ist (Bind n (PVar t) sc) = (n, delab ist t) : pvars ist sc pvars ist _ = [] -- TODO: Also build a 'binary' version of each declaration for fast reloading elabDecl :: ElabInfo -> PDecl -> Idris () elabDecl info d = idrisCatch (elabDecl' info d) (\e -> do let msg = show e setErrLine (getErrLine msg) iputStrLn msg) elabDecl' info (PFix _ _ _) = return () -- nothing to elaborate elabDecl' info (PSyntax _ p) = return () -- nothing to elaborate elabDecl' info (PTy s f n ty) = do iLOG $ "Elaborating type decl " ++ show n elabType info s f n ty elabDecl' info (PData s f d) = do iLOG $ "Elaborating " ++ show (d_name d) elabData info s f d elabDecl' info d@(PClauses f o n ps) = do iLOG $ "Elaborating clause " ++ show n elabClauses info f o n ps elabDecl' info (PParams f ns ps) = mapM_ (elabDecl' pinfo) ps where pinfo = let ds = concatMap declared ps newps = params info ++ ns dsParams = map (\n -> (n, map fst newps)) ds newb = addAlist dsParams (inblock info) in info { params = newps, inblock = newb } elabDecl' info (PNamespace n ps) = mapM_ (elabDecl' ninfo) ps where ninfo = case namespace info of Nothing -> info { namespace = Just [n] } Just ns -> info { namespace = Just (n:ns) } elabDecl' info (PClass s f cs n ps ds) = do iLOG $ "Elaborating class " ++ show n elabClass info s f cs n ps ds elabDecl' info (PInstance s f cs n ps t ds) = do iLOG $ "Elaborating instance " ++ show n elabInstance info s f cs n ps t ds elabDecl' info (PDirective i) = i elabCaseBlock info d@(PClauses f o n ps) = do addIBC (IBCDef n) elabDecl' info d -- elabDecl' info (PImport i) = loadModule i -- Check that the result of type checking matches what the programmer wrote -- (i.e. - if we inferred any arguments that the user provided, make sure -- they are the same!) checkInferred :: FC -> PTerm -> PTerm -> Idris () checkInferred fc inf user = do logLvl 6 $ "Checked to\n" ++ showImp True inf ++ "\n" ++ showImp True user tclift $ case matchClause' True user inf of Right vs -> return () Left (x, y) -> tfail $ At fc (Msg $ "The type-checked term and given term do not match: " ++ show x ++ " and " ++ show y) -- ++ "\n" ++ showImp True inf ++ "\n" ++ showImp True user)