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 |
94 |
95 2) alpha_ty relations are generated for all the types being defined: |
95 2) alpha_ty relations are generated for all the types being defined: |
96 |
96 |
97 !!! permutations !!! |
97 For each constructor we gather all the arguments that are bound, |
98 |
98 and for each of those we add a permutation. We associate those |
99 An alpha_ty for a constructor is true if a conjunction of |
99 permutations with the bindings. Note that two bindings can have |
100 propositions for each argument holds. |
100 the same permutation if the arguments being bound are the same. |
|
101 |
|
102 An alpha_ty for a constructor is true if there exist permutations |
|
103 as above such that a conjunction of propositions for all arguments holds. |
101 |
104 |
102 For an argument we allow bindings where only one of the following |
105 For an argument we allow bindings where only one of the following |
103 holds: |
106 holds: |
104 |
107 |
105 - Argument is bound in some shallow bindings: We return true |
108 - Argument is bound in some shallow bindings: We return true |
106 - Argument is bound in some deep recursive bindings |
109 - Argument of type ty is bound recursively in some other |
107 !!! still to describe !!! |
110 arguments [i1, .. in] with one binding function bn. |
|
111 We return: |
|
112 |
|
113 (bn argl, (argl, argl_i1, ..., argl_in)) \<approx>gen |
|
114 \<lambda>(argl,argl1,..,argln) (argr,argr1,..,argrn). |
|
115 (alpha_ty argl argr) \<and> (alpha_i1 argl1 argr1) \<and> .. \<and> (alpha_in argln argrn) |
|
116 \<lambda>(arg,arg1,..,argn). (fv_ty arg) \<union> (fv_i1 arg1) \<union> .. \<union> (fv_in argn) |
|
117 pi |
|
118 (bn argr, (argr, argr_i1, ..., argr_in)) |
|
119 |
108 - Argument is bound in some deep non-recursive bindings. |
120 - Argument is bound in some deep non-recursive bindings. |
109 We return: alpha_bn argl argr |
121 We return: alpha_bn argl argr |
110 - Argument has some shallow and/or non-recursive bindings. |
122 - Argument of type ty has some shallow bindings [b1..bn] and/or |
111 !!! still to describe !!! |
123 non-recursive bindings [f1 a1, .., fm am], where the bindings |
|
124 have the permutations p1..pl. We return: |
|
125 |
|
126 (b1l \<union>..\<union> bnl \<union> f1 a1l \<union>..\<union> fn anl, argl) \<approx>gen |
|
127 alpha_ty fv_ty (p1 +..+ pl) |
|
128 (b1r \<union>..\<union> bnr \<union> f1 a1r \<union>..\<union> fn anr, argr) |
|
129 |
112 - Argument has some recursive bindings. The bindings were |
130 - Argument has some recursive bindings. The bindings were |
113 already treated in 2nd case so we return: True |
131 already treated in 2nd case so we return: True |
114 - Argument has no bindings and is not bound. |
132 - Argument has no bindings and is not bound. |
115 If it is recursive for type ty, we return: alpha_ty argl argr |
133 If it is recursive for type ty, we return: alpha_ty argl argr |
116 Otherwise we return: argl = argr |
134 Otherwise we return: argl = argr |