src/Pure/primitive_defs.ML
author paulson <lp15@cam.ac.uk>
Sun, 20 May 2018 18:37:34 +0100
changeset 68239 0764ee22a4d1
parent 67721 5348bea4accd
child 74230 d637611b41bd
permissions -rw-r--r--
tidy up of Derivative
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24259
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/primitive_defs.ML
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
     3
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
     4
Primitive definition forms.
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
     5
*)
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
     6
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
     7
signature PRIMITIVE_DEFS =
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
     8
sig
63042
741263be960e more rigid check of lhs;
wenzelm
parents: 63038
diff changeset
     9
  val dest_def: Proof.context ->
741263be960e more rigid check of lhs;
wenzelm
parents: 63038
diff changeset
    10
    {check_head: term -> bool,
741263be960e more rigid check of lhs;
wenzelm
parents: 63038
diff changeset
    11
     check_free_lhs: string -> bool,
741263be960e more rigid check of lhs;
wenzelm
parents: 63038
diff changeset
    12
     check_free_rhs: string -> bool,
741263be960e more rigid check of lhs;
wenzelm
parents: 63038
diff changeset
    13
     check_tfree: string -> bool} ->
63395
734723445a8c PIDE reports of implicit variable scope;
wenzelm
parents: 63042
diff changeset
    14
    term -> (term * term) * term list * term
24259
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    15
  val abs_def: term -> term * term
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    16
end;
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    17
33385
fb2358edcfb6 modernized structure Primitive_Defs;
wenzelm
parents: 30364
diff changeset
    18
structure Primitive_Defs: PRIMITIVE_DEFS =
24259
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    19
struct
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    20
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    21
fun term_kind (Const _) = "existing constant "
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    22
  | term_kind (Free _) = "free variable "
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    23
  | term_kind (Bound _) = "bound variable "
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    24
  | term_kind _ = "";
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    25
67721
5348bea4accd eliminated ASCII syntax from Pure bootstrap;
wenzelm
parents: 64596
diff changeset
    26
(*c x \<equiv> t[x] to \<And>x. c x \<equiv> t[x]*)
63042
741263be960e more rigid check of lhs;
wenzelm
parents: 63038
diff changeset
    27
fun dest_def ctxt {check_head, check_free_lhs, check_free_rhs, check_tfree} eq =
24259
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    28
  let
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    29
    fun err msg = raise TERM (msg, [eq]);
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    30
    val eq_vars = Term.strip_all_vars eq;
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    31
    val eq_body = Term.strip_all_body eq;
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    32
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    33
    val display_terms =
42284
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 35989
diff changeset
    34
      commas_quote o map (Syntax.string_of_term ctxt o Syntax_Trans.bound_vars eq_vars);
24981
4ec3f95190bf dest/cert_def: replaced Pretty.pp by explicit Proof.context;
wenzelm
parents: 24259
diff changeset
    35
    val display_types = commas_quote o map (Syntax.string_of_typ ctxt);
24259
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    36
64596
51f8e259de50 tuned messages -- more symbols;
wenzelm
parents: 63395
diff changeset
    37
    val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (\<equiv>)";
24259
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    38
    val lhs = Envir.beta_eta_contract raw_lhs;
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    39
    val (head, args) = Term.strip_comb lhs;
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    40
    val head_tfrees = Term.add_tfrees head [];
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    41
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    42
    fun check_arg (Bound _) = true
63042
741263be960e more rigid check of lhs;
wenzelm
parents: 63038
diff changeset
    43
      | check_arg (Free (x, _)) = check_free_lhs x
56243
2e10a36b8d46 more qualified names;
wenzelm
parents: 46218
diff changeset
    44
      | check_arg (Const ("Pure.type", Type ("itself", [TFree _]))) = true
24259
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    45
      | check_arg _ = false;
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    46
    fun close_arg (Bound _) t = t
46214
wenzelm
parents: 44241
diff changeset
    47
      | close_arg x t = Logic.all x t;
24259
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    48
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    49
    val lhs_bads = filter_out check_arg args;
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    50
    val lhs_dups = duplicates (op aconv) args;
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    51
    val rhs_extras = Term.fold_aterms (fn v as Free (x, _) =>
63042
741263be960e more rigid check of lhs;
wenzelm
parents: 63038
diff changeset
    52
      if check_free_rhs x orelse member (op aconv) args v then I
24259
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    53
      else insert (op aconv) v | _ => I) rhs [];
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    54
    val rhs_extrasT = Term.fold_aterms (Term.fold_types (fn v as TFree (a, S) =>
63042
741263be960e more rigid check of lhs;
wenzelm
parents: 63038
diff changeset
    55
      if check_tfree a orelse member (op =) head_tfrees (a, S) then I
24259
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    56
      else insert (op =) v | _ => I)) rhs [];
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    57
  in
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    58
    if not (check_head head) then
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    59
      err ("Bad head of lhs: " ^ term_kind head ^ display_terms [head])
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    60
    else if not (null lhs_bads) then
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    61
      err ("Bad arguments on lhs: " ^ display_terms lhs_bads)
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    62
    else if not (null lhs_dups) then
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    63
      err ("Duplicate arguments on lhs: " ^ display_terms lhs_dups)
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    64
    else if not (null rhs_extras) then
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    65
      err ("Extra variables on rhs: " ^ display_terms rhs_extras)
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    66
    else if not (null rhs_extrasT) then
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    67
      err ("Extra type variables on rhs: " ^ display_types rhs_extrasT)
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    68
    else if exists_subterm (fn t => t aconv head) rhs then
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    69
      err "Entity to be defined occurs on rhs"
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    70
    else
63395
734723445a8c PIDE reports of implicit variable scope;
wenzelm
parents: 63042
diff changeset
    71
      ((lhs, rhs), args,
734723445a8c PIDE reports of implicit variable scope;
wenzelm
parents: 63042
diff changeset
    72
        fold_rev close_arg args (Logic.list_all (eq_vars, (Logic.mk_equals (lhs, rhs)))))
24259
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    73
  end;
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    74
67721
5348bea4accd eliminated ASCII syntax from Pure bootstrap;
wenzelm
parents: 64596
diff changeset
    75
(*\<And>x. c x \<equiv> t[x] to c \<equiv> \<lambda>x. t[x]*)
24259
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    76
fun abs_def eq =
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    77
  let
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    78
    val body = Term.strip_all_body eq;
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    79
    val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq));
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    80
    val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (vars, body));
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    81
    val (lhs', args) = Term.strip_comb lhs;
44241
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 42284
diff changeset
    82
    val rhs' = fold_rev (absfree o dest_Free) args rhs;
24259
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    83
  in (lhs', rhs') end;
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    84
c9e05c49d02c Primitive definition forms.
wenzelm
parents:
diff changeset
    85
end;