src/Pure/Syntax/type_ext.ML
author wenzelm
Wed Jun 02 11:09:26 2010 +0200 (2010-06-02 ago)
changeset 37251 72c7e636067b
parent 37216 3165bc303f66
child 39288 f1ae2493d93f
permissions -rw-r--r--
normalize and postprocess proof body in a separate future, taking care of platforms without multithreading (greately improves parallelization in general without the overhead of promised proofs, cf. usedir -q 0);
     1 (*  Title:      Pure/Syntax/type_ext.ML
     2     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     3 
     4 Utilities for input and output of types.  The concrete syntax of types.
     5 *)
     6 
     7 signature TYPE_EXT0 =
     8 sig
     9   val sort_of_term: term -> sort
    10   val term_sorts: term -> (indexname * sort) list
    11   val typ_of_term: (indexname -> sort) -> term -> typ
    12   val type_constraint: typ -> term -> term
    13   val decode_term: (((string * int) * sort) list -> string * int -> sort) ->
    14     (string -> bool * string) -> (string -> string option) -> term -> term
    15   val term_of_typ: bool -> typ -> term
    16   val no_brackets: unit -> bool
    17   val no_type_brackets: unit -> bool
    18   val type_ast_trs:
    19    {read_class: Proof.context -> string -> string,
    20     read_type: Proof.context -> string -> string} ->
    21     (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
    22 end;
    23 
    24 signature TYPE_EXT =
    25 sig
    26   include TYPE_EXT0
    27   val term_of_sort: sort -> term
    28   val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    29   val sortT: typ
    30   val type_ext: Syn_Ext.syn_ext
    31 end;
    32 
    33 structure Type_Ext: TYPE_EXT =
    34 struct
    35 
    36 (** input utils **)
    37 
    38 (* sort_of_term *)
    39 
    40 fun sort_of_term tm =
    41   let
    42     fun err () = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
    43 
    44     fun class s = Lexicon.unmark_class s handle Fail _ => err ();
    45 
    46     fun classes (Const (s, _)) = [class s]
    47       | classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs
    48       | classes _ = err ();
    49 
    50     fun sort (Const ("_topsort", _)) = []
    51       | sort (Const (s, _)) = [class s]
    52       | sort (Const ("_sort", _) $ cs) = classes cs
    53       | sort _ = err ();
    54   in sort tm end;
    55 
    56 
    57 (* term_sorts *)
    58 
    59 fun term_sorts tm =
    60   let
    61     val sort_of = sort_of_term;
    62 
    63     fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) =
    64           insert (op =) ((x, ~1), sort_of cs)
    65       | add_env (Const ("_ofsort", _) $ (Const ("_tfree", _) $ Free (x, _)) $ cs) =
    66           insert (op =) ((x, ~1), sort_of cs)
    67       | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) =
    68           insert (op =) (xi, sort_of cs)
    69       | add_env (Const ("_ofsort", _) $ (Const ("_tvar", _) $ Var (xi, _)) $ cs) =
    70           insert (op =) (xi, sort_of cs)
    71       | add_env (Abs (_, _, t)) = add_env t
    72       | add_env (t1 $ t2) = add_env t1 #> add_env t2
    73       | add_env _ = I;
    74   in add_env tm [] end;
    75 
    76 
    77 (* typ_of_term *)
    78 
    79 fun typ_of_term get_sort tm =
    80   let
    81     fun err () = raise TERM ("typ_of_term: bad encoding of type", [tm]);
    82 
    83     fun typ_of (Free (x, _)) = TFree (x, get_sort (x, ~1))
    84       | typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
    85       | typ_of (Const ("_tfree",_) $ (t as Free _)) = typ_of t
    86       | typ_of (Const ("_tvar",_) $ (t as Var _)) = typ_of t
    87       | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = TFree (x, get_sort (x, ~1))
    88       | typ_of (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ _) =
    89           TFree (x, get_sort (x, ~1))
    90       | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi)
    91       | typ_of (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ _) =
    92           TVar (xi, get_sort xi)
    93       | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", sort_of_term t)
    94       | typ_of t =
    95           let
    96             val (head, args) = Term.strip_comb t;
    97             val a =
    98               (case head of
    99                 Const (c, _) => (Lexicon.unmark_type c handle Fail _ => err ())
   100               | _ => err ());
   101           in Type (a, map typ_of args) end;
   102   in typ_of tm end;
   103 
   104 
   105 (* decode_term -- transform parse tree into raw term *)
   106 
   107 fun type_constraint T t =
   108   if T = dummyT then t
   109   else Const ("_type_constraint_", T --> T) $ t;
   110 
   111 fun decode_term get_sort map_const map_free tm =
   112   let
   113     val decodeT = typ_of_term (get_sort (term_sorts tm));
   114 
   115     fun decode (Const ("_constrain", _) $ t $ typ) =
   116           type_constraint (decodeT typ) (decode t)
   117       | decode (Const ("_constrainAbs", _) $ (Abs (x, T, t)) $ typ) =
   118           if T = dummyT then Abs (x, decodeT typ, decode t)
   119           else type_constraint (decodeT typ --> dummyT) (Abs (x, T, decode t))
   120       | decode (Abs (x, T, t)) = Abs (x, T, decode t)
   121       | decode (t $ u) = decode t $ decode u
   122       | decode (Const (a, T)) =
   123           (case try Lexicon.unmark_fixed a of
   124             SOME x => Free (x, T)
   125           | NONE =>
   126               let val c =
   127                 (case try Lexicon.unmark_const a of
   128                   SOME c => c
   129                 | NONE => snd (map_const a))
   130               in Const (c, T) end)
   131       | decode (Free (a, T)) =
   132           (case (map_free a, map_const a) of
   133             (SOME x, _) => Free (x, T)
   134           | (_, (true, c)) => Const (c, T)
   135           | (_, (false, c)) => (if Long_Name.is_qualified c then Const else Free) (c, T))
   136       | decode (Var (xi, T)) = Var (xi, T)
   137       | decode (t as Bound _) = t;
   138   in decode tm end;
   139 
   140 
   141 
   142 (** output utils **)
   143 
   144 (* term_of_sort *)
   145 
   146 fun term_of_sort S =
   147   let
   148     val class = Lexicon.const o Lexicon.mark_class;
   149 
   150     fun classes [c] = class c
   151       | classes (c :: cs) = Lexicon.const "_classes" $ class c $ classes cs;
   152   in
   153     (case S of
   154       [] => Lexicon.const "_topsort"
   155     | [c] => class c
   156     | cs => Lexicon.const "_sort" $ classes cs)
   157   end;
   158 
   159 
   160 (* term_of_typ *)
   161 
   162 fun term_of_typ show_sorts ty =
   163   let
   164     fun of_sort t S =
   165       if show_sorts then Lexicon.const "_ofsort" $ t $ term_of_sort S
   166       else t;
   167 
   168     fun term_of (Type (a, Ts)) =
   169           Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts)
   170       | term_of (TFree (x, S)) = of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
   171       | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
   172   in term_of ty end;
   173 
   174 
   175 
   176 (** the type syntax **)
   177 
   178 (* print mode *)
   179 
   180 val bracketsN = "brackets";
   181 val no_bracketsN = "no_brackets";
   182 
   183 fun no_brackets () =
   184   find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN)
   185     (print_mode_value ()) = SOME no_bracketsN;
   186 
   187 val type_bracketsN = "type_brackets";
   188 val no_type_bracketsN = "no_type_brackets";
   189 
   190 fun no_type_brackets () =
   191   find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN)
   192     (print_mode_value ()) <> SOME type_bracketsN;
   193 
   194 
   195 (* parse ast translations *)
   196 
   197 val class_ast = Ast.Constant o Lexicon.mark_class;
   198 val type_ast = Ast.Constant o Lexicon.mark_type;
   199 
   200 fun class_name_tr read_class (*"_class_name"*) [Ast.Variable c] = class_ast (read_class c)
   201   | class_name_tr _ (*"_class_name"*) asts = raise Ast.AST ("class_name_tr", asts);
   202 
   203 fun classes_tr read_class (*"_classes"*) [Ast.Variable c, ast] =
   204       Ast.mk_appl (Ast.Constant "_classes") [class_ast (read_class c), ast]
   205   | classes_tr _ (*"_classes"*) asts = raise Ast.AST ("classes_tr", asts);
   206 
   207 fun type_name_tr read_type (*"_type_name"*) [Ast.Variable c] = type_ast (read_type c)
   208   | type_name_tr _ (*"_type_name"*) asts = raise Ast.AST ("type_name_tr", asts);
   209 
   210 fun tapp_ast_tr read_type (*"_tapp"*) [ty, Ast.Variable c] =
   211       Ast.Appl [type_ast (read_type c), ty]
   212   | tapp_ast_tr _ (*"_tapp"*) asts = raise Ast.AST ("tapp_ast_tr", asts);
   213 
   214 fun tappl_ast_tr read_type (*"_tappl"*) [ty, tys, Ast.Variable c] =
   215       Ast.Appl (type_ast (read_type c) :: ty :: Ast.unfold_ast "_types" tys)
   216   | tappl_ast_tr _ (*"_tappl"*) asts = raise Ast.AST ("tappl_ast_tr", asts);
   217 
   218 fun bracket_ast_tr (*"_bracket"*) [dom, cod] =
   219       Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
   220   | bracket_ast_tr (*"_bracket"*) asts = raise Ast.AST ("bracket_ast_tr", asts);
   221 
   222 
   223 (* print ast translations *)
   224 
   225 fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f])
   226   | tappl_ast_tr' (f, [ty]) = Ast.Appl [Ast.Constant "_tapp", ty, f]
   227   | tappl_ast_tr' (f, ty :: tys) =
   228       Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f];
   229 
   230 fun fun_ast_tr' (*"\\<^type>fun"*) asts =
   231   if no_brackets () orelse no_type_brackets () then raise Match
   232   else
   233     (case Ast.unfold_ast_p "\\<^type>fun" (Ast.Appl (Ast.Constant "\\<^type>fun" :: asts)) of
   234       (dom as _ :: _ :: _, cod)
   235         => Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod]
   236     | _ => raise Match);
   237 
   238 
   239 (* type_ext *)
   240 
   241 val sortT = Type ("sort", []);
   242 val classesT = Type ("classes", []);
   243 val typesT = Type ("types", []);
   244 
   245 local open Lexicon Syn_Ext in
   246 
   247 val type_ext = syn_ext' false (K false)
   248   [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
   249    Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
   250    Mfix ("_",           idT --> typeT,                 "_type_name", [], max_pri),
   251    Mfix ("_",           longidT --> typeT,             "_type_name", [], max_pri),
   252    Mfix ("_::_",        [tidT, sortT] ---> typeT,      "_ofsort", [max_pri, 0], max_pri),
   253    Mfix ("_::_",        [tvarT, sortT] ---> typeT,     "_ofsort", [max_pri, 0], max_pri),
   254    Mfix ("'_()::_",     sortT --> typeT,               "_dummy_ofsort", [0], max_pri),
   255    Mfix ("_",           idT --> sortT,                 "_class_name", [], max_pri),
   256    Mfix ("_",           longidT --> sortT,             "_class_name", [], max_pri),
   257    Mfix ("{}",          sortT,                         "_topsort", [], max_pri),
   258    Mfix ("{_}",         classesT --> sortT,            "_sort", [], max_pri),
   259    Mfix ("_",           idT --> classesT,              "_class_name", [], max_pri),
   260    Mfix ("_",           longidT --> classesT,          "_class_name", [], max_pri),
   261    Mfix ("_,_",         [idT, classesT] ---> classesT, "_classes", [], max_pri),
   262    Mfix ("_,_",         [longidT, classesT] ---> classesT, "_classes", [], max_pri),
   263    Mfix ("_ _",         [typeT, idT] ---> typeT,       "_tapp", [max_pri, 0], max_pri),
   264    Mfix ("_ _",         [typeT, longidT] ---> typeT,   "_tapp", [max_pri, 0], max_pri),
   265    Mfix ("((1'(_,/ _')) _)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri),
   266    Mfix ("((1'(_,/ _')) _)", [typeT, typesT, longidT] ---> typeT, "_tappl", [], max_pri),
   267    Mfix ("_",           typeT --> typesT,              "", [], max_pri),
   268    Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
   269    Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "\\<^type>fun", [1, 0], 0),
   270    Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0),
   271    Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri),
   272    Mfix ("'_",          typeT,                         "\\<^type>dummy", [], max_pri)]
   273   ["_type_prop"]
   274   ([], [], [], map Syn_Ext.mk_trfun [("\\<^type>fun", K fun_ast_tr')])
   275   []
   276   ([], []);
   277 
   278 fun type_ast_trs {read_class, read_type} =
   279  [("_class_name", class_name_tr o read_class),
   280   ("_classes", classes_tr o read_class),
   281   ("_type_name", type_name_tr o read_type),
   282   ("_tapp", tapp_ast_tr o read_type),
   283   ("_tappl", tappl_ast_tr o read_type),
   284   ("_bracket", K bracket_ast_tr)];
   285 
   286 end;
   287 
   288 end;