a244cd5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #2212 from david-christiansen/wip/tactical

a244cd5David Christiansen11 years ago

libs/prelude/Language/Reflection/Elab.idr+27−1

compare with master

unifiedsplit

@@ -65,10 +65,15 @@ data Elab : Type -> Type where

66 prim__Claim : TTName -> Raw -> Elab ()

67 prim__Intro : Maybe TTName -> Elab ()

68+ prim__Forall : TTName -> Raw -> Elab ()

69+ prim__PatVar : TTName -> Elab ()

70+ prim__PatBind : TTName -> Elab ()

69 prim__DeclareType : TyDecl -> Elab ()

72 prim__DeclareType : TyDecl -> Elab ()

70 prim__DefineFunction : FunDefn -> Elab ()

73 prim__DefineFunction : FunDefn -> Elab ()

75+ prim__RecursiveElab : Raw -> Elab () -> Elab (TT, TT)

76+

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

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

@@ -150,9 +155,27 @@ attack = prim__Attack

150claim : TTName -> Raw -> Elab ()

155claim : TTName -> Raw -> Elab ()

151claim n ty = prim__Claim n ty

156claim n ty = prim__Claim n ty

152

157

158+||| Introduce a lambda binding around the current hole and focus on

159+||| the body. Requires that the hole be in binding form (use

160+||| `attack`).

161+|||

162+||| @ n the name to use for the argument, or `Nothing` to use the name

163+||| in the corresponding hole type (a dependent function)

153−intro : Maybe TTName -> Elab ()

164+intro : (n : Maybe TTName) -> Elab ()

154intro n = prim__Intro n

165intro n = prim__Intro n

155

166

167+||| Introduce a dependent function type binding into the current hole,

168+||| and focus on the body.

169+forall : TTName -> Raw -> Elab ()

170+forall n ty = prim__Forall n ty

171+

172+patvar : TTName -> Elab ()

173+patvar n = prim__PatVar n

174+

175+patbind : TTName -> Elab ()

176+patbind n = prim__PatBind n

177+

178+

156||| Find out the present source context for the tactic script

179||| Find out the present source context for the tactic script

157getSourceLocation : Elab SourceLocation

180getSourceLocation : Elab SourceLocation

158getSourceLocation = prim__SourceLocation

181getSourceLocation = prim__SourceLocation

@@ -175,5 +198,8 @@ defineFunction defun = prim__DefineFunction defun

175debug : Elab a

198debug : Elab a

176debug = prim__Debug Nothing

199debug = prim__Debug Nothing

177

200

201+runElab : Raw -> Elab () -> Elab (TT, TT)

202+runElab goal script = prim__RecursiveElab goal script

203+

178debugMessage : String -> Elab a

204debugMessage : String -> Elab a

179debugMessage msg = prim__Debug (Just msg)

205debugMessage msg = prim__Debug (Just msg)

src/Idris/AbsSyntax.hs+1

@@ -2023,6 +2023,7 @@ substMatchShadow n shs tm t = sm shs t where

2023 sm xs (PHidden x) = PHidden (sm xs x)

2024 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)

2025 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)

2026+ sm xs (PRunElab fc script) = PRunElab fc (sm xs script)

2026 sm xs x = x

2027 sm xs x = x

2027

2028

2028 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))

2029 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))

src/Idris/Core/Evaluate.hs+2−2

@@ -74,12 +74,12 @@ instance Show (a -> b) where

74-- | Normalise fully type checked terms (so, assume all names/let bindings resolved)

75normaliseC :: Context -> Env -> TT Name -> TT Name

76normaliseC ctxt env t

77− = evalState (do val <- eval False ctxt [] env t []

77+ = evalState (do val <- eval False ctxt [] (map finalEntry env) t []

78 quote 0 val) initEval

80normaliseAll :: Context -> Env -> TT Name -> TT Name

81normaliseAll ctxt env t

82− = evalState (do val <- eval False ctxt [] env t [AtREPL]

82+ = evalState (do val <- eval False ctxt [] (map finalEntry env) t [AtREPL]

83 quote 0 val) initEval

85normalise :: Context -> Env -> TT Name -> TT Name

src/Idris/Elab/Term.hs+41−6

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

15import Idris.Core.TT

16import Idris.Core.Evaluate

17import Idris.Core.Unify

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

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

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

20import Idris.ErrReverse (errReverse)

21import Idris.ElabQuasiquote (extractUnquotes)

@@ -1100,7 +1100,9 @@ elab ist info emode opts fn tm

1100 do attack

1101 n <- getNameFrom (sMN 0 "tacticScript")

1102 n' <- getNameFrom (sMN 0 "tacticExpr")

1103− let scriptTy = RApp (Var (sNS (sUN "Elab") ["Elab", "Reflection", "Language"])) (Var unitTy)

1103+ let scriptTy = RApp (Var (sNS (sUN "Elab")

1104+ ["Elab", "Reflection", "Language"]))

1105+ (Var unitTy)

1104 claim n scriptTy

1106 claim n scriptTy

1105 movelast n

1107 movelast n

1106 letbind n' scriptTy (Var n)

1108 letbind n' scriptTy (Var n)

@@ -1108,11 +1110,10 @@ elab ist info emode opts fn tm

1108 elab' ina (Just fc') tm

1110 elab' ina (Just fc') tm

1109 env <- get_env

1111 env <- get_env

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

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

1111− EState _ _ todo <- getAux

1112 solve

1113 solve

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

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

1114

1115

1115− delayElab t = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [t] })

1116+ delayElab t = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [t] })

1116

1117

1117 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))

1118 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))

1118 isScr (PRef _ n) (n', b) = (n', (n == n', b))

1119 isScr (PRef _ n) (n', b) = (n', (n == n', b))

@@ -1623,6 +1624,7 @@ runTactical fc env tm = do tm' <- eval tm

1623 return ()

1624 return ()

1624 where

1625 where

1625 eval tm = do ctxt <- get_context

1626 eval tm = do ctxt <- get_context

1627+ env <- get_env

1626 return $ normaliseAll ctxt env (finalise tm)

1628 return $ normaliseAll ctxt env (finalise tm)

1627

1629

1628 returnUnit = fmap fst $ get_type_val (Var unitCon)

1630 returnUnit = fmap fst $ get_type_val (Var unitCon)

@@ -1737,7 +1739,7 @@ runTactical fc env tm = do tm' <- eval tm

1737 = return tm

1739 = return tm

1738 | n == tacN "prim__BindElab", [_a, _b, first, andThen] <- args

1740 | n == tacN "prim__BindElab", [_a, _b, first, andThen] <- args

1739 = do first' <- eval first

1741 = do first' <- eval first

1740− res <- runTacTm first'

1742+ res <- eval =<< runTacTm first'

1741 next <- eval (App Complete andThen res)

1743 next <- eval (App Complete andThen res)

1742 runTacTm next

1744 runTacTm next

1743 | n == tacN "prim__Try", [_a, first, alt] <- args

1745 | n == tacN "prim__Try", [_a, first, alt] <- args

@@ -1745,7 +1747,7 @@ runTactical fc env tm = do tm' <- eval tm

1745 alt' <- eval alt

1747 alt' <- eval alt

1746 try' (runTacTm first') (runTacTm alt') True

1748 try' (runTacTm first') (runTacTm alt') True

1747 | n == tacN "prim__Fill", [raw] <- args

1749 | n == tacN "prim__Fill", [raw] <- args

1748− = do raw' <- reifyRaw raw

1750+ = do raw' <- reifyRaw =<< eval raw

1749 apply raw' []

1751 apply raw' []

1750 returnUnit

1752 returnUnit

1751 | n == tacN "prim__Gensym", [hint] <- args

1753 | n == tacN "prim__Gensym", [hint] <- args

@@ -1784,6 +1786,19 @@ runTactical fc env tm = do tm' <- eval tm

1784 Just name -> fmap Just $ reifyTTName name

1786 Just name -> fmap Just $ reifyTTName name

1785 intro n

1787 intro n

1786 returnUnit

1788 returnUnit

1789+ | n == tacN "prim__Forall", [n, ty] <- args

1790+ = do n' <- reifyTTName n

1791+ ty' <- reifyRaw ty

1792+ forall n' Nothing ty'

1793+ returnUnit

1794+ | n == tacN "prim__PatVar", [n] <- args

1795+ = do n' <- reifyTTName n

1796+ patvar n'

1797+ returnUnit

1798+ | n == tacN "prim__PatBind", [n] <- args

1799+ = do n' <- reifyTTName n

1800+ patbind n'

1801+ returnUnit

1787 | n == tacN "prim__DeclareType", [decl] <- args

1802 | n == tacN "prim__DeclareType", [decl] <- args

1788 = do (RDeclare n args res) <- reifyTyDecl decl

1803 = do (RDeclare n args res) <- reifyTyDecl decl

1789 ctxt <- get_context

1804 ctxt <- get_context

@@ -1812,6 +1827,26 @@ runTactical fc env tm = do tm' <- eval tm

1812 = do defn <- reifyFunDefn decl

1827 = do defn <- reifyFunDefn decl

1813 defineFunction defn

1828 defineFunction defn

1814 returnUnit

1829 returnUnit

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

1831+ = do goal' <- reifyRaw goal

1832+ ctxt <- get_context

1833+ script <- eval script

1834+ (goalTT, goalTy) <- lift $ check ctxt [] goal'

1835+ lift $ isType ctxt [] goalTy

1836+ recH <- getNameFrom (sMN 0 "recElabHole")

1837+ aux <- getAux

1838+ datatypes <- get_datatypes

1839+ env <- get_env

1840+ (tm_out, ES (_, aux') _ _) <-

1841+ lift $ runElab aux (runTactical fc env script >> solve >> get_term)

1842+ (newProof recH ctxt datatypes goalTT)

1843+ updateAux $ const aux'

1844+ env' <- get_env

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

1846+ let (tm', ty') = (reflect tm, reflect ty)

1847+ fmap fst . get_type_val $

1848+ rawPair (Var $ reflm "TT", Var $ reflm "TT")

1849+ (tm', ty')

1815 | n == tacN "prim__Debug", [ty, msg] <- args

1850 | n == tacN "prim__Debug", [ty, msg] <- args

1816 = do let msg' = fromTTMaybe msg

1851 = do let msg' = fromTTMaybe msg

1817 case msg' of

1852 case msg' of