git.iko.soy/Idris-dev
on master help sign in
Add new-style tactics for getting source locations
commit1e488afc95a69088c353ba316c331d57c95de518 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 2 Mar 2015, 15:14 (12 years ago) parent3d79f1b
2 files changed+35−16
compare with master
unifiedsplit
libs/prelude/Language/Reflection/Tactical.idr+12 src/Idris/ElabTerm.hs+23−16
libs/prelude/Language/Reflection/Tactical.idr+12
@@ -22,6 +22,8 @@ data Tactical : Type -> Type where
2222 prim__Holes : Tactical (List TTName)
2323 prim__Guess : Tactical (Maybe TT)
2424
25+ prim__SourceLocation : Tactical SourceLocation
26+
2527 prim__Forget : TT -> Tactical Raw
2628
2729 prim__Gensym : String -> Tactical TTName
@@ -97,3 +99,13 @@ claim n ty = prim__Claim n ty
9799
98100intro : Maybe TTName -> Tactical ()
99101intro 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 ()
15401540 else fmap fst . get_type_val $
15411541 RApp (Var (sNS (sUN "Nothing") ["Maybe", "Prelude"]))
15421542 (Var (reflm "TT"))
1543+ | n == tacN "prim__SourceLocation", [] <- args
1544+ = fmap fst . get_type_val $
1545+ reflectFC fc
15431546 | n == tacN "prim__Env", [] <- args
15441547 = do env <- get_env
15451548 fmap fst . get_type_val $ reflectEnv env
@@ -1835,22 +1838,7 @@ runTac autoSolve ist perhapsFC fn tac
18351838 case perhapsFC of
18361839 Nothing -> lift . tfail $ Msg "There is no source location available."
18371840 Just fc ->
1838− do let intTy = RConstant (AType (ATInt ITNative))
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− ]
1841+ do fill $ reflectFC fc
18541842 solve
18551843 runT x = fail $ "Not implemented " ++ show x
18561844
@@ -2623,6 +2611,25 @@ reflectErr (LoadingFailed str err) =
26232611 raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]
26242612reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]
26252613
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+
26262633elaboratingArgErr :: [(Name, Name)] -> Err -> Err
26272634elaboratingArgErr [] err = err
26282635elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)