Primitive definition forms.
1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Pure/primitive_defs.ML Tue Aug 14 13:20:17 2007 +0200
1.3 @@ -0,0 +1,88 @@
1.4 +(* Title: Pure/primitive_defs.ML
1.5 + ID: $Id$
1.6 + Author: Makarius
1.7 +
1.8 +Primitive definition forms.
1.9 +*)
1.10 +
1.11 +signature PRIMITIVE_DEFS =
1.12 +sig
1.13 + val dest_def: Pretty.pp -> (term -> bool) -> (string -> bool) -> (string -> bool) ->
1.14 + term -> (term * term) * term
1.15 + val abs_def: term -> term * term
1.16 + val mk_defpair: term * term -> string * term
1.17 +end;
1.18 +
1.19 +structure PrimitiveDefs: PRIMITIVE_DEFS =
1.20 +struct
1.21 +
1.22 +fun term_kind (Const _) = "existing constant "
1.23 + | term_kind (Free _) = "free variable "
1.24 + | term_kind (Bound _) = "bound variable "
1.25 + | term_kind _ = "";
1.26 +
1.27 +(*c x == t[x] to !!x. c x == t[x]*)
1.28 +fun dest_def pp check_head is_fixed is_fixedT eq =
1.29 + let
1.30 + fun err msg = raise TERM (msg, [eq]);
1.31 + val eq_vars = Term.strip_all_vars eq;
1.32 + val eq_body = Term.strip_all_body eq;
1.33 +
1.34 + val display_terms =
1.35 + commas_quote o map (Pretty.string_of_term pp o Syntax.bound_vars eq_vars);
1.36 + val display_types = commas_quote o map (Pretty.string_of_typ pp);
1.37 +
1.38 + val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (==)";
1.39 + val lhs = Envir.beta_eta_contract raw_lhs;
1.40 + val (head, args) = Term.strip_comb lhs;
1.41 + val head_tfrees = Term.add_tfrees head [];
1.42 +
1.43 + fun check_arg (Bound _) = true
1.44 + | check_arg (Free (x, _)) = not (is_fixed x)
1.45 + | check_arg (Const ("TYPE", Type ("itself", [TFree _]))) = true
1.46 + | check_arg _ = false;
1.47 + fun close_arg (Bound _) t = t
1.48 + | close_arg x t = Term.all (Term.fastype_of x) $ lambda x t;
1.49 +
1.50 + val lhs_bads = filter_out check_arg args;
1.51 + val lhs_dups = duplicates (op aconv) args;
1.52 + val rhs_extras = Term.fold_aterms (fn v as Free (x, _) =>
1.53 + if is_fixed x orelse member (op aconv) args v then I
1.54 + else insert (op aconv) v | _ => I) rhs [];
1.55 + val rhs_extrasT = Term.fold_aterms (Term.fold_types (fn v as TFree (a, S) =>
1.56 + if is_fixedT a orelse member (op =) head_tfrees (a, S) then I
1.57 + else insert (op =) v | _ => I)) rhs [];
1.58 + in
1.59 + if not (check_head head) then
1.60 + err ("Bad head of lhs: " ^ term_kind head ^ display_terms [head])
1.61 + else if not (null lhs_bads) then
1.62 + err ("Bad arguments on lhs: " ^ display_terms lhs_bads)
1.63 + else if not (null lhs_dups) then
1.64 + err ("Duplicate arguments on lhs: " ^ display_terms lhs_dups)
1.65 + else if not (null rhs_extras) then
1.66 + err ("Extra variables on rhs: " ^ display_terms rhs_extras)
1.67 + else if not (null rhs_extrasT) then
1.68 + err ("Extra type variables on rhs: " ^ display_types rhs_extrasT)
1.69 + else if exists_subterm (fn t => t aconv head) rhs then
1.70 + err "Entity to be defined occurs on rhs"
1.71 + else
1.72 + ((lhs, rhs), fold_rev close_arg args (Term.list_all (eq_vars, (Logic.mk_equals (lhs, rhs)))))
1.73 + end;
1.74 +
1.75 +(*!!x. c x == t[x] to c == %x. t[x]*)
1.76 +fun abs_def eq =
1.77 + let
1.78 + val body = Term.strip_all_body eq;
1.79 + val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq));
1.80 + val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (vars, body));
1.81 + val (lhs', args) = Term.strip_comb lhs;
1.82 + val rhs' = Term.list_abs_free (map Term.dest_Free args, rhs);
1.83 + in (lhs', rhs') end;
1.84 +
1.85 +fun mk_defpair (lhs, rhs) =
1.86 + (case Term.head_of lhs of
1.87 + Const (name, _) =>
1.88 + (NameSpace.base name ^ "_def", Logic.mk_equals (lhs, rhs))
1.89 + | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
1.90 +
1.91 +end;