27 -> theory -> theory) -> theory -> theory |
27 -> theory -> theory) -> theory -> theory |
28 val add_case: thm -> theory -> theory |
28 val add_case: thm -> theory -> theory |
29 val add_undefined: string -> theory -> theory |
29 val add_undefined: string -> theory -> theory |
30 val purge_data: theory -> theory |
30 val purge_data: theory -> theory |
31 |
31 |
32 val coregular_algebra: theory -> Sorts.algebra |
|
33 val operational_algebra: theory -> (sort -> sort) * Sorts.algebra |
|
34 val these_eqns: theory -> string -> (thm * bool) list |
32 val these_eqns: theory -> string -> (thm * bool) list |
35 val these_raw_eqns: theory -> string -> (thm * bool) list |
33 val these_raw_eqns: theory -> string -> (thm * bool) list |
36 val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list) |
34 val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list) |
37 val get_datatype_of_constr: theory -> string -> string option |
35 val get_datatype_of_constr: theory -> string -> string option |
38 val get_case_scheme: theory -> string -> (int * (int * string list)) option |
36 val get_case_scheme: theory -> string -> (int * (int * string list)) option |
467 Code_Unit.error_thm ((if linear then check_linear else I) o Code_Unit.mk_eqn thy); |
465 Code_Unit.error_thm ((if linear then check_linear else I) o Code_Unit.mk_eqn thy); |
468 fun mk_syntactic_eqn thy = Code_Unit.warning_thm (Code_Unit.mk_eqn thy); |
466 fun mk_syntactic_eqn thy = Code_Unit.warning_thm (Code_Unit.mk_eqn thy); |
469 fun mk_default_eqn thy = Code_Unit.try_thm (check_linear o Code_Unit.mk_eqn thy); |
467 fun mk_default_eqn thy = Code_Unit.try_thm (check_linear o Code_Unit.mk_eqn thy); |
470 |
468 |
471 |
469 |
472 (** operational sort algebra and class discipline **) |
|
473 |
|
474 local |
|
475 |
|
476 fun arity_constraints thy algebra (class, tyco) = |
|
477 let |
|
478 val base_constraints = Sorts.mg_domain algebra tyco [class]; |
|
479 val classparam_constraints = Sorts.complete_sort algebra [class] |
|
480 |> maps (map fst o these o try (#params o AxClass.get_info thy)) |
|
481 |> map_filter (fn c => try (AxClass.param_of_inst thy) (c, tyco)) |
|
482 |> maps (map fst o get_eqns thy) |
|
483 |> map (map (snd o dest_TVar) o Sign.const_typargs thy o Code_Unit.const_typ_eqn); |
|
484 val inter_sorts = map2 (curry (Sorts.inter_sort algebra)); |
|
485 in fold inter_sorts classparam_constraints base_constraints end; |
|
486 |
|
487 fun retrieve_algebra thy operational = |
|
488 Sorts.subalgebra (Syntax.pp_global thy) operational |
|
489 (SOME o arity_constraints thy (Sign.classes_of thy)) |
|
490 (Sign.classes_of thy); |
|
491 |
|
492 in |
|
493 |
|
494 fun coregular_algebra thy = retrieve_algebra thy (K true) |> snd; |
|
495 fun operational_algebra thy = |
|
496 let |
|
497 fun add_iff_operational class = |
|
498 can (AxClass.get_info thy) class ? cons class; |
|
499 val operational_classes = fold add_iff_operational (Sign.all_classes thy) [] |
|
500 in retrieve_algebra thy (member (op =) operational_classes) end; |
|
501 |
|
502 end; (*local*) |
|
503 |
|
504 |
|
505 (** interfaces and attributes **) |
470 (** interfaces and attributes **) |
506 |
471 |
507 fun delete_force msg key xs = |
472 fun delete_force msg key xs = |
508 if AList.defined (op =) xs key then AList.delete (op =) key xs |
473 if AList.defined (op =) xs key then AList.delete (op =) key xs |
509 else error ("No such " ^ msg ^ ": " ^ quote key); |
474 else error ("No such " ^ msg ^ ": " ^ quote key); |