added sort_of_term;
authorwenzelm
Sun May 21 14:32:47 2000 +0200 (2000-05-21)
changeset 88952913a54e64cf
parent 8894 0281bde335ca
child 8896 c80aba8c1d5e
added sort_of_term;
export sortT;
src/Pure/Syntax/type_ext.ML
     1.1 --- a/src/Pure/Syntax/type_ext.ML	Sun May 21 14:31:41 2000 +0200
     1.2 +++ b/src/Pure/Syntax/type_ext.ML	Sun May 21 14:32:47 2000 +0200
     1.3 @@ -2,12 +2,13 @@
     1.4      ID:         $Id$
     1.5      Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Utilities for input and output of types. Also the concrete syntax of
     1.8 -types, which is used to bootstrap Pure.
     1.9 +Utilities for input and output of types.  Also the concrete syntax of
    1.10 +types, which is required to bootstrap Pure.
    1.11  *)
    1.12  
    1.13  signature TYPE_EXT0 =
    1.14  sig
    1.15 +  val sort_of_term: term -> sort
    1.16    val raw_term_sorts: term -> (indexname * sort) list
    1.17    val typ_of_term: (indexname -> sort) -> term -> typ
    1.18    val term_of_typ: bool -> typ -> term
    1.19 @@ -18,6 +19,7 @@
    1.20    include TYPE_EXT0
    1.21    val term_of_sort: sort -> term
    1.22    val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    1.23 +  val sortT: typ
    1.24    val type_ext: SynExt.syn_ext
    1.25  end;
    1.26  
    1.27 @@ -27,30 +29,34 @@
    1.28  
    1.29  (** input utils **)
    1.30  
    1.31 -(* raw_term_sorts *)
    1.32 +(* sort_of_term *)
    1.33  
    1.34 -fun raw_term_sorts tm =
    1.35 +fun sort_of_term tm =
    1.36    let
    1.37      fun classes (Const (c, _)) = [c]
    1.38        | classes (Free (c, _)) = [c]
    1.39        | classes (Const ("_classes", _) $ Const (c, _) $ cs) = c :: classes cs
    1.40        | classes (Const ("_classes", _) $ Free (c, _) $ cs) = c :: classes cs
    1.41 -      | classes tm = raise TERM ("raw_term_sorts: bad encoding of classes", [tm]);
    1.42 +      | classes tm = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
    1.43  
    1.44      fun sort (Const ("_topsort", _)) = []
    1.45        | sort (Const (c, _)) = [c]
    1.46        | sort (Free (c, _)) = [c]
    1.47        | sort (Const ("_sort", _) $ cs) = classes cs
    1.48 -      | sort tm = raise TERM ("raw_term_sorts: bad encoding of sort", [tm]);
    1.49 +      | sort tm = raise TERM ("sort_of_term: bad encoding of sort", [tm]);
    1.50 +  in sort tm end;
    1.51 +
    1.52  
    1.53 -    fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) env = ((x, ~1), sort cs) ins env
    1.54 -      | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) env = (xi, sort cs) ins env
    1.55 +(* raw_term_sorts *)
    1.56 +
    1.57 +fun raw_term_sorts tm =
    1.58 +  let
    1.59 +    fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) env = ((x, ~1), sort_of_term cs) ins env
    1.60 +      | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) env = (xi, sort_of_term cs) ins env
    1.61        | add_env (Abs (_, _, t)) env = add_env t env
    1.62        | add_env (t1 $ t2) env = add_env t1 (add_env t2 env)
    1.63        | add_env t env = env;
    1.64 -  in
    1.65 -    add_env tm []
    1.66 -  end;
    1.67 +  in add_env tm [] end;
    1.68  
    1.69  
    1.70  (* typ_of_term *)
    1.71 @@ -76,9 +82,7 @@
    1.72            in
    1.73              Type (a, map typ_of ts)
    1.74            end;
    1.75 -  in
    1.76 -    typ_of t
    1.77 -  end;
    1.78 +  in typ_of t end;
    1.79  
    1.80  
    1.81  
    1.82 @@ -112,9 +116,7 @@
    1.83      fun term_of (Type (a, Ts)) = list_comb (Lexicon.const a, map term_of Ts)
    1.84        | term_of (TFree (x, S)) = of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
    1.85        | term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
    1.86 -  in
    1.87 -    term_of ty
    1.88 -  end;
    1.89 +  in term_of ty end;
    1.90  
    1.91  
    1.92  
    1.93 @@ -191,5 +193,4 @@
    1.94  
    1.95  end;
    1.96  
    1.97 -
    1.98  end;