src/Pure/Syntax/type_ext.ML
author paulson
Fri Feb 16 17:24:51 1996 +0100 (1996-02-16)
changeset 1511 09354d37a5ab
parent 764 b60e77395d1a
child 2438 b630fded4566
permissions -rw-r--r--
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.
     1 (*  Title:      Pure/Syntax/type_ext.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     4 
     5 The concrete syntax of types (used to bootstrap Pure).
     6 *)
     7 
     8 signature TYPE_EXT0 =
     9   sig
    10   val raw_term_sorts: term -> (indexname * sort) list
    11   val typ_of_term: (indexname * sort) list -> (indexname -> sort) -> term -> typ
    12   end;
    13 
    14 signature TYPE_EXT =
    15   sig
    16   include TYPE_EXT0
    17   val term_of_typ: bool -> typ -> term
    18   val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    19   val type_ext: SynExt.syn_ext
    20   end;
    21 
    22 structure TypeExt : TYPE_EXT =
    23 struct
    24 open Lexicon SynExt Ast;
    25 
    26 (** raw_term_sorts **)
    27 
    28 fun raw_term_sorts tm =
    29   let
    30     fun show_var (xi as (x, i)) = if i < 0 then x else string_of_vname xi;
    31 
    32     fun classes (Const (c, _)) = [c]
    33       | classes (Free (c, _)) = [c]
    34       | classes (Const ("_classes", _) $ Const (c, _) $ cls) = c :: classes cls
    35       | classes (Const ("_classes", _) $ Free (c, _) $ cls) = c :: classes cls
    36       | classes tm = raise_term "raw_term_sorts: bad encoding of classes" [tm];
    37 
    38     fun sort (Const ("_emptysort", _)) = []
    39       | sort (Const (s, _)) = [s]
    40       | sort (Free (s, _)) = [s]
    41       | sort (Const ("_sort", _) $ cls) = classes cls
    42       | sort tm = raise_term "raw_term_sorts: bad encoding of sort" [tm];
    43 
    44     fun env_of (Const ("_ofsort", _) $ Free (x, _) $ srt) = [((x, ~1), sort srt)]
    45       | env_of (Const ("_ofsort", _) $ Var (xi, _) $ srt) = [(xi, sort srt)]
    46       | env_of (Abs (_, _, t)) = env_of t
    47       | env_of (t1 $ t2) = env_of t1 @ env_of t2
    48       | env_of t = [];
    49 
    50     val env = distinct (env_of tm);
    51   in
    52     (case gen_duplicates eq_fst env of
    53       [] => env
    54     | dups => error ("Inconsistent sort constraints for type variable(s) " ^
    55         commas (map (quote o show_var o #1) dups)))
    56   end;
    57 
    58 
    59 
    60 (** typ_of_term **)
    61 
    62 fun typ_of_term sort_env def_sort t =
    63   let
    64     fun get_sort xi =
    65       (case assoc (sort_env, xi) of
    66         None => def_sort xi
    67       | Some s => s);
    68 
    69     fun typ_of (Free (x, _)) =
    70           if is_tid x then TFree (x, get_sort (x, ~1))
    71           else Type (x, [])
    72       | typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
    73       | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) =
    74           TFree (x, get_sort (x, ~1))
    75       | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) =
    76           TVar (xi, get_sort xi)
    77       | typ_of tm =
    78           let
    79             val (t, ts) = strip_comb tm;
    80             val a =
    81               (case t of
    82                 Const (x, _) => x
    83               | Free (x, _) => x
    84               | _ => raise_term "typ_of_term: bad encoding of type" [tm]);
    85           in
    86             Type (a, map typ_of ts)
    87           end;
    88   in
    89     typ_of t
    90   end;
    91 
    92 
    93 
    94 (** term_of_typ **)
    95 
    96 fun term_of_typ show_sorts ty =
    97   let
    98     fun classes [] = raise Match
    99       | classes [c] = free c
   100       | classes (c :: cs) = const "_classes" $ free c $ classes cs;
   101 
   102     fun sort [] = const "_emptysort"
   103       | sort [s] = free s
   104       | sort ss = const "_sort" $ classes ss;
   105 
   106     fun of_sort t ss =
   107       if show_sorts then const "_ofsort" $ t $ sort ss else t;
   108 
   109     fun term_of (Type (a, tys)) = list_comb (const a, map term_of tys)
   110       | term_of (TFree (x, ss)) = of_sort (free x) ss
   111       | term_of (TVar (xi, ss)) = of_sort (var xi) ss;
   112   in
   113     term_of ty
   114   end;
   115 
   116 
   117 
   118 (** the type syntax **)
   119 
   120 (* parse ast translations *)
   121 
   122 fun tapp_ast_tr (*"_tapp"*) [ty, f] = Appl [f, ty]
   123   | tapp_ast_tr (*"_tapp"*) asts = raise_ast "tapp_ast_tr" asts;
   124 
   125 fun tappl_ast_tr (*"_tappl"*) [ty, tys, f] =
   126       Appl (f :: ty :: unfold_ast "_types" tys)
   127   | tappl_ast_tr (*"_tappl"*) asts = raise_ast "tappl_ast_tr" asts;
   128 
   129 fun bracket_ast_tr (*"_bracket"*) [dom, cod] =
   130       fold_ast_p "fun" (unfold_ast "_types" dom, cod)
   131   | bracket_ast_tr (*"_bracket"*) asts = raise_ast "bracket_ast_tr" asts;
   132 
   133 
   134 (* print ast translations *)
   135 
   136 fun tappl_ast_tr' (f, []) = raise_ast "tappl_ast_tr'" [f]
   137   | tappl_ast_tr' (f, [ty]) = Appl [Constant "_tapp", ty, f]
   138   | tappl_ast_tr' (f, ty :: tys) =
   139       Appl [Constant "_tappl", ty, fold_ast "_types" tys, f];
   140 
   141 fun fun_ast_tr' (*"fun"*) asts =
   142   (case unfold_ast_p "fun" (Appl (Constant "fun" :: asts)) of
   143     (dom as _ :: _ :: _, cod)
   144       => Appl [Constant "_bracket", fold_ast "_types" dom, cod]
   145   | _ => raise Match);
   146 
   147 
   148 (* type_ext *)
   149 
   150 val sortT = Type ("sort", []);
   151 val classesT = Type ("classes", []);
   152 val typesT = Type ("types", []);
   153 
   154 val type_ext = mk_syn_ext false []
   155   [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
   156    Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
   157    Mfix ("_",           idT --> typeT,                 "", [], max_pri),
   158    Mfix ("_::_",        [tidT, sortT] ---> typeT,      "_ofsort", [max_pri, 0], max_pri),
   159    Mfix ("_::_",        [tvarT, sortT] ---> typeT,     "_ofsort", [max_pri, 0], max_pri),
   160    Mfix ("_",           idT --> sortT,                 "", [], max_pri),
   161    Mfix ("{}",          sortT,                         "_emptysort", [], max_pri),
   162    Mfix ("{_}",         classesT --> sortT,            "_sort", [], max_pri),
   163    Mfix ("_",           idT --> classesT,              "", [], max_pri),
   164    Mfix ("_,_",         [idT, classesT] ---> classesT, "_classes", [], max_pri),
   165    Mfix ("_ _",         [typeT, idT] ---> typeT,       "_tapp", [max_pri, 0], max_pri),
   166    Mfix ("((1'(_,/ _'))_)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri),
   167    Mfix ("_",           typeT --> typesT,              "", [], max_pri),
   168    Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
   169    Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "fun", [1, 0], 0),
   170    Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0),
   171    Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri)]
   172   []
   173   ([("_tapp", tapp_ast_tr), ("_tappl", tappl_ast_tr), ("_bracket", bracket_ast_tr)],
   174    [],
   175    [],
   176    [("fun", fun_ast_tr')])
   177   ([], []);
   178 
   179 end;