src/Pure/Syntax/type_ext.ML
author wenzelm
Thu Apr 17 16:30:53 2008 +0200 (2008-04-17)
changeset 26708 fc2e7d2f763d
parent 26039 a27710a07d10
child 27197 d1b8b6938b23
permissions -rw-r--r--
moved default token translations to proof_context.ML, if all fails the pretty printer falls back on plain output;
wenzelm@18
     1
(*  Title:      Pure/Syntax/type_ext.ML
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
clasohm@0
     4
wenzelm@8895
     5
Utilities for input and output of types.  Also the concrete syntax of
wenzelm@8895
     6
types, which is required to bootstrap Pure.
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
signature TYPE_EXT0 =
wenzelm@2584
    10
sig
wenzelm@22704
    11
  val sort_of_term: (sort -> sort) -> term -> sort
wenzelm@22704
    12
  val term_sorts: (sort -> sort) -> term -> (indexname * sort) list
wenzelm@12317
    13
  val typ_of_term: (indexname -> sort) -> (sort -> sort) -> term -> typ
wenzelm@22764
    14
  val decode_term: (((string * int) * sort) list -> string * int -> sort) ->
wenzelm@22704
    15
    (string -> string option) -> (string -> string option) ->
wenzelm@22704
    16
    (typ -> typ) -> (sort -> sort) -> term -> term
wenzelm@6901
    17
  val term_of_typ: bool -> typ -> term
wenzelm@10572
    18
  val no_brackets: unit -> bool
wenzelm@16614
    19
  val no_type_brackets: unit -> bool
wenzelm@2584
    20
end;
clasohm@0
    21
clasohm@0
    22
signature TYPE_EXT =
wenzelm@2584
    23
sig
clasohm@0
    24
  include TYPE_EXT0
wenzelm@2584
    25
  val term_of_sort: sort -> term
paulson@1511
    26
  val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
wenzelm@8895
    27
  val sortT: typ
paulson@1511
    28
  val type_ext: SynExt.syn_ext
wenzelm@2584
    29
end;
clasohm@0
    30
wenzelm@15750
    31
structure TypeExt: TYPE_EXT =
clasohm@0
    32
struct
wenzelm@2584
    33
wenzelm@2584
    34
(** input utils **)
clasohm@0
    35
wenzelm@8895
    36
(* sort_of_term *)
wenzelm@2584
    37
wenzelm@22704
    38
fun sort_of_term (map_sort: sort -> sort) tm =
wenzelm@557
    39
  let
wenzelm@18
    40
    fun classes (Const (c, _)) = [c]
wenzelm@18
    41
      | classes (Free (c, _)) = [c]
wenzelm@26039
    42
      | classes (Const ("_class", _) $ Free (c, _)) = [c]
wenzelm@3778
    43
      | classes (Const ("_classes", _) $ Const (c, _) $ cs) = c :: classes cs
wenzelm@3778
    44
      | classes (Const ("_classes", _) $ Free (c, _) $ cs) = c :: classes cs
wenzelm@26039
    45
      | classes (Const ("_classes", _) $ (Const ("_class", _) $ Free (c, _)) $ cs) = c :: classes cs
wenzelm@8895
    46
      | classes tm = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
clasohm@0
    47
wenzelm@2584
    48
    fun sort (Const ("_topsort", _)) = []
wenzelm@2584
    49
      | sort (Const (c, _)) = [c]
wenzelm@2584
    50
      | sort (Free (c, _)) = [c]
wenzelm@26039
    51
      | sort (Const ("_class", _) $ Free (c, _)) = [c]
wenzelm@3778
    52
      | sort (Const ("_sort", _) $ cs) = classes cs
wenzelm@8895
    53
      | sort tm = raise TERM ("sort_of_term: bad encoding of sort", [tm]);
wenzelm@22704
    54
  in map_sort (sort tm) end;
wenzelm@8895
    55
wenzelm@2584
    56
wenzelm@22704
    57
(* term_sorts *)
wenzelm@8895
    58
wenzelm@22704
    59
fun term_sorts map_sort tm =
wenzelm@8895
    60
  let
wenzelm@22704
    61
    val sort_of = sort_of_term map_sort;
wenzelm@22704
    62
wenzelm@22704
    63
    fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) =
wenzelm@22704
    64
          insert (op =) ((x, ~1), sort_of cs)
wenzelm@22704
    65
      | add_env (Const ("_ofsort", _) $ (Const ("_tfree", _) $ Free (x, _)) $ cs) =
wenzelm@22704
    66
          insert (op =) ((x, ~1), sort_of cs)
wenzelm@22704
    67
      | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) =
wenzelm@22704
    68
          insert (op =) (xi, sort_of cs)
wenzelm@22704
    69
      | add_env (Const ("_ofsort", _) $ (Const ("_tvar", _) $ Var (xi, _)) $ cs) =
wenzelm@22704
    70
          insert (op =) (xi, sort_of cs)
wenzelm@22704
    71
      | add_env (Abs (_, _, t)) = add_env t
wenzelm@22704
    72
      | add_env (t1 $ t2) = add_env t1 #> add_env t2
wenzelm@22704
    73
      | add_env _ = I;
wenzelm@8895
    74
  in add_env tm [] end;
wenzelm@557
    75
wenzelm@557
    76
wenzelm@2584
    77
(* typ_of_term *)
clasohm@0
    78
wenzelm@12317
    79
fun typ_of_term get_sort map_sort t =
wenzelm@557
    80
  let
wenzelm@557
    81
    fun typ_of (Free (x, _)) =
wenzelm@5690
    82
          if Lexicon.is_tid x then TFree (x, get_sort (x, ~1))
wenzelm@557
    83
          else Type (x, [])
wenzelm@557
    84
      | typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
schirmer@14255
    85
      | typ_of (Const ("_tfree",_) $ (t as Free x)) = typ_of t
schirmer@14255
    86
      | typ_of (Const ("_tvar",_) $ (t as Var x)) = typ_of t
wenzelm@12317
    87
      | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = TFree (x, get_sort (x, ~1))
wenzelm@16614
    88
      | typ_of (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ _) =
wenzelm@16614
    89
          TFree (x, get_sort (x, ~1))
wenzelm@12317
    90
      | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi)
wenzelm@16614
    91
      | typ_of (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ _) =
wenzelm@16614
    92
          TVar (xi, get_sort xi)
wenzelm@22704
    93
      | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", sort_of_term map_sort t)
wenzelm@557
    94
      | typ_of tm =
clasohm@0
    95
          let
wenzelm@16614
    96
            val (t, ts) = Term.strip_comb tm;
clasohm@0
    97
            val a =
wenzelm@18
    98
              (case t of
clasohm@0
    99
                Const (x, _) => x
clasohm@0
   100
              | Free (x, _) => x
wenzelm@3778
   101
              | _ => raise TERM ("typ_of_term: bad encoding of type", [tm]));
wenzelm@12317
   102
          in Type (a, map typ_of ts) end;
wenzelm@8895
   103
  in typ_of t end;
clasohm@0
   104
clasohm@0
   105
wenzelm@22764
   106
(* decode_term -- transform parse tree into raw term *)
wenzelm@22704
   107
wenzelm@22764
   108
fun decode_term get_sort map_const map_free map_type map_sort tm =
wenzelm@22704
   109
  let
wenzelm@22704
   110
    val sort_env = term_sorts map_sort tm;
wenzelm@22704
   111
    val decodeT = map_type o typ_of_term (get_sort sort_env) map_sort;
wenzelm@22704
   112
wenzelm@22704
   113
    fun decode (Const ("_constrain", _) $ t $ typ) =
wenzelm@24680
   114
          TypeInfer.constrain (decodeT typ) (decode t)
wenzelm@22704
   115
      | decode (Const ("_constrainAbs", _) $ (Abs (x, T, t)) $ typ) =
wenzelm@22704
   116
          if T = dummyT then Abs (x, decodeT typ, decode t)
wenzelm@24680
   117
          else TypeInfer.constrain (decodeT typ --> dummyT) (Abs (x, map_type T, decode t))
wenzelm@22704
   118
      | decode (Abs (x, T, t)) = Abs (x, map_type T, decode t)
wenzelm@22704
   119
      | decode (t $ u) = decode t $ decode u
wenzelm@22704
   120
      | decode (Const (a, T)) =
wenzelm@22704
   121
          let val c =
wenzelm@22704
   122
            (case try (unprefix Lexicon.constN) a of SOME c => c | NONE => perhaps map_const a)
wenzelm@22704
   123
          in Const (c, map_type T) end
wenzelm@22704
   124
      | decode (Free (a, T)) =
wenzelm@22704
   125
          (case (map_free a, map_const a) of
wenzelm@22704
   126
            (SOME x, _) => Free (x, map_type T)
wenzelm@22704
   127
          | (_, SOME c) => Const (c, map_type T)
wenzelm@23167
   128
          | _ => (if NameSpace.is_qualified a then Const else Free) (a, map_type T))
wenzelm@22704
   129
      | decode (Var (xi, T)) = Var (xi, map_type T)
wenzelm@22704
   130
      | decode (t as Bound _) = t;
wenzelm@22704
   131
  in decode tm end;
wenzelm@22704
   132
wenzelm@22704
   133
clasohm@0
   134
wenzelm@2584
   135
(** output utils **)
wenzelm@2584
   136
wenzelm@2699
   137
(* term_of_sort *)
wenzelm@2584
   138
wenzelm@2584
   139
fun term_of_sort S =
wenzelm@2584
   140
  let
wenzelm@5690
   141
    fun class c = Lexicon.const "_class" $ Lexicon.free c;
wenzelm@2584
   142
wenzelm@2584
   143
    fun classes [] = sys_error "term_of_sort"
wenzelm@2584
   144
      | classes [c] = class c
wenzelm@5690
   145
      | classes (c :: cs) = Lexicon.const "_classes" $ class c $ classes cs;
wenzelm@2584
   146
  in
wenzelm@2584
   147
    (case S of
wenzelm@5690
   148
      [] => Lexicon.const "_topsort"
wenzelm@2584
   149
    | [c] => class c
wenzelm@5690
   150
    | cs => Lexicon.const "_sort" $ classes cs)
wenzelm@2584
   151
  end;
wenzelm@2584
   152
wenzelm@2584
   153
wenzelm@2584
   154
(* term_of_typ *)
clasohm@0
   155
clasohm@0
   156
fun term_of_typ show_sorts ty =
clasohm@0
   157
  let
wenzelm@2584
   158
    fun of_sort t S =
wenzelm@5690
   159
      if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S
wenzelm@2584
   160
      else t;
clasohm@0
   161
wenzelm@16614
   162
    fun term_of (Type (a, Ts)) = Term.list_comb (Lexicon.const a, map term_of Ts)
wenzelm@5690
   163
      | term_of (TFree (x, S)) = of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
wenzelm@5690
   164
      | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
wenzelm@8895
   165
  in term_of ty end;
clasohm@0
   166
clasohm@0
   167
clasohm@0
   168
clasohm@0
   169
(** the type syntax **)
clasohm@0
   170
wenzelm@10572
   171
(* print mode *)
wenzelm@10572
   172
wenzelm@10572
   173
val bracketsN = "brackets";
wenzelm@10572
   174
val no_bracketsN = "no_brackets";
wenzelm@10572
   175
wenzelm@10572
   176
fun no_brackets () =
wenzelm@24613
   177
  find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN)
wenzelm@24613
   178
    (print_mode_value ()) = SOME no_bracketsN;
nipkow@11312
   179
nipkow@11312
   180
val type_bracketsN = "type_brackets";
nipkow@11312
   181
val no_type_bracketsN = "no_type_brackets";
nipkow@11312
   182
nipkow@11312
   183
fun no_type_brackets () =
wenzelm@24613
   184
  find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN)
wenzelm@24613
   185
    (print_mode_value ()) <> SOME type_bracketsN;
wenzelm@10572
   186
wenzelm@10572
   187
wenzelm@18
   188
(* parse ast translations *)
clasohm@0
   189
wenzelm@5690
   190
fun tapp_ast_tr (*"_tapp"*) [ty, f] = Ast.Appl [f, ty]
wenzelm@5690
   191
  | tapp_ast_tr (*"_tapp"*) asts = raise Ast.AST ("tapp_ast_tr", asts);
wenzelm@347
   192
wenzelm@347
   193
fun tappl_ast_tr (*"_tappl"*) [ty, tys, f] =
wenzelm@5690
   194
      Ast.Appl (f :: ty :: Ast.unfold_ast "_types" tys)
wenzelm@5690
   195
  | tappl_ast_tr (*"_tappl"*) asts = raise Ast.AST ("tappl_ast_tr", asts);
clasohm@0
   196
clasohm@0
   197
fun bracket_ast_tr (*"_bracket"*) [dom, cod] =
wenzelm@5690
   198
      Ast.fold_ast_p "fun" (Ast.unfold_ast "_types" dom, cod)
wenzelm@5690
   199
  | bracket_ast_tr (*"_bracket"*) asts = raise Ast.AST ("bracket_ast_tr", asts);
clasohm@0
   200
clasohm@0
   201
wenzelm@18
   202
(* print ast translations *)
clasohm@0
   203
wenzelm@5690
   204
fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f])
wenzelm@5690
   205
  | tappl_ast_tr' (f, [ty]) = Ast.Appl [Ast.Constant "_tapp", ty, f]
wenzelm@347
   206
  | tappl_ast_tr' (f, ty :: tys) =
wenzelm@5690
   207
      Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f];
clasohm@0
   208
clasohm@0
   209
fun fun_ast_tr' (*"fun"*) asts =
wenzelm@16614
   210
  if no_brackets () orelse no_type_brackets () then raise Match
wenzelm@10572
   211
  else
wenzelm@10572
   212
    (case Ast.unfold_ast_p "fun" (Ast.Appl (Ast.Constant "fun" :: asts)) of
wenzelm@10572
   213
      (dom as _ :: _ :: _, cod)
wenzelm@10572
   214
        => Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod]
wenzelm@10572
   215
    | _ => raise Match);
clasohm@0
   216
clasohm@0
   217
clasohm@0
   218
(* type_ext *)
clasohm@0
   219
clasohm@0
   220
val sortT = Type ("sort", []);
clasohm@0
   221
val classesT = Type ("classes", []);
clasohm@0
   222
val typesT = Type ("types", []);
clasohm@0
   223
wenzelm@5690
   224
local open Lexicon SynExt in
wenzelm@5690
   225
wenzelm@14903
   226
val type_ext = syn_ext' false (K false)
wenzelm@347
   227
  [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
wenzelm@239
   228
   Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
wenzelm@239
   229
   Mfix ("_",           idT --> typeT,                 "", [], max_pri),
wenzelm@3829
   230
   Mfix ("_",           longidT --> typeT,             "", [], max_pri),
clasohm@330
   231
   Mfix ("_::_",        [tidT, sortT] ---> typeT,      "_ofsort", [max_pri, 0], max_pri),
wenzelm@239
   232
   Mfix ("_::_",        [tvarT, sortT] ---> typeT,     "_ofsort", [max_pri, 0], max_pri),
wenzelm@14838
   233
   Mfix ("'_()::_",     sortT --> typeT,               "_dummy_ofsort", [0], max_pri),
wenzelm@239
   234
   Mfix ("_",           idT --> sortT,                 "", [], max_pri),
wenzelm@3829
   235
   Mfix ("_",           longidT --> sortT,             "", [], max_pri),
wenzelm@2584
   236
   Mfix ("{}",          sortT,                         "_topsort", [], max_pri),
wenzelm@239
   237
   Mfix ("{_}",         classesT --> sortT,            "_sort", [], max_pri),
wenzelm@239
   238
   Mfix ("_",           idT --> classesT,              "", [], max_pri),
wenzelm@3829
   239
   Mfix ("_",           longidT --> classesT,          "", [], max_pri),
wenzelm@239
   240
   Mfix ("_,_",         [idT, classesT] ---> classesT, "_classes", [], max_pri),
wenzelm@3829
   241
   Mfix ("_,_",         [longidT, classesT] ---> classesT, "_classes", [], max_pri),
clasohm@330
   242
   Mfix ("_ _",         [typeT, idT] ---> typeT,       "_tapp", [max_pri, 0], max_pri),
wenzelm@3829
   243
   Mfix ("_ _",         [typeT, longidT] ---> typeT,   "_tapp", [max_pri, 0], max_pri),
wenzelm@9067
   244
   Mfix ("((1'(_,/ _')) _)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri),
wenzelm@9067
   245
   Mfix ("((1'(_,/ _')) _)", [typeT, typesT, longidT] ---> typeT, "_tappl", [], max_pri),
wenzelm@239
   246
   Mfix ("_",           typeT --> typesT,              "", [], max_pri),
wenzelm@239
   247
   Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
wenzelm@239
   248
   Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "fun", [1, 0], 0),
clasohm@624
   249
   Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0),
wenzelm@2678
   250
   Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri),
wenzelm@2678
   251
   Mfix ("'_",          typeT,                         "dummy", [], max_pri)]
wenzelm@258
   252
  []
wenzelm@15750
   253
  (map SynExt.mk_trfun
wenzelm@16614
   254
   [("_tapp", K tapp_ast_tr), ("_tappl", K tappl_ast_tr), ("_bracket", K bracket_ast_tr)],
wenzelm@239
   255
   [],
wenzelm@239
   256
   [],
wenzelm@16614
   257
   map SynExt.mk_trfun [("fun", K fun_ast_tr')])
wenzelm@26708
   258
  []
wenzelm@239
   259
  ([], []);
clasohm@0
   260
clasohm@0
   261
end;
wenzelm@5690
   262
wenzelm@5690
   263
end;