equal
deleted
inserted
replaced
52 |
52 |
53 2) fv functions generated for all new datatypes: |
53 2) fv functions generated for all new datatypes: |
54 |
54 |
55 An fv for a constructor is a union of values for the arguments. |
55 An fv for a constructor is a union of values for the arguments. |
56 |
56 |
57 For an argument x that bound in a non-recursive binding |
57 For an argument that is bound in a shallow binding we return empty. |
|
58 |
|
59 For an argument x that bound in a non-recursive deep binding |
58 we return: fv_bn x. |
60 we return: fv_bn x. |
59 |
61 |
60 Otherwise we return the free variables of the argument minus the |
62 Otherwise we return the free variables of the argument minus the |
61 bound variables of the argument. |
63 bound variables of the argument. |
62 |
64 |
68 |
70 |
69 The bound variables are a union of results of all bindings that |
71 The bound variables are a union of results of all bindings that |
70 involve the given argument. For a paricular binding: |
72 involve the given argument. For a paricular binding: |
71 |
73 |
72 - for a binding function bn: bn x |
74 - for a binding function bn: bn x |
73 - for an atom: {atom x} |
|
74 - for atom set: atom ` x |
|
75 - for a recursive argument of type ty': fv_fy' x |
75 - for a recursive argument of type ty': fv_fy' x |
76 - for nominal datatype ty' return: fv_ty' x |
76 - for nominal datatype ty' return: fv_ty' x |
77 *) |
77 *) |
78 |
78 |
79 ML {* |
79 ML {* |