search

data61 / PSL

Other
65 stars 9 forks source link

MiLkMaId: each node in a syntax tree should have a unique identifier (of type integer?) #51

Open yutakang opened 6 years ago

yutakang commented 6 years ago

Currently, each point has only three fields: cname, utyp, and level. Therefore, it is possible that a syntax tree has multiple points of the same value. We should avoid such situation.

yutakang commented 6 years ago

It turned out to be a bad idea to convert un-curried syntax trees to tables. And I found out that it is more intuitive, straightforward, and functional to work directly on un-curried syntax trees.

However, tagging each node in un-curried syntax tree with a unique identifier still might be a good idea when handling induct_tac and de-Bruijn indices in future.