wneuper/isa: src/Pure/Syntax/type

     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)

     6 Utilities for input and output of types.  Also the concrete syntax of

     7 types, which is required to bootstrap Pure.

     8 *)

    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;

    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;

    28 structure TypeExt : TYPE_EXT =

    29 struct

    32 (** input utils **)

    34 (* sort_of_term *)

    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]);

    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;

    53 (* raw_term_sorts *)

    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;

    69 (* typ_of_term *)

    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))

    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;

   100 (** output utils **)

   102 (* term_of_sort *)

   104 fun term_of_sort S =

   105   let

   106     fun class c = Lexicon.const "_class" $ Lexicon.free c;

   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;

   119 (* term_of_typ *)

   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;

   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;

   134 (** the type syntax **)

   136 (* print mode *)

   138 val bracketsN = "brackets";

   139 val no_bracketsN = "no_brackets";

   141 fun no_brackets () =

   142   Library.find_first (equal bracketsN orf equal no_bracketsN) (! print_mode)

   143   = Some no_bracketsN;

   145 val type_bracketsN = "type_brackets";

   146 val no_type_bracketsN = "no_type_brackets";

   148 fun no_type_brackets () =

   149   Library.find_first (equal type_bracketsN orf equal no_type_bracketsN)

   150                      (! print_mode)

   151   <> Some type_bracketsN;

   154 (* parse ast translations *)

   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);

   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);

   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);

   168 (* print ast translations *)

   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];

   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);

   184 (* type_ext *)

   186 val sortT = Type ("sort", []);

   187 val classesT = Type ("classes", []);

   188 val typesT = Type ("types", []);

   190 local open Lexicon SynExt in

   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   ([], []);

   226 end;

   228 end;

author	wenzelm
	Sat, 29 May 2004 15:07:42 +0200
changeset 14838	b12855d44c97
parent 14255	e6e3e3f0deed
child 14903	d264b8ad3eec
permissions	-rw-r--r--