[ fix #698 ] Safe reflection module

[gallais]

Now that Agda internalises all the properties we need, we should be able to
finally turn the --safe option on in the Reflection module.

[L-TChen]

Defining a function over Term, Clause, etc. by structural recursion is painfully tedious, so I come up with a partial solution by packing every case in a record type and pre-cooking some instances like identity and an any instance for Term, etc.

Then, to define functions over them, one can use the record update syntax to change the necessary part leaving other cases as they are. For example, to check if a term contains some Meta, the only interesting case is meta : (x : Meta) → List (Arg Term) → Term so one only need to update the meta case in the any instance.

PS. I call it partial because

The above point can be done via Traversable or a general fold function.

• recursor and eliminator should be generated by the reflection mechanism
• the record update does not support copattern syntax, and I haven't figured out a suitable change for it.

[gallais]

I am not planning to write any additional traversals, I am just redistributing
and refactoring the existing functions and renaming them to be closer to conventions.

[gallais]

Last thing missing: the deprecated names moved to Reflection.Term.