src/Pure/primitive_defs.ML
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 24259 c9e05c49d02c
child 24981 4ec3f95190bf
permissions -rw-r--r--
Name.uu, Name.aT;
     1 (*  Title:      Pure/primitive_defs.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Primitive definition forms.
     6 *)
     7 
     8 signature PRIMITIVE_DEFS =
     9 sig
    10   val dest_def: Pretty.pp -> (term -> bool) -> (string -> bool) -> (string -> bool) ->
    11     term -> (term * term) * term
    12   val abs_def: term -> term * term
    13   val mk_defpair: term * term -> string * term
    14 end;
    15 
    16 structure PrimitiveDefs: PRIMITIVE_DEFS =
    17 struct
    18 
    19 fun term_kind (Const _) = "existing constant "
    20   | term_kind (Free _) = "free variable "
    21   | term_kind (Bound _) = "bound variable "
    22   | term_kind _ = "";
    23 
    24 (*c x == t[x] to !!x. c x == t[x]*)
    25 fun dest_def pp check_head is_fixed is_fixedT eq =
    26   let
    27     fun err msg = raise TERM (msg, [eq]);
    28     val eq_vars = Term.strip_all_vars eq;
    29     val eq_body = Term.strip_all_body eq;
    30 
    31     val display_terms =
    32       commas_quote o map (Pretty.string_of_term pp o Syntax.bound_vars eq_vars);
    33     val display_types = commas_quote o map (Pretty.string_of_typ pp);
    34 
    35     val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (==)";
    36     val lhs = Envir.beta_eta_contract raw_lhs;
    37     val (head, args) = Term.strip_comb lhs;
    38     val head_tfrees = Term.add_tfrees head [];
    39 
    40     fun check_arg (Bound _) = true
    41       | check_arg (Free (x, _)) = not (is_fixed x)
    42       | check_arg (Const ("TYPE", Type ("itself", [TFree _]))) = true
    43       | check_arg _ = false;
    44     fun close_arg (Bound _) t = t
    45       | close_arg x t = Term.all (Term.fastype_of x) $ lambda x t;
    46 
    47     val lhs_bads = filter_out check_arg args;
    48     val lhs_dups = duplicates (op aconv) args;
    49     val rhs_extras = Term.fold_aterms (fn v as Free (x, _) =>
    50       if is_fixed x orelse member (op aconv) args v then I
    51       else insert (op aconv) v | _ => I) rhs [];
    52     val rhs_extrasT = Term.fold_aterms (Term.fold_types (fn v as TFree (a, S) =>
    53       if is_fixedT a orelse member (op =) head_tfrees (a, S) then I
    54       else insert (op =) v | _ => I)) rhs [];
    55   in
    56     if not (check_head head) then
    57       err ("Bad head of lhs: " ^ term_kind head ^ display_terms [head])
    58     else if not (null lhs_bads) then
    59       err ("Bad arguments on lhs: " ^ display_terms lhs_bads)
    60     else if not (null lhs_dups) then
    61       err ("Duplicate arguments on lhs: " ^ display_terms lhs_dups)
    62     else if not (null rhs_extras) then
    63       err ("Extra variables on rhs: " ^ display_terms rhs_extras)
    64     else if not (null rhs_extrasT) then
    65       err ("Extra type variables on rhs: " ^ display_types rhs_extrasT)
    66     else if exists_subterm (fn t => t aconv head) rhs then
    67       err "Entity to be defined occurs on rhs"
    68     else
    69       ((lhs, rhs), fold_rev close_arg args (Term.list_all (eq_vars, (Logic.mk_equals (lhs, rhs)))))
    70   end;
    71 
    72 (*!!x. c x == t[x] to c == %x. t[x]*)
    73 fun abs_def eq =
    74   let
    75     val body = Term.strip_all_body eq;
    76     val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq));
    77     val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (vars, body));
    78     val (lhs', args) = Term.strip_comb lhs;
    79     val rhs' = Term.list_abs_free (map Term.dest_Free args, rhs);
    80   in (lhs', rhs') end;
    81 
    82 fun mk_defpair (lhs, rhs) =
    83   (case Term.head_of lhs of
    84     Const (name, _) =>
    85       (NameSpace.base name ^ "_def", Logic.mk_equals (lhs, rhs))
    86   | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
    87 
    88 end;