a244cd5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

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

Further elaborator reflection improvements

commita244cd59b3e14e476903943493ae6e07d2aabf2a authorDavid Christiansen <david@davidchristiansen.dk> dateThu 30 Apr 2015, 10:10 (11 years ago) parent1044dbb 0453200

4 files changed+71−9

compare with master

unifiedsplit

libs/prelude/Language/Reflection/Elab.idr+27−1 src/Idris/AbsSyntax.hs+1 src/Idris/Core/Evaluate.hs+2−2 src/Idris/Elab/Term.hs+41−6

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

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

6565

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

6767 prim__Intro : Maybe TTName -> Elab ()

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

69+ prim__PatVar : TTName -> Elab ()

70+ prim__PatBind : TTName -> Elab ()

6871

6972 prim__DeclareType : TyDecl -> Elab ()

7073 prim__DefineFunction : FunDefn -> Elab ()

7174

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

76+

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

7378

7479

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

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

151156claim n ty = prim__Claim n ty

152157

153−intro : Maybe TTName -> Elab ()

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)

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

154165intro n = prim__Intro n

155166

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+

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

157180getSourceLocation : Elab SourceLocation

158181getSourceLocation = prim__SourceLocation

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

175198debug : Elab a

176199debug = prim__Debug Nothing

177200

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

202+runElab goal script = prim__RecursiveElab goal script

203+

178204debugMessage : String -> Elab a

179205debugMessage msg = prim__Debug (Just msg)

src/Idris/AbsSyntax.hs+1

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

20232023 sm xs (PHidden x) = PHidden (sm xs x)

20242024 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)

20252025 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)

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

20262027 sm xs x = x

20272028

20282029 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

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

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

7676normaliseC ctxt env t

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

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

7878 quote 0 val) initEval

7979

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

8181normaliseAll 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]

8383 quote 0 val) initEval

8484

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

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

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

1515import Idris.Core.TT

1616import Idris.Core.Evaluate

1717import Idris.Core.Unify

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

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

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

2020import Idris.ErrReverse (errReverse)

2121import Idris.ElabQuasiquote (extractUnquotes)

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

11001100 do attack

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

11021102 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)

11041106 claim n scriptTy

11051107 movelast n

11061108 letbind n' scriptTy (Var n)

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

11081110 elab' ina (Just fc') tm

11091111 env <- get_env

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

1111− EState _ _ todo <- getAux

11121113 solve

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

11141115

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

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

11161117

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

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

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

16231624 return ()

16241625 where

16251626 eval tm = do ctxt <- get_context

1627+ env <- get_env

16261628 return $ normaliseAll ctxt env (finalise tm)

16271629

16281630 returnUnit = fmap fst $ get_type_val (Var unitCon)

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

17371739 = return tm

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

17391741 = do first' <- eval first

1740− res <- runTacTm first'

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

17411743 next <- eval (App Complete andThen res)

17421744 runTacTm next

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

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

17451747 alt' <- eval alt

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

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

1748− = do raw' <- reifyRaw raw

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

17491751 apply raw' []

17501752 returnUnit

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

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

17841786 Just name -> fmap Just $ reifyTTName name

17851787 intro n

17861788 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

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

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

17891804 ctxt <- get_context

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

18121827 = do defn <- reifyFunDefn decl

18131828 defineFunction defn

18141829 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')

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

18161851 = do let msg' = fromTTMaybe msg

18171852 case msg' of