src/Pure/Syntax/type_ext.ML
author wenzelm
Wed Oct 31 21:59:07 2001 +0100 (2001-10-31)
changeset 12004 1703de633aaf
parent 11312 4104bd8d1528
child 12317 fed7bed97293
permissions -rw-r--r--
IsarThy.theorem_i: no locale;
     1 (*  Title:      Pure/Syntax/type_ext.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     4 
     5 Utilities for input and output of types.  Also the concrete syntax of
     6 types, which is required to bootstrap Pure.
     7 *)
     8 
     9 signature TYPE_EXT0 =
    10 sig
    11   val sort_of_term: term -> sort
    12   val raw_term_sorts: term -> (indexname * sort) list
    13   val typ_of_term: (indexname -> sort) -> term -> typ
    14   val term_of_typ: bool -> typ -> term
    15   val no_brackets: unit -> bool
    16 end;
    17 
    18 signature TYPE_EXT =
    19 sig
    20   include TYPE_EXT0
    21   val term_of_sort: sort -> term
    22   val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    23   val sortT: typ
    24   val type_ext: SynExt.syn_ext
    25 end;
    26 
    27 structure TypeExt : TYPE_EXT =
    28 struct
    29 
    30 
    31 (** input utils **)
    32 
    33 (* sort_of_term *)
    34 
    35 fun sort_of_term tm =
    36   let
    37     fun classes (Const (c, _)) = [c]
    38       | classes (Free (c, _)) = [c]
    39       | classes (Const ("_classes", _) $ Const (c, _) $ cs) = c :: classes cs
    40       | classes (Const ("_classes", _) $ Free (c, _) $ cs) = c :: classes cs
    41       | classes tm = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
    42 
    43     fun sort (Const ("_topsort", _)) = []
    44       | sort (Const (c, _)) = [c]
    45       | sort (Free (c, _)) = [c]
    46       | sort (Const ("_sort", _) $ cs) = classes cs
    47       | sort tm = raise TERM ("sort_of_term: bad encoding of sort", [tm]);
    48   in sort tm end;
    49 
    50 
    51 (* raw_term_sorts *)
    52 
    53 fun raw_term_sorts tm =
    54   let
    55     fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) env = ((x, ~1), sort_of_term cs) ins env
    56       | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) env = (xi, sort_of_term cs) ins env
    57       | add_env (Abs (_, _, t)) env = add_env t env
    58       | add_env (t1 $ t2) env = add_env t1 (add_env t2 env)
    59       | add_env t env = env;
    60   in add_env tm [] end;
    61 
    62 
    63 (* typ_of_term *)
    64 
    65 fun typ_of_term get_sort t =
    66   let
    67     fun typ_of (Free (x, _)) =
    68           if Lexicon.is_tid x then TFree (x, get_sort (x, ~1))
    69           else Type (x, [])
    70       | typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
    71       | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) =
    72           TFree (x, get_sort (x, ~1))
    73       | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) =
    74           TVar (xi, get_sort xi)
    75       | typ_of tm =
    76           let
    77             val (t, ts) = strip_comb tm;
    78             val a =
    79               (case t of
    80                 Const (x, _) => x
    81               | Free (x, _) => x
    82               | _ => raise TERM ("typ_of_term: bad encoding of type", [tm]));
    83           in
    84             Type (a, map typ_of ts)
    85           end;
    86   in typ_of t end;
    87 
    88 
    89 
    90 (** output utils **)
    91 
    92 (* term_of_sort *)
    93 
    94 fun term_of_sort S =
    95   let
    96     fun class c = Lexicon.const "_class" $ Lexicon.free c;
    97 
    98     fun classes [] = sys_error "term_of_sort"
    99       | classes [c] = class c
   100       | classes (c :: cs) = Lexicon.const "_classes" $ class c $ classes cs;
   101   in
   102     (case S of
   103       [] => Lexicon.const "_topsort"
   104     | [c] => class c
   105     | cs => Lexicon.const "_sort" $ classes cs)
   106   end;
   107 
   108 
   109 (* term_of_typ *)
   110 
   111 fun term_of_typ show_sorts ty =
   112   let
   113     fun of_sort t S =
   114       if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S
   115       else t;
   116 
   117     fun term_of (Type (a, Ts)) = list_comb (Lexicon.const a, map term_of Ts)
   118       | term_of (TFree (x, S)) = of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
   119       | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
   120   in term_of ty end;
   121 
   122 
   123 
   124 (** the type syntax **)
   125 
   126 (* print mode *)
   127 
   128 val bracketsN = "brackets";
   129 val no_bracketsN = "no_brackets";
   130 
   131 fun no_brackets () =
   132   Library.find_first (equal bracketsN orf equal no_bracketsN) (! print_mode)
   133   = Some no_bracketsN;
   134 
   135 val type_bracketsN = "type_brackets";
   136 val no_type_bracketsN = "no_type_brackets";
   137 
   138 fun no_type_brackets () =
   139   Library.find_first (equal type_bracketsN orf equal no_type_bracketsN)
   140                      (! print_mode)
   141   = Some no_type_bracketsN;
   142 
   143 
   144 (* parse ast translations *)
   145 
   146 fun tapp_ast_tr (*"_tapp"*) [ty, f] = Ast.Appl [f, ty]
   147   | tapp_ast_tr (*"_tapp"*) asts = raise Ast.AST ("tapp_ast_tr", asts);
   148 
   149 fun tappl_ast_tr (*"_tappl"*) [ty, tys, f] =
   150       Ast.Appl (f :: ty :: Ast.unfold_ast "_types" tys)
   151   | tappl_ast_tr (*"_tappl"*) asts = raise Ast.AST ("tappl_ast_tr", asts);
   152 
   153 fun bracket_ast_tr (*"_bracket"*) [dom, cod] =
   154       Ast.fold_ast_p "fun" (Ast.unfold_ast "_types" dom, cod)
   155   | bracket_ast_tr (*"_bracket"*) asts = raise Ast.AST ("bracket_ast_tr", asts);
   156 
   157 
   158 (* print ast translations *)
   159 
   160 fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f])
   161   | tappl_ast_tr' (f, [ty]) = Ast.Appl [Ast.Constant "_tapp", ty, f]
   162   | tappl_ast_tr' (f, ty :: tys) =
   163       Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f];
   164 
   165 fun fun_ast_tr' (*"fun"*) asts =
   166   if no_brackets() orelse no_type_brackets() then raise Match
   167   else
   168     (case Ast.unfold_ast_p "fun" (Ast.Appl (Ast.Constant "fun" :: asts)) of
   169       (dom as _ :: _ :: _, cod)
   170         => Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod]
   171     | _ => raise Match);
   172 
   173 
   174 (* type_ext *)
   175 
   176 val sortT = Type ("sort", []);
   177 val classesT = Type ("classes", []);
   178 val typesT = Type ("types", []);
   179 
   180 local open Lexicon SynExt in
   181 
   182 val type_ext = mk_syn_ext false ["dummy"]
   183   [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
   184    Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
   185    Mfix ("_",           idT --> typeT,                 "", [], max_pri),
   186    Mfix ("_",           longidT --> typeT,             "", [], max_pri),
   187    Mfix ("_::_",        [tidT, sortT] ---> typeT,      "_ofsort", [max_pri, 0], max_pri),
   188    Mfix ("_::_",        [tvarT, sortT] ---> typeT,     "_ofsort", [max_pri, 0], max_pri),
   189    Mfix ("_",           idT --> sortT,                 "", [], max_pri),
   190    Mfix ("_",           longidT --> sortT,             "", [], max_pri),
   191    Mfix ("{}",          sortT,                         "_topsort", [], max_pri),
   192    Mfix ("{_}",         classesT --> sortT,            "_sort", [], max_pri),
   193    Mfix ("_",           idT --> classesT,              "", [], max_pri),
   194    Mfix ("_",           longidT --> classesT,          "", [], max_pri),
   195    Mfix ("_,_",         [idT, classesT] ---> classesT, "_classes", [], max_pri),
   196    Mfix ("_,_",         [longidT, classesT] ---> classesT, "_classes", [], max_pri),
   197    Mfix ("_ _",         [typeT, idT] ---> typeT,       "_tapp", [max_pri, 0], max_pri),
   198    Mfix ("_ _",         [typeT, longidT] ---> typeT,   "_tapp", [max_pri, 0], max_pri),
   199    Mfix ("((1'(_,/ _')) _)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri),
   200    Mfix ("((1'(_,/ _')) _)", [typeT, typesT, longidT] ---> typeT, "_tappl", [], max_pri),
   201    Mfix ("_",           typeT --> typesT,              "", [], max_pri),
   202    Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
   203    Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "fun", [1, 0], 0),
   204    Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0),
   205    Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri),
   206    Mfix ("'_",          typeT,                         "dummy", [], max_pri)]
   207   []
   208   ([("_tapp", tapp_ast_tr), ("_tappl", tappl_ast_tr), ("_bracket", bracket_ast_tr)],
   209    [],
   210    [],
   211    [("fun", fun_ast_tr')])
   212   TokenTrans.token_translation
   213   ([], []);
   214 
   215 end;
   216 
   217 end;