src/Pure/Isar/code_unit.ML

removed redundant strip_vars/abs_eqn, use improved Drule.abs_def instead;
renamed cert_instantiations to check_instantiations, check input only once (simultaneously!);

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

Basic notions of code generation.  Auxiliary.
*)

signature CODE_UNIT =
sig
  (*generic non-sense*)
  val bad_thm: string -> 'a
  val error_thm: (thm -> thm) -> thm -> thm
  val warning_thm: (thm -> thm) -> thm -> thm option
  val try_thm: (thm -> thm) -> thm -> thm option

  (*typ instantiations*)
  val typ_sort_inst: Sorts.algebra -> typ * sort
    -> sort Vartab.table -> sort Vartab.table
  val inst_thm: sort Vartab.table -> thm -> thm

  (*constants*)
  val string_of_typ: theory -> typ -> string
  val string_of_const: theory -> string -> string
  val no_args: theory -> string -> int
  val read_bare_const: theory -> string -> string * typ
  val read_const: theory -> string -> string
  val read_const_exprs: theory -> (string list -> string list)
    -> string list -> bool * string list

  (*constructor sets*)
  val constrset_of_consts: theory -> (string * typ) list
    -> string * ((string * sort) list * (string * typ list) list)

  (*defining equations*)
  val assert_rew: thm -> thm
  val mk_rew: thm -> thm
  val mk_func: thm -> thm
  val head_func: thm -> string * typ
  val expand_eta: int -> thm -> thm
  val rewrite_func: thm list -> thm -> thm
  val norm_args: thm list -> thm list 
  val norm_varnames: (string -> string) -> (string -> string) -> thm list -> thm list

  (*case certificates*)
  val case_cert: thm -> string * (int * string list)
end;

structure CodeUnit: CODE_UNIT =
struct


(* auxiliary *)

exception BAD_THM of string;
fun bad_thm msg = raise BAD_THM msg;
fun error_thm f thm = f thm handle BAD_THM msg => error msg;
fun warning_thm f thm = SOME (f thm) handle BAD_THM msg
  => (warning ("code generator: " ^ msg); NONE);
fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE;

fun string_of_typ thy = setmp show_sorts true (Sign.string_of_typ thy);
fun string_of_const thy c = case Class.param_const thy c
 of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco)
  | NONE => Sign.extern_const thy c;

fun no_args thy = length o fst o strip_type o Sign.the_const_type thy;

(* reading constants as terms and wildcards pattern *)

fun read_bare_const thy raw_t =
  let
    val t = Syntax.read_term_global 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 = Class.unoverload_const 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 belongs_here thyname c =
          not (exists (fn thy' => Sign.declared_const thy' c) (Theory.parents_of this_thy))
  in case some_thyname
   of NONE => cs
    | SOME thyname => filter (belongs_here thyname) cs
  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 exprs =
  case (pairself flat o split_list o map (read_const_expr thy)) exprs
   of (consts, []) => (false, consts)
    | (consts, consts') => (true, consts @ select consts');

end; (*local*)


(* constructor sets *)

fun constrset_of_consts thy cs =
  let
    fun no_constr (c, ty) = error ("Not a datatype constructor: " ^ string_of_const thy c
      ^ " :: " ^ string_of_typ thy ty);
    fun last_typ c_ty ty =
      let
        val frees = typ_tfrees ty;
        val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) ty
          handle TYPE _ => no_constr c_ty
        val _ = if has_duplicates (eq_fst (op =)) vs then no_constr c_ty else ();
        val _ = if length frees <> length vs then no_constr c_ty else ();
      in (tyco, vs) end;
    fun ty_sorts (c, ty) =
      let
        val ty_decl = (Logic.unvarifyT o Sign.the_const_type thy) c;
        val (tyco, vs_decl) = last_typ (c, ty) ty_decl;
        val (_, vs) = last_typ (c, ty) ty;
      in ((tyco, map snd vs), (c, (map fst vs, ty_decl))) end;
    fun add ((tyco', sorts'), c) ((tyco, sorts), cs) =
      let
        val _ = if tyco' <> tyco
          then error "Different type constructors in constructor set"
          else ();
        val sorts'' = map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts
      in ((tyco, sorts), c :: cs) end;
    fun inst vs' (c, (vs, ty)) =
      let
        val the_v = the o AList.lookup (op =) (vs ~~ vs');
        val ty' = map_atyps (fn TFree (v, _) => TFree (the_v v)) ty;
      in (c, (fst o strip_type) ty') end;
    val c' :: cs' = map ty_sorts cs;
    val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
    val vs = Name.names Name.context Name.aT sorts;
    val cs''' = map (inst vs) cs'';
  in (tyco, (vs, cs''')) end;


(* dictionary values *)

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;


(* making rewrite theorems *)

fun assert_rew thm =
  let
    val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
      handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm)
          | THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm);
    fun vars_of t = fold_aterms
     (fn Var (v, _) => insert (op =) v
       | Free _ => bad_thm ("Illegal free variable in rewrite theorem\n"
           ^ Display.string_of_thm thm)
       | _ => I) t [];
    fun tvars_of t = fold_term_types
     (fn _ => fold_atyps (fn TVar (v, _) => insert (op =) v
                          | TFree _ => bad_thm 
      ("Illegal free type variable in rewrite theorem\n" ^ Display.string_of_thm thm))) t [];
    val lhs_vs = vars_of lhs;
    val rhs_vs = vars_of rhs;
    val lhs_tvs = tvars_of lhs;
    val rhs_tvs = tvars_of lhs;
    val _ = if null (subtract (op =) lhs_vs rhs_vs)
      then ()
      else bad_thm ("Free variables on right hand side of rewrite theorem\n"
        ^ Display.string_of_thm thm);
    val _ = if null (subtract (op =) lhs_tvs rhs_tvs)
      then ()
      else bad_thm ("Free type variables on right hand side of rewrite theorem\n"
        ^ Display.string_of_thm thm)
  in thm end;

fun mk_rew thm =
  let
    val thy = Thm.theory_of_thm thm;
    val ctxt = ProofContext.init thy;
  in
    thm
    |> LocalDefs.meta_rewrite_rule ctxt
    |> assert_rew
  end;


(* making defining equations *)

fun assert_func thm =
  let
    val thy = Thm.theory_of_thm thm;
    val (head, args) = (strip_comb o fst o Logic.dest_equals
      o ObjectLogic.drop_judgment thy o Thm.plain_prop_of) thm;
    val _ = case head of Const _ => () | _ =>
      bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm thm);
    val _ =
      if has_duplicates (op =)
        ((fold o fold_aterms) (fn Var (v, _) => cons v
          | _ => I
        ) args [])
      then bad_thm ("Duplicated variables on left hand side of equation\n"
        ^ Display.string_of_thm thm)
      else ()
    fun check _ (Abs _) = bad_thm
          ("Abstraction on left hand side of equation\n"
            ^ Display.string_of_thm thm)
      | check 0 (Var _) = ()
      | check _ (Var _) = bad_thm
          ("Variable with application on left hand side of defining equation\n"
            ^ Display.string_of_thm thm)
      | check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
      | check n (Const (_, ty)) = if n <> (length o fst o strip_type) ty
          then bad_thm
            ("Partially applied constant on left hand side of equation\n"
               ^ Display.string_of_thm thm)
          else ();
    val _ = map (check 0) args;
  in thm end;

val mk_func = assert_func o mk_rew;

fun head_func thm =
  let
    val thy = Thm.theory_of_thm thm;
    val Const (c, ty) = (fst o strip_comb o fst o Logic.dest_equals
      o ObjectLogic.drop_judgment thy o Thm.plain_prop_of) thm;
  in (c, ty) end;


(* utilities *)

fun inst_thm tvars' thm =
  let
    val thy = Thm.theory_of_thm thm;
    val tvars = (Term.add_tvars o Thm.prop_of) thm [];
    fun mk_inst (tvar as (v, _)) = case Vartab.lookup tvars' v
     of SOME sort => SOME (pairself (Thm.ctyp_of thy o TVar) (tvar, (v, sort)))
      | NONE => NONE;
    val insts = map_filter mk_inst tvars;
  in Thm.instantiate (insts, []) thm end;

fun expand_eta k thm =
  let
    val thy = Thm.theory_of_thm thm;
    val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm;
    val (head, args) = strip_comb lhs;
    val l = if k = ~1
      then (length o fst o strip_abs) rhs
      else Int.max (0, k - length args);
    val used = Name.make_context (map (fst o fst) (Term.add_vars lhs []));
    fun get_name _ 0 used = ([], used)
      | get_name (Abs (v, ty, t)) k used =
          used
          |> Name.variants [v]
          ||>> get_name t (k - 1)
          |>> (fn ([v'], vs') => (v', ty) :: vs')
      | get_name t k used = 
          let
            val (tys, _) = (strip_type o fastype_of) t
          in case tys
           of [] => raise TERM ("expand_eta", [t])
            | ty :: _ =>
                used
                |> Name.variants [""]
                |-> (fn [v] => get_name (t $ Var ((v, 0), ty)) (k - 1)
                #>> (fn vs' => (v, ty) :: vs'))
          end;
    val (vs, _) = get_name rhs l used;
    val vs_refl = map (fn (v, ty) => Thm.reflexive (Thm.cterm_of thy (Var ((v, 0), ty)))) vs;
  in
    thm
    |> fold (fn refl => fn thm => Thm.combination thm refl) vs_refl
    |> Conv.fconv_rule Drule.beta_eta_conversion
  end;

fun rewrite_func rewrites thm =
  let
    val rewrite = MetaSimplifier.rewrite false rewrites;
    val (ct_eq, [ct_lhs, ct_rhs]) = (Drule.strip_comb o Thm.cprop_of) thm;
    val Const ("==", _) = Thm.term_of ct_eq;
    val (ct_f, ct_args) = Drule.strip_comb ct_lhs;
    val rhs' = rewrite ct_rhs;
    val args' = map rewrite ct_args;
    val lhs' = Thm.symmetric (fold (fn th1 => fn th2 => Thm.combination th2 th1)
      args' (Thm.reflexive ct_f));
  in Thm.transitive (Thm.transitive lhs' thm) rhs' end;

fun norm_args thms =
  let
    val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals;
    val k = fold (curry Int.max o num_args_of o Thm.plain_prop_of) thms 0;
  in
    thms
    |> map (expand_eta k)
    |> map (Conv.fconv_rule Drule.beta_eta_conversion)
  end;

fun canonical_tvars purify_tvar thm =
  let
    val ctyp = Thm.ctyp_of (Thm.theory_of_thm thm);
    fun tvars_subst_for thm = (fold_types o fold_atyps)
      (fn TVar (v_i as (v, _), sort) => let
            val v' = purify_tvar v
          in if v = v' then I
          else insert (op =) (v_i, (v', sort)) end
        | _ => I) (prop_of thm) [];
    fun mk_inst (v_i, (v', sort)) (maxidx, acc) =
      let
        val ty = TVar (v_i, sort)
      in
        (maxidx + 1, (ctyp ty, ctyp (TVar ((v', maxidx), sort))) :: acc)
      end;
    val maxidx = Thm.maxidx_of thm + 1;
    val (_, inst) = fold mk_inst (tvars_subst_for thm) (maxidx + 1, []);
  in Thm.instantiate (inst, []) thm end;

fun canonical_vars purify_var thm =
  let
    val cterm = Thm.cterm_of (Thm.theory_of_thm thm);
    fun vars_subst_for thm = fold_aterms
      (fn Var (v_i as (v, _), ty) => let
            val v' = purify_var v
          in if v = v' then I
          else insert (op =) (v_i, (v', ty)) end
        | _ => I) (prop_of thm) [];
    fun mk_inst (v_i as (v, i), (v', ty)) (maxidx, acc) =
      let
        val t = Var (v_i, ty)
      in
        (maxidx + 1, (cterm t, cterm (Var ((v', maxidx), ty))) :: acc)
      end;
    val maxidx = Thm.maxidx_of thm + 1;
    val (_, inst) = fold mk_inst (vars_subst_for thm) (maxidx + 1, []);
  in Thm.instantiate ([], inst) thm end;

fun canonical_absvars purify_var thm =
  let
    val t = Thm.plain_prop_of thm;
    val t' = Term.map_abs_vars purify_var t;
  in Thm.rename_boundvars t t' thm end;

fun norm_varnames purify_tvar purify_var thms =
  let
    fun burrow_thms f [] = []
      | burrow_thms f thms =
          thms
          |> Conjunction.intr_balanced
          |> f
          |> Conjunction.elim_balanced (length thms)
  in
    thms
    |> burrow_thms (canonical_tvars purify_tvar)
    |> map (canonical_vars purify_var)
    |> map (canonical_absvars purify_var)
    |> map Drule.zero_var_indexes
  end;


(* case cerificates *)

fun case_certificate thm =
  let
    val thy = Thm.theory_of_thm thm;
    val ((head, raw_case_expr), cases) = (apfst Logic.dest_equals
      o apsnd Logic.dest_conjunctions o Logic.dest_implies o Thm.prop_of) thm;
    val _ = case head of Free _ => true
      | Var _ => true
      | _ => raise TERM ("case_cert", []);
    val ([(case_var, _)], case_expr) = Term.strip_abs_eta 1 raw_case_expr;
    val (Const (case_const, _), raw_params) = strip_comb case_expr;
    val n = find_index (fn Free (v, _) => v = case_var | _ => false) raw_params;
    val _ = if n = ~1 then raise TERM ("case_cert", []) else ();
    val params = map (fst o dest_Var) (nth_drop n raw_params);
    fun dest_case t =
      let
        val (head' $ t_co, rhs) = Logic.dest_equals t;
        val _ = if head' = head then () else raise TERM ("case_cert", []);
        val (Const (co, _), args) = strip_comb t_co;
        val (Var (param, _), args') = strip_comb rhs;
        val _ = if args' = args then () else raise TERM ("case_cert", []);
      in (param, co) end;
    fun analyze_cases cases =
      let
        val co_list = fold (AList.update (op =) o dest_case) cases [];
      in map (the o AList.lookup (op =) co_list) params end;
    fun analyze_let t =
      let
        val (head' $ arg, Var (param', _) $ arg') = Logic.dest_equals t;
        val _ = if head' = head then () else raise TERM ("case_cert", []);
        val _ = if arg' = arg then () else raise TERM ("case_cert", []);
        val _ = if [param'] = params then () else raise TERM ("case_cert", []);
      in [] end;
    fun analyze (cases as [let_case]) =
          (analyze_cases cases handle Bind => analyze_let let_case)
      | analyze cases = analyze_cases cases;
  in (case_const, (n, analyze cases)) end;

fun case_cert thm = case_certificate thm
  handle Bind => error "bad case certificate"
      | TERM _ => error "bad case certificate";

end;