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