105 |
105 |
106 (* reading and processing class specifications *) |
106 (* reading and processing class specifications *) |
107 |
107 |
108 fun prep_class_elems prep_decl thy sups raw_elems = |
108 fun prep_class_elems prep_decl thy sups raw_elems = |
109 let |
109 let |
110 |
|
111 (* user space type system: only permits 'a type variable, improves towards 'a *) |
110 (* user space type system: only permits 'a type variable, improves towards 'a *) |
112 val algebra = Sign.classes_of thy; |
111 val algebra = Sign.classes_of thy; |
113 val inter_sort = curry (Sorts.inter_sort algebra); |
112 val inter_sort = curry (Sorts.inter_sort algebra); |
114 val proto_base_sort = |
113 val proto_base_sort = |
115 if null sups then Sign.defaultS thy |
114 if null sups then Sign.defaultS thy |
116 else fold inter_sort (map (Class.base_sort thy) sups) []; |
115 else fold inter_sort (map (Class.base_sort thy) sups) []; |
117 val is_param = member (op =) (map fst (Class.these_params thy sups)); |
116 val is_param = member (op =) (map fst (Class.these_params thy sups)); |
118 val base_constraints = (map o apsnd) |
117 val base_constraints = (map o apsnd) |
119 (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o fst o snd) |
118 (map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o fst o snd) |
120 (Class.these_operations thy sups); |
119 (Class.these_operations thy sups); |
121 fun singleton_fixateT Ts = |
120 val singleton_fixate = burrow_types (fn Ts => |
122 let |
121 let |
123 val tfrees = fold Term.add_tfreesT Ts []; |
122 val tfrees = fold Term.add_tfreesT Ts []; |
124 val inferred_sort = |
123 val inferred_sort = |
125 (fold o fold_atyps) (fn TVar (_, S) => inter_sort S | _ => I) Ts []; |
124 (fold o fold_atyps) (fn TVar (_, S) => inter_sort S | _ => I) Ts []; |
126 val fixate_sort = |
125 val fixate_sort = |
138 | _ => error "Multiple type variables in class specification"); |
137 | _ => error "Multiple type variables in class specification"); |
139 val fixateT = TFree (Name.aT, fixate_sort); |
138 val fixateT = TFree (Name.aT, fixate_sort); |
140 in |
139 in |
141 (map o map_atyps) |
140 (map o map_atyps) |
142 (fn T as TVar (xi, _) => if Type_Infer.is_param xi then fixateT else T | T => T) Ts |
141 (fn T as TVar (xi, _) => if Type_Infer.is_param xi then fixateT else T | T => T) Ts |
143 end; |
142 end); |
144 fun singleton_fixate _ ts = burrow_types singleton_fixateT ts; |
143 fun unify_params ts = |
145 fun unify_params ctxt ts = |
|
146 let |
144 let |
147 val param_Ts = (fold o fold_aterms) |
145 val param_Ts = (fold o fold_aterms) |
148 (fn Free (v, T) => if is_param v then fold_atyps (insert (op =)) T else I | _ => I) ts []; |
146 (fn Free (v, T) => if is_param v then fold_atyps (insert (op =)) T else I | _ => I) ts []; |
149 val param_namesT = map_filter (try (fst o dest_TVar)) param_Ts; |
147 val param_namesT = map_filter (try (fst o dest_TVar)) param_Ts; |
150 val param_T = if null param_namesT then NONE |
148 val param_T = if null param_namesT then NONE |
160 val raw_supexpr = |
158 val raw_supexpr = |
161 (map (fn sup => (sup, (("", false), Expression.Positional []))) sups, []); |
159 (map (fn sup => (sup, (("", false), Expression.Positional []))) sups, []); |
162 val init_class_body = |
160 val init_class_body = |
163 fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints |
161 fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints |
164 #> Class.redeclare_operations thy sups |
162 #> Class.redeclare_operations thy sups |
165 #> Context.proof_map (Syntax_Phases.term_check 0 "singleton_fixate" singleton_fixate); |
163 #> Context.proof_map (Syntax_Phases.term_check 0 "singleton_fixate" (K singleton_fixate)); |
166 val ((raw_supparams, _, raw_inferred_elems, _), _) = |
164 val ((raw_supparams, _, raw_inferred_elems, _), _) = |
167 Proof_Context.init_global thy |
165 Proof_Context.init_global thy |
168 |> Context.proof_map (Syntax_Phases.term_check 0 "unify_params" unify_params) |
166 |> Context.proof_map (Syntax_Phases.term_check 0 "unify_params" (K unify_params)) |
169 |> prep_decl raw_supexpr init_class_body raw_elems; |
167 |> prep_decl raw_supexpr init_class_body raw_elems; |
170 fun filter_element (Element.Fixes []) = NONE |
168 fun filter_element (Element.Fixes []) = NONE |
171 | filter_element (e as Element.Fixes _) = SOME e |
169 | filter_element (e as Element.Fixes _) = SOME e |
172 | filter_element (Element.Constrains []) = NONE |
170 | filter_element (Element.Constrains []) = NONE |
173 | filter_element (e as Element.Constrains _) = SOME e |
171 | filter_element (e as Element.Constrains _) = SOME e |