48 - for atom set we return: atom ` x |
48 - for atom set we return: atom ` x |
49 - for a recursive call to type ty' we return: fv_ty' x |
49 - for a recursive call to type ty' we return: fv_ty' x |
50 with fv of the appropriate type |
50 with fv of the appropriate type |
51 - otherwise empty |
51 - otherwise empty |
52 |
52 |
53 2) fv functions generated for all new datatypes: |
53 2) fv_ty functions generated for all types being defined: |
54 |
54 |
55 An fv for a constructor is a union of values for the arguments. |
55 fv_ty for a constructor is a union of values for the arguments. |
56 |
56 |
57 For an argument that is bound in a shallow binding we return empty. |
57 For an argument that is bound in a shallow binding we return empty. |
58 |
58 |
59 For an argument x that bound in a non-recursive deep binding |
59 For an argument x that bound in a non-recursive deep binding |
60 we return: fv_bn x. |
60 we return: fv_bn x. |
89 |
89 |
90 - for a recursive argument in the bn function, we return: alpha_bn argl argr |
90 - for a recursive argument in the bn function, we return: alpha_bn argl argr |
91 - for a recursive argument for type ty not in bn, we return: alpha_ty argl argr |
91 - for a recursive argument for type ty not in bn, we return: alpha_ty argl argr |
92 - for other arguments in the bn function we return: True |
92 - for other arguments in the bn function we return: True |
93 - for other arguments not in the bn function we return: argl = argr |
93 - for other arguments not in the bn function we return: argl = argr |
|
94 |
|
95 2) alpha_ty relations are generated for all the types being defined: |
|
96 |
|
97 !!! permutations !!! |
|
98 |
|
99 An alpha_ty for a constructor is true if a conjunction of |
|
100 propositions for each argument holds. |
|
101 |
|
102 For an argument we allow bindings where only one of the following |
|
103 holds: |
|
104 |
|
105 - Argument is bound in some shallow bindings: We return true |
|
106 - Argument is bound in some deep recursive bindings |
|
107 !!! still to describe !!! |
|
108 - Argument is bound in some deep non-recursive bindings. |
|
109 We return: alpha_bn argl argr |
|
110 - Argument has some shallow and/or non-recursive bindings. |
|
111 !!! still to describe !!! |
|
112 - Argument has some recursive bindings. The bindings were |
|
113 already treated in 2nd case so we return: True |
|
114 - Argument has no bindings and is not bound. |
|
115 If it is recursive for type ty, we return: alpha_ty argl argr |
|
116 Otherwise we return: argl = argr |
94 |
117 |
95 *) |
118 *) |
96 |
119 |
97 ML {* |
120 ML {* |
98 fun is_atom thy typ = |
121 fun is_atom thy typ = |