src/HOL/Tools/Nunchaku/nunchaku_translate.ML

back to more basic defaults, independently on the accidental L&F: e.g. relevant for editor_style=false, and session_graph.pdf;

(*  Title:      HOL/Tools/Nunchaku/nunchaku_translate.ML
    Author:     Jasmin Blanchette, VU Amsterdam
    Copyright   2015, 2016, 2017

Translation of Isabelle/HOL problems to Nunchaku.
*)

signature NUNCHAKU_TRANSLATE =
sig
  type isa_problem = Nunchaku_Collect.isa_problem
  type ty = Nunchaku_Problem.ty
  type nun_problem = Nunchaku_Problem.nun_problem

  val flip_quote: string -> string
  val lowlevel_str_of_ty: ty -> string

  val nun_problem_of_isa: Proof.context -> isa_problem -> nun_problem
end;

structure Nunchaku_Translate : NUNCHAKU_TRANSLATE =
struct

open Nunchaku_Util;
open Nunchaku_Collect;
open Nunchaku_Problem;

fun flip_quote s =
  (case try (unprefix "'") s of
    SOME s' => s'
  | NONE => prefix "'" s);

fun lowlevel_str_of_ty (NType (id, tys)) =
  (if null tys then "" else encode_args (map lowlevel_str_of_ty tys)) ^ id;

fun strip_nun_abs 0 tm = ([], tm)
  | strip_nun_abs n (NAbs (var, body)) =
    strip_nun_abs (n - 1) body
    |>> cons var;

val strip_nun_comb =
  let
    fun strip args (NApp (func, arg)) = strip (arg :: args) func
      | strip args tm = (tm, args);
  in
    strip []
  end;

fun ty_of_isa (Type (s, Ts)) =
    let val tys = map ty_of_isa Ts in
      (case s of
        \<^type_name>\<open>bool\<close> => prop_ty
      | \<^type_name>\<open>fun\<close> => NType (nun_arrow, tys)
      | _ =>
        let
          val args = map lowlevel_str_of_ty tys;
          val id = nun_tconst_of_str args s;
        in
          NType (id, [])
        end)
    end
  | ty_of_isa (TFree (s, _)) = NType (nun_tfree_of_str (flip_quote s), [])
  | ty_of_isa (TVar _) = raise Fail "unexpected TVar";

fun gen_tm_of_isa in_prop ctxt t =
  let
    val thy = Proof_Context.theory_of ctxt;

    fun id_of_const (x as (s, _)) =
      let val args = map (lowlevel_str_of_ty o ty_of_isa) (Sign.const_typargs thy x) in
        nun_const_of_str args s
      end;

    fun tm_of_branch ctr_id var_count f_arg_tm =
      let val (vars, body) = strip_nun_abs var_count f_arg_tm in
        (ctr_id, vars, body)
      end;

    fun tm_of bounds (Const (x as (s, T))) =
        (case try (dest_co_datatype_case ctxt) x of
          SOME ctrs =>
          let
            val num_f_args = length ctrs;
            val min_args = num_f_args + 1;
            val var_counts = map (num_binder_types o snd) ctrs;

            val dummy_free = Free (Name.uu, T);
            val tm = tm_of bounds dummy_free;
            val tm' = eta_expandN_tm min_args tm;
            val (vars, body) = strip_nun_abs min_args tm';
            val (_, (f_args, obj :: other_args)) = strip_nun_comb body ||> chop num_f_args;
            val f_args' = map2 eta_expandN_tm var_counts f_args;

            val ctr_ids = map id_of_const ctrs;
          in
            NMatch (obj, @{map 3} tm_of_branch ctr_ids var_counts f_args')
            |> rcomb_tms other_args
            |> abs_tms vars
          end
        | NONE =>
          if s = \<^const_name>\<open>unreachable\<close> andalso in_prop then
            let val ty = ty_of_isa T in
              napps (NConst (nun_asserting, [ty], mk_arrows_ty ([ty, prop_ty], ty)),
                [NConst (id_of_const x, [], ty), NConst (nun_false, [], prop_ty)])
            end
          else
            let
              val id =
                (case s of
                  \<^const_name>\<open>All\<close> => nun_forall
                | \<^const_name>\<open>conj\<close> => nun_conj
                | \<^const_name>\<open>disj\<close> => nun_disj
                | \<^const_name>\<open>HOL.eq\<close> => nun_equals
                | \<^const_name>\<open>Eps\<close> => nun_choice
                | \<^const_name>\<open>Ex\<close> => nun_exists
                | \<^const_name>\<open>False\<close> => nun_false
                | \<^const_name>\<open>If\<close> => nun_if
                | \<^const_name>\<open>implies\<close> => nun_implies
                | \<^const_name>\<open>Not\<close> => nun_not
                | \<^const_name>\<open>The\<close> => nun_unique
                | \<^const_name>\<open>The_unsafe\<close> => nun_unique_unsafe
                | \<^const_name>\<open>True\<close> => nun_true
                | _ => id_of_const x);
            in
              NConst (id, [], ty_of_isa T)
            end)
      | tm_of _ (Free (s, T)) = NConst (nun_free_of_str s, [], ty_of_isa T)
      | tm_of _ (Var ((s, _), T)) = NConst (nun_var_of_str s, [], ty_of_isa T)
      | tm_of bounds (Abs (s, T, t)) =
        let
          val (s', bounds') = Name.variant s bounds;
          val x = Var ((s', 0), T);
        in
          NAbs (tm_of bounds' x, tm_of bounds' (subst_bound (x, t)))
        end
      | tm_of bounds (t $ u) = NApp (tm_of bounds t, tm_of bounds u)
      | tm_of _ (Bound _) = raise Fail "unexpected Bound";
  in
    t
    |> tm_of Name.context
    |> eta_expand_builtin_tm
  end;

val tm_of_isa = gen_tm_of_isa false;
val prop_of_isa = gen_tm_of_isa true;

fun nun_copy_spec_of_isa_typedef ctxt {abs_typ, rep_typ, wrt, abs, rep} =
  {abs_ty = ty_of_isa abs_typ, rep_ty = ty_of_isa rep_typ, subset = SOME (tm_of_isa ctxt wrt),
   quotient = NONE, abs = tm_of_isa ctxt abs, rep = tm_of_isa ctxt rep};

fun nun_copy_spec_of_isa_quotient ctxt {abs_typ, rep_typ, wrt, abs, rep} =
  {abs_ty = ty_of_isa abs_typ, rep_ty = ty_of_isa rep_typ, subset = NONE,
   quotient = SOME (tm_of_isa ctxt wrt), abs = tm_of_isa ctxt abs, rep = tm_of_isa ctxt rep};

fun nun_ctr_of_isa ctxt ctr =
  {ctr = tm_of_isa ctxt ctr, arg_tys = map ty_of_isa (binder_types (fastype_of ctr))};

fun nun_co_data_spec_of_isa ctxt {typ, ctrs} =
  {ty = ty_of_isa typ, ctrs = map (nun_ctr_of_isa ctxt) ctrs};

fun nun_const_spec_of_isa ctxt {const, props} =
  {const = tm_of_isa ctxt const, props = map (prop_of_isa ctxt) props};

fun nun_rec_spec_of_isa ctxt {const, props, ...} =
  {const = tm_of_isa ctxt const, props = map (prop_of_isa ctxt) props};

fun nun_consts_spec_of_isa ctxt {consts, props} =
  {consts = map (tm_of_isa ctxt) consts, props = map (prop_of_isa ctxt) props};

fun nun_problem_of_isa ctxt {commandss, sound, complete} =
  let
    fun cmd_of cmd =
      (case cmd of
        ITVal (T, cards) => NTVal (ty_of_isa T, cards)
      | ITypedef spec => NCopy (nun_copy_spec_of_isa_typedef ctxt spec)
      | IQuotient spec => NCopy (nun_copy_spec_of_isa_quotient ctxt spec)
      | ICoData (fp, specs) =>
        BNF_Util.case_fp fp NData NCodata (map (nun_co_data_spec_of_isa ctxt) specs)
      | IVal t => NVal (tm_of_isa ctxt t, ty_of_isa (fastype_of t))
      | ICoPred (fp, wf, specs) =>
        (if wf then curry NPred true
         else if fp = BNF_Util.Least_FP then curry NPred false
         else NCopred) (map (nun_const_spec_of_isa ctxt) specs)
      | IRec specs => NRec (map (nun_rec_spec_of_isa ctxt) specs)
      | ISpec spec => NSpec (nun_consts_spec_of_isa ctxt spec)
      | IAxiom prop => NAxiom (prop_of_isa ctxt prop)
      | IGoal prop => NGoal (prop_of_isa ctxt prop)
      | IEval t => NEval (tm_of_isa ctxt t));
  in
    {commandss = map (map cmd_of) commandss, sound = sound, complete = complete}
  end;

end;