Skip to content

Commit

Permalink
remove reflect
Browse files Browse the repository at this point in the history
  • Loading branch information
andrevidela committed Oct 30, 2024
1 parent 832f960 commit 0ac471b
Showing 1 changed file with 0 additions and 18 deletions.
18 changes: 0 additions & 18 deletions src/Core/Reflect.idr
Original file line number Diff line number Diff line change
Expand Up @@ -848,18 +848,6 @@ Reify FC where
_ => cantReify val "FC"
reify defs val = cantReify val "FC"

export
Reify a => Reify (WithFC a) where
reify defs con@(NDCon _ n _ _ args)
= case (dropAllNS !(full (gamma defs) n), args) of
(UN (Basic "MkFCVal"), [(_, fc), (_, val)])
=> do reifiedFC <- reify defs !(evalClosure defs fc)
reifiedVal <- reify defs !(evalClosure defs val)
pure (MkFCVal reifiedFC reifiedVal)
_ => cantReify con "WithFC1 + \{show con}"
reify _ con = cantReify con "WithFC2"


export
Reflect FC where
reflect fc defs True env _ = pure $ Erased fc Placeholder
Expand All @@ -875,12 +863,6 @@ Reflect FC where
appCon fc defs (reflectiontt "MkFC") [fn', start', end']
reflect fc defs lhs env EmptyFC = getCon fc defs (reflectiontt "EmptyFC")

export
Reflect a => Reflect (WithFC a) where
reflect fc defs lhs env (MkFCVal loc val)
= do refFC <- reflect fc defs lhs env loc
refVal <- reflect fc defs lhs env val
appCon fc defs (reflectiontt "MkFCVal") [refFC, refVal]

{-
-- Reflection of well typed terms: We don't reify terms because that involves
Expand Down

0 comments on commit 0ac471b

Please sign in to comment.