%macro
getTTImp : v -> Elab TTImp
getTTImp v = quote v
u1 = getFC $ getTTImp ('a' == 'b') -- this has physicalIdrSrc
u2 = getFC $ getTTImp (True == False) -- this has emptyFc
Motivation for this issue: Trying to implement some testing utilities
getFilePosition : TTImp -> String
getFilePosition x = case getFC x of
MkFC (PhysicalIdrSrc (MkMI path)) (line, column) _ =>
"\{foldl (\a, i => a ++ "/" ++ i) "src" $ reverse path}.idr:\{show $ line + 1}:\{show column}"
MkFC _ _ _ => "MkFC"
MkVirtualFC _ _ _ => "MkVirtualFC"
EmptyFC => "EmptyFc"
-- _ => ""
public export
%macro
assert : (() -> Bool) -> Elab (IO ())
assert condition = do
condition_quoted <- quote condition
let position = getFilePosition condition_quoted
let position_quoted = IPrimVal EmptyFC (Str position)
check `(if ~(condition_quoted) then putStrLn "SUCCESS \{~(position_quoted)}" else putStrLn "FAILURE \{~(position_quoted)}")
Steps to Reproduce
Motivation for this issue: Trying to implement some testing utilities