src/Pure/Syntax/type_ext.ML
changeset 14255 e6e3e3f0deed
parent 14086 a9be38579840
child 14838 b12855d44c97
     1.1 --- a/src/Pure/Syntax/type_ext.ML	Thu Nov 06 14:18:05 2003 +0100
     1.2 +++ b/src/Pure/Syntax/type_ext.ML	Thu Nov 06 20:45:02 2003 +0100
     1.3 @@ -44,6 +44,7 @@
     1.4      fun sort (Const ("_topsort", _)) = []
     1.5        | sort (Const (c, _)) = [c]
     1.6        | sort (Free (c, _)) = [c]
     1.7 +      | sort (Const ("_class",_) $ Free (c, _)) = [c]
     1.8        | sort (Const ("_sort", _) $ cs) = classes cs
     1.9        | sort tm = raise TERM ("sort_of_term: bad encoding of sort", [tm]);
    1.10    in sort tm end;
    1.11 @@ -54,7 +55,11 @@
    1.12  fun raw_term_sorts tm =
    1.13    let
    1.14      fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) env = ((x, ~1), sort_of_term cs) ins env
    1.15 +      | add_env (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ cs) env 
    1.16 +                = ((x, ~1), sort_of_term cs) ins env
    1.17        | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) env = (xi, sort_of_term cs) ins env
    1.18 +      | add_env (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ cs) env 
    1.19 +                = (xi, sort_of_term cs) ins env
    1.20        | add_env (Abs (_, _, t)) env = add_env t env
    1.21        | add_env (t1 $ t2) env = add_env t1 (add_env t2 env)
    1.22        | add_env t env = env;
    1.23 @@ -69,9 +74,16 @@
    1.24            if Lexicon.is_tid x then TFree (x, get_sort (x, ~1))
    1.25            else Type (x, [])
    1.26        | typ_of (Var (xi, _)) = TVar (xi, get_sort xi)
    1.27 +      | typ_of (Const ("_tfree",_) $ (t as Free x)) = typ_of t
    1.28 +      | typ_of (Const ("_tvar",_) $ (t as Var x)) = typ_of t
    1.29        | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = TFree (x, get_sort (x, ~1))
    1.30 +      | typ_of (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ _) 
    1.31 +               = TFree (x, get_sort (x, ~1))
    1.32        | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi)
    1.33 +      | typ_of (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ _) 
    1.34 +               = TVar (xi, get_sort xi)
    1.35        | typ_of (Const ("_dummy_ofsort", _) $ t) = TFree ("'_dummy_", map_sort (sort_of_term t))
    1.36 +     
    1.37        | typ_of tm =
    1.38            let
    1.39              val (t, ts) = strip_comb tm;