src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML

algebraic foundation for congruences

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

Reconstruction of Nunchaku models in Isabelle/HOL.
*)

signature NUNCHAKU_RECONSTRUCT =
sig
  type nun_model = Nunchaku_Model.nun_model

  type typ_entry = typ * term list
  type term_entry = term * term

  type isa_model =
    {type_model: typ_entry list,
     free_model: term_entry list,
     pat_complete_model: term_entry list,
     pat_incomplete_model: term_entry list,
     skolem_model: term_entry list,
     auxiliary_model: term_entry list}

  val str_of_isa_model: Proof.context -> isa_model -> string

  val isa_model_of_nun: Proof.context -> term list -> (typ option * string list) list ->
    nun_model -> isa_model
  val clean_up_isa_model: Proof.context -> isa_model -> isa_model
end;

structure Nunchaku_Reconstruct : NUNCHAKU_RECONSTRUCT =
struct

open Nunchaku_Util;
open Nunchaku_Problem;
open Nunchaku_Translate;
open Nunchaku_Model;

type typ_entry = typ * term list;
type term_entry = term * term;

type isa_model =
  {type_model: typ_entry list,
   free_model: term_entry list,
   pat_complete_model: term_entry list,
   pat_incomplete_model: term_entry list,
   skolem_model: term_entry list,
   auxiliary_model: term_entry list};

val anonymousN = "anonymous";
val irrelevantN = "irrelevant";
val unparsableN = "unparsable";

val nun_arrow_exploded = String.explode nun_arrow;

val is_ty_meta = member (op =) (String.explode "()->,");

fun next_token_lowlevel [] = (End_of_Stream, [])
  | next_token_lowlevel (c :: cs) =
    if Char.isSpace c then
      next_token_lowlevel cs
    else if not (is_ty_meta c) then
      let val n = find_index (Char.isSpace orf is_ty_meta) cs in
        (if n = ~1 then (cs, []) else chop n cs)
        |>> (cons c #> String.implode #> ident_of_str #> Ident)
      end
    else if is_prefix (op =) nun_arrow_exploded (c :: cs) then
      (Ident nun_arrow, tl cs)
    else
      (Symbol (String.str c), cs);

val tokenize_lowlevel =
  let
    fun toks cs =
      (case next_token_lowlevel cs of
        (End_of_Stream, []) => []
      | (tok, cs') => tok :: toks cs');
  in
    toks o String.explode
  end;

fun parse_lowlevel_ty tok =
  (Scan.optional
     (parse_sym "(" |-- Scan.repeat (parse_lowlevel_ty --| Scan.option (parse_sym ",")) --|
      parse_sym ")")
     []
   -- parse_ident >> (swap #> NType)) tok;

val ty_of_lowlevel_str = fst o parse_lowlevel_ty o tokenize_lowlevel;

fun ident_of_const (NConst (id, _, _)) = id
  | ident_of_const _ = nun_dummy;

fun str_of_typ_entry ctxt (T, ts) =
  "type " ^ Syntax.string_of_typ ctxt T  ^
  " := {" ^ commas (map (Syntax.string_of_term ctxt) ts) ^ "}.";

fun str_of_term_entry ctxt (tm, value) =
  "val " ^ Syntax.string_of_term ctxt tm ^ " := " ^ Syntax.string_of_term ctxt value ^ ".";

fun str_of_isa_model ctxt
    {type_model, free_model, pat_complete_model, pat_incomplete_model, skolem_model,
     auxiliary_model} =
  map (str_of_typ_entry ctxt) type_model @ "" ::
  map (str_of_term_entry ctxt) free_model @ "" ::
  map (str_of_term_entry ctxt) pat_complete_model @ "" ::
  map (str_of_term_entry ctxt) pat_incomplete_model @ "" ::
  map (str_of_term_entry ctxt) skolem_model @ "" ::
  map (str_of_term_entry ctxt) auxiliary_model
  |> cat_lines;

fun typ_of_nun ctxt =
  let
    fun typ_of (NType (id, tys)) =
      let val Ts = map typ_of tys in
        if id = nun_dummy then
          dummyT
        else if id = nun_prop then
          @{typ bool}
        else if id = nun_arrow then
          Type (@{type_name fun}, Ts)
        else
          (case try str_of_nun_tconst id of
            SOME (args, s) =>
            let val tys' = map ty_of_lowlevel_str args in
              Type (s, map typ_of (tys' @ tys))
            end
          | NONE =>
            (case try str_of_nun_tfree id of
              SOME s => TFree (Proof_Context.check_tfree ctxt (flip_quote s, dummyS))
            | NONE => raise Fail ("unknown type constructor: " ^ quote (str_of_ident id))))
      end;
  in
    typ_of
  end;

fun one_letter_of s =
  let val c = String.sub (Long_Name.base_name s, 0) in
    String.str (if Char.isAlpha c then c else #"x")
  end;

fun base_of_typ (Type (s, _)) = s
  | base_of_typ (TFree (s, _)) = flip_quote s
  | base_of_typ (TVar ((s, _), _)) = flip_quote s;

fun term_of_nun ctxt atomss =
  let
    val thy = Proof_Context.theory_of ctxt;

    val typ_of = typ_of_nun ctxt;

    fun nth_atom T j =
      let val ss = these (triple_lookup (typ_match thy) atomss T) in
        if j >= 0 andalso j < length ss then nth ss j
        else one_letter_of (base_of_typ T) ^ nat_subscript (j + 1)
      end;

    fun term_of _ (NAtom (j, ty)) =
        let val T = typ_of ty in Var ((nth_atom T j, 0), T) end
      | term_of bounds (NConst (id, tys0, ty)) =
        if id = nun_conj then
          HOLogic.conj
        else if id = nun_choice then
          Const (@{const_name Eps}, typ_of ty)
        else if id = nun_disj then
          HOLogic.disj
        else if id = nun_equals then
          Const (@{const_name HOL.eq}, typ_of ty)
        else if id = nun_false then
          @{const False}
        else if id = nun_if then
          Const (@{const_name If}, typ_of ty)
        else if id = nun_implies then
          @{term implies}
        else if id = nun_not then
          HOLogic.Not
        else if id = nun_unique then
          Const (@{const_name The}, typ_of ty)
        else if id = nun_unique_unsafe then
          Const (@{const_name The_unsafe}, typ_of ty)
        else if id = nun_true then
          @{const True}
        else if String.isPrefix nun_dollar_anon_fun_prefix id then
          let val j = Int.fromString (unprefix nun_dollar_anon_fun_prefix id) |> the_default ~1 in
            Var ((anonymousN ^ nat_subscript (j + 1), 0), typ_of ty)
          end
        else if String.isPrefix nun_irrelevant id then
          Var ((irrelevantN ^ nat_subscript (Value.parse_int (unprefix nun_irrelevant id)), 0),
            dummyT)
        else if id = nun_unparsable then
          Var ((unparsableN, 0), typ_of ty)
        else
          (case try str_of_nun_const id of
            SOME (args, s) =>
            let val tys = map ty_of_lowlevel_str args in
              Sign.mk_const thy (s, map typ_of (tys @ tys0))
            end
          | NONE =>
            (case try str_of_nun_free id of
              SOME s => Free (s, typ_of ty)
            | NONE =>
              (case try str_of_nun_var id of
                SOME s => Var ((s, 0), typ_of ty)
              | NONE =>
                (case find_index (fn bound => ident_of_const bound = id) bounds of
                  ~1 => Var ((str_of_ident id, 0), typ_of ty) (* shouldn't happen? *)
                | j => Bound j))))
      | term_of bounds (NAbs (var, body)) =
        let val T = typ_of (safe_ty_of var) in
          Abs (one_letter_of (base_of_typ T), T, term_of (var :: bounds) body)
        end
      | term_of bounds (NApp (func, arg)) =
        let
          fun same () = term_of bounds func $ term_of bounds arg;
        in
          (case (func, arg) of
            (NConst (id, _, _), NAbs _) =>
            if id = nun_mu then
              let val Abs (s, T, body) = term_of bounds arg in
                Const (@{const_name The}, (T --> HOLogic.boolT) --> T)
                $ Abs (s, T, HOLogic.eq_const T $ Bound 0 $ body)
              end
            else
              same ()
          | _ => same ())
        end
      | term_of _ (NMatch _) = raise Fail "unexpected match";

    fun rewrite_numbers (t as @{const Suc} $ _) =
        (case try HOLogic.dest_nat t of
          SOME n => HOLogic.mk_number @{typ nat} n
        | NONE => t)
      | rewrite_numbers (@{const Abs_Integ} $ (@{const Pair (nat, nat)} $ t $ u)) =
        HOLogic.mk_number @{typ int} (HOLogic.dest_nat t - HOLogic.dest_nat u)
      | rewrite_numbers (t $ u) = rewrite_numbers t $ rewrite_numbers u
      | rewrite_numbers (Abs (s, T, t)) = Abs (s, T, rewrite_numbers t)
      | rewrite_numbers t = t;
  in
    term_of []
    #> rewrite_numbers
  end;

fun isa_typ_entry_of_nun ctxt atomss (ty, atoms) =
  (typ_of_nun ctxt ty, map (term_of_nun ctxt atomss) atoms);

fun isa_term_entry_of_nun ctxt atomss (tm, value) =
  (term_of_nun ctxt atomss tm, term_of_nun ctxt atomss value);

fun isa_model_of_nun ctxt pat_completes atomss
    {type_model, const_model, skolem_model, auxiliary_model} =
  let
    val free_and_const_model = map (isa_term_entry_of_nun ctxt atomss) const_model;
    val (free_model, (pat_complete_model, pat_incomplete_model)) =
      List.partition (is_Free o fst) free_and_const_model
      ||> List.partition (member (op aconv) pat_completes o fst);
  in
    {type_model = map (isa_typ_entry_of_nun ctxt atomss) type_model, free_model = free_model,
     pat_complete_model = pat_complete_model, pat_incomplete_model = pat_incomplete_model,
     skolem_model = map (isa_term_entry_of_nun ctxt atomss) skolem_model,
     auxiliary_model = map (isa_term_entry_of_nun ctxt atomss) auxiliary_model}
  end;

fun clean_up_isa_model ctxt {type_model, free_model, pat_complete_model, pat_incomplete_model,
    skolem_model, auxiliary_model} =
  let
    val pat_complete_model' = if Config.get ctxt show_consts then pat_complete_model else [];
    val pat_incomplete_model' = pat_incomplete_model
      |> filter_out (can (fn Const (@{const_name unreachable}, _) => ()) o fst);

    val term_model = free_model @ pat_complete_model' @ pat_incomplete_model' @
      skolem_model @ auxiliary_model;

    (* Incomplete test: Can be led astray by references between the auxiliaries. *)
    fun is_auxiliary_referenced (aux, _) =
      exists (fn (lhs, rhs) =>
          not (lhs aconv aux) andalso exists_subterm (curry (op aconv) aux) rhs)
        term_model;

    val auxiliary_model' = filter is_auxiliary_referenced auxiliary_model;
  in
    {type_model = type_model, free_model = free_model, pat_complete_model = pat_complete_model',
     pat_incomplete_model = pat_incomplete_model', skolem_model = skolem_model,
     auxiliary_model = auxiliary_model'}
  end;

end;