30 |
30 |
31 (* calculating class-related rules including canonical interpretation *) |
31 (* calculating class-related rules including canonical interpretation *) |
32 |
32 |
33 fun calculate thy class sups base_sort param_map assm_axiom = |
33 fun calculate thy class sups base_sort param_map assm_axiom = |
34 let |
34 let |
35 val empty_ctxt = ProofContext.init thy; |
35 val empty_ctxt = ProofContext.init_global thy; |
36 |
36 |
37 (* instantiation of canonical interpretation *) |
37 (* instantiation of canonical interpretation *) |
38 val aT = TFree (Name.aT, base_sort); |
38 val aT = TFree (Name.aT, base_sort); |
39 val param_map_const = (map o apsnd) Const param_map; |
39 val param_map_const = (map o apsnd) Const param_map; |
40 val param_map_inst = (map o apsnd) |
40 val param_map_inst = (map o apsnd) |
141 #> redeclare_operations thy sups |
141 #> redeclare_operations thy sups |
142 #> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc |
142 #> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc |
143 #> add_typ_check ~10 "singleton_fixate" singleton_fixate; |
143 #> add_typ_check ~10 "singleton_fixate" singleton_fixate; |
144 val raw_supexpr = (map (fn sup => (sup, (("", false), |
144 val raw_supexpr = (map (fn sup => (sup, (("", false), |
145 Expression.Positional []))) sups, []); |
145 Expression.Positional []))) sups, []); |
146 val ((raw_supparams, _, inferred_elems), _) = ProofContext.init thy |
146 val ((raw_supparams, _, inferred_elems), _) = ProofContext.init_global thy |
147 |> prep_decl raw_supexpr init_class_body raw_elems; |
147 |> prep_decl raw_supexpr init_class_body raw_elems; |
148 fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs |
148 fun fold_element_types f (Element.Fixes fxs) = fold (fn (_, SOME T, _) => f T) fxs |
149 | fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs |
149 | fold_element_types f (Element.Constrains cnstrs) = fold (f o snd) cnstrs |
150 | fold_element_types f (Element.Assumes assms) = fold (fold (fn (t, ts) => |
150 | fold_element_types f (Element.Assumes assms) = fold (fold (fn (t, ts) => |
151 fold_types f t #> (fold o fold_types) f ts) o snd) assms |
151 fold_types f t #> (fold o fold_types) f ts) o snd) assms |
192 val (base_sort, supparam_names, supexpr, inferred_elems) = |
192 val (base_sort, supparam_names, supexpr, inferred_elems) = |
193 prep_class_elems thy sups raw_elems; |
193 prep_class_elems thy sups raw_elems; |
194 val sup_sort = inter_sort base_sort sups; |
194 val sup_sort = inter_sort base_sort sups; |
195 |
195 |
196 (* process elements as class specification *) |
196 (* process elements as class specification *) |
197 val class_ctxt = begin sups base_sort (ProofContext.init thy); |
197 val class_ctxt = begin sups base_sort (ProofContext.init_global thy); |
198 val ((_, _, syntax_elems), _) = class_ctxt |
198 val ((_, _, syntax_elems), _) = class_ctxt |
199 |> Expression.cert_declaration supexpr I inferred_elems; |
199 |> Expression.cert_declaration supexpr I inferred_elems; |
200 fun check_vars e vs = if null vs |
200 fun check_vars e vs = if null vs |
201 then error ("No type variable in part of specification element " |
201 then error ("No type variable in part of specification element " |
202 ^ (Pretty.output o Pretty.chunks) (Element.pretty_ctxt class_ctxt e)) |
202 ^ (Pretty.output o Pretty.chunks) (Element.pretty_ctxt class_ctxt e)) |