(* Title: Pure/Isar/code_unit.ML
ID: $Id$
Author: Florian Haftmann, TU Muenchen
Basic units of code generation. Auxiliary.
*)
signature CODE_UNIT =
sig
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
val constrset_of_consts: theory -> (string * typ) list
-> string * ((string * sort) list * (string * typ list) list)
val typ_sort_inst: Sorts.algebra -> typ * sort
-> sort Vartab.table -> sort Vartab.table
val assert_rew: thm -> thm
val mk_rew: thm -> thm
val mk_func: thm -> thm
val head_func: thm -> string * typ
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
val inst_thm: sort Vartab.table -> thm -> thm
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
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 "'a" 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;
end;