@@ -10,12 +10,13 @@ import Idris.Error
1010import Idris.ProofSearch
1111import Idris.Output (pshow)
1212
13−import Idris.Core.CaseTree (SC, SC'(STerm))
13+import Idris.Core.CaseTree (SC, SC'(STerm), findCalls, findUsedArgs)
1414import Idris.Core.Elaborate hiding (Tactic(..))
1515import Idris.Core.TT
1616import Idris.Core.Evaluate
1717import Idris.Core.Unify
1818import Idris.Core.Typecheck (check, recheck)
19+import Idris.Coverage (buildSCG, checkDeclTotality, genClauses, recoverableCoverage, validCoverageCase)
1920import Idris.ErrReverse (errReverse)
2021import Idris.ElabQuasiquote (extractUnquotes)
2122import Idris.Elab.Utils
@@ -49,24 +50,6 @@ data ElabResult =
4950 -- ^ Meta-info about the new type declarations
5051 }
5152
52−processTacticDecls :: [RDeclInstructions] -> Idris ()
53−processTacticDecls info =
54− forM_ info $ \case
55− RTyDeclInstrs n fc impls ty ->
56− do logLvl 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty
57− logLvl 3 $ " It has impls " ++ show impls
58− updateIState $ \i -> i { idris_implicits =
59− addDef n impls (idris_implicits i) }
60− addIBC (IBCImp n)
61− ds <- checkDef fc (\_ e -> e) [(n, (-1, Nothing, ty))]
62− addIBC (IBCDef n)
63− let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
64− addDeferred ds'
65− RClausesInstrs n cs ->
66− do logLvl 3 $ "Pattern-matching definition from tactics: " ++ show n
67− solveDeferred n
68− updateIState $ \i -> i { idris_patdefs = addDef n (cs, []) $ idris_patdefs i } -- TODO: missing clauses
69− addIBC (IBCDef n)
7053
7154-- Using the elaborator, convert a term in raw syntax to a fully
7255-- elaborated, typechecked term.
@@ -1628,7 +1611,7 @@ runTactical fc env tm = do tm' <- eval tm
16281611 addCasedef n (const [])
16291612 info False (STerm Erased)
16301613 True False -- TODO what are these?
1631− [] [] -- TODO argument types, inaccessible types
1614+ (map snd $ getArgTys ty) [] -- TODO inaccessible types
16321615 clauses'
16331616 clauses''
16341617 clauses''
@@ -2088,3 +2071,107 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
20882071 parts -> ReflectionError errorparts e
20892072
20902073solveAll = try (do solve; solveAll) (return ())
2074+
2075+-- | Do the left-over work after creating declarations in reflected
2076+-- elaborator scripts
2077+processTacticDecls :: ElabInfo -> [RDeclInstructions] -> Idris ()
2078+processTacticDecls info steps =
2079+ -- The order of steps is important: type declarations might
2080+ -- establish metavars that later function bodies resolve.
2081+ forM_ (reverse steps) $ \case
2082+ RTyDeclInstrs n fc impls ty ->
2083+ do logLvl 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty
2084+ logLvl 3 $ " It has impls " ++ show impls
2085+ updateIState $ \i -> i { idris_implicits =
2086+ addDef n impls (idris_implicits i) }
2087+ addIBC (IBCImp n)
2088+ ds <- checkDef fc (\_ e -> e) [(n, (-1, Nothing, ty))]
2089+ addIBC (IBCDef n)
2090+ ctxt <- getContext
2091+ case lookupDef n ctxt of
2092+ (TyDecl _ _ : _) ->
2093+ -- If the function isn't defined at the end of the elab script,
2094+ -- then it must be added as a metavariable. This needs guarding
2095+ -- to prevent overwriting case defs with a metavar, if the case
2096+ -- defs come after the type decl in the same script!
2097+ let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds
2098+ in addDeferred ds'
2099+ _ -> return ()
2100+ RClausesInstrs n cs ->
2101+ do logLvl 3 $ "Pattern-matching definition from tactics: " ++ show n
2102+ solveDeferred n
2103+ let lhss = map (\(_, lhs, _) -> lhs) cs
2104+ let fc = fileFC "elab_reflected"
2105+ pmissing <-
2106+ do ist <- getIState
2107+ possible <- genClauses fc n lhss
2108+ (map (\lhs ->
2109+ delab' ist lhs True True) lhss)
2110+ missing <- filterM (checkPossible n) possible
2111+ return (filter (noMatch ist lhss) missing)
2112+ let tot = if null pmissing
2113+ then Unchecked -- still need to check recursive calls
2114+ else Partial NotCovering -- missing cases implies not total
2115+ setTotality n tot
2116+ updateIState $ \i -> i { idris_patdefs =
2117+ addDef n (cs, pmissing) $ idris_patdefs i }
2118+ addIBC (IBCDef n)
2119+
2120+ ctxt <- getContext
2121+ case lookupDefExact n ctxt of
2122+ Just (CaseOp _ _ _ _ _ cd) ->
2123+ -- Here, we populate the call graph with a list of things
2124+ -- we refer to, so that if they aren't total, the whole
2125+ -- thing won't be.
2126+ let (scargs, sc) = cases_compiletime cd
2127+ (scargs', sc') = cases_runtime cd
2128+ calls = findCalls sc' scargs
2129+ used = findUsedArgs sc' scargs'
2130+ cg = CGInfo scargs' calls [] used []
2131+ in do logLvl 2 $ "Called names in reflected elab: " ++ show cg
2132+ addToCG n cg
2133+ addToCalledG n (nub (map fst calls))
2134+ addIBC $ IBCCG n
2135+ Just _ -> return () -- TODO throw internal error
2136+ Nothing -> return ()
2137+
2138+ -- checkDeclTotality requires that the call graph be present
2139+ -- before calling it.
2140+ -- TODO: reduce code duplication with Idris.Elab.Clause
2141+ buildSCG (fc, n)
2142+
2143+ -- Actually run the totality checker. In the main clause
2144+ -- elaborator, this is deferred until after. Here, we run it
2145+ -- now to get totality information as early as possible.
2146+ tot' <- checkDeclTotality (fc, n)
2147+ setTotality n tot'
2148+ when (tot' /= Unchecked) $ addIBC (IBCTotal n tot')
2149+ where
2150+ -- TODO: see if the code duplication with Idris.Elab.Clause can be
2151+ -- reduced or eliminated.
2152+ checkPossible :: Name -> PTerm -> Idris Bool
2153+ checkPossible fname lhs_in =
2154+ do ctxt <- getContext
2155+ ist <- getIState
2156+ let lhs = addImplPat ist lhs_in
2157+ let fc = fileFC "elab_reflected_totality"
2158+ let tcgen = False -- TODO: later we may support dictionary generation
2159+ case elaborate ctxt (sMN 0 "refPatLHS") infP initEState
2160+ (erun fc (buildTC ist info ELHS [] fname (infTerm lhs))) of
2161+ OK (ElabResult lhs' _ _ _ _, _) ->
2162+ do -- not recursively calling here, because we don't
2163+ -- want to run infinitely many times
2164+ let lhs_tm = orderPats (getInferTerm lhs')
2165+ case recheck ctxt [] (forget lhs_tm) lhs_tm of
2166+ OK _ -> return True
2167+ err -> return False
2168+ -- if it's a recoverable error, the case may become possible
2169+ Error err -> if tcgen then return (recoverableCoverage ctxt err)
2170+ else return (validCoverageCase ctxt err ||
2171+ recoverableCoverage ctxt err)
2172+
2173+
2174+ -- TODO: Attempt to reduce/eliminate code duplication with Idris.Elab.Clause
2175+ noMatch i cs tm = all (\x -> case matchClause i (delab' i x True True) tm of
2176+ Right _ -> False
2177+ Left _ -> True) cs