src/Pure/Tools/codegen_consts.ML

consts in consts_code Isar commands are now referred to by usual term syntax

(*  Title:      Pure/Tools/codegen_consts.ML
    ID:         $Id$
    Author:     Florian Haftmann, TU Muenchen

Identifying constants by name plus normalized type instantantiation schemes.
Convenient data structures for constants.  Auxiliary.
*)

signature CODEGEN_CONSTS =
sig
  type const = string * string option (*constant name, possibly instance*)
  val const_ord: const * const -> order
  val eq_const: const * const -> bool
  structure Consttab: TABLE
  val const_of_cexpr: theory -> string * typ -> const
  val string_of_typ: theory -> typ -> string
  val string_of_const: theory -> const -> string
  val read_bare_const: theory -> string -> string * typ
  val read_const: theory -> string -> const
  val read_const_exprs: theory -> (const list -> const list)
    -> string list -> const list

  val co_of_const: theory -> const
    -> string * ((string * sort) list * (string * typ list))
  val co_of_const': theory -> const
    -> (string * ((string * sort) list * (string * typ list))) option
  val cos_of_consts: theory -> const list
    -> string * ((string * sort) list * (string * typ list) list)
  val const_of_co: theory -> string -> (string * sort) list
    -> string * typ list -> const
  val consts_of_cos: theory -> string -> (string * sort) list
    -> (string * typ list) list -> const list

  val typargs: theory -> string * typ -> typ list
  val typ_sort_inst: Sorts.algebra -> typ * sort
    -> sort Vartab.table -> sort Vartab.table
end;

structure CodegenConsts: CODEGEN_CONSTS =
struct


(* basic data structures *)

type const = string * string option;
val const_ord = prod_ord fast_string_ord (option_ord string_ord);
val eq_const = is_equal o const_ord;

structure Consttab =
  TableFun(
    type key = const;
    val ord = const_ord;
  );

fun string_of_typ thy = setmp show_sorts true (Sign.string_of_typ thy);


(* conversion between constant expressions and constants *)

fun const_of_cexpr thy (c_ty as (c, _)) =
  case AxClass.class_of_param thy c
   of SOME class => (case Sign.const_typargs thy c_ty
       of [Type (tyco, _)] => if can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class]
              then (c, SOME tyco)
              else (c, NONE)
        | [_] => (c, NONE))
    | NONE => (c, NONE);

fun string_of_const thy (c, NONE) = Sign.extern_const thy c
  | string_of_const thy (c, SOME tyco) = Sign.extern_const thy c
      ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco);


(* reading constants as terms and wildcards pattern *)

fun read_bare_const thy raw_t =
  let
    val t = Sign.read_term thy raw_t;
  in case try dest_Const t
   of SOME c_ty => c_ty
    | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
  end;

fun read_const thy = const_of_cexpr thy o read_bare_const thy;

local

fun consts_of thy some_thyname =
  let
    val this_thy = Option.map theory some_thyname |> the_default thy;
    val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
      ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) this_thy) [];
    fun classop c = case AxClass.class_of_param thy c
     of NONE => [(c, NONE)]
      | SOME class => Symtab.fold
          (fn (tyco, classes) => if AList.defined (op =) classes class
            then cons (c, SOME tyco) else I)
          ((#arities o Sorts.rep_algebra o Sign.classes_of) this_thy)
          [(c, NONE)];
    val consts = maps classop cs;
    fun test_instance thy (class, tyco) =
      can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class]
    fun belongs_here thyname (c, NONE) =
          not (exists (fn thy' => Sign.declared_const thy' c) (Theory.parents_of this_thy))
      | belongs_here thyname (c, SOME tyco) =
          let
            val SOME class = AxClass.class_of_param thy c
          in not (exists (fn thy' => test_instance thy' (class, tyco))
            (Theory.parents_of this_thy))
          end;
  in case some_thyname
   of NONE => consts
    | SOME thyname => filter (belongs_here thyname) consts
  end;

fun read_const_expr thy "*" = ([], consts_of thy NONE)
  | read_const_expr thy s = if String.isSuffix ".*" s
      then ([], consts_of thy (SOME (unsuffix ".*" s)))
      else ([read_const thy s], []);

in

fun read_const_exprs thy select =
  (op @) o apsnd select o pairself flat o split_list o map (read_const_expr thy);

end; (*local*)

(* conversion between constants, constant expressions and datatype constructors *)

fun const_of_co thy tyco vs (co, tys) =
  const_of_cexpr thy (co, tys ---> Type (tyco, map TFree vs));

fun consts_of_cos thy tyco vs cos =
  let
    val dty = Type (tyco, map TFree vs);
    fun mk_co (co, tys) = const_of_cexpr thy (co, tys ---> dty);
  in map mk_co cos end;

local

exception BAD of string;

fun mg_typ_of_const thy (c, NONE) = Sign.the_const_type thy c
  | mg_typ_of_const thy (c, SOME tyco) =
      let
        val SOME class = AxClass.class_of_param thy c;
        val ty = Sign.the_const_type thy c;
          (*an approximation*)
        val sorts = Sorts.mg_domain (Sign.classes_of thy) tyco [class]
          handle CLASS_ERROR => raise BAD ("No such instance: " ^ tyco ^ " :: " ^ class
            ^ ",\nrequired for overloaded constant " ^ c);
        val vs = Name.invents Name.context "'a" (length sorts);
      in map_atyps (K (Type (tyco, map (fn v => TVar ((v, 0), [])) vs))) ty end;

fun gen_co_of_const thy const =
  let
    val (c, _) = const;
    val ty = (Logic.unvarifyT o mg_typ_of_const thy) const;
    fun err () = raise BAD
     ("Illegal type for datatype constructor: " ^ string_of_typ thy ty);
    val (tys, ty') = strip_type ty;
    val (tyco, vs) = ((apsnd o map) dest_TFree o dest_Type) ty'
      handle TYPE _ => err ();
    val sorts = if has_duplicates (eq_fst op =) vs then err ()
      else map snd vs;
    val vs_names = Name.invent_list [] "'a" (length vs);
    val vs_map = map fst vs ~~ vs_names;
    val vs' = vs_names ~~ sorts;
    val tys' = (map o map_type_tfree) (fn (v, sort) =>
      (TFree ((the o AList.lookup (op =) vs_map) v, sort))) tys
      handle Option => err ();
  in (tyco, (vs', (c, tys'))) end;

in

fun co_of_const thy const = gen_co_of_const thy const handle BAD msg => error msg;
fun co_of_const' thy const = SOME (gen_co_of_const thy const) handle BAD msg => NONE;

end;

fun cos_of_consts thy consts =
  let
    val raw_cos  = map (co_of_const thy) consts;
    val (tyco, (vs_names, sorts_cos)) = if (length o distinct (eq_fst op =)) raw_cos = 1
      then ((fst o hd) raw_cos, ((map fst o fst o snd o hd) raw_cos,
        map ((apfst o map) snd o snd) raw_cos))
      else error ("Term constructors not referring to the same type: "
        ^ commas (map (string_of_const thy) consts));
    val sorts = foldr1 ((uncurry o map2 o curry o Sorts.inter_sort) (Sign.classes_of thy))
      (map fst sorts_cos);
    val cos = map snd sorts_cos;
    val vs = vs_names ~~ sorts;
  in (tyco, (vs, cos)) end;


(* dictionary values *)

fun typargs thy (c_ty as (c, ty)) =
  let
    val opt_class = AxClass.class_of_param thy c;
    val tys = Sign.const_typargs thy (c, ty);
  in case (opt_class, tys)
   of (SOME class, ty as [Type (tyco, tys')]) =>
        if can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class]
        then tys' else ty
    | _ => tys
  end;

fun typ_sort_inst algebra =
  let
    val inters = Sorts.inter_sort algebra;
    fun match _ [] = I
      | match (TVar (v, S)) S' = Vartab.map_default (v, []) (fn S'' => inters (S, inters (S', S'')))
      | match (Type (a, Ts)) S =
          fold2 match Ts (Sorts.mg_domain algebra a S)
  in uncurry match end;

end;