%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

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)}")