137 in |
137 in |
138 (map o map_atyps) |
138 (map o map_atyps) |
139 (fn T as TFree _ => T | T as TVar (vi, _) => |
139 (fn T as TFree _ => T | T as TVar (vi, _) => |
140 if Type_Infer.is_param vi then Type_Infer.param 0 (Name.aT, sort') else T) Ts |
140 if Type_Infer.is_param vi then Type_Infer.param 0 (Name.aT, sort') else T) Ts |
141 end; |
141 end; |
142 fun add_typ_check level name f = Context.proof_map |
|
143 (Syntax.add_typ_check level name (fn Ts => fn ctxt => |
|
144 let val Ts' = f Ts in if eq_list (op =) (Ts, Ts') then NONE else SOME (Ts', ctxt) end)); |
|
145 |
142 |
146 (* preprocessing elements, retrieving base sort from type-checked elements *) |
143 (* preprocessing elements, retrieving base sort from type-checked elements *) |
147 val raw_supexpr = (map (fn sup => (sup, (("", false), |
144 val raw_supexpr = |
148 Expression.Positional []))) sups, []); |
145 (map (fn sup => (sup, (("", false), Expression.Positional []))) sups, []); |
149 val init_class_body = fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints |
146 val init_class_body = |
|
147 fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints |
150 #> Class.redeclare_operations thy sups |
148 #> Class.redeclare_operations thy sups |
151 #> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc |
149 #> Context.proof_map (Syntax.add_typ_check 10 "reject_bcd_etc" (K reject_bcd_etc)) |
152 #> add_typ_check ~10 "singleton_fixate" singleton_fixate; |
150 #> Context.proof_map (Syntax.add_typ_check ~10 "singleton_fixate" (K singleton_fixate)); |
153 val ((raw_supparams, _, raw_inferred_elems), _) = Proof_Context.init_global thy |
151 val ((raw_supparams, _, raw_inferred_elems), _) = |
154 |> add_typ_check 5 "after_infer_fixate" after_infer_fixate |
152 Proof_Context.init_global thy |
|
153 |> Context.proof_map (Syntax.add_typ_check 5 "after_infer_fixate" (K after_infer_fixate)) |
155 |> prep_decl raw_supexpr init_class_body raw_elems; |
154 |> prep_decl raw_supexpr init_class_body raw_elems; |
156 fun filter_element (Element.Fixes []) = NONE |
155 fun filter_element (Element.Fixes []) = NONE |
157 | filter_element (e as Element.Fixes _) = SOME e |
156 | filter_element (e as Element.Fixes _) = SOME e |
158 | filter_element (Element.Constrains []) = NONE |
157 | filter_element (Element.Constrains []) = NONE |
159 | filter_element (e as Element.Constrains _) = SOME e |
158 | filter_element (e as Element.Constrains _) = SOME e |
163 | filter_element (Element.Notes _) = error ("\"notes\" element not allowed in class specification."); |
162 | filter_element (Element.Notes _) = error ("\"notes\" element not allowed in class specification."); |
164 val inferred_elems = map_filter filter_element raw_inferred_elems; |
163 val inferred_elems = map_filter filter_element raw_inferred_elems; |
165 fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs |
164 fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs |
166 | fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs |
165 | fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs |
167 | fold_element_types f (Element.Assumes assms) = fold (fold (fn (t, ts) => |
166 | fold_element_types f (Element.Assumes assms) = fold (fold (fn (t, ts) => |
168 fold_types f t #> (fold o fold_types) f ts) o snd) assms |
167 fold_types f t #> (fold o fold_types) f ts) o snd) assms; |
169 val base_sort = if null inferred_elems then proto_base_sort else |
168 val base_sort = if null inferred_elems then proto_base_sort else |
170 case (fold o fold_element_types) Term.add_tfreesT inferred_elems [] |
169 case (fold o fold_element_types) Term.add_tfreesT inferred_elems [] |
171 of [] => error "No type variable in class specification" |
170 of [] => error "No type variable in class specification" |
172 | [(_, sort)] => sort |
171 | [(_, sort)] => sort |
173 | _ => error "Multiple type variables in class specification"; |
172 | _ => error "Multiple type variables in class specification"; |