268 (* policies *) |
268 (* policies *) |
269 |
269 |
270 local |
270 local |
271 fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy); |
271 fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy); |
272 fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy); |
272 fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy); |
273 fun thyname_of_const' thy = #theory_name o Name_Space.the_entry (Sign.const_space thy); |
|
274 fun thyname_of_instance thy inst = case AxClass.thynames_of_arity thy inst |
273 fun thyname_of_instance thy inst = case AxClass.thynames_of_arity thy inst |
275 of [] => error ("No such instance: " ^ quote (snd inst ^ " :: " ^ fst inst)) |
274 of [] => error ("No such instance: " ^ quote (snd inst ^ " :: " ^ fst inst)) |
276 | thyname :: _ => thyname; |
275 | thyname :: _ => thyname; |
277 fun thyname_of_const thy c = case AxClass.class_of_param thy c |
276 fun thyname_of_const thy c = case AxClass.class_of_param thy c |
278 of SOME class => thyname_of_class thy class |
277 of SOME class => thyname_of_class thy class |
279 | NONE => (case Code.get_type_of_constr_or_abstr thy c |
278 | NONE => (case Code.get_type_of_constr_or_abstr thy c |
280 of SOME (tyco, _) => thyname_of_type thy tyco |
279 of SOME (tyco, _) => thyname_of_type thy tyco |
281 | NONE => thyname_of_const' thy c); |
280 | NONE => #theory_name (Name_Space.the_entry (Sign.const_space thy) c)); |
282 fun purify_base "==>" = "follows" |
281 fun purify_base "==>" = "follows" |
283 | purify_base "==" = "meta_eq" |
282 | purify_base "==" = "meta_eq" |
284 | purify_base s = Name.desymbolize false s; |
283 | purify_base s = Name.desymbolize false s; |
285 fun namify thy get_basename get_thyname name = |
284 fun namify thy get_basename get_thyname name = |
286 let |
285 let |
469 | _ => false; |
468 | _ => false; |
470 |
469 |
471 fun is_case (Fun (_, (_, SOME _))) = true |
470 fun is_case (Fun (_, (_, SOME _))) = true |
472 | is_case _ = false; |
471 | is_case _ = false; |
473 |
472 |
474 fun lookup_classparam_instance program name = program |> Graph.get_first |
|
475 (fn (_, (Classinst ((class, _), (_, (param_insts, _))), _)) => |
|
476 Option.map (fn ((const, _), _) => (class, const)) |
|
477 (find_first (fn ((_, (inst_const, _)), _) => inst_const = name) param_insts) | _ => NONE) |
|
478 |
|
479 fun labelled_name thy program name = |
473 fun labelled_name thy program name = |
480 let val ctxt = Proof_Context.init_global thy in |
474 let val ctxt = Proof_Context.init_global thy in |
481 case Graph.get_node program name of |
475 case Graph.get_node program name of |
482 Fun (c, _) => quote (Code.string_of_const thy c) |
476 Fun (c, _) => quote (Code.string_of_const thy c) |
483 | Datatype (tyco, _) => "type " ^ quote (Proof_Context.extern_type ctxt tyco) |
477 | Datatype (tyco, _) => "type " ^ quote (Proof_Context.extern_type ctxt tyco) |