Do any practical programming languages support term graph rewriting of infinite but regular terms? For example the toy language CoCaml  supports computations on infinite regular streams. Coq supports coinduction  but not infinitary rewriting, as far as I can tell. By "infinite regular term graph", I mean those inhabitants of coalgebraic datatypes that can be defined in terms of finitely many equations.
-  Jean-Baptiste Jeannin, Dexter Kozen, Alexandra Silva (2017) CoCaml: Functional Programming with Regular Coinductive Types
-  Yves Bertot, Ekaterina Komendantskaya (2008) Inductive and Coinductive Components of Corecursive Functions in Coq