src/Pure/Syntax/type_ext.ML
author wenzelm
Tue Mar 22 15:32:47 2011 +0100 (2011-03-22)
changeset 42052 34f1d2d81284
parent 42050 5a505dfec04e
child 42053 006095137a81
permissions -rw-r--r--
statespace syntax: strip positions -- type constraints are unexpected here;
wenzelm@18
     1
(*  Title:      Pure/Syntax/type_ext.ML
clasohm@0
     2
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
clasohm@0
     3
wenzelm@35429
     4
Utilities for input and output of types.  The concrete syntax of types.
clasohm@0
     5
*)
clasohm@0
     6
clasohm@0
     7
signature TYPE_EXT0 =
wenzelm@2584
     8
sig
wenzelm@35429
     9
  val sort_of_term: term -> sort
wenzelm@35429
    10
  val term_sorts: term -> (indexname * sort) list
wenzelm@35429
    11
  val typ_of_term: (indexname -> sort) -> term -> typ
wenzelm@42050
    12
  val strip_positions: term -> term
wenzelm@42052
    13
  val strip_positions_ast: Ast.ast -> Ast.ast
wenzelm@22764
    14
  val decode_term: (((string * int) * sort) list -> string * int -> sort) ->
wenzelm@35429
    15
    (string -> bool * string) -> (string -> string option) -> term -> term
wenzelm@6901
    16
  val term_of_typ: bool -> typ -> term
wenzelm@10572
    17
  val no_brackets: unit -> bool
wenzelm@16614
    18
  val no_type_brackets: unit -> bool
wenzelm@35668
    19
  val type_ast_trs:
wenzelm@35668
    20
   {read_class: Proof.context -> string -> string,
wenzelm@35668
    21
    read_type: Proof.context -> string -> string} ->
wenzelm@35668
    22
    (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
wenzelm@2584
    23
end;
clasohm@0
    24
clasohm@0
    25
signature TYPE_EXT =
wenzelm@2584
    26
sig
clasohm@0
    27
  include TYPE_EXT0
wenzelm@2584
    28
  val term_of_sort: sort -> term
paulson@1511
    29
  val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
wenzelm@8895
    30
  val sortT: typ
wenzelm@37216
    31
  val type_ext: Syn_Ext.syn_ext
wenzelm@2584
    32
end;
clasohm@0
    33
wenzelm@37216
    34
structure Type_Ext: TYPE_EXT =
clasohm@0
    35
struct
wenzelm@2584
    36
wenzelm@2584
    37
(** input utils **)
clasohm@0
    38
wenzelm@8895
    39
(* sort_of_term *)
wenzelm@2584
    40
wenzelm@35429
    41
fun sort_of_term tm =
wenzelm@557
    42
  let
wenzelm@35429
    43
    fun err () = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
wenzelm@35429
    44
wenzelm@35429
    45
    fun class s = Lexicon.unmark_class s handle Fail _ => err ();
wenzelm@35429
    46
wenzelm@35429
    47
    fun classes (Const (s, _)) = [class s]
wenzelm@35429
    48
      | classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs
wenzelm@35429
    49
      | classes _ = err ();
clasohm@0
    50
wenzelm@2584
    51
    fun sort (Const ("_topsort", _)) = []
wenzelm@35429
    52
      | sort (Const (s, _)) = [class s]
wenzelm@3778
    53
      | sort (Const ("_sort", _) $ cs) = classes cs
wenzelm@35429
    54
      | sort _ = err ();
wenzelm@35429
    55
  in sort tm end;
wenzelm@8895
    56
wenzelm@2584
    57
wenzelm@22704
    58
(* term_sorts *)
wenzelm@8895
    59
wenzelm@35429
    60
fun term_sorts tm =
wenzelm@8895
    61
  let
wenzelm@35429
    62
    val sort_of = sort_of_term;
wenzelm@22704
    63
wenzelm@22704
    64
    fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) =
wenzelm@22704
    65
          insert (op =) ((x, ~1), sort_of cs)
wenzelm@22704
    66
      | add_env (Const ("_ofsort", _) $ (Const ("_tfree", _) $ Free (x, _)) $ cs) =
wenzelm@22704
    67
          insert (op =) ((x, ~1), sort_of cs)
wenzelm@22704
    68
      | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) =
wenzelm@22704
    69
          insert (op =) (xi, sort_of cs)
wenzelm@22704
    70
      | add_env (Const ("_ofsort", _) $ (Const ("_tvar", _) $ Var (xi, _)) $ cs) =
wenzelm@22704
    71
          insert (op =) (xi, sort_of cs)
wenzelm@22704
    72
      | add_env (Abs (_, _, t)) = add_env t
wenzelm@22704
    73
      | add_env (t1 $ t2) = add_env t1 #> add_env t2
wenzelm@22704
    74
      | add_env _ = I;
wenzelm@8895
    75
  in add_env tm [] end;
wenzelm@557
    76
wenzelm@557
    77
wenzelm@2584
    78
(* typ_of_term *)
clasohm@0
    79
wenzelm@35429
    80
fun typ_of_term get_sort tm =
wenzelm@557
    81
  let
wenzelm@35429
    82
    fun err () = raise TERM ("typ_of_term: bad encoding of type", [tm]);
wenzelm@35429
    83
wenzelm@35429
    84
    fun typ_of (Free (x, _)) = TFree (x, get_sort (x, ~1))
wenzelm@557
    85
      | typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
wenzelm@32784
    86
      | typ_of (Const ("_tfree",_) $ (t as Free _)) = typ_of t
wenzelm@32784
    87
      | typ_of (Const ("_tvar",_) $ (t as Var _)) = typ_of t
wenzelm@12317
    88
      | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = TFree (x, get_sort (x, ~1))
wenzelm@16614
    89
      | typ_of (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ _) =
wenzelm@16614
    90
          TFree (x, get_sort (x, ~1))
wenzelm@12317
    91
      | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi)
wenzelm@16614
    92
      | typ_of (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ _) =
wenzelm@16614
    93
          TVar (xi, get_sort xi)
wenzelm@35429
    94
      | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", sort_of_term t)
wenzelm@35429
    95
      | typ_of t =
clasohm@0
    96
          let
wenzelm@35429
    97
            val (head, args) = Term.strip_comb t;
clasohm@0
    98
            val a =
wenzelm@35429
    99
              (case head of
wenzelm@35429
   100
                Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ())
wenzelm@35429
   101
              | _ => err ());
wenzelm@35429
   102
          in Type (a, map typ_of args) end;
wenzelm@35429
   103
  in typ_of tm end;
clasohm@0
   104
clasohm@0
   105
wenzelm@42050
   106
(* positions *)
wenzelm@22704
   107
wenzelm@42048
   108
fun is_position (Free (x, _)) = is_some (Lexicon.decode_position x)
wenzelm@42048
   109
  | is_position _ = false;
wenzelm@42048
   110
wenzelm@42050
   111
fun strip_positions ((t as Const (c, _)) $ u $ v) =
wenzelm@42050
   112
      if (c = "_constrain" orelse c = "_constrainAbs") andalso is_position v
wenzelm@42050
   113
      then strip_positions u
wenzelm@42050
   114
      else t $ strip_positions u $ strip_positions v
wenzelm@42050
   115
  | strip_positions (t $ u) = strip_positions t $ strip_positions u
wenzelm@42050
   116
  | strip_positions (Abs (x, T, t)) = Abs (x, T, strip_positions t)
wenzelm@42050
   117
  | strip_positions t = t;
wenzelm@42050
   118
wenzelm@42052
   119
fun strip_positions_ast (Ast.Appl ((t as Ast.Constant c) :: u :: (v as Ast.Variable x) :: asts)) =
wenzelm@42052
   120
      if (c = "_constrain" orelse c = "_constrainAbs") andalso is_some (Lexicon.decode_position x)
wenzelm@42052
   121
      then Ast.mk_appl (strip_positions_ast u) (map strip_positions_ast asts)
wenzelm@42052
   122
      else Ast.Appl (map strip_positions_ast (t :: u :: v :: asts))
wenzelm@42052
   123
  | strip_positions_ast (Ast.Appl asts) = Ast.Appl (map strip_positions_ast asts)
wenzelm@42052
   124
  | strip_positions_ast ast = ast;
wenzelm@42052
   125
wenzelm@42050
   126
wenzelm@42050
   127
(* decode_term -- transform parse tree into raw term *)
wenzelm@42050
   128
wenzelm@35429
   129
fun decode_term get_sort map_const map_free tm =
wenzelm@22704
   130
  let
wenzelm@36448
   131
    val decodeT = typ_of_term (get_sort (term_sorts tm));
wenzelm@22704
   132
wenzelm@22704
   133
    fun decode (Const ("_constrain", _) $ t $ typ) =
wenzelm@42048
   134
          if is_position typ then decode t
wenzelm@42048
   135
          else Type.constraint (decodeT typ) (decode t)
wenzelm@42048
   136
      | decode (Const ("_constrainAbs", _) $ t $ typ) =
wenzelm@42048
   137
          if is_position typ then decode t
wenzelm@42048
   138
          else Type.constraint (decodeT typ --> dummyT) (decode t)
wenzelm@35429
   139
      | decode (Abs (x, T, t)) = Abs (x, T, decode t)
wenzelm@22704
   140
      | decode (t $ u) = decode t $ decode u
wenzelm@22704
   141
      | decode (Const (a, T)) =
wenzelm@36502
   142
          (case try Lexicon.unmark_fixed a of
wenzelm@36502
   143
            SOME x => Free (x, T)
wenzelm@36502
   144
          | NONE =>
wenzelm@36502
   145
              let val c =
wenzelm@36502
   146
                (case try Lexicon.unmark_const a of
wenzelm@36502
   147
                  SOME c => c
wenzelm@36502
   148
                | NONE => snd (map_const a))
wenzelm@36502
   149
              in Const (c, T) end)
wenzelm@22704
   150
      | decode (Free (a, T)) =
wenzelm@22704
   151
          (case (map_free a, map_const a) of
wenzelm@35429
   152
            (SOME x, _) => Free (x, T)
wenzelm@35429
   153
          | (_, (true, c)) => Const (c, T)
wenzelm@35429
   154
          | (_, (false, c)) => (if Long_Name.is_qualified c then Const else Free) (c, T))
wenzelm@35429
   155
      | decode (Var (xi, T)) = Var (xi, T)
wenzelm@22704
   156
      | decode (t as Bound _) = t;
wenzelm@22704
   157
  in decode tm end;
wenzelm@22704
   158
wenzelm@22704
   159
clasohm@0
   160
wenzelm@2584
   161
(** output utils **)
wenzelm@2584
   162
wenzelm@2699
   163
(* term_of_sort *)
wenzelm@2584
   164
wenzelm@2584
   165
fun term_of_sort S =
wenzelm@2584
   166
  let
wenzelm@35429
   167
    val class = Lexicon.const o Lexicon.mark_class;
wenzelm@2584
   168
wenzelm@35429
   169
    fun classes [c] = class c
wenzelm@5690
   170
      | classes (c :: cs) = Lexicon.const "_classes" $ class c $ classes cs;
wenzelm@2584
   171
  in
wenzelm@2584
   172
    (case S of
wenzelm@5690
   173
      [] => Lexicon.const "_topsort"
wenzelm@2584
   174
    | [c] => class c
wenzelm@5690
   175
    | cs => Lexicon.const "_sort" $ classes cs)
wenzelm@2584
   176
  end;
wenzelm@2584
   177
wenzelm@2584
   178
wenzelm@2584
   179
(* term_of_typ *)
clasohm@0
   180
clasohm@0
   181
fun term_of_typ show_sorts ty =
clasohm@0
   182
  let
wenzelm@2584
   183
    fun of_sort t S =
wenzelm@5690
   184
      if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S
wenzelm@2584
   185
      else t;
clasohm@0
   186
wenzelm@35429
   187
    fun term_of (Type (a, Ts)) =
wenzelm@35429
   188
          Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts)
wenzelm@42048
   189
      | term_of (TFree (x, S)) =
wenzelm@42048
   190
          if is_some (Lexicon.decode_position x) then Lexicon.free x
wenzelm@42048
   191
          else of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
wenzelm@5690
   192
      | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
wenzelm@8895
   193
  in term_of ty end;
clasohm@0
   194
clasohm@0
   195
clasohm@0
   196
clasohm@0
   197
(** the type syntax **)
clasohm@0
   198
wenzelm@10572
   199
(* print mode *)
wenzelm@10572
   200
wenzelm@10572
   201
val bracketsN = "brackets";
wenzelm@10572
   202
val no_bracketsN = "no_brackets";
wenzelm@10572
   203
wenzelm@10572
   204
fun no_brackets () =
wenzelm@24613
   205
  find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN)
wenzelm@24613
   206
    (print_mode_value ()) = SOME no_bracketsN;
nipkow@11312
   207
nipkow@11312
   208
val type_bracketsN = "type_brackets";
nipkow@11312
   209
val no_type_bracketsN = "no_type_brackets";
nipkow@11312
   210
nipkow@11312
   211
fun no_type_brackets () =
wenzelm@24613
   212
  find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN)
wenzelm@24613
   213
    (print_mode_value ()) <> SOME type_bracketsN;
wenzelm@10572
   214
wenzelm@10572
   215
wenzelm@18
   216
(* parse ast translations *)
clasohm@0
   217
wenzelm@35429
   218
val class_ast = Ast.Constant o Lexicon.mark_class;
wenzelm@35429
   219
val type_ast = Ast.Constant o Lexicon.mark_type;
wenzelm@35429
   220
wenzelm@35429
   221
fun class_name_tr read_class (*"_class_name"*) [Ast.Variable c] = class_ast (read_class c)
wenzelm@35429
   222
  | class_name_tr _ (*"_class_name"*) asts = raise Ast.AST ("class_name_tr", asts);
wenzelm@35429
   223
wenzelm@35429
   224
fun classes_tr read_class (*"_classes"*) [Ast.Variable c, ast] =
wenzelm@35429
   225
      Ast.mk_appl (Ast.Constant "_classes") [class_ast (read_class c), ast]
wenzelm@35429
   226
  | classes_tr _ (*"_classes"*) asts = raise Ast.AST ("classes_tr", asts);
wenzelm@347
   227
wenzelm@35429
   228
fun type_name_tr read_type (*"_type_name"*) [Ast.Variable c] = type_ast (read_type c)
wenzelm@35429
   229
  | type_name_tr _ (*"_type_name"*) asts = raise Ast.AST ("type_name_tr", asts);
wenzelm@35429
   230
wenzelm@35429
   231
fun tapp_ast_tr read_type (*"_tapp"*) [ty, Ast.Variable c] =
wenzelm@35429
   232
      Ast.Appl [type_ast (read_type c), ty]
wenzelm@35429
   233
  | tapp_ast_tr _ (*"_tapp"*) asts = raise Ast.AST ("tapp_ast_tr", asts);
wenzelm@35429
   234
wenzelm@35429
   235
fun tappl_ast_tr read_type (*"_tappl"*) [ty, tys, Ast.Variable c] =
wenzelm@35429
   236
      Ast.Appl (type_ast (read_type c) :: ty :: Ast.unfold_ast "_types" tys)
wenzelm@35429
   237
  | tappl_ast_tr _ (*"_tappl"*) asts = raise Ast.AST ("tappl_ast_tr", asts);
clasohm@0
   238
clasohm@0
   239
fun bracket_ast_tr (*"_bracket"*) [dom, cod] =
wenzelm@35429
   240
      Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
wenzelm@5690
   241
  | bracket_ast_tr (*"_bracket"*) asts = raise Ast.AST ("bracket_ast_tr", asts);
clasohm@0
   242
clasohm@0
   243
wenzelm@18
   244
(* print ast translations *)
clasohm@0
   245
wenzelm@5690
   246
fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f])
wenzelm@5690
   247
  | tappl_ast_tr' (f, [ty]) = Ast.Appl [Ast.Constant "_tapp", ty, f]
wenzelm@347
   248
  | tappl_ast_tr' (f, ty :: tys) =
wenzelm@5690
   249
      Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f];
clasohm@0
   250
wenzelm@35429
   251
fun fun_ast_tr' (*"\\<^type>fun"*) asts =
wenzelm@16614
   252
  if no_brackets () orelse no_type_brackets () then raise Match
wenzelm@10572
   253
  else
wenzelm@35429
   254
    (case Ast.unfold_ast_p "\\<^type>fun" (Ast.Appl (Ast.Constant "\\<^type>fun" :: asts)) of
wenzelm@10572
   255
      (dom as _ :: _ :: _, cod)
wenzelm@10572
   256
        => Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod]
wenzelm@10572
   257
    | _ => raise Match);
clasohm@0
   258
clasohm@0
   259
clasohm@0
   260
(* type_ext *)
clasohm@0
   261
clasohm@0
   262
val sortT = Type ("sort", []);
clasohm@0
   263
val classesT = Type ("classes", []);
clasohm@0
   264
val typesT = Type ("types", []);
clasohm@0
   265
wenzelm@37216
   266
local open Lexicon Syn_Ext in
wenzelm@5690
   267
wenzelm@35668
   268
val type_ext = syn_ext' false (K false)
wenzelm@347
   269
  [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
wenzelm@239
   270
   Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
wenzelm@35429
   271
   Mfix ("_",           idT --> typeT,                 "_type_name", [], max_pri),
wenzelm@35429
   272
   Mfix ("_",           longidT --> typeT,             "_type_name", [], max_pri),
clasohm@330
   273
   Mfix ("_::_",        [tidT, sortT] ---> typeT,      "_ofsort", [max_pri, 0], max_pri),
wenzelm@239
   274
   Mfix ("_::_",        [tvarT, sortT] ---> typeT,     "_ofsort", [max_pri, 0], max_pri),
wenzelm@14838
   275
   Mfix ("'_()::_",     sortT --> typeT,               "_dummy_ofsort", [0], max_pri),
wenzelm@35429
   276
   Mfix ("_",           idT --> sortT,                 "_class_name", [], max_pri),
wenzelm@35429
   277
   Mfix ("_",           longidT --> sortT,             "_class_name", [], max_pri),
wenzelm@2584
   278
   Mfix ("{}",          sortT,                         "_topsort", [], max_pri),
wenzelm@239
   279
   Mfix ("{_}",         classesT --> sortT,            "_sort", [], max_pri),
wenzelm@35429
   280
   Mfix ("_",           idT --> classesT,              "_class_name", [], max_pri),
wenzelm@35429
   281
   Mfix ("_",           longidT --> classesT,          "_class_name", [], max_pri),
wenzelm@239
   282
   Mfix ("_,_",         [idT, classesT] ---> classesT, "_classes", [], max_pri),
wenzelm@3829
   283
   Mfix ("_,_",         [longidT, classesT] ---> classesT, "_classes", [], max_pri),
clasohm@330
   284
   Mfix ("_ _",         [typeT, idT] ---> typeT,       "_tapp", [max_pri, 0], max_pri),
wenzelm@3829
   285
   Mfix ("_ _",         [typeT, longidT] ---> typeT,   "_tapp", [max_pri, 0], max_pri),
wenzelm@9067
   286
   Mfix ("((1'(_,/ _')) _)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri),
wenzelm@9067
   287
   Mfix ("((1'(_,/ _')) _)", [typeT, typesT, longidT] ---> typeT, "_tappl", [], max_pri),
wenzelm@239
   288
   Mfix ("_",           typeT --> typesT,              "", [], max_pri),
wenzelm@239
   289
   Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
wenzelm@35429
   290
   Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "\\<^type>fun", [1, 0], 0),
clasohm@624
   291
   Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0),
wenzelm@2678
   292
   Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri),
wenzelm@35429
   293
   Mfix ("'_",          typeT,                         "\\<^type>dummy", [], max_pri)]
wenzelm@35433
   294
  ["_type_prop"]
wenzelm@37216
   295
  ([], [], [], map Syn_Ext.mk_trfun [("\\<^type>fun", K fun_ast_tr')])
wenzelm@26708
   296
  []
wenzelm@239
   297
  ([], []);
clasohm@0
   298
wenzelm@35668
   299
fun type_ast_trs {read_class, read_type} =
wenzelm@35668
   300
 [("_class_name", class_name_tr o read_class),
wenzelm@35668
   301
  ("_classes", classes_tr o read_class),
wenzelm@35668
   302
  ("_type_name", type_name_tr o read_type),
wenzelm@35668
   303
  ("_tapp", tapp_ast_tr o read_type),
wenzelm@35668
   304
  ("_tappl", tappl_ast_tr o read_type),
wenzelm@35668
   305
  ("_bracket", K bracket_ast_tr)];
wenzelm@35668
   306
clasohm@0
   307
end;
wenzelm@5690
   308
wenzelm@5690
   309
end;