e80793d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Allow Elab scripts to do type class resolution

e80793dDavid Raymond Christiansen11 years ago

libs/prelude/Language/Reflection/Elab.idr+8

compare with master

unifiedsplit

@@ -76,6 +76,7 @@ data Elab : Type -> Type where

76 prim__DefineFunction : FunDefn -> Elab ()

77 prim__AddInstance : TTName -> TTName -> Elab ()

79+ prim__ResolveTC : TTName -> Elab ()

79 prim__RecursiveElab : Raw -> Elab () -> Elab (TT, TT)

80 prim__RecursiveElab : Raw -> Elab () -> Elab (TT, TT)

81 prim__Debug : {a : Type} -> Maybe String -> Elab a

82 prim__Debug : {a : Type} -> Maybe String -> Elab a

@@ -212,6 +213,13 @@ defineFunction defun = prim__DefineFunction defun

212addInstance : (className, instName : TTName) -> Elab ()

213addInstance : (className, instName : TTName) -> Elab ()

213addInstance className instName = prim__AddInstance className instName

214addInstance className instName = prim__AddInstance className instName

214

215

216+||| Attempt to solve the current goal with a type class dictionary

217+|||

218+||| @ fn the name of the definition being elaborated (to prevent Idris

219+||| from looping)

220+resolveTC : (fn : TTName) -> Elab ()

221+resolveTC fn = prim__ResolveTC fn

222+

215debug : Elab a

223debug : Elab a

216debug = prim__Debug Nothing

224debug = prim__Debug Nothing

217

225

src/Idris/Elab/Term.hs+21−14

@@ -15,6 +15,7 @@ import Idris.Core.Elaborate hiding (Tactic(..))

15import Idris.Core.TT

16import Idris.Core.Evaluate

17import Idris.Core.Unify

18+import Idris.Core.ProofTerm (getProofTerm)

18import Idris.Core.Typecheck (check, recheck, isType)

19import Idris.Core.Typecheck (check, recheck, isType)

19import Idris.Coverage (buildSCG, checkDeclTotality, genClauses, recoverableCoverage, validCoverageCase)

20import Idris.Coverage (buildSCG, checkDeclTotality, genClauses, recoverableCoverage, validCoverageCase)

20import Idris.ErrReverse (errReverse)

21import Idris.ErrReverse (errReverse)

@@ -1156,7 +1157,7 @@ elab ist info emode opts fn tm

1156 focus n

1157 focus n

1157 elab' ina (Just fc') tm

1158 elab' ina (Just fc') tm

1158 env <- get_env

1159 env <- get_env

1159− runTactical (maybe fc' id fc) env (P Bound n' Erased)

1160+ runTactical ist (maybe fc' id fc) env (P Bound n' Erased)

1160 solve

1161 solve

1161 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

1162 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

1162

1163

@@ -1470,12 +1471,12 @@ proofSearch' ist rec ambigok depth prv top n hints

1470

1471

1471-- | Resolve type classes. This will only pick up 'normal' instances, never

1472-- | Resolve type classes. This will only pick up 'normal' instances, never

1472-- named instances (which is enforced by 'findInstances').

1473-- named instances (which is enforced by 'findInstances').

1473−resolveTC :: Bool -- using default Int

1474+resolveTC :: Bool -- ^ using default Int

1474− -> Bool -- allow metavariables in the goal

1475+ -> Bool -- ^ allow metavariables in the goal

1475− -> Int -- depth

1476+ -> Int -- ^ depth

1476− -> Term -- top level goal

1477+ -> Term -- ^ top level goal, for error messages

1477− -> Name -- top level function name

1478+ -> Name -- ^ top level function name, to prevent loops

1478− -> IState -> ElabD ()

1479+ -> IState -> ElabD ()

1479resolveTC def mvok depth top fn ist

1480resolveTC def mvok depth top fn ist

1480 = do hs <- get_holes

1481 = do hs <- get_holes

1481 resTC' [] def hs depth top fn ist

1482 resTC' [] def hs depth top fn ist

@@ -1671,16 +1672,16 @@ case_ ind autoSolve ist fn tm = do

1671 when autoSolve solveAll

1672 when autoSolve solveAll

1672

1673

1674

1674−runTactical :: FC -> Env -> Term -> ElabD ()

1675+runTactical :: IState -> FC -> Env -> Term -> ElabD ()

1675−runTactical fc env tm = do tm' <- eval tm

1676+runTactical ist fc env tm = do tm' <- eval tm

1676− runTacTm tm'

1677+ runTacTm tm'

1677− return ()

1678+ return ()

1678 where

1679 where

1679 eval tm = do ctxt <- get_context

1680 eval tm = do ctxt <- get_context

1680 env <- get_env

1681 env <- get_env

1681 return $ normaliseAll ctxt env (finalise tm)

1682 return $ normaliseAll ctxt env (finalise tm)

1682

1683

1683− returnUnit = fmap fst $ get_type_val (Var unitCon)

1684+ returnUnit = return $ P (DCon 0 0 False) unitCon (P (TCon 0 0) unitTy Erased)

1684

1685

1685 patvars :: [Name] -> Term -> ([Name], Term)

1686 patvars :: [Name] -> Term -> ([Name], Term)

1686 patvars ns (Bind n (PVar t) sc) = patvars (n : ns) (instantiate (P Bound n t) sc)

1687 patvars ns (Bind n (PVar t) sc) = patvars (n : ns) (instantiate (P Bound n t) sc)

@@ -1892,6 +1893,11 @@ runTactical fc env tm = do tm' <- eval tm

1892 updateAux $ \e -> e { new_tyDecls = RAddInstance className instName :

1893 updateAux $ \e -> e { new_tyDecls = RAddInstance className instName :

1893 new_tyDecls e}

1894 new_tyDecls e}

1894 returnUnit

1895 returnUnit

1896+ | n == tacN "prim__ResolveTC", [fn] <- args

1897+ = do g <- goal

1898+ fn <- reifyTTName fn

1899+ resolveTC False True 100 g fn ist

1900+ returnUnit

1895 | n == tacN "prim__RecursiveElab", [goal, script] <- args

1901 | n == tacN "prim__RecursiveElab", [goal, script] <- args

1896 = do goal' <- reifyRaw goal

1902 = do goal' <- reifyRaw goal

1897 ctxt <- get_context

1903 ctxt <- get_context

@@ -1902,9 +1908,10 @@ runTactical fc env tm = do tm' <- eval tm

1902 aux <- getAux

1908 aux <- getAux

1903 datatypes <- get_datatypes

1909 datatypes <- get_datatypes

1904 env <- get_env

1910 env <- get_env

1905− (tm_out, ES (_, aux') _ _) <-

1911+ (_, ES (p, aux') _ _) <-

1906− lift $ runElab aux (runTactical fc env script >> solve >> get_term)

1912+ lift $ runElab aux (runTactical ist fc [] script)

1907 (newProof recH ctxt datatypes goalTT)

1913 (newProof recH ctxt datatypes goalTT)

1914+ let tm_out = getProofTerm (pterm p)

1908 updateAux $ const aux'

1915 updateAux $ const aux'

1909 env' <- get_env

1916 env' <- get_env

1910 (tm, ty, _) <- lift $ recheck ctxt env (forget tm_out) tm_out

1917 (tm, ty, _) <- lift $ recheck ctxt env (forget tm_out) tm_out