File ‹hol_datatype.ML›

signature HOL_DATATYPE = sig
  val mk_typ: bool -> typ -> term
  val mk_dt_def: Proof.context -> string -> term
end

structure HOL_Datatype : HOL_DATATYPE = struct

fun check_sort [@{class type}] = ()
  | check_sort _ = error "non-standard sorts are not supported"

fun mk_tvar ((name, idx), sort) =
  (check_sort sort; mk_name (name ^ "." ^ Value.print_int idx))

fun mk_tfree (name, sort) =
  (check_sort sort; mk_name name)

fun mk_typ schematic t =
  let
    fun aux (Type (typ, args)) =
          @{const TApp} $ mk_name typ $ HOLogic.mk_list @{typ typ} (map aux args)
      | aux (TVar tvar) =
          if schematic then
            @{const TVar} $ mk_tvar tvar
          else
            error "schematic type variables are not supported"
      | aux (TFree tfree) =
          if schematic then
            error "free type variables are not supported"
          else
            @{const TVar} $ mk_tfree tfree
  in aux t end

fun mk_dt_def ctxt typ =
  let
    val {ctrs, T, ...} = the (Ctr_Sugar.ctr_sugar_of ctxt typ)

    val tparams =
      dest_Type T |> snd
      |> map (mk_tvar o dest_TVar)
      |> HOLogic.mk_list @{typ name}

    fun mk_ctr ctr =
      let
        val (name, typ) = dest_Const ctr
        val params = strip_type typ |> fst |> map (mk_typ true) |> HOLogic.mk_list @{typ typ}
      in (mk_name name, params) end

    val ctrs =
      map mk_ctr ctrs
      |> mk_fmap (@{typ name}, @{typ "typ list"})
  in
    @{const make_dt_def} $ tparams $ ctrs
  end

end