src/Pure/Syntax/type_ext.ML
author paulson
Thu Sep 25 12:09:41 1997 +0200 (1997-09-25)
changeset 3706 e57b5902822f
parent 2699 932fae4271d7
child 3778 b70c41bc7491
permissions -rw-r--r--
Generalized and exported biresolution_from_nets_tac to allow the declaration
of Clarify_tac
     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 used to bootstrap Pure.
     7 *)
     8 
     9 signature TYPE_EXT0 =
    10 sig
    11   val raw_term_sorts: (sort * sort -> bool) -> term -> (indexname * sort) list
    12   val typ_of_term: (indexname -> sort) -> term -> typ
    13 end;
    14 
    15 signature TYPE_EXT =
    16 sig
    17   include TYPE_EXT0
    18   val term_of_sort: sort -> term
    19   val term_of_typ: bool -> typ -> term
    20   val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    21   val type_ext: SynExt.syn_ext
    22 end;
    23 
    24 structure TypeExt : TYPE_EXT =
    25 struct
    26 
    27 open Lexicon SynExt Ast;
    28 
    29 
    30 (** input utils **)
    31 
    32 (* raw_term_sorts *)
    33 
    34 fun raw_term_sorts eq_sort tm =
    35   let
    36     fun classes (Const (c, _)) = [c]
    37       | classes (Free (c, _)) = [c]
    38       | classes (Const ("_classes", _) $ Const (c, _) $ cls) = c :: classes cls
    39       | classes (Const ("_classes", _) $ Free (c, _) $ cls) = c :: classes cls
    40       | classes tm = raise_term "raw_term_sorts: bad encoding of classes" [tm];
    41 
    42     fun sort (Const ("_topsort", _)) = []
    43       | sort (Const (c, _)) = [c]
    44       | sort (Free (c, _)) = [c]
    45       | sort (Const ("_sort", _) $ cls) = classes cls
    46       | sort tm = raise_term "raw_term_sorts: bad encoding of sort" [tm];
    47 
    48     fun eq ((xi, S), (xi', S')) =
    49       xi = xi' andalso eq_sort (S, S');
    50 
    51     fun env_of (Const ("_ofsort", _) $ Free (x, _) $ cls) = [((x, ~1), sort cls)]
    52       | env_of (Const ("_ofsort", _) $ Var (xi, _) $ cls) = [(xi, sort cls)]
    53       | env_of (Abs (_, _, t)) = env_of t
    54       | env_of (t1 $ t2) = gen_union eq (env_of t1, env_of t2)
    55       | env_of t = [];
    56 
    57     val env = env_of tm;
    58   in
    59     (case gen_duplicates eq_fst env of
    60       [] => env
    61     | dups => error ("Inconsistent sort constraints for type variable(s) " ^
    62         commas (map (quote o string_of_vname' o #1) dups)))
    63   end;
    64 
    65 
    66 (* typ_of_term *)
    67 
    68 fun typ_of_term get_sort t =
    69   let
    70     fun typ_of (Free (x, _)) =
    71           if is_tid x then TFree (x, get_sort (x, ~1))
    72           else Type (x, [])
    73       | typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
    74       | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) =
    75           TFree (x, get_sort (x, ~1))
    76       | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) =
    77           TVar (xi, get_sort xi)
    78       | typ_of tm =
    79           let
    80             val (t, ts) = strip_comb tm;
    81             val a =
    82               (case t of
    83                 Const (x, _) => x
    84               | Free (x, _) => x
    85               | _ => raise_term "typ_of_term: bad encoding of type" [tm]);
    86           in
    87             Type (a, map typ_of ts)
    88           end;
    89   in
    90     typ_of t
    91   end;
    92 
    93 
    94 
    95 (** output utils **)
    96 
    97 (* term_of_sort *)
    98 
    99 fun term_of_sort S =
   100   let
   101     fun class c = const "_class" $ free c;
   102 
   103     fun classes [] = sys_error "term_of_sort"
   104       | classes [c] = class c
   105       | classes (c :: cs) = const "_classes" $ class c $ classes cs;
   106   in
   107     (case S of
   108       [] => const "_topsort"
   109     | [c] => class c
   110     | cs => const "_sort" $ classes cs)
   111   end;
   112 
   113 
   114 (* term_of_typ *)
   115 
   116 fun term_of_typ show_sorts ty =
   117   let
   118     fun of_sort t S =
   119       if show_sorts then const "_ofsort" $ t $ term_of_sort S
   120       else t;
   121 
   122     fun term_of (Type (a, Ts)) = list_comb (const a, map term_of Ts)
   123       | term_of (TFree (x, S)) = of_sort (const "_tfree" $ free x) S
   124       | term_of (TVar (xi, S)) = of_sort (const "_tvar" $ var xi) S;
   125   in
   126     term_of ty
   127   end;
   128 
   129 
   130 
   131 (** the type syntax **)
   132 
   133 (* parse ast translations *)
   134 
   135 fun tapp_ast_tr (*"_tapp"*) [ty, f] = Appl [f, ty]
   136   | tapp_ast_tr (*"_tapp"*) asts = raise_ast "tapp_ast_tr" asts;
   137 
   138 fun tappl_ast_tr (*"_tappl"*) [ty, tys, f] =
   139       Appl (f :: ty :: unfold_ast "_types" tys)
   140   | tappl_ast_tr (*"_tappl"*) asts = raise_ast "tappl_ast_tr" asts;
   141 
   142 fun bracket_ast_tr (*"_bracket"*) [dom, cod] =
   143       fold_ast_p "fun" (unfold_ast "_types" dom, cod)
   144   | bracket_ast_tr (*"_bracket"*) asts = raise_ast "bracket_ast_tr" asts;
   145 
   146 
   147 (* print ast translations *)
   148 
   149 fun tappl_ast_tr' (f, []) = raise_ast "tappl_ast_tr'" [f]
   150   | tappl_ast_tr' (f, [ty]) = Appl [Constant "_tapp", ty, f]
   151   | tappl_ast_tr' (f, ty :: tys) =
   152       Appl [Constant "_tappl", ty, fold_ast "_types" tys, f];
   153 
   154 fun fun_ast_tr' (*"fun"*) asts =
   155   (case unfold_ast_p "fun" (Appl (Constant "fun" :: asts)) of
   156     (dom as _ :: _ :: _, cod)
   157       => Appl [Constant "_bracket", fold_ast "_types" dom, cod]
   158   | _ => raise Match);
   159 
   160 
   161 (* type_ext *)
   162 
   163 val sortT = Type ("sort", []);
   164 val classesT = Type ("classes", []);
   165 val typesT = Type ("types", []);
   166 
   167 val type_ext = mk_syn_ext false []
   168   [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
   169    Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
   170    Mfix ("_",           idT --> typeT,                 "", [], max_pri),
   171    Mfix ("_::_",        [tidT, sortT] ---> typeT,      "_ofsort", [max_pri, 0], max_pri),
   172    Mfix ("_::_",        [tvarT, sortT] ---> typeT,     "_ofsort", [max_pri, 0], max_pri),
   173    Mfix ("_",           idT --> sortT,                 "", [], max_pri),
   174    Mfix ("{}",          sortT,                         "_topsort", [], max_pri),
   175    Mfix ("{_}",         classesT --> sortT,            "_sort", [], max_pri),
   176    Mfix ("_",           idT --> classesT,              "", [], max_pri),
   177    Mfix ("_,_",         [idT, classesT] ---> classesT, "_classes", [], max_pri),
   178    Mfix ("_ _",         [typeT, idT] ---> typeT,       "_tapp", [max_pri, 0], max_pri),
   179    Mfix ("((1'(_,/ _'))_)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri),
   180    Mfix ("_",           typeT --> typesT,              "", [], max_pri),
   181    Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
   182    Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "fun", [1, 0], 0),
   183    Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0),
   184    Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri),
   185    Mfix ("'_",          typeT,                         "dummy", [], max_pri)]
   186   []
   187   ([("_tapp", tapp_ast_tr), ("_tappl", tappl_ast_tr), ("_bracket", bracket_ast_tr)],
   188    [],
   189    [],
   190    [("fun", fun_ast_tr')])
   191   TokenTrans.token_translation
   192   ([], []);
   193 
   194 end;