src/Pure/Syntax/sextension.ML
author wenzelm
Mon, 09 Nov 1998 15:42:08 +0100
changeset 5840 e2d2b896c717
parent 473 fdacecc688a1
permissions -rw-r--r--
Object logic specific operations.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
     1
(*  Title:      Pure/Syntax/sextension.ML
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
165
793be9f1e88e improved comments;
wenzelm
parents: 113
diff changeset
     5
Syntax extensions (external interface): mixfix declarations, infixes,
793be9f1e88e improved comments;
wenzelm
parents: 113
diff changeset
     6
binders, translation rules / functions and the Pure syntax.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
TODO:
238
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
     9
  move ast_to_term, pt_to_ast (?)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
infix |-> <-| <->;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
signature SEXTENSION0 =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
sig
238
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
    16
  structure Parser: PARSER
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
    17
  local open Parser.SynExt.Ast in
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
    datatype mixfix =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
      Mixfix of string * string * string * int list * int |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
      Delimfix of string * string * string |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
      Infixl of string * string * int |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
      Infixr of string * string * int |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
      Binder of string * string * string * int * int |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
      TInfixl of string * string * int |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
      TInfixr of string * string * int
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
    datatype xrule =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
      op |-> of (string * string) * (string * string) |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
      op <-| of (string * string) * (string * string) |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
      op <-> of (string * string) * (string * string)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
    datatype sext =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
      Sext of {
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
        mixfix: mixfix list,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
        parse_translation: (string * (term list -> term)) list,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
        print_translation: (string * (term list -> term)) list} |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
      NewSext of {
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
        mixfix: mixfix list,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
        xrules: xrule list,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
        parse_ast_translation: (string * (ast list -> ast)) list,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
        parse_translation: (string * (term list -> term)) list,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
        print_translation: (string * (term list -> term)) list,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
        print_ast_translation: (string * (ast list -> ast)) list}
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
    val eta_contract: bool ref
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
    val mk_binder_tr: string * string -> string * (term list -> term)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
    val mk_binder_tr': string * string -> string * (term list -> term)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
    val dependent_tr': string * string -> term list -> term
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
    val max_pri: int
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
  end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
signature SEXTENSION1 =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
  include SEXTENSION0
382
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
    53
  local open Parser.SynExt.Ast in
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
    54
    val empty_sext: sext
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
    55
    val simple_sext: mixfix list -> sext
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
    56
    val constants: sext -> (string list * string) list
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
    57
    val pure_sext: sext
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
    58
    val syntax_types: string list
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
    59
    val syntax_consts: (string list * string) list
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
    60
    val constrainAbsC: string
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
    61
    val pure_trfuns:
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
    62
      (string * (ast list -> ast)) list *
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
    63
      (string * (term list -> term)) list *
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
    64
      (string * (term list -> term)) list *
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
    65
      (string * (ast list -> ast)) list
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
    66
  end
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
signature SEXTENSION =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
  include SEXTENSION1
238
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
    72
  local open Parser Parser.SynExt Parser.SynExt.Ast in
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
    val xrules_of: sext -> xrule list
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
    val abs_tr': term -> term
382
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
    75
    val prop_tr': bool -> term -> term
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
    val appl_ast_tr': ast * ast list -> ast
330
2fda15dd1e0f changed the way a grammar is generated to allow the new parser to work;
clasohm
parents: 276
diff changeset
    77
    val syn_ext_of_sext: string list -> string list -> string list -> (string -> typ) -> sext -> syn_ext
238
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
    78
    val pt_to_ast: (string -> (ast list -> ast) option) -> parsetree -> ast
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
    val ast_to_term: (string -> (term list -> term) option) -> ast -> term
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
  end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
382
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
    83
functor SExtensionFun(structure TypeExt: TYPE_EXT and Parser: PARSER
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
    84
  sharing TypeExt.SynExt = Parser.SynExt): SEXTENSION =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
238
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
    87
structure Parser = Parser;
382
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
    88
open TypeExt Parser.Lexicon Parser.SynExt.Ast Parser.SynExt Parser;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
382
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
    91
(** datatype sext **)   (* FIXME remove *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
datatype mixfix =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
  Mixfix of string * string * string * int list * int |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
  Delimfix of string * string * string |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
  Infixl of string * string * int |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
  Infixr of string * string * int |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
  Binder of string * string * string * int * int |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
  TInfixl of string * string * int |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
  TInfixr of string * string * int;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
382
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   102
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   103
(* FIXME -> syntax.ML, BASIC_SYNTAX, SYNTAX *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
datatype xrule =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
  op |-> of (string * string) * (string * string) |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
  op <-| of (string * string) * (string * string) |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
  op <-> of (string * string) * (string * string);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
datatype sext =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
  Sext of {
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
    mixfix: mixfix list,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
    parse_translation: (string * (term list -> term)) list,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
    print_translation: (string * (term list -> term)) list} |
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
  NewSext of {
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
    mixfix: mixfix list,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
    xrules: xrule list,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
    parse_ast_translation: (string * (ast list -> ast)) list,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
    parse_translation: (string * (term list -> term)) list,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
    print_translation: (string * (term list -> term)) list,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
    print_ast_translation: (string * (ast list -> ast)) list};
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
(* simple_sext *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125
fun simple_sext mixfix =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   126
  Sext {mixfix = mixfix, parse_translation = [], print_translation = []};
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   127
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   128
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   129
(* empty_sext *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   130
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   131
val empty_sext = simple_sext [];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   132
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   133
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   134
(* sext_components *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   135
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   136
fun sext_components (Sext {mixfix, parse_translation, print_translation}) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   137
      {mixfix = mixfix,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   138
        xrules = [],
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   139
        parse_ast_translation = [],
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   140
        parse_translation = parse_translation,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   141
        print_translation = print_translation,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   142
        print_ast_translation = []}
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   143
  | sext_components (NewSext cmps) = cmps;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   144
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   145
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   146
(* mixfix_of *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   147
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   148
fun mixfix_of (Sext {mixfix, ...}) = mixfix
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   149
  | mixfix_of (NewSext {mixfix, ...}) = mixfix;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   150
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   151
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   152
(* xrules_of *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   153
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   154
fun xrules_of (Sext _) = []
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   155
  | xrules_of (NewSext {xrules, ...}) = xrules;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   156
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   157
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   158
382
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   159
(*** translation functions ***) (* FIXME -> trans.ML *)
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   160
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   161
fun const c = Const (c, dummyT);
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   162
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   163
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   164
(** parse (ast) translations **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   165
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   166
(* application *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   167
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   168
fun appl_ast_tr (*"_appl"*) [f, args] = Appl (f :: unfold_ast "_args" args)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   169
  | appl_ast_tr (*"_appl"*) asts = raise_ast "appl_ast_tr" asts;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   170
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   171
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   172
(* abstraction *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   173
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   174
fun idtyp_ast_tr (*"_idtyp"*) [x, ty] = Appl [Constant constrainC, x, ty]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   175
  | idtyp_ast_tr (*"_idtyp"*) asts = raise_ast "idtyp_ast_tr" asts;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   176
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   177
fun lambda_ast_tr (*"_lambda"*) [idts, body] =
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   178
      fold_ast_p "_abs" (unfold_ast "_idts" idts, body)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   179
  | lambda_ast_tr (*"_lambda"*) asts = raise_ast "lambda_ast_tr" asts;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   180
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   181
fun abs_tr (*"_abs"*) [Free (x, T), body] = absfree (x, T, body)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   182
  | abs_tr (*"_abs"*) (ts as [Const (c, _) $ Free (x, T) $ tT, body]) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   183
      if c = constrainC then
382
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   184
        const "_constrainAbs" $ absfree (x, T, body) $ tT
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   185
      else raise_term "abs_tr" ts
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   186
  | abs_tr (*"_abs"*) ts = raise_term "abs_tr" ts;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   187
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   188
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   189
(* nondependent abstraction *)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   190
276
4cf7139e5b7a changed "x" to "uu" for implicit name of the
lcp
parents: 272
diff changeset
   191
fun k_tr (*"_K"*) [t] = Abs ("uu", dummyT, incr_boundvars 1 t)
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   192
  | k_tr (*"_K"*) ts = raise_term "k_tr" ts;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   193
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   194
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   195
(* binder *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   196
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   197
fun mk_binder_tr (sy, name) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   198
  let
382
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   199
    fun tr (Free (x, T), t) = const name $ absfree (x, T, t)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   200
      | tr (Const ("_idts", _) $ idt $ idts, t) = tr (idt, tr (idts, t))
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   201
      | tr (t1 as Const (c, _) $ Free (x, T) $ tT, t) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   202
          if c = constrainC then
382
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   203
            const name $ (const "_constrainAbs" $ absfree (x, T, t) $ tT)
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   204
          else raise_term "binder_tr" [t1, t]
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   205
      | tr (t1, t2) = raise_term "binder_tr" [t1, t2];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   206
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   207
    fun binder_tr (*sy*) [idts, body] = tr (idts, body)
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   208
      | binder_tr (*sy*) ts = raise_term "binder_tr" ts;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   209
  in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   210
    (sy, binder_tr)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   211
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   212
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   213
382
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   214
(* meta propositions *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   215
382
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   216
fun aprop_tr (*"_aprop"*) [t] = const constrainC $ t $ const "prop"
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   217
  | aprop_tr (*"_aprop"*) ts = raise_term "aprop_tr" ts;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   218
473
fdacecc688a1 minor internal renamings;
wenzelm
parents: 382
diff changeset
   219
fun ofclass_tr (*"_ofclass"*) [ty, cls] =
fdacecc688a1 minor internal renamings;
wenzelm
parents: 382
diff changeset
   220
      cls $ (const constrainC $ const "TYPE" $ (const "itself" $ ty))
fdacecc688a1 minor internal renamings;
wenzelm
parents: 382
diff changeset
   221
  | ofclass_tr (*"_ofclass"*) ts = raise_term "ofclass_tr" ts;
382
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   222
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   223
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   224
(* meta implication *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   225
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   226
fun bigimpl_ast_tr (*"_bigimpl"*) [asms, concl] =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   227
      fold_ast_p "==>" (unfold_ast "_asms" asms, concl)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   228
  | bigimpl_ast_tr (*"_bigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   229
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   230
259
9c648760dba3 added type 'syntax';
wenzelm
parents: 238
diff changeset
   231
(* explode atoms *)
238
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   232
272
0f6270bb9fe9 improved explode_tr;
wenzelm
parents: 259
diff changeset
   233
fun explode_tr (*"_explode"*) (ts as [consC, nilC, bit0, bit1, txt]) =
238
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   234
      let
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   235
        fun mk_list [] = nilC
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   236
          | mk_list (t :: ts) = consC $ t $ mk_list ts;
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   237
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   238
        fun encode_bit 0 = bit0
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   239
          | encode_bit 1 = bit1
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   240
          | encode_bit _ = sys_error "encode_bit";
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   241
259
9c648760dba3 added type 'syntax';
wenzelm
parents: 238
diff changeset
   242
        fun encode_char c =   (* FIXME leading 0s (?) *)
238
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   243
          mk_list (map encode_bit (radixpand (2, (ord c))));
272
0f6270bb9fe9 improved explode_tr;
wenzelm
parents: 259
diff changeset
   244
0f6270bb9fe9 improved explode_tr;
wenzelm
parents: 259
diff changeset
   245
        val str =
0f6270bb9fe9 improved explode_tr;
wenzelm
parents: 259
diff changeset
   246
          (case txt of
0f6270bb9fe9 improved explode_tr;
wenzelm
parents: 259
diff changeset
   247
            Free (s, _) => s
0f6270bb9fe9 improved explode_tr;
wenzelm
parents: 259
diff changeset
   248
          | Const (s, _) => s
0f6270bb9fe9 improved explode_tr;
wenzelm
parents: 259
diff changeset
   249
          | _ => raise_term "explode_tr" ts);
238
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   250
      in
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   251
        mk_list (map encode_char (explode str))
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   252
      end
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   253
  | explode_tr (*"_explode"*) ts = raise_term "explode_tr" ts;
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   254
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   255
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   256
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   257
(** print (ast) translations **)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   258
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   259
(* application *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   260
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   261
fun appl_ast_tr' (f, []) = raise_ast "appl_ast_tr'" [f]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   262
  | appl_ast_tr' (f, args) = Appl [Constant "_appl", f, fold_ast "_args" args];
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   263
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   264
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   265
(* abstraction *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   266
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   267
fun strip_abss vars_of body_of tm =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   268
  let
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   269
    fun free (x, _) = Free (x, dummyT);
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   270
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   271
    val vars = vars_of tm;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   272
    val body = body_of tm;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   273
    val rev_new_vars = rename_wrt_term body vars;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   274
  in
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   275
    (map Free (rev rev_new_vars), subst_bounds (map free rev_new_vars, body))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   276
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   277
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   278
(*do (partial) eta-contraction before printing*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   279
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   280
val eta_contract = ref false;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   281
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   282
fun eta_contr tm =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   283
  let
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   284
    fun eta_abs (Abs (a, T, t)) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   285
          (case eta_abs t of
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   286
            t' as f $ u =>
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   287
              (case eta_abs u of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   288
                Bound 0 =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   289
                  if not (0 mem loose_bnos f) then incr_boundvars ~1 f
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   290
                  else Abs (a, T, t')
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   291
              | _ => Abs (a, T, t'))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   292
          | t' => Abs (a, T, t'))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   293
      | eta_abs t = t;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   294
  in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   295
    if ! eta_contract then eta_abs tm else tm
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   296
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   297
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   298
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   299
fun abs_tr' tm =
382
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   300
  foldr (fn (x, t) => const "_abs" $ x $ t)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   301
    (strip_abss strip_abs_vars strip_abs_body (eta_contr tm));
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   302
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   303
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   304
fun abs_ast_tr' (*"_abs"*) asts =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   305
  (case unfold_ast_p "_abs" (Appl (Constant "_abs" :: asts)) of
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   306
    ([], _) => raise_ast "abs_ast_tr'" asts
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   307
  | (xs, body) => Appl [Constant "_lambda", fold_ast "_idts" xs, body]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   308
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   309
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   310
(* binder *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   311
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   312
fun mk_binder_tr' (name, sy) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   313
  let
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   314
    fun mk_idts [] = raise Match    (*abort translation*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   315
      | mk_idts [idt] = idt
382
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   316
      | mk_idts (idt :: idts) = const "_idts" $ idt $ mk_idts idts;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   317
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   318
    fun tr' t =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   319
      let
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   320
        val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   321
      in
382
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   322
        const sy $ mk_idts xs $ bd
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   323
      end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   324
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   325
    fun binder_tr' (*name*) (t :: ts) =
382
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   326
          list_comb (tr' (const name $ t), ts)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   327
      | binder_tr' (*name*) [] = raise Match;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   328
  in
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   329
    (name, binder_tr')
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   330
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   331
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   332
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   333
(* idts *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   334
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   335
fun idts_ast_tr' (*"_idts"*) [Appl [Constant c, x, ty], xs] =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   336
      if c = constrainC then
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   337
        Appl [Constant "_idts", Appl [Constant "_idtyp", x, ty], xs]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   338
      else raise Match
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   339
  | idts_ast_tr' (*"_idts"*) _ = raise Match;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   340
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   341
382
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   342
(* meta propositions *)
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   343
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   344
fun prop_tr' show_sorts tm =
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   345
  let
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   346
    fun aprop t = const "_aprop" $ t;
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   347
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   348
    fun is_prop tys t =
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   349
      fastype_of1 (tys, t) = propT handle TERM _ => false;
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   350
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   351
    fun tr' _ (t as Const _) = t
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   352
      | tr' _ (t as Free (x, ty)) =
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   353
          if ty = propT then aprop (Free (x, dummyT)) else t
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   354
      | tr' _ (t as Var (xi, ty)) =
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   355
          if ty = propT then aprop (Var (xi, dummyT)) else t
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   356
      | tr' tys (t as Bound _) =
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   357
          if is_prop tys t then aprop t else t
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   358
      | tr' tys (Abs (x, ty, t)) = Abs (x, ty, tr' (ty :: tys) t)
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   359
      | tr' tys (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [ty])))) =
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   360
          if is_prop tys t then
473
fdacecc688a1 minor internal renamings;
wenzelm
parents: 382
diff changeset
   361
            const "_ofclass" $ term_of_typ show_sorts ty $ tr' tys t1
382
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   362
          else tr' tys t1 $ tr' tys t2
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   363
      | tr' tys (t as t1 $ t2) =
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   364
          (if is_Const (head_of t) orelse not (is_prop tys t)
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   365
            then I else aprop) (tr' tys t1 $ tr' tys t2);
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   366
  in
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   367
    tr' [] tm
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   368
  end;
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   369
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   370
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   371
(* meta implication *)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   372
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   373
fun impl_ast_tr' (*"==>"*) asts =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   374
  (case unfold_ast_p "==>" (Appl (Constant "==>" :: asts)) of
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   375
    (asms as _ :: _ :: _, concl)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   376
      => Appl [Constant "_bigimpl", fold_ast "_asms" asms, concl]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   377
  | _ => raise Match);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   378
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   379
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   380
(* dependent / nondependent quantifiers *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   381
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   382
fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   383
      if 0 mem (loose_bnos B) then
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   384
        let val (x', B') = variant_abs (x, dummyT, B);
382
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   385
        in list_comb (const q $ Free (x', T) $ A $ B', ts) end
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   386
      else list_comb (const r $ A $ B, ts)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   387
  | dependent_tr' _ _ = raise Match;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   388
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   389
259
9c648760dba3 added type 'syntax';
wenzelm
parents: 238
diff changeset
   390
(* implode atoms *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   391
238
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   392
fun implode_ast_tr' (*"_implode"*) (asts as [Constant cons_name, nilC,
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   393
    bit0, bit1, bitss]) =
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   394
      let
259
9c648760dba3 added type 'syntax';
wenzelm
parents: 238
diff changeset
   395
        fun err () = raise_ast "implode_ast_tr'" asts;
238
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   396
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   397
        fun strip_list lst =
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   398
          let val (xs, y) = unfold_ast_p cons_name lst
259
9c648760dba3 added type 'syntax';
wenzelm
parents: 238
diff changeset
   399
          in if y = nilC then xs else err ()
238
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   400
          end;
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   401
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   402
        fun decode_bit bit =
259
9c648760dba3 added type 'syntax';
wenzelm
parents: 238
diff changeset
   403
          if bit = bit0 then "0"
9c648760dba3 added type 'syntax';
wenzelm
parents: 238
diff changeset
   404
          else if bit = bit1 then "1"
9c648760dba3 added type 'syntax';
wenzelm
parents: 238
diff changeset
   405
          else err ();
238
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   406
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   407
        fun decode_char bits =
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   408
          chr (#1 (scan_radixint (2, map decode_bit (strip_list bits))));
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   409
      in
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   410
        Variable (implode (map decode_char (strip_list bitss)))
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   411
      end
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   412
  | implode_ast_tr' (*"_implode"*) asts = raise_ast "implode_ast_tr'" asts;
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   413
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   414
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   415
382
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   416
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   417
(** syn_ext_of_sext **)   (* FIXME remove *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   418
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   419
fun strip_esc str =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   420
  let
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   421
    fun strip ("'" :: c :: cs) = c :: strip cs
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   422
      | strip ["'"] = []
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   423
      | strip (c :: cs) = c :: strip cs
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   424
      | strip [] = [];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   425
  in
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   426
    implode (strip (explode str))
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   427
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   428
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   429
fun infix_name sy = "op " ^ strip_esc sy;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   430
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   431
330
2fda15dd1e0f changed the way a grammar is generated to allow the new parser to work;
clasohm
parents: 276
diff changeset
   432
fun syn_ext_of_sext all_roots new_roots xconsts read_typ sext =
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   433
  let
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   434
    val {mixfix, parse_ast_translation, parse_translation, print_translation,
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   435
      print_ast_translation, ...} = sext_components sext;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   436
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   437
    val tinfixT = [typeT, typeT] ---> typeT;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   438
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   439
    fun binder (Binder (sy, _, name, _, _)) = Some (sy, name)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   440
      | binder _ = None;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   441
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   442
    fun binder_typ ty =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   443
      (case read_typ ty of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   444
        Type ("fun", [Type ("fun", [_, T2]), T3]) =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   445
          [Type ("idts", []), T2] ---> T3
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   446
      | _ => error ("Illegal binder type " ^ quote ty));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   447
238
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   448
    fun mk_infix sy ty c p1 p2 p3 =
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   449
      [Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3),
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   450
       Mfix ("op " ^ sy, ty, c, [], max_pri)];
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   451
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   452
    fun mfix_of (Mixfix (sy, ty, c, ps, p)) = [Mfix (sy, read_typ ty, c, ps, p)]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   453
      | mfix_of (Delimfix (sy, ty, c)) = [Mfix (sy, read_typ ty, c, [], max_pri)]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   454
      | mfix_of (Infixl (sy, ty, p)) =
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   455
          mk_infix sy (read_typ ty) (infix_name sy) p (p + 1) p
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   456
      | mfix_of (Infixr (sy, ty, p)) =
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   457
          mk_infix sy (read_typ ty) (infix_name sy) (p + 1) p p
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   458
      | mfix_of (Binder (sy, ty, _, p, q)) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   459
          [Mfix ("(3" ^ sy ^ "_./ _)", binder_typ ty, sy, [0, p], q)]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   460
      | mfix_of (TInfixl (s, c, p)) =
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   461
          [Mfix ("(_ " ^ s ^ "/ _)", tinfixT, c, [p, p + 1], p)]
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   462
      | mfix_of (TInfixr (s, c, p)) =
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   463
          [Mfix ("(_ " ^ s ^ "/ _)", tinfixT, c, [p + 1, p], p)];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   464
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   465
    val mfix = flat (map mfix_of mixfix);
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   466
    val binders = mapfilter binder mixfix;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   467
    val bparses = map mk_binder_tr binders;
238
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   468
    val bprints = map (mk_binder_tr' o swap) binders;
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   469
  in
330
2fda15dd1e0f changed the way a grammar is generated to allow the new parser to work;
clasohm
parents: 276
diff changeset
   470
    syn_ext all_roots new_roots mfix (distinct (filter is_xid xconsts))
238
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   471
      (parse_ast_translation,
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   472
        bparses @ parse_translation,
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   473
        bprints @ print_translation,
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   474
        print_ast_translation)
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   475
      ([], [])
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   476
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   477
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   478
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   479
382
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   480
(** constants **)     (* FIXME remove *)
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   481
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   482
fun constants sext =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   483
  let
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   484
    fun consts (Delimfix (_, ty, c)) = ([c], ty)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   485
      | consts (Mixfix (_, ty, c, _, _)) = ([c], ty)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   486
      | consts (Infixl (c, ty, _)) = ([infix_name c], ty)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   487
      | consts (Infixr (c, ty, _)) = ([infix_name c], ty)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   488
      | consts (Binder (_, ty, c, _, _)) = ([c], ty)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   489
      | consts _ = ([""], "");    (*is filtered out below*)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   490
  in
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   491
    distinct (filter_out (fn (l, _) => l = [""]) (map consts (mixfix_of sext)))
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   492
  end;
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   493
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   494
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   495
238
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   496
(** pt_to_ast **)
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   497
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   498
fun pt_to_ast trf pt =
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   499
  let
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   500
    fun trans a args =
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   501
      (case trf a of
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   502
        None => mk_appl (Constant a) args
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   503
      | Some f => f args handle exn
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   504
          => (writeln ("Error in parse ast translation for " ^ quote a); raise exn));
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   505
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   506
    fun ast_of (Node (a, pts)) = trans a (map ast_of pts)
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   507
      | ast_of (Tip tok) = Variable (str_of_token tok);
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   508
  in
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   509
    ast_of pt
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   510
  end;
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   511
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   512
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   513
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   514
(** ast_to_term **)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   515
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   516
fun ast_to_term trf ast =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   517
  let
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   518
    fun trans a args =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   519
      (case trf a of
382
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   520
        None => list_comb (const a, args)
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   521
      | Some f => f args handle exn
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   522
          => (writeln ("Error in parse translation for " ^ quote a); raise exn));
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   523
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   524
    fun term_of (Constant a) = trans a []
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   525
      | term_of (Variable x) = scan_var x
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   526
      | term_of (Appl (Constant a :: (asts as _ :: _))) =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   527
          trans a (map term_of asts)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   528
      | term_of (Appl (ast :: (asts as _ :: _))) =
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   529
          list_comb (term_of ast, map term_of asts)
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   530
      | term_of (ast as Appl _) = raise_ast "ast_to_term: malformed ast" [ast];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   531
  in
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   532
    term_of ast
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   533
  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   534
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   535
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   536
382
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   537
(** pure_trfuns **)
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   538
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   539
val pure_trfuns =
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   540
 ([(applC, appl_ast_tr), ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr),
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   541
    ("_bigimpl", bigimpl_ast_tr)],
473
fdacecc688a1 minor internal renamings;
wenzelm
parents: 382
diff changeset
   542
  [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),
fdacecc688a1 minor internal renamings;
wenzelm
parents: 382
diff changeset
   543
    ("_K", k_tr), ("_explode", explode_tr)],
382
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   544
  [],
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   545
  [("_abs", abs_ast_tr'), ("_idts", idts_ast_tr'), ("==>", impl_ast_tr'),
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   546
    ("_implode", implode_ast_tr')]);
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   547
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   548
val constrainAbsC = "_constrainAbs";
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   549
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   550
2d876467663b added insort_tr, prop_tr' (for axclasses);
wenzelm
parents: 330
diff changeset
   551
(** the Pure syntax **)   (* FIXME remove *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   552
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   553
val pure_sext =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   554
  NewSext {
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   555
    mixfix = [
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   556
      Mixfix   ("(3%_./ _)",  "[idts, 'a] => ('b => 'a)",      "_lambda", [0], 0),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   557
      Delimfix ("_",          "'a => " ^ args,                 ""),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   558
      Delimfix ("_,/ _",      "['a, " ^ args ^ "] => " ^ args, "_args"),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   559
      Delimfix ("_",          "id => idt",                     ""),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   560
      Mixfix   ("_::_",       "[id, type] => idt",             "_idtyp", [0, 0], 0),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   561
      Delimfix ("'(_')",      "idt => idt",                    ""),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   562
      Delimfix ("_",          "idt => idts",                   ""),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   563
      Mixfix   ("_/ _",       "[idt, idts] => idts",           "_idts", [1, 0], 0),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   564
      Delimfix ("_",          "id => aprop",                   ""),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   565
      Delimfix ("_",          "var => aprop",                  ""),
272
0f6270bb9fe9 improved explode_tr;
wenzelm
parents: 259
diff changeset
   566
      Mixfix   ("(1_/(1'(_')))", "[('b => 'a), " ^ args ^ "] => aprop", applC, [max_pri, 0], max_pri),
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   567
      Delimfix ("PROP _",     "aprop => prop",                 "_aprop"),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   568
      Delimfix ("_",          "prop => asms",                  ""),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   569
      Delimfix ("_;/ _",      "[prop, asms] => asms",          "_asms"),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   570
      Mixfix   ("((3[| _ |]) ==>/ _)", "[asms, prop] => prop", "_bigimpl", [0, 1], 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   571
      Mixfix   ("(_ ==/ _)",  "['a::{}, 'a] => prop",          "==", [3, 2], 2),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   572
      Mixfix   ("(_ =?=/ _)", "['a::{}, 'a] => prop",          "=?=", [3, 2], 2),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   573
      Mixfix   ("(_ ==>/ _)", "[prop, prop] => prop",          "==>", [2, 1], 1),
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   574
      Binder   ("!!",         "('a::logic => prop) => prop",   "all", 0, 0)],
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   575
    xrules = [],
238
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   576
    parse_ast_translation = [(applC, appl_ast_tr), ("_lambda", lambda_ast_tr),
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   577
      ("_idtyp", idtyp_ast_tr), ("_bigimpl", bigimpl_ast_tr)],
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   578
    parse_translation = [("_abs", abs_tr), ("_aprop", aprop_tr), ("_K", k_tr),
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   579
      ("_explode", explode_tr)],
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   580
    print_translation = [],
18
c9ec452ff08f lots of internal cleaning and tuning;
wenzelm
parents: 0
diff changeset
   581
    print_ast_translation = [("_abs", abs_ast_tr'), ("_idts", idts_ast_tr'),
238
6af40e3a2bcb MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents: 165
diff changeset
   582
      ("==>", impl_ast_tr'), ("_implode", implode_ast_tr')]};
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   583
259
9c648760dba3 added type 'syntax';
wenzelm
parents: 238
diff changeset
   584
val syntax_types = terminals @ ["syntax", logic, "type", "types", "sort",
9c648760dba3 added type 'syntax';
wenzelm
parents: 238
diff changeset
   585
  "classes", args, "idt", "idts", "aprop", "asms"];
9c648760dba3 added type 'syntax';
wenzelm
parents: 238
diff changeset
   586
9c648760dba3 added type 'syntax';
wenzelm
parents: 238
diff changeset
   587
val syntax_consts = [(["_K", "_explode", "_implode"], "syntax")];
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   588
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   589
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   590
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   591