@@ -2007,15 +2007,27 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
20072007 getRetTy (Bind _ (Pi _ _ _) sc) = getRetTy sc
20082008 getRetTy ty = ty
20092009
2010+ elabScriptStuck :: Term -> ElabD a
2011+ elabScriptStuck x = lift . tfail $ ElabScriptStuck x
2012+
2013+
2014+ -- Should be dependent
2015+ tacTmArgs :: Int -> Term -> [Term] -> ElabD [Term]
2016+ tacTmArgs l t args | length args == l = return args
2017+ | otherwise = elabScriptStuck t -- Probably should be an argument size mismatch internal error
2018+
2019+
20102020 -- | Do a step in the reflected elaborator monad. The input is the
20112021 -- step, the output is the (reflected) term returned.
20122022 runTacTm :: Term -> ElabD Term
2013− runTacTm (unApply -> tac@(P _ n _, args))
2014− | n == tacN "Prim__Solve", [] <- args
2015− = do solve
2023+ runTacTm tac@(unApply -> (P _ n _, args))
2024+ | n == tacN "Prim__Solve"
2025+ = do ~[] <- tacTmArgs 0 tac args -- patterns are irrefutable because `tacTmArgs` returns lists of exactly the size given to it as first argument
2026+ solve
20162027 returnUnit
2017− | n == tacN "Prim__Goal", [] <- args
2018− = do hs <- get_holes
2028+ | n == tacN "Prim__Goal"
2029+ = do ~[] <- tacTmArgs 0 tac args
2030+ hs <- get_holes
20192031 case hs of
20202032 (h : _) -> do t <- goal
20212033 fmap fst . checkClosed $
@@ -2024,15 +2036,18 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
20242036 [] -> lift . tfail . Msg $
20252037 "Elaboration is complete. There are no goals."
20262038
2027− | n == tacN "Prim__Holes", [] <- args
2028− = do hs <- get_holes
2039+ | n == tacN "Prim__Holes"
2040+ = do ~[] <- tacTmArgs 0 tac args
2041+ hs <- get_holes
20292042 fmap fst . checkClosed $
20302043 mkList (Var $ reflm "TTName") (map reflectName hs)
2031− | n == tacN "Prim__Guess", [] <- args
2032− = do g <- get_guess
2044+ | n == tacN "Prim__Guess"
2045+ = do ~[] <- tacTmArgs 0 tac args
2046+ g <- get_guess
20332047 fmap fst . checkClosed $ reflect g
2034− | n == tacN "Prim__LookupTy", [n] <- args
2035− = do n' <- reifyTTName n
2048+ | n == tacN "Prim__LookupTy"
2049+ = do ~[name] <- tacTmArgs 1 tac args
2050+ n' <- reifyTTName name
20362051 ctxt <- get_context
20372052 let getNameTypeAndType = \case Function ty _ -> (Ref, ty)
20382053 TyDecl nt ty -> (nt, ty)
@@ -2053,20 +2068,23 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
20532068 , raw_apply (Var pairTy) [ Var (reflm "NameType")
20542069 , Var (reflm "TT")]])
20552070 defs
2056− | n == tacN "Prim__LookupDatatype", [name] <- args
2057− = do n' <- reifyTTName name
2071+ | n == tacN "Prim__LookupDatatype"
2072+ = do ~[name] <- tacTmArgs 1 tac args
2073+ n' <- reifyTTName name
20582074 datatypes <- get_datatypes
20592075 ctxt <- get_context
20602076 fmap fst . checkClosed $
20612077 rawList (Var (tacN "Datatype"))
20622078 (map reflectDatatype (buildDatatypes ist n'))
2063− | n == tacN "Prim__LookupFunDefn", [name] <- args
2064− = do n' <- reifyTTName name
2079+ | n == tacN "Prim__LookupFunDefn"
2080+ = do ~[name] <- tacTmArgs 1 tac args
2081+ n' <- reifyTTName name
20652082 fmap fst . checkClosed $
20662083 rawList (RApp (Var $ tacN "FunDefn") (Var $ reflm "TT"))
20672084 (map reflectFunDefn (buildFunDefns ist n'))
2068− | n == tacN "Prim__LookupArgs", [name] <- args
2069− = do n' <- reifyTTName name
2085+ | n == tacN "Prim__LookupArgs"
2086+ = do ~[name] <- tacTmArgs 1 tac args
2087+ n' <- reifyTTName name
20702088 let listTy = Var (sNS (sUN "List") ["List", "Prelude"])
20712089 listFunArg = RApp listTy (Var (tacN "FunArg"))
20722090 -- Idris tuples nest to the right
@@ -2089,37 +2107,45 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
20892107 (Var (tacN "FunArg"))
20902108 , Var (reflm "Raw")]])
20912109 out
2092− | n == tacN "Prim__SourceLocation", [] <- args
2093− = fmap fst . checkClosed $
2094− reflectFC fc
2095− | n == tacN "Prim__Namespace", [] <- args
2096− = fmap fst . checkClosed $
2097− rawList (RConstant StrType) (map (RConstant . Str) ns)
2098− | n == tacN "Prim__Env", [] <- args
2099− = do env <- get_env
2110+ | n == tacN "Prim__SourceLocation"
2111+ = do ~[] <- tacTmArgs 0 tac args
2112+ fmap fst . checkClosed $
2113+ reflectFC fc
2114+ | n == tacN "Prim__Namespace"
2115+ = do ~[] <- tacTmArgs 0 tac args
2116+ fmap fst . checkClosed $
2117+ rawList (RConstant StrType) (map (RConstant . Str) ns)
2118+ | n == tacN "Prim__Env"
2119+ = do ~[] <- tacTmArgs 0 tac args
2120+ env <- get_env
21002121 fmap fst . checkClosed $ reflectEnv env
2101− | n == tacN "Prim__Fail", [_a, errs] <- args
2102− = do errs' <- eval errs
2122+ | n == tacN "Prim__Fail"
2123+ = do ~[_a, errs] <- tacTmArgs 2 tac args
2124+ errs' <- eval errs
21032125 parts <- reifyReportParts errs'
21042126 lift . tfail $ ReflectionError [parts] (Msg "")
2105− | n == tacN "Prim__PureElab", [_a, tm] <- args
2106− = return tm
2107− | n == tacN "Prim__BindElab", [_a, _b, first, andThen] <- args
2108− = do first' <- eval first
2127+ | n == tacN "Prim__PureElab"
2128+ = do ~[_a, tm] <- tacTmArgs 2 tac args
2129+ return tm
2130+ | n == tacN "Prim__BindElab"
2131+ = do ~[_a, _b, first, andThen] <- tacTmArgs 4 tac args
2132+ first' <- eval first
21092133 res <- eval =<< runTacTm first'
21102134 next <- eval (App Complete andThen res)
21112135 runTacTm next
2112− | n == tacN "Prim__Try", [_a, first, alt] <- args
2113− = do first' <- eval first
2136+ | n == tacN "Prim__Try"
2137+ = do ~[_a, first, alt] <- tacTmArgs 3 tac args
2138+ first' <- eval first
21142139 alt' <- eval alt
21152140 try' (runTacTm first') (runTacTm alt') True
2116− | n == tacN "Prim__Fill", [raw] <- args
2117− = do raw' <- reifyRaw =<< eval raw
2141+ | n == tacN "Prim__Fill"
2142+ = do ~[raw] <- tacTmArgs 1 tac args
2143+ raw' <- reifyRaw =<< eval raw
21182144 apply raw' []
21192145 returnUnit
21202146 | n == tacN "Prim__Apply" || n == tacN "Prim__MatchApply"
2121− , [raw, argSpec] <- args
2122− = do raw' <- reifyRaw =<< eval raw
2147+ = do ~[raw, argSpec] <- tacTmArgs 2 tac args
2148+ raw' <- reifyRaw =<< eval raw
21232149 argSpec' <- map (\b -> (b, 0)) <$> reifyList reifyBool argSpec
21242150 let op = if n == tacN "Prim__Apply"
21252151 then apply
@@ -2131,89 +2157,105 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
21312157 (reflectName n1, reflectName n2)
21322158 | (n1, n2) <- ns
21332159 ]
2134− | n == tacN "Prim__Gensym", [hint] <- args
2135− = do hintStr <- eval hint
2160+ | n == tacN "Prim__Gensym"
2161+ = do ~[hint] <- tacTmArgs 1 tac args
2162+ hintStr <- eval hint
21362163 case hintStr of
21372164 Constant (Str h) -> do
21382165 n <- getNameFrom (sMN 0 h)
21392166 fmap fst $ get_type_val (reflectName n)
21402167 _ -> fail "no hint"
2141− | n == tacN "Prim__Claim", [n, ty] <- args
2142− = do n' <- reifyTTName n
2168+ | n == tacN "Prim__Claim"
2169+ = do ~[n, ty] <- tacTmArgs 2 tac args
2170+ n' <- reifyTTName n
21432171 ty' <- reifyRaw ty
21442172 claim n' ty'
21452173 returnUnit
2146− | n == tacN "Prim__Check", [env', raw] <- args
2147− = do env <- reifyEnv env'
2174+ | n == tacN "Prim__Check"
2175+ = do ~[env', raw] <- tacTmArgs 2 tac args
2176+ env <- reifyEnv env'
21482177 raw' <- reifyRaw =<< eval raw
21492178 ctxt <- get_context
21502179 (tm, ty) <- lift $ check ctxt env raw'
21512180 fmap fst . checkClosed $
21522181 rawPair (Var (reflm "TT"), Var (reflm "TT"))
21532182 (reflect tm, reflect ty)
2154− | n == tacN "Prim__Attack", [] <- args
2155− = do attack
2183+ | n == tacN "Prim__Attack"
2184+ = do ~[] <- tacTmArgs 0 tac args
2185+ attack
21562186 returnUnit
2157− | n == tacN "Prim__Rewrite", [rule] <- args
2158− = do r <- reifyRaw rule
2187+ | n == tacN "Prim__Rewrite"
2188+ = do ~[rule] <- tacTmArgs 1 tac args
2189+ r <- reifyRaw rule
21592190 rewrite r
21602191 returnUnit
2161− | n == tacN "Prim__Focus", [what] <- args
2162− = do n' <- reifyTTName what
2192+ | n == tacN "Prim__Focus"
2193+ = do ~[what] <- tacTmArgs 1 tac args
2194+ n' <- reifyTTName what
21632195 hs <- get_holes
21642196 if elem n' hs
21652197 then focus n' >> returnUnit
21662198 else lift . tfail . Msg $ "The name " ++ show n' ++ " does not denote a hole"
2167− | n == tacN "Prim__Unfocus", [what] <- args
2168− = do n' <- reifyTTName what
2199+ | n == tacN "Prim__Unfocus"
2200+ = do ~[what] <- tacTmArgs 1 tac args
2201+ n' <- reifyTTName what
21692202 movelast n'
21702203 returnUnit
2171− | n == tacN "Prim__Intro", [mn] <- args
2172− = do n <- case fromTTMaybe mn of
2204+ | n == tacN "Prim__Intro"
2205+ = do ~[mn] <- tacTmArgs 1 tac args
2206+ n <- case fromTTMaybe mn of
21732207 Nothing -> return Nothing
21742208 Just name -> fmap Just $ reifyTTName name
21752209 intro n
21762210 returnUnit
2177− | n == tacN "Prim__Forall", [n, ty] <- args
2178− = do n' <- reifyTTName n
2211+ | n == tacN "Prim__Forall"
2212+ = do ~[n, ty] <- tacTmArgs 2 tac args
2213+ n' <- reifyTTName n
21792214 ty' <- reifyRaw ty
21802215 forall n' Nothing ty'
21812216 returnUnit
2182− | n == tacN "Prim__PatVar", [n] <- args
2183− = do n' <- reifyTTName n
2217+ | n == tacN "Prim__PatVar"
2218+ = do ~[n] <- tacTmArgs 1 tac args
2219+ n' <- reifyTTName n
21842220 patvar' n'
21852221 returnUnit
2186− | n == tacN "Prim__PatBind", [n] <- args
2187− = do n' <- reifyTTName n
2222+ | n == tacN "Prim__PatBind"
2223+ = do ~[n] <- tacTmArgs 1 tac args
2224+ n' <- reifyTTName n
21882225 patbind n'
21892226 returnUnit
2190− | n == tacN "Prim__LetBind", [n, ty, tm] <- args
2191− = do n' <- reifyTTName n
2227+ | n == tacN "Prim__LetBind"
2228+ = do ~[n, ty, tm] <- tacTmArgs 3 tac args
2229+ n' <- reifyTTName n
21922230 ty' <- reifyRaw ty
21932231 tm' <- reifyRaw tm
21942232 letbind n' ty' tm'
21952233 returnUnit
2196− | n == tacN "Prim__Compute", [] <- args
2197− = do compute ; returnUnit
2198− | n == tacN "Prim__Normalise", [env, tm] <- args
2199− = do env' <- reifyEnv env
2234+ | n == tacN "Prim__Compute"
2235+ = do ~[] <- tacTmArgs 0 tac args; compute ; returnUnit
2236+ | n == tacN "Prim__Normalise"
2237+ = do ~[env, tm] <- tacTmArgs 2 tac args
2238+ env' <- reifyEnv env
22002239 tm' <- reifyTT tm
22012240 ctxt <- get_context
22022241 let out = normaliseAll ctxt env' (finalise tm')
22032242 fmap fst . checkClosed $ reflect out
2204− | n == tacN "Prim__Whnf", [tm] <- args
2205− = do tm' <- reifyTT tm
2243+ | n == tacN "Prim__Whnf"
2244+ = do ~[tm] <- tacTmArgs 1 tac args
2245+ tm' <- reifyTT tm
22062246 ctxt <- get_context
22072247 fmap fst . checkClosed . reflect $ whnf ctxt tm'
2208− | n == tacN "Prim__Converts", [env, tm1, tm2] <- args
2209− = do env' <- reifyEnv env
2248+ | n == tacN "Prim__Converts"
2249+ = do ~[env, tm1, tm2] <- tacTmArgs 3 tac args
2250+ env' <- reifyEnv env
22102251 tm1' <- reifyTT tm1
22112252 tm2' <- reifyTT tm2
22122253 ctxt <- get_context
22132254 lift $ converts ctxt env' tm1' tm2'
22142255 returnUnit
2215− | n == tacN "Prim__DeclareType", [decl] <- args
2216− = do (RDeclare n args res) <- reifyTyDecl decl
2256+ | n == tacN "Prim__DeclareType"
2257+ = do ~[decl] <- tacTmArgs 1 tac args
2258+ (RDeclare n args res) <- reifyTyDecl decl
22172259 ctxt <- get_context
22182260 let rty = foldr mkPi res args
22192261 (checked, ty') <- lift $ check ctxt [] rty
@@ -2225,12 +2267,14 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
22252267 updateAux $ \e -> e { new_tyDecls = (RTyDeclInstrs n fc (map rFunArgToPArg args) checked) :
22262268 new_tyDecls e }
22272269 returnUnit
2228− | n == tacN "Prim__DefineFunction", [decl] <- args
2229− = do defn <- reifyFunDefn decl
2270+ | n == tacN "Prim__DefineFunction"
2271+ = do ~[decl] <- tacTmArgs 1 tac args
2272+ defn <- reifyFunDefn decl
22302273 defineFunction defn
22312274 returnUnit
2232− | n == tacN "Prim__DeclareDatatype", [decl] <- args
2233− = do RDeclare n args resTy <- reifyTyDecl decl
2275+ | n == tacN "Prim__DeclareDatatype"
2276+ = do ~[decl] <- tacTmArgs 1 tac args
2277+ RDeclare n args resTy <- reifyTyDecl decl
22342278 ctxt <- get_context
22352279 let tcTy = foldr mkPi resTy args
22362280 (checked, ty') <- lift $ check ctxt [] tcTy
@@ -2240,8 +2284,9 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
22402284 set_context ctxt'
22412285 updateAux $ \e -> e { new_tyDecls = RDatatypeDeclInstrs n (map rFunArgToPArg args) : new_tyDecls e }
22422286 returnUnit
2243− | n == tacN "Prim__DefineDatatype", [defn] <- args
2244− = do RDefineDatatype n ctors <- reifyRDataDefn defn
2287+ | n == tacN "Prim__DefineDatatype"
2288+ = do ~[defn] <- tacTmArgs 1 tac args
2289+ RDefineDatatype n ctors <- reifyRDataDefn defn
22452290 ctxt <- get_context
22462291 tyconTy <- case lookupTyExact n ctxt of
22472292 Just t -> return t
@@ -2264,24 +2309,28 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
22642309 -- the rest happens in a bit
22652310 updateAux $ \e -> e { new_tyDecls = RDatatypeDefnInstrs n tyconTy ctors' : new_tyDecls e }
22662311 returnUnit
2267− | n == tacN "Prim__AddInstance", [cls, inst] <- args
2268− = do className <- reifyTTName cls
2312+ | n == tacN "Prim__AddInstance"
2313+ = do ~[cls, inst] <- tacTmArgs 2 tac args
2314+ className <- reifyTTName cls
22692315 instName <- reifyTTName inst
22702316 updateAux $ \e -> e { new_tyDecls = RAddInstance className instName :
22712317 new_tyDecls e }
22722318 returnUnit
2273− | n == tacN "Prim__IsTCName", [n] <- args
2274− = do n' <- reifyTTName n
2319+ | n == tacN "Prim__IsTCName"
2320+ = do ~[n] <- tacTmArgs 1 tac args
2321+ n' <- reifyTTName n
22752322 case lookupCtxtExact n' (idris_classes ist) of
22762323 Just _ -> fmap fst . checkClosed $ Var (sNS (sUN "True") ["Bool", "Prelude"])
22772324 Nothing -> fmap fst . checkClosed $ Var (sNS (sUN "False") ["Bool", "Prelude"])
2278− | n == tacN "Prim__ResolveTC", [fn] <- args
2279− = do g <- goal
2325+ | n == tacN "Prim__ResolveTC"
2326+ = do ~[fn] <- tacTmArgs 1 tac args
2327+ g <- goal
22802328 fn <- reifyTTName fn
22812329 resolveTC' False True 100 g fn ist
22822330 returnUnit
2283− | n == tacN "Prim__Search", [depth, hints] <- args
2284− = do d <- eval depth
2331+ | n == tacN "Prim__Search"
2332+ = do ~[depth, hints] <- tacTmArgs 2 tac args
2333+ d <- eval depth
22852334 hints' <- eval hints
22862335 case (d, unList hints') of
22872336 (Constant (I i), Just hs) ->
@@ -2293,8 +2342,9 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
22932342 (Constant (I _), Nothing ) ->
22942343 lift . tfail . InternalMsg $ "Not a list: " ++ show hints'
22952344 (_, _) -> lift . tfail . InternalMsg $ "Can't reify int " ++ show d
2296− | n == tacN "Prim__RecursiveElab", [goal, script] <- args
2297− = do goal' <- reifyRaw goal
2345+ | n == tacN "Prim__RecursiveElab"
2346+ = do ~[goal, script] <- tacTmArgs 2 tac args
2347+ goal' <- reifyRaw goal
22982348 ctxt <- get_context
22992349 script <- eval script
23002350 (goalTT, goalTy) <- lift $ check ctxt [] goal'
@@ -2327,8 +2377,9 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
23272377 fmap fst . checkClosed $
23282378 rawPair (Var $ reflm "TT", Var $ reflm "TT")
23292379 (tm', ty')
2330− | n == tacN "Prim__Metavar", [n] <- args
2331− = do n' <- reifyTTName n
2380+ | n == tacN "Prim__Metavar"
2381+ = do ~[n] <- tacTmArgs 1 tac args
2382+ n' <- reifyTTName n
23322383 ctxt <- get_context
23332384 ptm <- get_term
23342385 -- See documentation above in the elab case for PMetavar
@@ -2338,8 +2389,9 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
23382389 defer unique_used mvn
23392390 solve
23402391 returnUnit
2341− | n == tacN "Prim__Fixity", [op'] <- args
2342− = do opTm <- eval op'
2392+ | n == tacN "Prim__Fixity"
2393+ = do ~[op'] <- tacTmArgs 1 tac args
2394+ opTm <- eval op'
23432395 case opTm of
23442396 Constant (Str op) ->
23452397 let opChars = ":!#$%&*+./<=>?@\\^|-~"
@@ -2352,11 +2404,12 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm
23522404 [f] -> fmap fst . checkClosed $ reflectFixity f
23532405 many -> lift . tfail . InternalMsg $ "Ambiguous fixity for '" ++ op ++ "'! Found " ++ show many
23542406 _ -> lift . tfail . Msg $ "Not a constant string for an operator name: " ++ show opTm
2355− | n == tacN "Prim__Debug", [ty, msg] <- args
2356− = do msg' <- eval msg
2407+ | n == tacN "Prim__Debug"
2408+ = do ~[ty, msg] <- tacTmArgs 2 tac args
2409+ msg' <- eval msg
23572410 parts <- reifyReportParts msg
23582411 debugElaborator parts
2359− runTacTm x = lift . tfail $ ElabScriptStuck x
2412+ runTacTm x = elabScriptStuck x
23602413
23612414-- Running tactics directly
23622415-- if a tactic adds unification problems, return an error