Possibilities rewrite rules LHS unclear

[markuzzz]

Suppose we have

map
	test: List(Int) -> Int;
var
	ls: List(Int);
	i: Int;

Then the equation test(i |> ls) = i is fine. test[i] will be rewritten to i. However, test(ls <| i) = i is not fine, test([1]) can not be rewritten further. I suspect left append is a constructor for lists while right append is not (and only constructors can be used in the left hand side?). I understand not every left hand side of a rewrite rule can be used for matching. However, for the user it is unclear what will work and what will not. It would be good warn the user that a rewrite rule is not usable for matching.

[jgroote]

I am afraid a part of your data type is missing. I expect an equation using the eqn keyword.

[markuzzz]

The equations are listed in the text.

map
	test: List(Int) -> Int;
var
	ls: List(Int);
	i: Int;
eqn
	test(ls <| i) = i;

[Valo13]

I think that this is indeed due to <| not being a constructor. There are rewrite rules that can relate |> and <| (namely [] <| d = d |> [] and (d |> s) <| e = d |> (s <| e)), but afaik rewrite rules are only applied from left to right (otherwise it will never terminate since it could go back and forth). Therefore, the list [1], internally represented as 1 |> [], will not be rewritten to [] <| 1 to match your rewrite rule for test. I'd say that a general rule for creating rewrite rules is that the lefthand side should only consist of the mapping where this rewrite rule is defined for (in your case test) as top term, with only constructors as subterms.

[jgroote]

This is indeed correct. Rewriting works with matching of patterns. If there is no match, -- as in your case -- rewriting does not take place. If you are not aware of it, it can be confusing.

[markuzzz]

Would it then not be a good idea to check whether the left hand side of rewrite rules consists of a top term with only constructors as subterms. If this is violated (as is the case in my example) a warning could be given: "Warning, the left hand side of the rewrite rule test(ls <| i) = i; contains subterms that are not constructors. The rewrite rule will therefore never match a term."

[jgroote]

I do like this. For your rule, there could be a matching term namely test(l <| i) where l is a variable. In such a case l <| i is a normal form. So, it is not immediately clear how such a check should look like. I transform this in a feature request.