src/Pure/Syntax/syntax_trans.ML
author wenzelm
Sun, 26 May 2013 22:47:00 +0200
changeset 52163 72e83c82c1d4
parent 52144 9065615d0360
child 52177 15fcad6eb956
permissions -rw-r--r--
position constraint for bound dummy -- more PIDE markup;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42284
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42278
diff changeset
     1
(*  Title:      Pure/Syntax/syntax_trans.ML
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
     2
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
12208de7edfe added this file;
wenzelm
parents:
diff changeset
     3
12208de7edfe added this file;
wenzelm
parents:
diff changeset
     4
Syntax translation functions.
12208de7edfe added this file;
wenzelm
parents:
diff changeset
     5
*)
12208de7edfe added this file;
wenzelm
parents:
diff changeset
     6
42284
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42278
diff changeset
     7
signature BASIC_SYNTAX_TRANS =
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42278
diff changeset
     8
sig
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42278
diff changeset
     9
  val eta_contract: bool Config.T
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42278
diff changeset
    10
end
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42278
diff changeset
    11
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42278
diff changeset
    12
signature SYNTAX_TRANS =
2698
8bccb3ab4ca4 added mark_bound(T), variant_abs';
wenzelm
parents: 1511
diff changeset
    13
sig
42284
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42278
diff changeset
    14
  include BASIC_SYNTAX_TRANS
45057
86c9b73158a8 default print mode for Isabelle/Scala, not just Isabelle/jEdit;
wenzelm
parents: 44433
diff changeset
    15
  val bracketsN: string
86c9b73158a8 default print mode for Isabelle/Scala, not just Isabelle/jEdit;
wenzelm
parents: 44433
diff changeset
    16
  val no_bracketsN: string
42284
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42278
diff changeset
    17
  val no_brackets: unit -> bool
45057
86c9b73158a8 default print mode for Isabelle/Scala, not just Isabelle/jEdit;
wenzelm
parents: 44433
diff changeset
    18
  val type_bracketsN: string
86c9b73158a8 default print mode for Isabelle/Scala, not just Isabelle/jEdit;
wenzelm
parents: 44433
diff changeset
    19
  val no_type_bracketsN: string
42284
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42278
diff changeset
    20
  val no_type_brackets: unit -> bool
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42278
diff changeset
    21
  val abs_tr: term list -> term
52143
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
    22
  val mk_binder_tr: string * string -> string * (Proof.context -> term list -> term)
42284
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42278
diff changeset
    23
  val antiquote_tr: string -> term -> term
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42278
diff changeset
    24
  val quote_tr: string -> term -> term
52143
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
    25
  val quote_antiquote_tr: string -> string -> string ->
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
    26
    string * (Proof.context -> term list -> term)
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
    27
  val non_typed_tr': (Proof.context -> term list -> term) ->
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
    28
    Proof.context -> typ -> term list -> term
42284
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42278
diff changeset
    29
  val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42278
diff changeset
    30
  val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42278
diff changeset
    31
  val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
39163
4d701c0388c3 more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
wenzelm
parents: 39128
diff changeset
    32
  val eta_contract_raw: Config.raw
49660
de49d9b4d7bc more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents: 46236
diff changeset
    33
  val mark_bound_abs: string * typ -> term
de49d9b4d7bc more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents: 46236
diff changeset
    34
  val mark_bound_body: string * typ -> term
42284
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42278
diff changeset
    35
  val bound_vars: (string * typ) list -> term -> term
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42278
diff changeset
    36
  val abs_tr': Proof.context -> term -> term
13762
9dd78dab72bc *** empty log message ***
nipkow
parents: 12785
diff changeset
    37
  val atomic_abs_tr': string * typ * term -> term * term
42086
74bf78db0d87 added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
wenzelm
parents: 42085
diff changeset
    38
  val const_abs_tr': term -> term
52143
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
    39
  val mk_binder_tr': string * string -> string * (Proof.context -> term list -> term)
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
    40
  val preserve_binder_abs_tr': string -> string -> string * (Proof.context -> term list -> term)
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
    41
  val preserve_binder_abs2_tr': string -> string -> string * (Proof.context -> term list -> term)
42284
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42278
diff changeset
    42
  val prop_tr': term -> term
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42278
diff changeset
    43
  val variant_abs: string * typ * term -> string * term
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42278
diff changeset
    44
  val variant_abs': string * typ * term -> string * term
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
    45
  val dependent_tr': string * string -> term list -> term
8577
4a3cdf01531b improved (anti)quote_tr(');
wenzelm
parents: 8575
diff changeset
    46
  val antiquote_tr': string -> term -> term
4a3cdf01531b improved (anti)quote_tr(');
wenzelm
parents: 8575
diff changeset
    47
  val quote_tr': string -> term -> term
52143
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
    48
  val quote_antiquote_tr': string -> string -> string ->
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
    49
    string * (Proof.context -> term list -> term)
35145
f132a4fd8679 moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents: 32786
diff changeset
    50
  val update_name_tr': term -> term
52143
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
    51
  val pure_parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
    52
  val pure_parse_translation: (string * (Proof.context -> term list -> term)) list
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
    53
  val pure_print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
52144
wenzelm
parents: 52143
diff changeset
    54
  val struct_tr: string list -> string * (Proof.context -> term list -> term)
wenzelm
parents: 52143
diff changeset
    55
  val struct_ast_tr': string list -> string * (Proof.context -> Ast.ast list -> Ast.ast)
2698
8bccb3ab4ca4 added mark_bound(T), variant_abs';
wenzelm
parents: 1511
diff changeset
    56
end;
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
    57
42284
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42278
diff changeset
    58
structure Syntax_Trans: SYNTAX_TRANS =
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
    59
struct
2698
8bccb3ab4ca4 added mark_bound(T), variant_abs';
wenzelm
parents: 1511
diff changeset
    60
42476
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42288
diff changeset
    61
structure Syntax = Lexicon.Syntax;
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42288
diff changeset
    62
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42288
diff changeset
    63
42262
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
    64
(* print mode *)
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
    65
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
    66
val bracketsN = "brackets";
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
    67
val no_bracketsN = "no_brackets";
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
    68
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
    69
fun no_brackets () =
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
    70
  find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN)
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
    71
    (print_mode_value ()) = SOME no_bracketsN;
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
    72
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
    73
val type_bracketsN = "type_brackets";
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
    74
val no_type_bracketsN = "no_type_brackets";
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
    75
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
    76
fun no_type_brackets () =
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
    77
  find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN)
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
    78
    (print_mode_value ()) <> SOME type_bracketsN;
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
    79
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
    80
2698
8bccb3ab4ca4 added mark_bound(T), variant_abs';
wenzelm
parents: 1511
diff changeset
    81
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
    82
(** parse (ast) translations **)
12208de7edfe added this file;
wenzelm
parents:
diff changeset
    83
42057
3eba96ff3d3e more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents: 42055
diff changeset
    84
(* strip_positions *)
3eba96ff3d3e more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents: 42055
diff changeset
    85
42264
b6c1b0c4c511 separate structure Term_Position;
wenzelm
parents: 42262
diff changeset
    86
fun strip_positions_ast_tr [ast] = Ast.strip_positions ast
42057
3eba96ff3d3e more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents: 42055
diff changeset
    87
  | strip_positions_ast_tr asts = raise Ast.AST ("strip_positions_ast_tr", asts);
3eba96ff3d3e more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents: 42055
diff changeset
    88
3eba96ff3d3e more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
wenzelm
parents: 42055
diff changeset
    89
11491
085a0d2857e8 added constify_ast_tr;
wenzelm
parents: 10572
diff changeset
    90
(* constify *)
085a0d2857e8 added constify_ast_tr;
wenzelm
parents: 10572
diff changeset
    91
46236
ae79f2978a67 position constraints for numerals enable PIDE markup;
wenzelm
parents: 45389
diff changeset
    92
fun constify_ast_tr [Ast.Appl [c as Ast.Constant "_constrain", ast1, ast2]] =
ae79f2978a67 position constraints for numerals enable PIDE markup;
wenzelm
parents: 45389
diff changeset
    93
      Ast.Appl [c, constify_ast_tr [ast1], ast2]
ae79f2978a67 position constraints for numerals enable PIDE markup;
wenzelm
parents: 45389
diff changeset
    94
  | constify_ast_tr [Ast.Variable c] = Ast.Constant c
11491
085a0d2857e8 added constify_ast_tr;
wenzelm
parents: 10572
diff changeset
    95
  | constify_ast_tr asts = raise Ast.AST ("constify_ast_tr", asts);
085a0d2857e8 added constify_ast_tr;
wenzelm
parents: 10572
diff changeset
    96
085a0d2857e8 added constify_ast_tr;
wenzelm
parents: 10572
diff changeset
    97
42262
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
    98
(* type syntax *)
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
    99
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
   100
fun tapp_ast_tr [ty, c] = Ast.Appl [c, ty]
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
   101
  | tapp_ast_tr asts = raise Ast.AST ("tapp_ast_tr", asts);
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
   102
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
   103
fun tappl_ast_tr [ty, tys, c] = Ast.mk_appl c (ty :: Ast.unfold_ast "_types" tys)
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
   104
  | tappl_ast_tr asts = raise Ast.AST ("tappl_ast_tr", asts);
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
   105
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
   106
fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
   107
  | bracket_ast_tr asts = raise Ast.AST ("bracket_ast_tr", asts);
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
   108
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
   109
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   110
(* application *)
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   111
5690
4b056ee5435c no open;
wenzelm
parents: 5288
diff changeset
   112
fun appl_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_args" args)
4b056ee5435c no open;
wenzelm
parents: 5288
diff changeset
   113
  | appl_ast_tr asts = raise Ast.AST ("appl_ast_tr", asts);
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 639
diff changeset
   114
5690
4b056ee5435c no open;
wenzelm
parents: 5288
diff changeset
   115
fun applC_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_cargs" args)
4b056ee5435c no open;
wenzelm
parents: 5288
diff changeset
   116
  | applC_ast_tr asts = raise Ast.AST ("applC_ast_tr", asts);
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   117
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   118
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   119
(* abstraction *)
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   120
42278
088a2d69746f clarified sources -- removed odd comments;
wenzelm
parents: 42264
diff changeset
   121
fun idtyp_ast_tr [x, ty] = Ast.Appl [Ast.Constant "_constrain", x, ty]
088a2d69746f clarified sources -- removed odd comments;
wenzelm
parents: 42264
diff changeset
   122
  | idtyp_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts);
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   123
42278
088a2d69746f clarified sources -- removed odd comments;
wenzelm
parents: 42264
diff changeset
   124
fun lambda_ast_tr [pats, body] = Ast.fold_ast_p "_abs" (Ast.unfold_ast "_pttrns" pats, body)
088a2d69746f clarified sources -- removed odd comments;
wenzelm
parents: 42264
diff changeset
   125
  | lambda_ast_tr asts = raise Ast.AST ("lambda_ast_tr", asts);
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   126
44241
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43326
diff changeset
   127
fun absfree_proper (x, T) t =
42048
afd11ca8e018 support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents: 42045
diff changeset
   128
  if can Name.dest_internal x
afd11ca8e018 support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents: 42045
diff changeset
   129
  then error ("Illegal internal variable in abstraction: " ^ quote x)
44241
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43326
diff changeset
   130
  else absfree (x, T) t;
21773
0038f5fc2065 advanced translation functions: Proof.context;
wenzelm
parents: 21750
diff changeset
   131
44241
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43326
diff changeset
   132
fun abs_tr [Free x, t] = absfree_proper x t
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43326
diff changeset
   133
  | abs_tr [Const ("_idtdummy", T), t] = absdummy T t
42284
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42278
diff changeset
   134
  | abs_tr [Const ("_constrain", _) $ x $ tT, t] =
42476
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42288
diff changeset
   135
      Syntax.const "_constrainAbs" $ abs_tr [x, t] $ tT
42048
afd11ca8e018 support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents: 42045
diff changeset
   136
  | abs_tr ts = raise TERM ("abs_tr", ts);
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   137
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   138
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   139
(* binder *)
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   140
21535
wenzelm
parents: 20202
diff changeset
   141
fun mk_binder_tr (syn, name) =
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   142
  let
42055
ad87c485ff30 binder_tr: more informative exception;
wenzelm
parents: 42053
diff changeset
   143
    fun err ts = raise TERM ("binder_tr: " ^ syn, ts)
42048
afd11ca8e018 support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents: 42045
diff changeset
   144
    fun binder_tr [Const ("_idts", _) $ idt $ idts, t] = binder_tr [idt, binder_tr [idts, t]]
afd11ca8e018 support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents: 42045
diff changeset
   145
      | binder_tr [x, t] =
42055
ad87c485ff30 binder_tr: more informative exception;
wenzelm
parents: 42053
diff changeset
   146
          let val abs = abs_tr [x, t] handle TERM _ => err [x, t]
42476
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42288
diff changeset
   147
          in Syntax.const name $ abs end
42055
ad87c485ff30 binder_tr: more informative exception;
wenzelm
parents: 42053
diff changeset
   148
      | binder_tr ts = err ts;
52143
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   149
  in (syn, fn _ => binder_tr) end;
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   150
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   151
28628
06737d425249 added translations for SORT_CONSTRAINT
wenzelm
parents: 26424
diff changeset
   152
(* type propositions *)
06737d425249 added translations for SORT_CONSTRAINT
wenzelm
parents: 26424
diff changeset
   153
35255
2cb27605301f authentic syntax for *all* term constants;
wenzelm
parents: 35198
diff changeset
   154
fun mk_type ty =
42476
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42288
diff changeset
   155
  Syntax.const "_constrain" $
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42288
diff changeset
   156
    Syntax.const "\\<^const>TYPE" $ (Syntax.const "\\<^type>itself" $ ty);
28628
06737d425249 added translations for SORT_CONSTRAINT
wenzelm
parents: 26424
diff changeset
   157
42278
088a2d69746f clarified sources -- removed odd comments;
wenzelm
parents: 42264
diff changeset
   158
fun ofclass_tr [ty, cls] = cls $ mk_type ty
088a2d69746f clarified sources -- removed odd comments;
wenzelm
parents: 42264
diff changeset
   159
  | ofclass_tr ts = raise TERM ("ofclass_tr", ts);
28628
06737d425249 added translations for SORT_CONSTRAINT
wenzelm
parents: 26424
diff changeset
   160
42476
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42288
diff changeset
   161
fun sort_constraint_tr [ty] = Syntax.const "\\<^const>Pure.sort_constraint" $ mk_type ty
42278
088a2d69746f clarified sources -- removed odd comments;
wenzelm
parents: 42264
diff changeset
   162
  | sort_constraint_tr ts = raise TERM ("sort_constraint_tr", ts);
28628
06737d425249 added translations for SORT_CONSTRAINT
wenzelm
parents: 26424
diff changeset
   163
06737d425249 added translations for SORT_CONSTRAINT
wenzelm
parents: 26424
diff changeset
   164
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   165
(* meta propositions *)
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   166
42476
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42288
diff changeset
   167
fun aprop_tr [t] = Syntax.const "_constrain" $ t $ Syntax.const "\\<^type>prop"
42278
088a2d69746f clarified sources -- removed odd comments;
wenzelm
parents: 42264
diff changeset
   168
  | aprop_tr ts = raise TERM ("aprop_tr", ts);
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   169
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   170
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   171
(* meta implication *)
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   172
42278
088a2d69746f clarified sources -- removed odd comments;
wenzelm
parents: 42264
diff changeset
   173
fun bigimpl_ast_tr (asts as [asms, concl]) =
16612
48be8ef738df transform_failure in translation functions: TRANSLATION_FAIL;
wenzelm
parents: 15570
diff changeset
   174
      let val prems =
48be8ef738df transform_failure in translation functions: TRANSLATION_FAIL;
wenzelm
parents: 15570
diff changeset
   175
        (case Ast.unfold_ast_p "_asms" asms of
48be8ef738df transform_failure in translation functions: TRANSLATION_FAIL;
wenzelm
parents: 15570
diff changeset
   176
          (asms', Ast.Appl [Ast.Constant "_asm", asm']) => asms' @ [asm']
48be8ef738df transform_failure in translation functions: TRANSLATION_FAIL;
wenzelm
parents: 15570
diff changeset
   177
        | _ => raise Ast.AST ("bigimpl_ast_tr", asts))
35255
2cb27605301f authentic syntax for *all* term constants;
wenzelm
parents: 35198
diff changeset
   178
      in Ast.fold_ast_p "\\<^const>==>" (prems, concl) end
42278
088a2d69746f clarified sources -- removed odd comments;
wenzelm
parents: 42264
diff changeset
   179
  | bigimpl_ast_tr asts = raise Ast.AST ("bigimpl_ast_tr", asts);
15421
fcf747c0b6b8 Syntax: last premise of "_bigimpl" is wrapped with "_asm", to have a hook for
schirmer
parents: 14981
diff changeset
   180
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   181
23824
8ad7131dbfcf moved print_translations from Pure.thy to Syntax/syn_trans.ML;
wenzelm
parents: 21773
diff changeset
   182
(* type/term reflection *)
4148
e0e5a2820ac1 adapted pure_trfunsT;
wenzelm
parents: 3928
diff changeset
   183
42278
088a2d69746f clarified sources -- removed odd comments;
wenzelm
parents: 42264
diff changeset
   184
fun type_tr [ty] = mk_type ty
088a2d69746f clarified sources -- removed odd comments;
wenzelm
parents: 42264
diff changeset
   185
  | type_tr ts = raise TERM ("type_tr", ts);
4148
e0e5a2820ac1 adapted pure_trfunsT;
wenzelm
parents: 3928
diff changeset
   186
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   187
6761
aa71a04f4b93 added dddot_tr;
wenzelm
parents: 5690
diff changeset
   188
(* dddot *)
aa71a04f4b93 added dddot_tr;
wenzelm
parents: 5690
diff changeset
   189
42476
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42288
diff changeset
   190
fun dddot_tr ts = Term.list_comb (Syntax.var Syntax_Ext.dddot_indexname, ts);
6761
aa71a04f4b93 added dddot_tr;
wenzelm
parents: 5690
diff changeset
   191
aa71a04f4b93 added dddot_tr;
wenzelm
parents: 5690
diff changeset
   192
5084
a676ada3b380 tuned loose bound vars check;
wenzelm
parents: 4700
diff changeset
   193
(* quote / antiquote *)
a676ada3b380 tuned loose bound vars check;
wenzelm
parents: 4700
diff changeset
   194
8577
4a3cdf01531b improved (anti)quote_tr(');
wenzelm
parents: 8575
diff changeset
   195
fun antiquote_tr name =
4a3cdf01531b improved (anti)quote_tr(');
wenzelm
parents: 8575
diff changeset
   196
  let
4a3cdf01531b improved (anti)quote_tr(');
wenzelm
parents: 8575
diff changeset
   197
    fun tr i ((t as Const (c, _)) $ u) =
4a3cdf01531b improved (anti)quote_tr(');
wenzelm
parents: 8575
diff changeset
   198
          if c = name then tr i u $ Bound i
4a3cdf01531b improved (anti)quote_tr(');
wenzelm
parents: 8575
diff changeset
   199
          else tr i t $ tr i u
4a3cdf01531b improved (anti)quote_tr(');
wenzelm
parents: 8575
diff changeset
   200
      | tr i (t $ u) = tr i t $ tr i u
4a3cdf01531b improved (anti)quote_tr(');
wenzelm
parents: 8575
diff changeset
   201
      | tr i (Abs (x, T, t)) = Abs (x, T, tr (i + 1) t)
4a3cdf01531b improved (anti)quote_tr(');
wenzelm
parents: 8575
diff changeset
   202
      | tr _ a = a;
4a3cdf01531b improved (anti)quote_tr(');
wenzelm
parents: 8575
diff changeset
   203
  in tr 0 end;
4a3cdf01531b improved (anti)quote_tr(');
wenzelm
parents: 8575
diff changeset
   204
4a3cdf01531b improved (anti)quote_tr(');
wenzelm
parents: 8575
diff changeset
   205
fun quote_tr name t = Abs ("s", dummyT, antiquote_tr name (Term.incr_boundvars 1 t));
4a3cdf01531b improved (anti)quote_tr(');
wenzelm
parents: 8575
diff changeset
   206
5084
a676ada3b380 tuned loose bound vars check;
wenzelm
parents: 4700
diff changeset
   207
fun quote_antiquote_tr quoteN antiquoteN name =
a676ada3b380 tuned loose bound vars check;
wenzelm
parents: 4700
diff changeset
   208
  let
42476
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42288
diff changeset
   209
    fun tr [t] = Syntax.const name $ quote_tr antiquoteN t
8577
4a3cdf01531b improved (anti)quote_tr(');
wenzelm
parents: 8575
diff changeset
   210
      | tr ts = raise TERM ("quote_tr", ts);
52143
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   211
  in (quoteN, fn _ => tr) end;
5084
a676ada3b380 tuned loose bound vars check;
wenzelm
parents: 4700
diff changeset
   212
a676ada3b380 tuned loose bound vars check;
wenzelm
parents: 4700
diff changeset
   213
35145
f132a4fd8679 moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents: 32786
diff changeset
   214
(* corresponding updates *)
f132a4fd8679 moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents: 32786
diff changeset
   215
f132a4fd8679 moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents: 32786
diff changeset
   216
fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts)
f132a4fd8679 moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents: 32786
diff changeset
   217
  | update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update" x, T), ts)
f132a4fd8679 moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents: 32786
diff changeset
   218
  | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
42264
b6c1b0c4c511 separate structure Term_Position;
wenzelm
parents: 42262
diff changeset
   219
      if Term_Position.is_position ty then list_comb (c $ update_name_tr [t] $ ty, ts)
42053
006095137a81 update_name_tr: more precise handling of explicit constraints, including positions;
wenzelm
parents: 42048
diff changeset
   220
      else
006095137a81 update_name_tr: more precise handling of explicit constraints, including positions;
wenzelm
parents: 42048
diff changeset
   221
        list_comb (c $ update_name_tr [t] $
42080
58b465952287 update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
wenzelm
parents: 42057
diff changeset
   222
          (Lexicon.fun_type $
58b465952287 update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
wenzelm
parents: 42057
diff changeset
   223
            (Lexicon.fun_type $ Lexicon.dummy_type $ ty) $ Lexicon.dummy_type), ts)
35145
f132a4fd8679 moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents: 32786
diff changeset
   224
  | update_name_tr ts = raise TERM ("update_name_tr", ts);
f132a4fd8679 moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents: 32786
diff changeset
   225
f132a4fd8679 moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents: 32786
diff changeset
   226
14697
5ad13d05049b improved indexed syntax / implicit structures;
wenzelm
parents: 14647
diff changeset
   227
(* indexed syntax *)
5ad13d05049b improved indexed syntax / implicit structures;
wenzelm
parents: 14647
diff changeset
   228
45389
bc0d50f8ae19 discontinued numbered structure indexes (legacy feature);
wenzelm
parents: 45057
diff changeset
   229
fun indexdefault_ast_tr [] =
bc0d50f8ae19 discontinued numbered structure indexes (legacy feature);
wenzelm
parents: 45057
diff changeset
   230
      Ast.Appl [Ast.Constant "_index",
bc0d50f8ae19 discontinued numbered structure indexes (legacy feature);
wenzelm
parents: 45057
diff changeset
   231
        Ast.Appl [Ast.Constant "_struct", Ast.Constant "_indexdefault"]]
bc0d50f8ae19 discontinued numbered structure indexes (legacy feature);
wenzelm
parents: 45057
diff changeset
   232
  | indexdefault_ast_tr asts = raise Ast.AST ("indexdefault_ast_tr", asts);
bc0d50f8ae19 discontinued numbered structure indexes (legacy feature);
wenzelm
parents: 45057
diff changeset
   233
bc0d50f8ae19 discontinued numbered structure indexes (legacy feature);
wenzelm
parents: 45057
diff changeset
   234
fun indexvar_ast_tr [] = Ast.Appl [Ast.Constant "_index", Ast.Variable "some_index"]
bc0d50f8ae19 discontinued numbered structure indexes (legacy feature);
wenzelm
parents: 45057
diff changeset
   235
  | indexvar_ast_tr asts = raise Ast.AST ("indexvar_ast_tr", asts);
bc0d50f8ae19 discontinued numbered structure indexes (legacy feature);
wenzelm
parents: 45057
diff changeset
   236
42278
088a2d69746f clarified sources -- removed odd comments;
wenzelm
parents: 42264
diff changeset
   237
fun struct_ast_tr [Ast.Appl [Ast.Constant "_index", ast]] = ast
088a2d69746f clarified sources -- removed odd comments;
wenzelm
parents: 42264
diff changeset
   238
  | struct_ast_tr asts = Ast.mk_appl (Ast.Constant "_struct") asts;
14697
5ad13d05049b improved indexed syntax / implicit structures;
wenzelm
parents: 14647
diff changeset
   239
42278
088a2d69746f clarified sources -- removed odd comments;
wenzelm
parents: 42264
diff changeset
   240
fun index_tr [t] = t
088a2d69746f clarified sources -- removed odd comments;
wenzelm
parents: 42264
diff changeset
   241
  | index_tr ts = raise TERM ("index_tr", ts);
14697
5ad13d05049b improved indexed syntax / implicit structures;
wenzelm
parents: 14647
diff changeset
   242
52144
wenzelm
parents: 52143
diff changeset
   243
fun struct_tr structs =
wenzelm
parents: 52143
diff changeset
   244
  ("_struct", fn _ =>
wenzelm
parents: 52143
diff changeset
   245
    (fn [Const ("_indexdefault", _)] =>
wenzelm
parents: 52143
diff changeset
   246
        (case structs of
wenzelm
parents: 52143
diff changeset
   247
          x :: _ => Syntax.const (Lexicon.mark_fixed x)
wenzelm
parents: 52143
diff changeset
   248
        | _ => error "Illegal reference to implicit structure")
wenzelm
parents: 52143
diff changeset
   249
      | ts => raise TERM ("struct_tr", ts)));
12122
7f8d88ed4f21 indexvar_ast_tr (for \<index> placeholder);
wenzelm
parents: 11491
diff changeset
   250
7f8d88ed4f21 indexvar_ast_tr (for \<index> placeholder);
wenzelm
parents: 11491
diff changeset
   251
5084
a676ada3b380 tuned loose bound vars check;
wenzelm
parents: 4700
diff changeset
   252
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   253
(** print (ast) translations **)
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   254
14647
3f9d3d5cd0cd non_typed_tr';
wenzelm
parents: 13762
diff changeset
   255
(* types *)
3f9d3d5cd0cd non_typed_tr';
wenzelm
parents: 13762
diff changeset
   256
52143
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   257
fun non_typed_tr' f ctxt _ ts = f ctxt ts;
14647
3f9d3d5cd0cd non_typed_tr';
wenzelm
parents: 13762
diff changeset
   258
3f9d3d5cd0cd non_typed_tr';
wenzelm
parents: 13762
diff changeset
   259
42262
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
   260
(* type syntax *)
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
   261
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
   262
fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f])
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
   263
  | tappl_ast_tr' (f, [ty]) = Ast.Appl [Ast.Constant "_tapp", ty, f]
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
   264
  | tappl_ast_tr' (f, ty :: tys) =
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
   265
      Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f];
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
   266
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
   267
fun fun_ast_tr' asts =
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
   268
  if no_brackets () orelse no_type_brackets () then raise Match
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
   269
  else
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
   270
    (case Ast.unfold_ast_p "\\<^type>fun" (Ast.Appl (Ast.Constant "\\<^type>fun" :: asts)) of
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
   271
      (dom as _ :: _ :: _, cod)
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
   272
        => Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod]
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
   273
    | _ => raise Match);
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
   274
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
   275
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   276
(* application *)
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   277
5690
4b056ee5435c no open;
wenzelm
parents: 5288
diff changeset
   278
fun appl_ast_tr' (f, []) = raise Ast.AST ("appl_ast_tr'", [f])
4b056ee5435c no open;
wenzelm
parents: 5288
diff changeset
   279
  | appl_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_appl", f, Ast.fold_ast "_args" args];
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   280
5690
4b056ee5435c no open;
wenzelm
parents: 5288
diff changeset
   281
fun applC_ast_tr' (f, []) = raise Ast.AST ("applC_ast_tr'", [f])
4b056ee5435c no open;
wenzelm
parents: 5288
diff changeset
   282
  | applC_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_applC", f, Ast.fold_ast "_cargs" args];
922
196ca0973a6d added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents: 639
diff changeset
   283
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   284
42085
wenzelm
parents: 42084
diff changeset
   285
(* partial eta-contraction before printing *)
wenzelm
parents: 42084
diff changeset
   286
wenzelm
parents: 42084
diff changeset
   287
fun eta_abs (Abs (a, T, t)) =
wenzelm
parents: 42084
diff changeset
   288
      (case eta_abs t of
wenzelm
parents: 42084
diff changeset
   289
        t' as Const ("_aprop", _) $ _ => Abs (a, T, t')
wenzelm
parents: 42084
diff changeset
   290
      | t' as f $ u =>
wenzelm
parents: 42084
diff changeset
   291
          (case eta_abs u of
wenzelm
parents: 42084
diff changeset
   292
            Bound 0 =>
wenzelm
parents: 42084
diff changeset
   293
              if Term.is_dependent f then Abs (a, T, t')
wenzelm
parents: 42084
diff changeset
   294
              else incr_boundvars ~1 f
wenzelm
parents: 42084
diff changeset
   295
          | _ => Abs (a, T, t'))
wenzelm
parents: 42084
diff changeset
   296
      | t' => Abs (a, T, t'))
wenzelm
parents: 42084
diff changeset
   297
  | eta_abs t = t;
wenzelm
parents: 42084
diff changeset
   298
52043
286629271d65 more system options as context-sensitive config options;
wenzelm
parents: 51656
diff changeset
   299
val eta_contract_raw = Config.declare_option "eta_contract";
42085
wenzelm
parents: 42084
diff changeset
   300
val eta_contract = Config.bool eta_contract_raw;
wenzelm
parents: 42084
diff changeset
   301
wenzelm
parents: 42084
diff changeset
   302
fun eta_contr ctxt tm =
wenzelm
parents: 42084
diff changeset
   303
  if Config.get ctxt eta_contract then eta_abs tm else tm;
wenzelm
parents: 42084
diff changeset
   304
wenzelm
parents: 42084
diff changeset
   305
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   306
(* abstraction *)
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   307
49660
de49d9b4d7bc more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents: 46236
diff changeset
   308
fun mark_bound_abs (x, T) = Const ("_bound", T --> T) $ Free (x, T);
de49d9b4d7bc more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents: 46236
diff changeset
   309
fun mark_bound_body (x, T) = Const ("_bound", dummyT) $ Free (x, T);
2698
8bccb3ab4ca4 added mark_bound(T), variant_abs';
wenzelm
parents: 1511
diff changeset
   310
18958
9151a29d2864 added bound_vars;
wenzelm
parents: 18857
diff changeset
   311
fun bound_vars vars body =
49660
de49d9b4d7bc more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents: 46236
diff changeset
   312
  subst_bounds (map mark_bound_abs (Term.rename_wrt_term body vars), body);
18958
9151a29d2864 added bound_vars;
wenzelm
parents: 18857
diff changeset
   313
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   314
fun strip_abss vars_of body_of tm =
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   315
  let
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   316
    val vars = vars_of tm;
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   317
    val body = body_of tm;
29276
94b1ffec9201 qualified Term.rename_wrt_term;
wenzelm
parents: 28856
diff changeset
   318
    val rev_new_vars = Term.rename_wrt_term body vars;
21750
41986849fee0 abs/binder_tr': support printing of idtdummy;
wenzelm
parents: 21535
diff changeset
   319
    fun subst (x, T) b =
42083
e1209fc7ecdc added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
wenzelm
parents: 42080
diff changeset
   320
      if can Name.dest_internal x andalso not (Term.is_dependent b)
21750
41986849fee0 abs/binder_tr': support printing of idtdummy;
wenzelm
parents: 21535
diff changeset
   321
      then (Const ("_idtdummy", T), incr_boundvars ~1 b)
49660
de49d9b4d7bc more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents: 46236
diff changeset
   322
      else (mark_bound_abs (x, T), Term.subst_bound (mark_bound_body (x, T), b));
21750
41986849fee0 abs/binder_tr': support printing of idtdummy;
wenzelm
parents: 21535
diff changeset
   323
    val (rev_vars', body') = fold_map subst rev_new_vars body;
41986849fee0 abs/binder_tr': support printing of idtdummy;
wenzelm
parents: 21535
diff changeset
   324
  in (rev rev_vars', body') end;
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   325
3928
787d2659ce4a no longer tries bogus eta-contract involving aprops;
wenzelm
parents: 3777
diff changeset
   326
39128
93a7365fb4ee turned eta_contract into proper configuration option;
wenzelm
parents: 37216
diff changeset
   327
fun abs_tr' ctxt tm =
42476
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42288
diff changeset
   328
  uncurry (fold_rev (fn x => fn t => Syntax.const "_abs" $ x $ t))
39128
93a7365fb4ee turned eta_contract into proper configuration option;
wenzelm
parents: 37216
diff changeset
   329
    (strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm));
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   330
14697
5ad13d05049b improved indexed syntax / implicit structures;
wenzelm
parents: 14647
diff changeset
   331
fun atomic_abs_tr' (x, T, t) =
29276
94b1ffec9201 qualified Term.rename_wrt_term;
wenzelm
parents: 28856
diff changeset
   332
  let val [xT] = Term.rename_wrt_term t [(x, T)]
49660
de49d9b4d7bc more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents: 46236
diff changeset
   333
  in (mark_bound_abs xT, subst_bound (mark_bound_body xT, t)) end;
13762
9dd78dab72bc *** empty log message ***
nipkow
parents: 12785
diff changeset
   334
42085
wenzelm
parents: 42084
diff changeset
   335
fun abs_ast_tr' asts =
5690
4b056ee5435c no open;
wenzelm
parents: 5288
diff changeset
   336
  (case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of
4b056ee5435c no open;
wenzelm
parents: 5288
diff changeset
   337
    ([], _) => raise Ast.AST ("abs_ast_tr'", asts)
4b056ee5435c no open;
wenzelm
parents: 5288
diff changeset
   338
  | (xs, body) => Ast.Appl [Ast.Constant "_lambda", Ast.fold_ast "_pttrns" xs, body]);
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   339
42086
74bf78db0d87 added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
wenzelm
parents: 42085
diff changeset
   340
fun const_abs_tr' t =
74bf78db0d87 added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
wenzelm
parents: 42085
diff changeset
   341
  (case eta_abs t of
74bf78db0d87 added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
wenzelm
parents: 42085
diff changeset
   342
    Abs (_, _, t') =>
74bf78db0d87 added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
wenzelm
parents: 42085
diff changeset
   343
      if Term.is_dependent t' then raise Match
74bf78db0d87 added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
wenzelm
parents: 42085
diff changeset
   344
      else incr_boundvars ~1 t'
74bf78db0d87 added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
wenzelm
parents: 42085
diff changeset
   345
  | _ => raise Match);
74bf78db0d87 added Syntax.const_abs_tr' with proper eta_abs and Term.is_dependent;
wenzelm
parents: 42085
diff changeset
   346
32120
53a21a5e6889 attempt for more concise setup of non-etacontracting binders
haftmann
parents: 31542
diff changeset
   347
42085
wenzelm
parents: 42084
diff changeset
   348
(* binders *)
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   349
21535
wenzelm
parents: 20202
diff changeset
   350
fun mk_binder_tr' (name, syn) =
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   351
  let
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   352
    fun mk_idts [] = raise Match    (*abort translation*)
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   353
      | mk_idts [idt] = idt
42476
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42288
diff changeset
   354
      | mk_idts (idt :: idts) = Syntax.const "_idts" $ idt $ mk_idts idts;
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   355
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   356
    fun tr' t =
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   357
      let
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   358
        val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t;
42476
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42288
diff changeset
   359
      in Syntax.const syn $ mk_idts xs $ bd end;
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   360
42476
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42288
diff changeset
   361
    fun binder_tr' (t :: ts) = Term.list_comb (tr' (Syntax.const name $ t), ts)
21535
wenzelm
parents: 20202
diff changeset
   362
      | binder_tr' [] = raise Match;
52143
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   363
  in (name, fn _ => binder_tr') end;
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   364
52143
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   365
fun preserve_binder_abs_tr' name syn = (name, fn _ => fn Abs abs :: ts =>
42085
wenzelm
parents: 42084
diff changeset
   366
  let val (x, t) = atomic_abs_tr' abs
42476
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42288
diff changeset
   367
  in list_comb (Syntax.const syn $ x $ t, ts) end);
42085
wenzelm
parents: 42084
diff changeset
   368
52143
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   369
fun preserve_binder_abs2_tr' name syn = (name, fn _ => fn A :: Abs abs :: ts =>
42085
wenzelm
parents: 42084
diff changeset
   370
  let val (x, t) = atomic_abs_tr' abs
42476
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42288
diff changeset
   371
  in list_comb (Syntax.const syn $ x $ A $ t, ts) end);
42085
wenzelm
parents: 42084
diff changeset
   372
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   373
3691
f0396ac63e12 tuned lambda_ast_tr, idtyp_ast_tr' to accomodate fix of idt/idts
wenzelm
parents: 2698
diff changeset
   374
(* idtyp constraints *)
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   375
42045
wenzelm
parents: 42043
diff changeset
   376
fun idtyp_ast_tr' a [Ast.Appl [Ast.Constant "_constrain", x, ty], xs] =
wenzelm
parents: 42043
diff changeset
   377
      Ast.Appl [Ast.Constant a, Ast.Appl [Ast.Constant "_idtyp", x, ty], xs]
3691
f0396ac63e12 tuned lambda_ast_tr, idtyp_ast_tr' to accomodate fix of idt/idts
wenzelm
parents: 2698
diff changeset
   378
  | idtyp_ast_tr' _ _ = raise Match;
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   379
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   380
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   381
(* meta propositions *)
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   382
4148
e0e5a2820ac1 adapted pure_trfunsT;
wenzelm
parents: 3928
diff changeset
   383
fun prop_tr' tm =
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   384
  let
42476
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42288
diff changeset
   385
    fun aprop t = Syntax.const "_aprop" $ t;
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   386
2698
8bccb3ab4ca4 added mark_bound(T), variant_abs';
wenzelm
parents: 1511
diff changeset
   387
    fun is_prop Ts t =
8bccb3ab4ca4 added mark_bound(T), variant_abs';
wenzelm
parents: 1511
diff changeset
   388
      fastype_of1 (Ts, t) = propT handle TERM _ => false;
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   389
35429
afa8cf9e63d8 authentic syntax for classes and type constructors;
wenzelm
parents: 35255
diff changeset
   390
    fun is_term (Const ("Pure.term", _) $ _) = true
19848
a525275d36df improved treatment of TERM TYPE syntax;
wenzelm
parents: 19577
diff changeset
   391
      | is_term _ = false;
a525275d36df improved treatment of TERM TYPE syntax;
wenzelm
parents: 19577
diff changeset
   392
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   393
    fun tr' _ (t as Const _) = t
18478
29a5070b517c prop_tr': proper handling of aprop marked as bound;
wenzelm
parents: 18342
diff changeset
   394
      | tr' Ts (t as Const ("_bound", _) $ u) =
29a5070b517c prop_tr': proper handling of aprop marked as bound;
wenzelm
parents: 18342
diff changeset
   395
          if is_prop Ts u then aprop t else t
2698
8bccb3ab4ca4 added mark_bound(T), variant_abs';
wenzelm
parents: 1511
diff changeset
   396
      | tr' _ (t as Free (x, T)) =
42476
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42288
diff changeset
   397
          if T = propT then aprop (Syntax.free x) else t
2698
8bccb3ab4ca4 added mark_bound(T), variant_abs';
wenzelm
parents: 1511
diff changeset
   398
      | tr' _ (t as Var (xi, T)) =
42476
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42288
diff changeset
   399
          if T = propT then aprop (Syntax.var xi) else t
2698
8bccb3ab4ca4 added mark_bound(T), variant_abs';
wenzelm
parents: 1511
diff changeset
   400
      | tr' Ts (t as Bound _) =
8bccb3ab4ca4 added mark_bound(T), variant_abs';
wenzelm
parents: 1511
diff changeset
   401
          if is_prop Ts t then aprop t else t
8bccb3ab4ca4 added mark_bound(T), variant_abs';
wenzelm
parents: 1511
diff changeset
   402
      | tr' Ts (Abs (x, T, t)) = Abs (x, T, tr' (T :: Ts) t)
35429
afa8cf9e63d8 authentic syntax for classes and type constructors;
wenzelm
parents: 35255
diff changeset
   403
      | tr' Ts (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [T])))) =
28628
06737d425249 added translations for SORT_CONSTRAINT
wenzelm
parents: 26424
diff changeset
   404
          if is_prop Ts t andalso not (is_term t) then Const ("_type_prop", T) $ tr' Ts t1
2698
8bccb3ab4ca4 added mark_bound(T), variant_abs';
wenzelm
parents: 1511
diff changeset
   405
          else tr' Ts t1 $ tr' Ts t2
8bccb3ab4ca4 added mark_bound(T), variant_abs';
wenzelm
parents: 1511
diff changeset
   406
      | tr' Ts (t as t1 $ t2) =
5690
4b056ee5435c no open;
wenzelm
parents: 5288
diff changeset
   407
          (if is_Const (Term.head_of t) orelse not (is_prop Ts t)
2698
8bccb3ab4ca4 added mark_bound(T), variant_abs';
wenzelm
parents: 1511
diff changeset
   408
            then I else aprop) (tr' Ts t1 $ tr' Ts t2);
16612
48be8ef738df transform_failure in translation functions: TRANSLATION_FAIL;
wenzelm
parents: 15570
diff changeset
   409
  in tr' [] tm end;
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   410
2698
8bccb3ab4ca4 added mark_bound(T), variant_abs';
wenzelm
parents: 1511
diff changeset
   411
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   412
(* meta implication *)
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   413
42278
088a2d69746f clarified sources -- removed odd comments;
wenzelm
parents: 42264
diff changeset
   414
fun impl_ast_tr' asts =
42262
4821a2a91548 moved type syntax translations to syn_trans.ML;
wenzelm
parents: 42247
diff changeset
   415
  if no_brackets () then raise Match
10572
b070825579b8 no_brackets mode;
wenzelm
parents: 8595
diff changeset
   416
  else
35255
2cb27605301f authentic syntax for *all* term constants;
wenzelm
parents: 35198
diff changeset
   417
    (case Ast.unfold_ast_p "\\<^const>==>" (Ast.Appl (Ast.Constant "\\<^const>==>" :: asts)) of
16612
48be8ef738df transform_failure in translation functions: TRANSLATION_FAIL;
wenzelm
parents: 15570
diff changeset
   418
      (prems as _ :: _ :: _, concl) =>
48be8ef738df transform_failure in translation functions: TRANSLATION_FAIL;
wenzelm
parents: 15570
diff changeset
   419
        let
48be8ef738df transform_failure in translation functions: TRANSLATION_FAIL;
wenzelm
parents: 15570
diff changeset
   420
          val (asms, asm) = split_last prems;
48be8ef738df transform_failure in translation functions: TRANSLATION_FAIL;
wenzelm
parents: 15570
diff changeset
   421
          val asms' = Ast.fold_ast_p "_asms" (asms, Ast.Appl [Ast.Constant "_asm", asm]);
48be8ef738df transform_failure in translation functions: TRANSLATION_FAIL;
wenzelm
parents: 15570
diff changeset
   422
        in Ast.Appl [Ast.Constant "_bigimpl", asms', concl] end
15421
fcf747c0b6b8 Syntax: last premise of "_bigimpl" is wrapped with "_asm", to have a hook for
schirmer
parents: 14981
diff changeset
   423
    | _ => raise Match);
fcf747c0b6b8 Syntax: last premise of "_bigimpl" is wrapped with "_asm", to have a hook for
schirmer
parents: 14981
diff changeset
   424
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   425
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   426
(* dependent / nondependent quantifiers *)
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   427
20202
87205ea2af06 added variant_abs (from term.ML);
wenzelm
parents: 20146
diff changeset
   428
fun var_abs mark (x, T, b) =
43326
47cf4bc789aa simplified Name.variant -- discontinued builtin fold_map;
wenzelm
parents: 42476
diff changeset
   429
  let val (x', _) = Name.variant x (Term.declare_term_names b Name.context)
20202
87205ea2af06 added variant_abs (from term.ML);
wenzelm
parents: 20146
diff changeset
   430
  in (x', subst_bound (mark (x', T), b)) end;
87205ea2af06 added variant_abs (from term.ML);
wenzelm
parents: 20146
diff changeset
   431
87205ea2af06 added variant_abs (from term.ML);
wenzelm
parents: 20146
diff changeset
   432
val variant_abs = var_abs Free;
49660
de49d9b4d7bc more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents: 46236
diff changeset
   433
val variant_abs' = var_abs mark_bound_abs;
2698
8bccb3ab4ca4 added mark_bound(T), variant_abs';
wenzelm
parents: 1511
diff changeset
   434
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   435
fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
42083
e1209fc7ecdc added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
wenzelm
parents: 42080
diff changeset
   436
      if Term.is_dependent B then
2698
8bccb3ab4ca4 added mark_bound(T), variant_abs';
wenzelm
parents: 1511
diff changeset
   437
        let val (x', B') = variant_abs' (x, dummyT, B);
49660
de49d9b4d7bc more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
wenzelm
parents: 46236
diff changeset
   438
        in Term.list_comb (Syntax.const q $ mark_bound_abs (x', T) $ A $ B', ts) end
42476
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42288
diff changeset
   439
      else Term.list_comb (Syntax.const r $ A $ incr_boundvars ~1 B, ts)
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   440
  | dependent_tr' _ _ = raise Match;
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   441
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   442
5084
a676ada3b380 tuned loose bound vars check;
wenzelm
parents: 4700
diff changeset
   443
(* quote / antiquote *)
a676ada3b380 tuned loose bound vars check;
wenzelm
parents: 4700
diff changeset
   444
8577
4a3cdf01531b improved (anti)quote_tr(');
wenzelm
parents: 8575
diff changeset
   445
fun antiquote_tr' name =
4a3cdf01531b improved (anti)quote_tr(');
wenzelm
parents: 8575
diff changeset
   446
  let
4a3cdf01531b improved (anti)quote_tr(');
wenzelm
parents: 8575
diff changeset
   447
    fun tr' i (t $ u) =
42476
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42288
diff changeset
   448
          if u aconv Bound i then Syntax.const name $ tr' i t
42084
532b3a76103f dependent_tr': formal treatment of bounds after stripping Abs, although it should only happen for malformed terms, since print_translations work top-down;
wenzelm
parents: 42083
diff changeset
   449
          else tr' i t $ tr' i u
8577
4a3cdf01531b improved (anti)quote_tr(');
wenzelm
parents: 8575
diff changeset
   450
      | tr' i (Abs (x, T, t)) = Abs (x, T, tr' (i + 1) t)
18139
wenzelm
parents: 17788
diff changeset
   451
      | tr' i a = if a aconv Bound i then raise Match else a;
8577
4a3cdf01531b improved (anti)quote_tr(');
wenzelm
parents: 8575
diff changeset
   452
  in tr' 0 end;
4a3cdf01531b improved (anti)quote_tr(');
wenzelm
parents: 8575
diff changeset
   453
4a3cdf01531b improved (anti)quote_tr(');
wenzelm
parents: 8575
diff changeset
   454
fun quote_tr' name (Abs (_, _, t)) = Term.incr_boundvars ~1 (antiquote_tr' name t)
4a3cdf01531b improved (anti)quote_tr(');
wenzelm
parents: 8575
diff changeset
   455
  | quote_tr' _ _ = raise Match;
4a3cdf01531b improved (anti)quote_tr(');
wenzelm
parents: 8575
diff changeset
   456
5084
a676ada3b380 tuned loose bound vars check;
wenzelm
parents: 4700
diff changeset
   457
fun quote_antiquote_tr' quoteN antiquoteN name =
a676ada3b380 tuned loose bound vars check;
wenzelm
parents: 4700
diff changeset
   458
  let
42476
d0bc1268ef09 clarified auxiliary structure Lexicon.Syntax;
wenzelm
parents: 42288
diff changeset
   459
    fun tr' (t :: ts) = Term.list_comb (Syntax.const quoteN $ quote_tr' antiquoteN t, ts)
8577
4a3cdf01531b improved (anti)quote_tr(');
wenzelm
parents: 8575
diff changeset
   460
      | tr' _ = raise Match;
52143
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   461
  in (name, fn _ => tr') end;
5084
a676ada3b380 tuned loose bound vars check;
wenzelm
parents: 4700
diff changeset
   462
a676ada3b380 tuned loose bound vars check;
wenzelm
parents: 4700
diff changeset
   463
35145
f132a4fd8679 moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents: 32786
diff changeset
   464
(* corresponding updates *)
f132a4fd8679 moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents: 32786
diff changeset
   465
42080
58b465952287 update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
wenzelm
parents: 42057
diff changeset
   466
local
58b465952287 update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
wenzelm
parents: 42057
diff changeset
   467
58b465952287 update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
wenzelm
parents: 42057
diff changeset
   468
fun upd_type (Type ("fun", [Type ("fun", [_, T]), _])) = T
58b465952287 update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
wenzelm
parents: 42057
diff changeset
   469
  | upd_type _ = dummyT;
58b465952287 update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
wenzelm
parents: 42057
diff changeset
   470
35145
f132a4fd8679 moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents: 32786
diff changeset
   471
fun upd_tr' (x_upd, T) =
f132a4fd8679 moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents: 32786
diff changeset
   472
  (case try (unsuffix "_update") x_upd of
42080
58b465952287 update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
wenzelm
parents: 42057
diff changeset
   473
    SOME x => (x, upd_type T)
35145
f132a4fd8679 moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents: 32786
diff changeset
   474
  | NONE => raise Match);
f132a4fd8679 moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents: 32786
diff changeset
   475
42080
58b465952287 update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
wenzelm
parents: 42057
diff changeset
   476
in
58b465952287 update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
wenzelm
parents: 42057
diff changeset
   477
35145
f132a4fd8679 moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents: 32786
diff changeset
   478
fun update_name_tr' (Free x) = Free (upd_tr' x)
f132a4fd8679 moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents: 32786
diff changeset
   479
  | update_name_tr' ((c as Const ("_free", _)) $ Free x) = c $ Free (upd_tr' x)
f132a4fd8679 moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents: 32786
diff changeset
   480
  | update_name_tr' (Const x) = Const (upd_tr' x)
f132a4fd8679 moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents: 32786
diff changeset
   481
  | update_name_tr' _ = raise Match;
f132a4fd8679 moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents: 32786
diff changeset
   482
42080
58b465952287 update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
wenzelm
parents: 42057
diff changeset
   483
end;
58b465952287 update_name: more uniform treatment of type constraints (NB: type equality is hard to establish in parse trees);
wenzelm
parents: 42057
diff changeset
   484
35145
f132a4fd8679 moved generic update_name to Pure syntax -- not specific to HOL/record;
wenzelm
parents: 32786
diff changeset
   485
14697
5ad13d05049b improved indexed syntax / implicit structures;
wenzelm
parents: 14647
diff changeset
   486
(* indexed syntax *)
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   487
42278
088a2d69746f clarified sources -- removed odd comments;
wenzelm
parents: 42264
diff changeset
   488
fun index_ast_tr' [Ast.Appl [Ast.Constant "_struct", ast]] = ast
14697
5ad13d05049b improved indexed syntax / implicit structures;
wenzelm
parents: 14647
diff changeset
   489
  | index_ast_tr' _ = raise Match;
5ad13d05049b improved indexed syntax / implicit structures;
wenzelm
parents: 14647
diff changeset
   490
52144
wenzelm
parents: 52143
diff changeset
   491
fun struct_ast_tr' structs =
wenzelm
parents: 52143
diff changeset
   492
  ("_struct", fn _ =>
wenzelm
parents: 52143
diff changeset
   493
    (fn [Ast.Constant "_indexdefault"] =>
wenzelm
parents: 52143
diff changeset
   494
        (case structs of
wenzelm
parents: 52143
diff changeset
   495
          x :: _ => Ast.Appl [Ast.Constant "_free", Ast.Variable x]
wenzelm
parents: 52143
diff changeset
   496
        | _ => raise Match)
wenzelm
parents: 52143
diff changeset
   497
      | _ => raise Match));
14697
5ad13d05049b improved indexed syntax / implicit structures;
wenzelm
parents: 14647
diff changeset
   498
5ad13d05049b improved indexed syntax / implicit structures;
wenzelm
parents: 14647
diff changeset
   499
5ad13d05049b improved indexed syntax / implicit structures;
wenzelm
parents: 14647
diff changeset
   500
5ad13d05049b improved indexed syntax / implicit structures;
wenzelm
parents: 14647
diff changeset
   501
(** Pure translations **)
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   502
52143
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   503
val pure_parse_ast_translation =
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   504
 [("_strip_positions", fn _ => strip_positions_ast_tr),
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   505
  ("_constify", fn _ => constify_ast_tr),
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   506
  ("_tapp", fn _ => tapp_ast_tr),
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   507
  ("_tappl", fn _ => tappl_ast_tr),
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   508
  ("_bracket", fn _ => bracket_ast_tr),
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   509
  ("_appl", fn _ => appl_ast_tr),
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   510
  ("_applC", fn _ => applC_ast_tr),
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   511
  ("_lambda", fn _ => lambda_ast_tr),
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   512
  ("_idtyp", fn _ => idtyp_ast_tr),
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   513
  ("_bigimpl", fn _ => bigimpl_ast_tr),
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   514
  ("_indexdefault", fn _ => indexdefault_ast_tr),
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   515
  ("_indexvar", fn _ => indexvar_ast_tr),
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   516
  ("_struct", fn _ => struct_ast_tr)];
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   517
52143
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   518
val pure_parse_translation =
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   519
 [("_abs", fn _ => abs_tr),
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   520
  ("_aprop", fn _ => aprop_tr),
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   521
  ("_ofclass", fn _ => ofclass_tr),
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   522
  ("_sort_constraint", fn _ => sort_constraint_tr),
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   523
  ("_TYPE", fn _ => type_tr),
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   524
  ("_DDDOT", fn _ => dddot_tr),
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   525
  ("_update_name", fn _ => update_name_tr),
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   526
  ("_index", fn _ => index_tr)];
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   527
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   528
val pure_print_ast_translation =
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   529
 [("\\<^type>fun", fn _ => fun_ast_tr'),
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   530
  ("_abs", fn _ => abs_ast_tr'),
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   531
  ("_idts", fn _ => idtyp_ast_tr' "_idts"),
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   532
  ("_pttrns", fn _ => idtyp_ast_tr' "_pttrns"),
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   533
  ("\\<^const>==>", fn _ => impl_ast_tr'),
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   534
  ("_index", fn _ => index_ast_tr')];
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 52043
diff changeset
   535
548
12208de7edfe added this file;
wenzelm
parents:
diff changeset
   536
end;
42284
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42278
diff changeset
   537
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42278
diff changeset
   538
structure Basic_Syntax_Trans: BASIC_SYNTAX_TRANS = Syntax_Trans;
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 42278
diff changeset
   539
open Basic_Syntax_Trans;