src/Pure/Syntax/sextension.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 18 c9ec452ff08f
permissions -rw-r--r--
Initial revision
clasohm@0
     1
(*  Title:      Pure/Syntax/sextension
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
clasohm@0
     4
clasohm@0
     5
Syntax extensions: mixfix declarations, syntax rules, infixes, binders and
clasohm@0
     6
the Pure syntax.
clasohm@0
     7
clasohm@0
     8
Changes:
clasohm@0
     9
  SEXTENSION: added Ast, xrule
clasohm@0
    10
  changed sext
clasohm@0
    11
  added ast_to_term
clasohm@0
    12
  ext_of_sext: added xconsts
clasohm@0
    13
  SEXTENSION1: added empty_sext, appl_ast_tr'
clasohm@0
    14
  SEXTENSION1: removed appl_tr'
clasohm@0
    15
TODO:
clasohm@0
    16
*)
clasohm@0
    17
clasohm@0
    18
clasohm@0
    19
infix |-> <-| <->;
clasohm@0
    20
clasohm@0
    21
signature SEXTENSION0 =
clasohm@0
    22
sig
clasohm@0
    23
  structure Ast: AST
clasohm@0
    24
  local open Ast in
clasohm@0
    25
    datatype mixfix =
clasohm@0
    26
      Mixfix of string * string * string * int list * int |
clasohm@0
    27
      Delimfix of string * string * string |
clasohm@0
    28
      Infixl of string * string * int |
clasohm@0
    29
      Infixr of string * string * int |
clasohm@0
    30
      Binder of string * string * string * int * int |
clasohm@0
    31
      TInfixl of string * string * int |
clasohm@0
    32
      TInfixr of string * string * int
clasohm@0
    33
    datatype xrule =
clasohm@0
    34
      op |-> of (string * string) * (string * string) |
clasohm@0
    35
      op <-| of (string * string) * (string * string) |
clasohm@0
    36
      op <-> of (string * string) * (string * string)
clasohm@0
    37
    datatype sext =
clasohm@0
    38
      Sext of {
clasohm@0
    39
        mixfix: mixfix list,
clasohm@0
    40
        parse_translation: (string * (term list -> term)) list,
clasohm@0
    41
        print_translation: (string * (term list -> term)) list} |
clasohm@0
    42
      NewSext of {
clasohm@0
    43
        mixfix: mixfix list,
clasohm@0
    44
        xrules: xrule list,
clasohm@0
    45
        parse_ast_translation: (string * (ast list -> ast)) list,
clasohm@0
    46
        parse_preproc: (ast -> ast) option,
clasohm@0
    47
        parse_postproc: (ast -> ast) option,
clasohm@0
    48
        parse_translation: (string * (term list -> term)) list,
clasohm@0
    49
        print_translation: (string * (term list -> term)) list,
clasohm@0
    50
        print_preproc: (ast -> ast) option,
clasohm@0
    51
        print_postproc: (ast -> ast) option,
clasohm@0
    52
        print_ast_translation: (string * (ast list -> ast)) list}
clasohm@0
    53
    val eta_contract: bool ref
clasohm@0
    54
    val mk_binder_tr: string * string -> string * (term list -> term)
clasohm@0
    55
    val mk_binder_tr': string * string -> string * (term list -> term)
clasohm@0
    56
    val ndependent_tr: string -> term list -> term
clasohm@0
    57
    val dependent_tr': string * string -> term list -> term
clasohm@0
    58
    val max_pri: int
clasohm@0
    59
  end
clasohm@0
    60
end;
clasohm@0
    61
clasohm@0
    62
signature SEXTENSION1 =
clasohm@0
    63
sig
clasohm@0
    64
  include SEXTENSION0
clasohm@0
    65
  val empty_sext: sext
clasohm@0
    66
  val simple_sext: mixfix list -> sext
clasohm@0
    67
  val constants: sext -> (string list * string) list
clasohm@0
    68
  val pure_sext: sext
clasohm@0
    69
  val syntax_types: string list
clasohm@0
    70
  val constrainAbsC: string
clasohm@0
    71
end;
clasohm@0
    72
clasohm@0
    73
signature SEXTENSION =
clasohm@0
    74
sig
clasohm@0
    75
  include SEXTENSION1
clasohm@0
    76
  structure Extension: EXTENSION
clasohm@0
    77
  sharing Extension.XGram.Ast = Ast
clasohm@0
    78
  local open Extension Ast in
clasohm@0
    79
    val xrules_of: sext -> xrule list
clasohm@0
    80
    val abs_tr': term -> term
clasohm@0
    81
    val appl_ast_tr': ast * ast list -> ast
clasohm@0
    82
    val ext_of_sext: string list -> string list -> (string -> typ) -> sext -> ext
clasohm@0
    83
    val ast_to_term: (string -> (term list -> term) option) -> ast -> term
clasohm@0
    84
    val constrainIdtC: string
clasohm@0
    85
    val apropC: string
clasohm@0
    86
  end
clasohm@0
    87
end;
clasohm@0
    88
clasohm@0
    89
functor SExtensionFun(structure TypeExt: TYPE_EXT and Lexicon: LEXICON)(*: SEXTENSION *) = (* FIXME *)
clasohm@0
    90
struct
clasohm@0
    91
clasohm@0
    92
structure Extension = TypeExt.Extension;
clasohm@0
    93
structure Ast = Extension.XGram.Ast;
clasohm@0
    94
open Extension Ast;
clasohm@0
    95
clasohm@0
    96
clasohm@0
    97
(** datatype sext **)
clasohm@0
    98
clasohm@0
    99
datatype mixfix =
clasohm@0
   100
  Mixfix of string * string * string * int list * int |
clasohm@0
   101
  Delimfix of string * string * string |
clasohm@0
   102
  Infixl of string * string * int |
clasohm@0
   103
  Infixr of string * string * int |
clasohm@0
   104
  Binder of string * string * string * int * int |
clasohm@0
   105
  TInfixl of string * string * int |
clasohm@0
   106
  TInfixr of string * string * int;
clasohm@0
   107
clasohm@0
   108
datatype xrule =
clasohm@0
   109
  op |-> of (string * string) * (string * string) |
clasohm@0
   110
  op <-| of (string * string) * (string * string) |
clasohm@0
   111
  op <-> of (string * string) * (string * string);
clasohm@0
   112
clasohm@0
   113
datatype sext =
clasohm@0
   114
  Sext of {
clasohm@0
   115
    mixfix: mixfix list,
clasohm@0
   116
    parse_translation: (string * (term list -> term)) list,
clasohm@0
   117
    print_translation: (string * (term list -> term)) list} |
clasohm@0
   118
  NewSext of {
clasohm@0
   119
    mixfix: mixfix list,
clasohm@0
   120
    xrules: xrule list,
clasohm@0
   121
    parse_ast_translation: (string * (ast list -> ast)) list,
clasohm@0
   122
    parse_preproc: (ast -> ast) option,
clasohm@0
   123
    parse_postproc: (ast -> ast) option,
clasohm@0
   124
    parse_translation: (string * (term list -> term)) list,
clasohm@0
   125
    print_translation: (string * (term list -> term)) list,
clasohm@0
   126
    print_preproc: (ast -> ast) option,
clasohm@0
   127
    print_postproc: (ast -> ast) option,
clasohm@0
   128
    print_ast_translation: (string * (ast list -> ast)) list};
clasohm@0
   129
clasohm@0
   130
clasohm@0
   131
(* simple_sext *)
clasohm@0
   132
clasohm@0
   133
fun simple_sext mixfix =
clasohm@0
   134
  Sext {mixfix = mixfix, parse_translation = [], print_translation = []};
clasohm@0
   135
clasohm@0
   136
clasohm@0
   137
(* empty_sext *)
clasohm@0
   138
clasohm@0
   139
val empty_sext = simple_sext [];
clasohm@0
   140
clasohm@0
   141
clasohm@0
   142
(* sext_components *)
clasohm@0
   143
clasohm@0
   144
fun sext_components (Sext {mixfix, parse_translation, print_translation}) =
clasohm@0
   145
      {mixfix = mixfix,
clasohm@0
   146
        xrules = [],
clasohm@0
   147
        parse_ast_translation = [],
clasohm@0
   148
        parse_preproc = None,
clasohm@0
   149
        parse_postproc = None,
clasohm@0
   150
        parse_translation = parse_translation,
clasohm@0
   151
        print_translation = print_translation,
clasohm@0
   152
        print_preproc = None,
clasohm@0
   153
        print_postproc = None,
clasohm@0
   154
        print_ast_translation = []}
clasohm@0
   155
  | sext_components (NewSext cmps) = cmps;
clasohm@0
   156
clasohm@0
   157
clasohm@0
   158
(* mixfix_of *)
clasohm@0
   159
clasohm@0
   160
fun mixfix_of (Sext {mixfix, ...}) = mixfix
clasohm@0
   161
  | mixfix_of (NewSext {mixfix, ...}) = mixfix;
clasohm@0
   162
clasohm@0
   163
clasohm@0
   164
(* xrules_of *)
clasohm@0
   165
clasohm@0
   166
fun xrules_of (Sext _) = []
clasohm@0
   167
  | xrules_of (NewSext {xrules, ...}) = xrules;
clasohm@0
   168
clasohm@0
   169
clasohm@0
   170
clasohm@0
   171
(** parse translations **)
clasohm@0
   172
clasohm@0
   173
(* application *)
clasohm@0
   174
clasohm@0
   175
fun appl_ast_tr (*"_appl"*) [f, args] = Appl (f :: unfold_ast "_args" args)
clasohm@0
   176
  | appl_ast_tr (*"_appl"*) asts = raise_ast "appl_ast_tr" asts;
clasohm@0
   177
clasohm@0
   178
clasohm@0
   179
(* abstraction *)
clasohm@0
   180
clasohm@0
   181
fun idtyp_ast_tr (*"_idtyp"*) [x, ty] = Appl [Constant constrainC, x, ty]
clasohm@0
   182
  | idtyp_ast_tr (*"_idtyp"*) asts = raise_ast "idtyp_ast_tr" asts;
clasohm@0
   183
clasohm@0
   184
fun lambda_ast_tr (*"_lambda"*) [idts, body] =
clasohm@0
   185
      fold_ast_p "_%" (unfold_ast "_idts" idts, body)
clasohm@0
   186
  | lambda_ast_tr (*"_lambda"*) asts = raise_ast "lambda_ast_tr" asts;
clasohm@0
   187
clasohm@0
   188
fun abs_tr (*"_%"*) [Free (x, T), body] = absfree (x, T, body)
clasohm@0
   189
  | abs_tr (*"_%"*) (ts as [Const (c, _) $ Free (x, T) $ tT, body]) =
clasohm@0
   190
      if c = constrainC then
clasohm@0
   191
        Const ("_constrainAbs", dummyT) $ absfree (x, T, body) $ tT
clasohm@0
   192
      else raise (TERM ("abs_tr", ts))
clasohm@0
   193
  | abs_tr (*"_%"*) ts = raise (TERM ("abs_tr", ts));
clasohm@0
   194
clasohm@0
   195
clasohm@0
   196
(* binder *)  (* FIXME check *) (* FIXME check *)
clasohm@0
   197
clasohm@0
   198
fun mk_binder_tr (sy, name) =
clasohm@0
   199
  let
clasohm@0
   200
    val const = Const (name, dummyT);
clasohm@0
   201
clasohm@0
   202
    fun tr (Free (x, T), t) = const $ absfree (x, T, t)
clasohm@0
   203
      | tr (Const ("_idts", _) $ idt $ idts, t) = tr (idt, tr (idts, t))
clasohm@0
   204
      | tr (t1 as (Const (c, _) $ Free (x, T) $ tT), t) =   (* FIXME *)
clasohm@0
   205
          if c = constrainC then
clasohm@0
   206
            const $ (Const ("_constrainAbs", dummyT) $ absfree (x, T, t) $ tT)
clasohm@0
   207
          else raise (TERM ("binder_tr", [t1, t]))
clasohm@0
   208
      | tr (t1, t2) = raise (TERM ("binder_tr", [t1, t2]));
clasohm@0
   209
clasohm@0
   210
    fun binder_tr (*sy*) [idts, body] = tr (idts, body)
clasohm@0
   211
      | binder_tr (*sy*) ts = raise (TERM ("binder_tr", ts));
clasohm@0
   212
  in
clasohm@0
   213
    (sy, binder_tr)
clasohm@0
   214
  end;
clasohm@0
   215
clasohm@0
   216
clasohm@0
   217
(* atomic props *)
clasohm@0
   218
clasohm@0
   219
fun aprop_ast_tr (*"_aprop"*) [ast] = ast
clasohm@0
   220
  | aprop_ast_tr (*"_aprop"*) asts = raise_ast "aprop_ast_tr" asts;
clasohm@0
   221
clasohm@0
   222
clasohm@0
   223
(* meta implication *)
clasohm@0
   224
clasohm@0
   225
fun bigimpl_ast_tr (*"_bigimpl"*) [asms, concl] =
clasohm@0
   226
      fold_ast_p "==>" (unfold_ast "_asms" asms, concl)
clasohm@0
   227
  | bigimpl_ast_tr (*"_bigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts;
clasohm@0
   228
clasohm@0
   229
clasohm@0
   230
(* 'dependent' type operators *)
clasohm@0
   231
clasohm@0
   232
fun ndependent_tr q [A, B] =
clasohm@0
   233
      Const (q, dummyT) $ A $ Abs ("x", dummyT, incr_boundvars 1 B)
clasohm@0
   234
  | ndependent_tr _ _ = raise Match;
clasohm@0
   235
clasohm@0
   236
clasohm@0
   237
clasohm@0
   238
(** print translations **)
clasohm@0
   239
clasohm@0
   240
(* application *)
clasohm@0
   241
clasohm@0
   242
fun appl_ast_tr' (f, []) = raise_ast "appl_ast_tr'" [f]
clasohm@0
   243
  | appl_ast_tr' (f, args) = Appl [Constant "_appl", f, fold_ast "_args" args];
clasohm@0
   244
clasohm@0
   245
clasohm@0
   246
(* abstraction *)   (* FIXME check *)
clasohm@0
   247
clasohm@0
   248
fun strip_abss vars_of body_of tm =
clasohm@0
   249
  let
clasohm@0
   250
    val vars = vars_of tm;
clasohm@0
   251
    val body = body_of tm;
clasohm@0
   252
    val rev_new_vars = rename_wrt_term body vars;
clasohm@0
   253
  in
clasohm@0
   254
    (map Free (rev rev_new_vars),
clasohm@0
   255
      subst_bounds (map (fn (x, _) => Free (x, dummyT)) rev_new_vars, body))
clasohm@0
   256
  end;
clasohm@0
   257
clasohm@0
   258
(*do (partial) eta-contraction before printing*)
clasohm@0
   259
clasohm@0
   260
val eta_contract = ref false;
clasohm@0
   261
clasohm@0
   262
fun eta_contr tm =
clasohm@0
   263
  let
clasohm@0
   264
    fun eta_abs (Abs (a, T, t)) =
clasohm@0
   265
          (case eta_abs t of
clasohm@0
   266
            t' as (f $ u) =>
clasohm@0
   267
              (case eta_abs u of
clasohm@0
   268
                Bound 0 =>
clasohm@0
   269
                  if not (0 mem loose_bnos f) then incr_boundvars ~1 f
clasohm@0
   270
                  else Abs (a, T, t')
clasohm@0
   271
              | _ => Abs (a, T, t'))
clasohm@0
   272
          | t' => Abs (a, T, t'))
clasohm@0
   273
      | eta_abs t = t;
clasohm@0
   274
  in
clasohm@0
   275
    if ! eta_contract then eta_abs tm else tm
clasohm@0
   276
  end;
clasohm@0
   277
clasohm@0
   278
clasohm@0
   279
fun abs_tr' tm =
clasohm@0
   280
  foldr (fn (x, t) => Const ("_%", dummyT) $ x $ t)
clasohm@0
   281
    (strip_abss strip_abs_vars strip_abs_body (eta_contr tm));
clasohm@0
   282
clasohm@0
   283
clasohm@0
   284
fun lambda_ast_tr' (*"_%"*) asts =
clasohm@0
   285
  (case unfold_ast_p "_%" (Appl (Constant "_%" :: asts)) of
clasohm@0
   286
    ([], _) => raise_ast "lambda_ast_tr'" asts
clasohm@0
   287
  | (xs, body) => Appl [Constant "_lambda", fold_ast "_idts" xs, body]);
clasohm@0
   288
clasohm@0
   289
clasohm@0
   290
(* binder *) (* FIXME check *)
clasohm@0
   291
clasohm@0
   292
fun mk_binder_tr' (name, sy) =
clasohm@0
   293
  let
clasohm@0
   294
    fun mk_idts [] = raise Match    (*abort translation*)
clasohm@0
   295
      | mk_idts [idt] = idt
clasohm@0
   296
      | mk_idts (idt :: idts) = Const ("_idts", dummyT) $ idt $ mk_idts idts;
clasohm@0
   297
clasohm@0
   298
    fun tr' t =
clasohm@0
   299
      let
clasohm@0
   300
        val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t;
clasohm@0
   301
      in
clasohm@0
   302
        Const (sy, dummyT) $ mk_idts xs $ bd
clasohm@0
   303
      end;
clasohm@0
   304
clasohm@0
   305
    fun binder_tr' (*name*) (t :: ts) =
clasohm@0
   306
          list_comb (tr' (Const (name, dummyT) $ t), ts)
clasohm@0
   307
      | binder_tr' (*name*) [] = raise Match;
clasohm@0
   308
  in
clasohm@0
   309
    (name, binder_tr')
clasohm@0
   310
  end;
clasohm@0
   311
clasohm@0
   312
clasohm@0
   313
(* idts *)
clasohm@0
   314
clasohm@0
   315
fun idts_ast_tr' (*"_idts"*) [Appl [Constant c, x, ty], xs] =
clasohm@0
   316
      if c = constrainC then
clasohm@0
   317
        Appl [Constant "_idts", Appl [Constant "_idtyp", x, ty], xs]
clasohm@0
   318
      else raise Match
clasohm@0
   319
  | idts_ast_tr' (*"_idts"*) _ = raise Match;
clasohm@0
   320
clasohm@0
   321
clasohm@0
   322
(* meta implication *)
clasohm@0
   323
clasohm@0
   324
fun impl_ast_tr' (*"==>"*) asts =
clasohm@0
   325
  (case unfold_ast_p "==>" (Appl (Constant "==>" :: asts)) of
clasohm@0
   326
    (asms as (_ :: _ :: _), concl)
clasohm@0
   327
      => Appl [Constant "_bigimpl", fold_ast "_asms" asms, concl]
clasohm@0
   328
  | _ => raise Match);
clasohm@0
   329
clasohm@0
   330
clasohm@0
   331
(* 'dependent' type operators *)
clasohm@0
   332
clasohm@0
   333
fun dependent_tr' (q, r) [A, Abs (x, T, B)] =
clasohm@0
   334
      if 0 mem (loose_bnos B) then
clasohm@0
   335
        let val (x', B') = variant_abs (x, dummyT, B);
clasohm@0
   336
        in Const (q, dummyT) $ Free (x', T) $ A $ B' end
clasohm@0
   337
      else Const (r, dummyT) $ A $ B
clasohm@0
   338
  | dependent_tr' _ _ = raise Match;
clasohm@0
   339
clasohm@0
   340
clasohm@0
   341
clasohm@0
   342
(** constants **)
clasohm@0
   343
clasohm@0
   344
(* FIXME opn, clean: move *)
clasohm@0
   345
val clean =
clasohm@0
   346
  let
clasohm@0
   347
    fun q ("'" :: c :: cs) = c ^ q cs
clasohm@0
   348
      | q (c :: cs) = c ^ q cs
clasohm@0
   349
      | q ([]) = ""
clasohm@0
   350
  in q o explode end;
clasohm@0
   351
clasohm@0
   352
val opn = "op ";
clasohm@0
   353
clasohm@0
   354
clasohm@0
   355
fun constants sext =
clasohm@0
   356
  let
clasohm@0
   357
    fun consts (Delimfix (_, ty, c)) = ([c], ty)
clasohm@0
   358
      | consts (Mixfix (_, ty, c, _, _)) = ([c], ty)
clasohm@0
   359
      | consts (Infixl (c, ty, _)) = ([opn ^ clean c], ty)
clasohm@0
   360
      | consts (Infixr (c, ty, _)) = ([opn ^ clean c], ty)
clasohm@0
   361
      | consts (Binder (_, ty, c, _, _)) = ([c], ty)
clasohm@0
   362
      | consts _ = ([""], "");    (*is filtered out below*)
clasohm@0
   363
  in
clasohm@0
   364
    distinct (filter_out (fn (l, _) => l = [""]) (map consts (mixfix_of sext)))
clasohm@0
   365
  end;
clasohm@0
   366
clasohm@0
   367
clasohm@0
   368
clasohm@0
   369
(** ext_of_sext **)   (* FIXME check, clean *)
clasohm@0
   370
clasohm@0
   371
fun ext_of_sext roots xconsts read_typ sext =
clasohm@0
   372
  let
clasohm@0
   373
    val
clasohm@0
   374
      {mixfix, parse_ast_translation, parse_preproc, parse_postproc,
clasohm@0
   375
        parse_translation, print_translation, print_preproc, print_postproc,
clasohm@0
   376
        print_ast_translation, ...} = sext_components sext;
clasohm@0
   377
clasohm@0
   378
    val infixT = [typeT, typeT] ---> typeT;
clasohm@0
   379
clasohm@0
   380
    fun binder (Binder (sy, _, name, _, _)) = Some (sy, name)
clasohm@0
   381
      | binder _ = None;
clasohm@0
   382
clasohm@0
   383
    fun binder_typ ty =
clasohm@0
   384
      (case read_typ ty of
clasohm@0
   385
        Type ("fun", [Type ("fun", [_, T2]), T3]) =>
clasohm@0
   386
          [Type ("idts", []), T2] ---> T3
clasohm@0
   387
      | _ => error (quote ty ^ " is not a valid binder type."));
clasohm@0
   388
clasohm@0
   389
    fun mfix_of (Mixfix (sy, ty, c, pl, p)) = [Mfix (sy, read_typ ty, c, pl, p)]
clasohm@0
   390
      | mfix_of (Delimfix (sy, ty, c)) = [Mfix (sy, read_typ ty, c, [], max_pri)]
clasohm@0
   391
      | mfix_of (Infixl (sy, ty, p)) =
clasohm@0
   392
          let val T = read_typ ty and c = opn ^ sy and c' = opn ^ clean sy
clasohm@0
   393
          in
clasohm@0
   394
            [Mfix (c, T, c', [], max_pri),
clasohm@0
   395
             Mfix("(_ " ^ sy ^ "/ _)", T, c', [p, p + 1], p)]
clasohm@0
   396
          end
clasohm@0
   397
      | mfix_of (Infixr (sy, ty, p)) =
clasohm@0
   398
          let val T = read_typ ty and c = opn ^ sy and c' = opn ^ clean sy
clasohm@0
   399
          in
clasohm@0
   400
            [Mfix(c, T, c', [], max_pri),
clasohm@0
   401
             Mfix("(_ " ^ sy ^ "/ _)", T, c', [p + 1, p], p)]
clasohm@0
   402
          end
clasohm@0
   403
      | mfix_of (Binder (sy, ty, _, p, q)) =
clasohm@0
   404
          [Mfix ("(3" ^ sy ^ "_./ _)", binder_typ ty, sy, [0, p], q)]
clasohm@0
   405
      | mfix_of (TInfixl (s, c, p)) =
clasohm@0
   406
          [Mfix ("(_ " ^ s ^ "/ _)", infixT, c, [p, p + 1], p)]
clasohm@0
   407
      | mfix_of (TInfixr (s, c, p)) =
clasohm@0
   408
          [Mfix ("(_ " ^ s ^ "/ _)", infixT, c, [p + 1, p], p)];
clasohm@0
   409
clasohm@0
   410
    val mfix = flat (map mfix_of mixfix);
clasohm@0
   411
    val mfix_consts = map (fn (Mfix (_, _, c, _, _)) => c) mfix;
clasohm@0
   412
    val bs = mapfilter binder mixfix;
clasohm@0
   413
    val bparses = map mk_binder_tr bs;
clasohm@0
   414
    val bprints = map (mk_binder_tr' o (fn (x, y) => (y, x))) bs;
clasohm@0
   415
  in
clasohm@0
   416
    Ext {
clasohm@0
   417
      roots = roots, mfix = mfix,
clasohm@0
   418
      extra_consts = distinct (filter Lexicon.is_identifier (xconsts @ mfix_consts)),
clasohm@0
   419
      parse_ast_translation = parse_ast_translation,
clasohm@0
   420
      parse_preproc = parse_preproc,
clasohm@0
   421
      parse_postproc = parse_postproc,
clasohm@0
   422
      parse_translation = bparses @ parse_translation,
clasohm@0
   423
      print_translation = bprints @ print_translation,
clasohm@0
   424
      print_preproc = print_preproc,
clasohm@0
   425
      print_postproc = print_postproc,
clasohm@0
   426
      print_ast_translation = print_ast_translation}
clasohm@0
   427
  end;
clasohm@0
   428
clasohm@0
   429
clasohm@0
   430
clasohm@0
   431
(** ast_to_term **)
clasohm@0
   432
clasohm@0
   433
fun ast_to_term trf ast =
clasohm@0
   434
  let
clasohm@0
   435
    fun scan_vname prfx cs =
clasohm@0
   436
      (case Lexicon.scan_varname cs of
clasohm@0
   437
        ((x, i), []) => Var ((prfx ^ x, i), dummyT)
clasohm@0
   438
      | _ => error ("ast_to_term: bad variable name " ^ quote (implode cs)));
clasohm@0
   439
clasohm@0
   440
    fun vname_to_var v =
clasohm@0
   441
      (case explode v of
clasohm@0
   442
        "?" :: "'" :: cs => scan_vname "'" cs
clasohm@0
   443
      | "?" :: cs => scan_vname "" cs
clasohm@0
   444
      | _ => Free (v, dummyT));
clasohm@0
   445
clasohm@0
   446
    fun trans a args =
clasohm@0
   447
      (case trf a of
clasohm@0
   448
        None => list_comb (Const (a, dummyT), args)
clasohm@0
   449
      | Some f => ((f args)
clasohm@0
   450
          handle _ => error ("ast_to_term: error in translation for " ^ quote a)));
clasohm@0
   451
clasohm@0
   452
    fun trav (Constant a) = trans a []
clasohm@0
   453
      | trav (Appl (Constant a :: (asts as _ :: _))) = trans a (map trav asts)
clasohm@0
   454
      | trav (Appl (ast :: (asts as _ :: _))) =
clasohm@0
   455
          list_comb (trav ast, map trav asts)
clasohm@0
   456
      | trav (ast as (Appl _)) = raise_ast "ast_to_term: malformed ast" [ast]
clasohm@0
   457
      | trav (Variable x) = vname_to_var x;
clasohm@0
   458
  in
clasohm@0
   459
    trav ast
clasohm@0
   460
  end;
clasohm@0
   461
clasohm@0
   462
clasohm@0
   463
clasohm@0
   464
(** the Pure syntax **)
clasohm@0
   465
clasohm@0
   466
val pure_sext =
clasohm@0
   467
  NewSext {
clasohm@0
   468
    mixfix = [
clasohm@0
   469
      Mixfix   ("(3%_./ _)",  "[idts, 'a] => ('b => 'a)",      "_lambda", [0], 0),
clasohm@0
   470
      Delimfix ("_",          "'a => " ^ args,                 ""),
clasohm@0
   471
      Delimfix ("_,/ _",      "['a, " ^ args ^ "] => " ^ args, "_args"),
clasohm@0
   472
      Delimfix ("_",          "id => idt",                     ""),
clasohm@0
   473
      Mixfix   ("_::_",       "[id, type] => idt",             "_idtyp", [0, 0], 0),
clasohm@0
   474
      Delimfix ("'(_')",      "idt => idt",                    ""),
clasohm@0
   475
      Delimfix ("_",          "idt => idts",                   ""),
clasohm@0
   476
      Mixfix   ("_/ _",       "[idt, idts] => idts",           "_idts", [1, 0], 0),
clasohm@0
   477
      Delimfix ("_",          "id => aprop",                   ""),
clasohm@0
   478
      Delimfix ("_",          "var => aprop",                  ""),
clasohm@0
   479
      Mixfix   ("_'(_')",     "[('b => 'a), " ^ args ^ "] => aprop", applC, [max_pri, 0], 0),
clasohm@0
   480
      Delimfix ("PROP _",     "aprop => prop",                 "_aprop"),
clasohm@0
   481
      Delimfix ("_",          "prop => asms",                  ""),
clasohm@0
   482
      Delimfix ("_;/ _",      "[prop, asms] => asms",          "_asms"),
clasohm@0
   483
      Mixfix   ("((3[| _ |]) ==>/ _)", "[asms, prop] => prop", "_bigimpl", [0, 1], 1),
clasohm@0
   484
      Mixfix   ("(_ ==/ _)",  "['a::{}, 'a] => prop",          "==", [3, 2], 2),
clasohm@0
   485
      Mixfix   ("(_ =?=/ _)", "['a::{}, 'a] => prop",          "=?=", [3, 2], 2),
clasohm@0
   486
      Mixfix   ("(_ ==>/ _)", "[prop, prop] => prop",          "==>", [2, 1], 1),
clasohm@0
   487
      Binder   ("!!",         "('a::logic => prop) => prop",   "all", 0, 0)],
clasohm@0
   488
    xrules = [],
clasohm@0
   489
    parse_ast_translation =
clasohm@0
   490
      [(applC, appl_ast_tr), ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr),
clasohm@0
   491
        ("_aprop", aprop_ast_tr), ("_bigimpl", bigimpl_ast_tr)],
clasohm@0
   492
    parse_preproc = None,
clasohm@0
   493
    parse_postproc = None,
clasohm@0
   494
    parse_translation = [("_%", abs_tr)],
clasohm@0
   495
    print_translation = [],
clasohm@0
   496
    print_preproc = None,
clasohm@0
   497
    print_postproc = None,
clasohm@0
   498
    print_ast_translation = [("_%", lambda_ast_tr'), ("_idts", idts_ast_tr'),
clasohm@0
   499
      ("==>", impl_ast_tr')]};
clasohm@0
   500
clasohm@0
   501
val syntax_types =    (* FIXME clean, check *)
clasohm@0
   502
  [logic, "aprop", args, "asms", id, "idt", "idts", tfree, tvar, "type", "types",
clasohm@0
   503
    var, "sort", "classes"]
clasohm@0
   504
clasohm@0
   505
val constrainIdtC = "_idtyp";
clasohm@0
   506
val constrainAbsC = "_constrainAbs";
clasohm@0
   507
val apropC = "_aprop";
clasohm@0
   508
clasohm@0
   509
clasohm@0
   510
end;
clasohm@0
   511