70 fun mk_mapfun_aux rty = |
70 fun mk_mapfun_aux rty = |
71 case rty of |
71 case rty of |
72 TVar _ => mk_Free rty |
72 TVar _ => mk_Free rty |
73 | Type (_, []) => mk_identity rty |
73 | Type (_, []) => mk_identity rty |
74 | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys) |
74 | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys) |
75 | _ => raise LIFT_MATCH ("mk_mapfun_aux (default)") |
75 | _ => raise LIFT_MATCH ("mk_mapfun (default)") |
76 in |
76 in |
77 fold_rev Term.lambda vs' (mk_mapfun_aux rty) |
77 fold_rev Term.lambda vs' (mk_mapfun_aux rty) |
78 end |
78 end |
79 |
79 |
80 (* looks up the (varified) rty and qty for *) |
80 (* looks up the (varified) rty and qty for *) |
118 ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) |
118 ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) |
119 end |
119 end |
120 |
120 |
121 (* produces an aggregate absrep function *) |
121 (* produces an aggregate absrep function *) |
122 (* *) |
122 (* *) |
123 (* - In case of equal types we just return the identity *) |
123 (* - In case of equal types we just return the identity. *) |
124 (* *) |
124 (* *) |
125 (* - In case of function types and TFrees, we recurse, taking in *) |
125 (* - In case of function types and TFrees, we recurse, taking in *) |
126 (* the first case the polarity change into account. *) |
126 (* the first case the polarity change into account. *) |
127 (* *) |
127 (* *) |
128 (* - If the type constructors are equal, we recurse for the *) |
128 (* - If the type constructors are equal, we recurse for the *) |
129 (* arguments and prefix the appropriate map function *) |
129 (* arguments and build the appropriate map function. *) |
130 (* *) |
130 (* *) |
131 (* - If the type constructors are unequal, there must be an *) |
131 (* - If the type constructors are unequal, there must be an *) |
132 (* instance of quotient types: *) |
132 (* instance of quotient types: *) |
133 (* - we first look up the corresponding rty_pat and qty_pat *) |
133 (* - we first look up the corresponding rty_pat and qty_pat *) |
134 (* from the quotient definition; the arguments of qty_pat *) |
134 (* from the quotient definition; the arguments of qty_pat *) |
135 (* must be some distinct TVars *) |
135 (* must be some distinct TVars *) |
136 (* - we then match the rty_pat with rty and qty_pat with qty; *) |
136 (* - we then match the rty_pat with rty and qty_pat with qty; *) |
137 (* if matching fails the types do not match *) |
137 (* if matching fails the types do not match *) |
138 (* - the matching produces two environments, we look up the *) |
138 (* - the matching produces two environments; we look up the *) |
139 (* assignments for the qty_pat variables and recurse on the *) |
139 (* assignments for the qty_pat variables and recurse on the *) |
140 (* assignmetnts *) |
140 (* assignments *) |
141 (* - we prefix the aggregate map function for the rty_pat, *) |
141 (* - we prefix the aggregate map function for the rty_pat, *) |
142 (* which is an abstraction over all type variables *) |
142 (* which is an abstraction over all type variables *) |
143 (* - finally we compse the result with the appropriate *) |
143 (* - finally we compose the result with the appropriate *) |
144 (* absrep function *) |
144 (* absrep function *) |
145 (* *) |
145 (* *) |
146 (* The composition is necessary for types like *) |
146 (* The composition is necessary for types like *) |
147 (* *) |
147 (* *) |
148 (* ('a list) list / ('a foo) foo *) |
148 (* ('a list) list / ('a foo) foo *) |