git.iko.soy/Idris-dev
on master help sign in
Add new-style tactics for getting source locations
1e488afDavid Raymond Christiansen
libs/prelude/Language/Reflection/Tactical.idr+12
compare with master
unifiedsplit
@@ -22,6 +22,8 @@ data Tactical : Type -> Type where
22 prim__Holes : Tactical (List TTName)
22 prim__Holes : Tactical (List TTName)
23 prim__Guess : Tactical (Maybe TT)
23 prim__Guess : Tactical (Maybe TT)
24
24
25+ prim__SourceLocation : Tactical SourceLocation
26+
25 prim__Forget : TT -> Tactical Raw
27 prim__Forget : TT -> Tactical Raw
26
28
27 prim__Gensym : String -> Tactical TTName
29 prim__Gensym : String -> Tactical TTName
@@ -97,3 +99,13 @@ claim n ty = prim__Claim n ty
97
99
98intro : Maybe TTName -> Tactical ()
100intro : Maybe TTName -> Tactical ()
99intro n = prim__Intro n
101intro n = prim__Intro n
102+
103+||| Find out the present source context for the tactic script
104+getSourceLocation : Tactical SourceLocation
105+getSourceLocation = prim__SourceLocation
106+
107+||| Attempt to solve the current goal with the source code location
108+sourceLocation : Tactical ()
109+sourceLocation = do loc <- getSourceLocation
110+ fill (quote loc)
111+ solve
src/Idris/ElabTerm.hs+23−16
@@ -1540,6 +1540,9 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
1540 else fmap fst . get_type_val $
1540 else fmap fst . get_type_val $
1541 RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
1541 RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
1542 (Var (reflm "TT"))
1542 (Var (reflm "TT"))
1543+ | n == tacN "prim__SourceLocation", [] <- args
1544+ = fmap fst . get_type_val $
1545+ reflectFC fc
1543 | n == tacN "prim__Env", [] <- args
1546 | n == tacN "prim__Env", [] <- args
1544 = do env <- get_env
1547 = do env <- get_env
1545 fmap fst . get_type_val $ reflectEnv env
1548 fmap fst . get_type_val $ reflectEnv env
@@ -1835,22 +1838,7 @@ runTac autoSolve ist perhapsFC fn tac
1835 case perhapsFC of
1838 case perhapsFC of
1836 Nothing -> lift . tfail $ Msg "There is no source location available."
1839 Nothing -> lift . tfail $ Msg "There is no source location available."
1837 Just fc ->
1840 Just fc ->
1838− do let intTy = RConstant (AType (ATInt ITNative))
1841+ do fill $ reflectFC fc
1839− fill $ raw_apply (Var (reflm "FileLoc"))
1840− [ RConstant (Str (fc_fname fc))
1841− , raw_apply (Var pairCon) $
1842− [intTy, intTy] ++
1843− map (RConstant . I)
1844− [ fst (fc_start fc)
1845− , snd (fc_start fc)
1846− ]
1847− , raw_apply (Var pairCon) $
1848− [intTy, intTy] ++
1849− map (RConstant . I)
1850− [ fst (fc_end fc)
1851− , snd (fc_end fc)
1852− ]
1853− ]
1854 solve
1842 solve
1855 runT x = fail $ "Not implemented " ++ show x
1843 runT x = fail $ "Not implemented " ++ show x
1856
1844
@@ -2623,6 +2611,25 @@ reflectErr (LoadingFailed str err) =
2623 raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]
2611 raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]
2624reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]
2612reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]
2625
2613
2614+-- | Reflect a file context
2615+reflectFC :: FC -> Raw
2616+reflectFC fc = raw_apply (Var (reflm "FileLoc"))
2617+ [ RConstant (Str (fc_fname fc))
2618+ , raw_apply (Var pairCon) $
2619+ [intTy, intTy] ++
2620+ map (RConstant . I)
2621+ [ fst (fc_start fc)
2622+ , snd (fc_start fc)
2623+ ]
2624+ , raw_apply (Var pairCon) $
2625+ [intTy, intTy] ++
2626+ map (RConstant . I)
2627+ [ fst (fc_end fc)
2628+ , snd (fc_end fc)
2629+ ]
2630+ ]
2631+ where intTy = RConstant (AType (ATInt ITNative))
2632+
2626elaboratingArgErr :: [(Name, Name)] -> Err -> Err
2633elaboratingArgErr :: [(Name, Name)] -> Err -> Err
2627elaboratingArgErr [] err = err
2634elaboratingArgErr [] err = err
2628elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)
2635elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)