src/Pure/Syntax/type_ext.ML
author wenzelm
Mon Jul 09 11:44:20 2007 +0200 (2007-07-09)
changeset 23660 18765718cf62
parent 23167 b9bbdf7eab3b
child 24613 bc889c3d55a3
permissions -rw-r--r--
type output = string indicates raw system output;
     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: (sort -> sort) -> term -> sort
    12   val term_sorts: (sort -> sort) -> term -> (indexname * sort) list
    13   val typ_of_term: (indexname -> sort) -> (sort -> sort) -> term -> typ
    14   val decode_term: (((string * int) * sort) list -> string * int -> sort) ->
    15     (string -> string option) -> (string -> string option) ->
    16     (typ -> typ) -> (sort -> sort) -> term -> term
    17   val term_of_typ: bool -> typ -> term
    18   val no_brackets: unit -> bool
    19   val no_type_brackets: unit -> bool
    20 end;
    21 
    22 signature TYPE_EXT =
    23 sig
    24   include TYPE_EXT0
    25   val term_of_sort: sort -> term
    26   val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    27   val sortT: typ
    28   val type_ext: SynExt.syn_ext
    29 end;
    30 
    31 structure TypeExt: TYPE_EXT =
    32 struct
    33 
    34 (** input utils **)
    35 
    36 (* sort_of_term *)
    37 
    38 fun sort_of_term (map_sort: sort -> sort) tm =
    39   let
    40     fun classes (Const (c, _)) = [c]
    41       | classes (Free (c, _)) = [c]
    42       | classes (Const ("_classes", _) $ Const (c, _) $ cs) = c :: classes cs
    43       | classes (Const ("_classes", _) $ Free (c, _) $ cs) = c :: classes cs
    44       | classes tm = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
    45 
    46     fun sort (Const ("_topsort", _)) = []
    47       | sort (Const (c, _)) = [c]
    48       | sort (Free (c, _)) = [c]
    49       | sort (Const ("_class",_) $ Free (c, _)) = [c]
    50       | sort (Const ("_sort", _) $ cs) = classes cs
    51       | sort tm = raise TERM ("sort_of_term: bad encoding of sort", [tm]);
    52   in map_sort (sort tm) end;
    53 
    54 
    55 (* term_sorts *)
    56 
    57 fun term_sorts map_sort tm =
    58   let
    59     val sort_of = sort_of_term map_sort;
    60 
    61     fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) =
    62           insert (op =) ((x, ~1), sort_of cs)
    63       | add_env (Const ("_ofsort", _) $ (Const ("_tfree", _) $ Free (x, _)) $ cs) =
    64           insert (op =) ((x, ~1), sort_of cs)
    65       | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) =
    66           insert (op =) (xi, sort_of cs)
    67       | add_env (Const ("_ofsort", _) $ (Const ("_tvar", _) $ Var (xi, _)) $ cs) =
    68           insert (op =) (xi, sort_of cs)
    69       | add_env (Abs (_, _, t)) = add_env t
    70       | add_env (t1 $ t2) = add_env t1 #> add_env t2
    71       | add_env _ = I;
    72   in add_env tm [] end;
    73 
    74 
    75 (* typ_of_term *)
    76 
    77 fun typ_of_term get_sort map_sort t =
    78   let
    79     fun typ_of (Free (x, _)) =
    80           if Lexicon.is_tid x then TFree (x, get_sort (x, ~1))
    81           else Type (x, [])
    82       | typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
    83       | typ_of (Const ("_tfree",_) $ (t as Free x)) = typ_of t
    84       | typ_of (Const ("_tvar",_) $ (t as Var x)) = typ_of t
    85       | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = TFree (x, get_sort (x, ~1))
    86       | typ_of (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ _) =
    87           TFree (x, get_sort (x, ~1))
    88       | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi)
    89       | typ_of (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ _) =
    90           TVar (xi, get_sort xi)
    91       | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", sort_of_term map_sort t)
    92       | typ_of tm =
    93           let
    94             val (t, ts) = Term.strip_comb tm;
    95             val a =
    96               (case t of
    97                 Const (x, _) => x
    98               | Free (x, _) => x
    99               | _ => raise TERM ("typ_of_term: bad encoding of type", [tm]));
   100           in Type (a, map typ_of ts) end;
   101   in typ_of t end;
   102 
   103 
   104 (* decode_term -- transform parse tree into raw term *)
   105 
   106 fun decode_term get_sort map_const map_free map_type map_sort tm =
   107   let
   108     val sort_env = term_sorts map_sort tm;
   109     val decodeT = map_type o typ_of_term (get_sort sort_env) map_sort;
   110 
   111     fun decode (Const ("_constrain", _) $ t $ typ) =
   112           TypeInfer.constrain (decode t) (decodeT typ)
   113       | decode (Const ("_constrainAbs", _) $ (Abs (x, T, t)) $ typ) =
   114           if T = dummyT then Abs (x, decodeT typ, decode t)
   115           else TypeInfer.constrain (Abs (x, map_type T, decode t)) (decodeT typ --> dummyT)
   116       | decode (Abs (x, T, t)) = Abs (x, map_type T, decode t)
   117       | decode (t $ u) = decode t $ decode u
   118       | decode (Const (a, T)) =
   119           let val c =
   120             (case try (unprefix Lexicon.constN) a of SOME c => c | NONE => perhaps map_const a)
   121           in Const (c, map_type T) end
   122       | decode (Free (a, T)) =
   123           (case (map_free a, map_const a) of
   124             (SOME x, _) => Free (x, map_type T)
   125           | (_, SOME c) => Const (c, map_type T)
   126           | _ => (if NameSpace.is_qualified a then Const else Free) (a, map_type T))
   127       | decode (Var (xi, T)) = Var (xi, map_type T)
   128       | decode (t as Bound _) = t;
   129   in decode tm end;
   130 
   131 
   132 
   133 (** output utils **)
   134 
   135 (* term_of_sort *)
   136 
   137 fun term_of_sort S =
   138   let
   139     fun class c = Lexicon.const "_class" $ Lexicon.free c;
   140 
   141     fun classes [] = sys_error "term_of_sort"
   142       | classes [c] = class c
   143       | classes (c :: cs) = Lexicon.const "_classes" $ class c $ classes cs;
   144   in
   145     (case S of
   146       [] => Lexicon.const "_topsort"
   147     | [c] => class c
   148     | cs => Lexicon.const "_sort" $ classes cs)
   149   end;
   150 
   151 
   152 (* term_of_typ *)
   153 
   154 fun term_of_typ show_sorts ty =
   155   let
   156     fun of_sort t S =
   157       if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S
   158       else t;
   159 
   160     fun term_of (Type (a, Ts)) = Term.list_comb (Lexicon.const a, map term_of Ts)
   161       | term_of (TFree (x, S)) = of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
   162       | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
   163   in term_of ty end;
   164 
   165 
   166 
   167 (** the type syntax **)
   168 
   169 (* print mode *)
   170 
   171 val bracketsN = "brackets";
   172 val no_bracketsN = "no_brackets";
   173 
   174 fun no_brackets () =
   175   find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN) (! print_mode)
   176     = SOME no_bracketsN;
   177 
   178 val type_bracketsN = "type_brackets";
   179 val no_type_bracketsN = "no_type_brackets";
   180 
   181 fun no_type_brackets () =
   182   find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN) (! print_mode)
   183     <> SOME type_bracketsN;
   184 
   185 
   186 (* parse ast translations *)
   187 
   188 fun tapp_ast_tr (*"_tapp"*) [ty, f] = Ast.Appl [f, ty]
   189   | tapp_ast_tr (*"_tapp"*) asts = raise Ast.AST ("tapp_ast_tr", asts);
   190 
   191 fun tappl_ast_tr (*"_tappl"*) [ty, tys, f] =
   192       Ast.Appl (f :: ty :: Ast.unfold_ast "_types" tys)
   193   | tappl_ast_tr (*"_tappl"*) asts = raise Ast.AST ("tappl_ast_tr", asts);
   194 
   195 fun bracket_ast_tr (*"_bracket"*) [dom, cod] =
   196       Ast.fold_ast_p "fun" (Ast.unfold_ast "_types" dom, cod)
   197   | bracket_ast_tr (*"_bracket"*) asts = raise Ast.AST ("bracket_ast_tr", asts);
   198 
   199 
   200 (* print ast translations *)
   201 
   202 fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f])
   203   | tappl_ast_tr' (f, [ty]) = Ast.Appl [Ast.Constant "_tapp", ty, f]
   204   | tappl_ast_tr' (f, ty :: tys) =
   205       Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f];
   206 
   207 fun fun_ast_tr' (*"fun"*) asts =
   208   if no_brackets () orelse no_type_brackets () then raise Match
   209   else
   210     (case Ast.unfold_ast_p "fun" (Ast.Appl (Ast.Constant "fun" :: asts)) of
   211       (dom as _ :: _ :: _, cod)
   212         => Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod]
   213     | _ => raise Match);
   214 
   215 
   216 (* type_ext *)
   217 
   218 val sortT = Type ("sort", []);
   219 val classesT = Type ("classes", []);
   220 val typesT = Type ("types", []);
   221 
   222 local open Lexicon SynExt in
   223 
   224 val type_ext = syn_ext' false (K false)
   225   [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
   226    Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
   227    Mfix ("_",           idT --> typeT,                 "", [], max_pri),
   228    Mfix ("_",           longidT --> typeT,             "", [], max_pri),
   229    Mfix ("_::_",        [tidT, sortT] ---> typeT,      "_ofsort", [max_pri, 0], max_pri),
   230    Mfix ("_::_",        [tvarT, sortT] ---> typeT,     "_ofsort", [max_pri, 0], max_pri),
   231    Mfix ("'_()::_",     sortT --> typeT,               "_dummy_ofsort", [0], max_pri),
   232    Mfix ("_",           idT --> sortT,                 "", [], max_pri),
   233    Mfix ("_",           longidT --> sortT,             "", [], max_pri),
   234    Mfix ("{}",          sortT,                         "_topsort", [], max_pri),
   235    Mfix ("{_}",         classesT --> sortT,            "_sort", [], max_pri),
   236    Mfix ("_",           idT --> classesT,              "", [], max_pri),
   237    Mfix ("_",           longidT --> classesT,          "", [], max_pri),
   238    Mfix ("_,_",         [idT, classesT] ---> classesT, "_classes", [], max_pri),
   239    Mfix ("_,_",         [longidT, classesT] ---> classesT, "_classes", [], max_pri),
   240    Mfix ("_ _",         [typeT, idT] ---> typeT,       "_tapp", [max_pri, 0], max_pri),
   241    Mfix ("_ _",         [typeT, longidT] ---> typeT,   "_tapp", [max_pri, 0], max_pri),
   242    Mfix ("((1'(_,/ _')) _)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri),
   243    Mfix ("((1'(_,/ _')) _)", [typeT, typesT, longidT] ---> typeT, "_tappl", [], max_pri),
   244    Mfix ("_",           typeT --> typesT,              "", [], max_pri),
   245    Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
   246    Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "fun", [1, 0], 0),
   247    Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0),
   248    Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri),
   249    Mfix ("'_",          typeT,                         "dummy", [], max_pri)]
   250   []
   251   (map SynExt.mk_trfun
   252    [("_tapp", K tapp_ast_tr), ("_tappl", K tappl_ast_tr), ("_bracket", K bracket_ast_tr)],
   253    [],
   254    [],
   255    map SynExt.mk_trfun [("fun", K fun_ast_tr')])
   256   (map (fn s => ("", s, Output.output_width)) SynExt.standard_token_classes)
   257   ([], []);
   258 
   259 end;
   260 
   261 end;