src/Pure/Syntax/type_ext.ML
changeset 8895 2913a54e64cf
parent 7500 299949eddba8
child 9067 64464b5f6867
equal deleted inserted replaced
8894:0281bde335ca 8895:2913a54e64cf
     1 (*  Title:      Pure/Syntax/type_ext.ML
     1 (*  Title:      Pure/Syntax/type_ext.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     3     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     4 
     4 
     5 Utilities for input and output of types. Also the concrete syntax of
     5 Utilities for input and output of types.  Also the concrete syntax of
     6 types, which is used to bootstrap Pure.
     6 types, which is required to bootstrap Pure.
     7 *)
     7 *)
     8 
     8 
     9 signature TYPE_EXT0 =
     9 signature TYPE_EXT0 =
    10 sig
    10 sig
       
    11   val sort_of_term: term -> sort
    11   val raw_term_sorts: term -> (indexname * sort) list
    12   val raw_term_sorts: term -> (indexname * sort) list
    12   val typ_of_term: (indexname -> sort) -> term -> typ
    13   val typ_of_term: (indexname -> sort) -> term -> typ
    13   val term_of_typ: bool -> typ -> term
    14   val term_of_typ: bool -> typ -> term
    14 end;
    15 end;
    15 
    16 
    16 signature TYPE_EXT =
    17 signature TYPE_EXT =
    17 sig
    18 sig
    18   include TYPE_EXT0
    19   include TYPE_EXT0
    19   val term_of_sort: sort -> term
    20   val term_of_sort: sort -> term
    20   val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    21   val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
       
    22   val sortT: typ
    21   val type_ext: SynExt.syn_ext
    23   val type_ext: SynExt.syn_ext
    22 end;
    24 end;
    23 
    25 
    24 structure TypeExt : TYPE_EXT =
    26 structure TypeExt : TYPE_EXT =
    25 struct
    27 struct
    26 
    28 
    27 
    29 
    28 (** input utils **)
    30 (** input utils **)
    29 
    31 
    30 (* raw_term_sorts *)
    32 (* sort_of_term *)
    31 
    33 
    32 fun raw_term_sorts tm =
    34 fun sort_of_term tm =
    33   let
    35   let
    34     fun classes (Const (c, _)) = [c]
    36     fun classes (Const (c, _)) = [c]
    35       | classes (Free (c, _)) = [c]
    37       | classes (Free (c, _)) = [c]
    36       | classes (Const ("_classes", _) $ Const (c, _) $ cs) = c :: classes cs
    38       | classes (Const ("_classes", _) $ Const (c, _) $ cs) = c :: classes cs
    37       | classes (Const ("_classes", _) $ Free (c, _) $ cs) = c :: classes cs
    39       | classes (Const ("_classes", _) $ Free (c, _) $ cs) = c :: classes cs
    38       | classes tm = raise TERM ("raw_term_sorts: bad encoding of classes", [tm]);
    40       | classes tm = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
    39 
    41 
    40     fun sort (Const ("_topsort", _)) = []
    42     fun sort (Const ("_topsort", _)) = []
    41       | sort (Const (c, _)) = [c]
    43       | sort (Const (c, _)) = [c]
    42       | sort (Free (c, _)) = [c]
    44       | sort (Free (c, _)) = [c]
    43       | sort (Const ("_sort", _) $ cs) = classes cs
    45       | sort (Const ("_sort", _) $ cs) = classes cs
    44       | sort tm = raise TERM ("raw_term_sorts: bad encoding of sort", [tm]);
    46       | sort tm = raise TERM ("sort_of_term: bad encoding of sort", [tm]);
       
    47   in sort tm end;
    45 
    48 
    46     fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) env = ((x, ~1), sort cs) ins env
    49 
    47       | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) env = (xi, sort cs) ins env
    50 (* raw_term_sorts *)
       
    51 
       
    52 fun raw_term_sorts tm =
       
    53   let
       
    54     fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) env = ((x, ~1), sort_of_term cs) ins env
       
    55       | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) env = (xi, sort_of_term cs) ins env
    48       | add_env (Abs (_, _, t)) env = add_env t env
    56       | add_env (Abs (_, _, t)) env = add_env t env
    49       | add_env (t1 $ t2) env = add_env t1 (add_env t2 env)
    57       | add_env (t1 $ t2) env = add_env t1 (add_env t2 env)
    50       | add_env t env = env;
    58       | add_env t env = env;
    51   in
    59   in add_env tm [] end;
    52     add_env tm []
       
    53   end;
       
    54 
    60 
    55 
    61 
    56 (* typ_of_term *)
    62 (* typ_of_term *)
    57 
    63 
    58 fun typ_of_term get_sort t =
    64 fun typ_of_term get_sort t =
    74               | Free (x, _) => x
    80               | Free (x, _) => x
    75               | _ => raise TERM ("typ_of_term: bad encoding of type", [tm]));
    81               | _ => raise TERM ("typ_of_term: bad encoding of type", [tm]));
    76           in
    82           in
    77             Type (a, map typ_of ts)
    83             Type (a, map typ_of ts)
    78           end;
    84           end;
    79   in
    85   in typ_of t end;
    80     typ_of t
       
    81   end;
       
    82 
    86 
    83 
    87 
    84 
    88 
    85 (** output utils **)
    89 (** output utils **)
    86 
    90 
   110       else t;
   114       else t;
   111 
   115 
   112     fun term_of (Type (a, Ts)) = list_comb (Lexicon.const a, map term_of Ts)
   116     fun term_of (Type (a, Ts)) = list_comb (Lexicon.const a, map term_of Ts)
   113       | term_of (TFree (x, S)) = of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
   117       | term_of (TFree (x, S)) = of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
   114       | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
   118       | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
   115   in
   119   in term_of ty end;
   116     term_of ty
       
   117   end;
       
   118 
   120 
   119 
   121 
   120 
   122 
   121 (** the type syntax **)
   123 (** the type syntax **)
   122 
   124 
   189   TokenTrans.token_translation
   191   TokenTrans.token_translation
   190   ([], []);
   192   ([], []);
   191 
   193 
   192 end;
   194 end;
   193 
   195 
   194 
       
   195 end;
   196 end;