80 let |
80 let |
81 fun typ_of (Free (x, _)) = |
81 fun typ_of (Free (x, _)) = |
82 if Lexicon.is_tid x then TFree (x, get_sort (x, ~1)) |
82 if Lexicon.is_tid x then TFree (x, get_sort (x, ~1)) |
83 else Type (x, []) |
83 else Type (x, []) |
84 | typ_of (Var (xi, _)) = TVar (xi, get_sort xi) |
84 | typ_of (Var (xi, _)) = TVar (xi, get_sort xi) |
85 | typ_of (Const ("_tfree",_) $ (t as Free x)) = typ_of t |
85 | typ_of (Const ("_tfree",_) $ (t as Free _)) = typ_of t |
86 | typ_of (Const ("_tvar",_) $ (t as Var x)) = 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)) |
87 | typ_of (Const ("_ofsort", _) $ Free (x, _) $ _) = TFree (x, get_sort (x, ~1)) |
88 | typ_of (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ _) = |
88 | typ_of (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ _) = |
89 TFree (x, get_sort (x, ~1)) |
89 TFree (x, get_sort (x, ~1)) |
90 | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi) |
90 | typ_of (Const ("_ofsort", _) $ Var (xi, _) $ _) = TVar (xi, get_sort xi) |
91 | typ_of (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ _) = |
91 | typ_of (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ _) = |