Skip to content

Commit

Permalink
improved look of types
Browse files Browse the repository at this point in the history 
git-svn-id: https://svn-agbkb.informatik.uni-bremen.de/Hets/trunk@4976 cec4b9c1-7d33-0410-9eda-942365e851bb
  • Loading branch information
Christian Maeder authored and Christian Maeder committed Aug 24, 2005
1 parent bd1c99a commit 2986838
Show file tree
Hide file tree
Showing 31 changed files with 1,376 additions and 4,596 deletions.
9 changes: 5 additions & 4 deletions HasCASL/PrintAs.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -75,9 +75,10 @@ parenPrec p1 (p2, d) = if p2 < p1 then d else BracketType Parens [d] nullRange

toMixType :: Type -> (TypePrec, Type)
toMixType typ = case typ of
ExpandedType t1 t2 -> (Prefix, ExpandedType
ExpandedType t1 _ -> toMixType t1
{- (Prefix, ExpandedType
(parenPrec Prefix $ toMixType t1)
$ parenPrec Prefix $ toMixType t2)
$ parenPrec Prefix $ toMixType t2) -}
BracketType k l ps -> (Outfix, BracketType k (map
(snd . toMixType) l) ps)
KindedType t kind ps -> (Prefix, KindedType
Expand Down Expand Up @@ -119,8 +120,8 @@ toMixType typ = case typ of

printType :: GlobalAnnos -> Type -> Doc
printType ga ty = case ty of
TypeName name _k i -> printText0 ga name <>
if i == 0 then empty else text ("_v"++ show i)
TypeName name _ _ -> printText0 ga name
-- if i == 0 then empty else text ("_v"++ show i)
TypeAppl t1 t2 -> parens (printType ga t1) <>
parens (printType ga t2)
ExpandedType t1 t2 -> printType ga t1 <> text asP <> printType ga t2
Expand Down
2 changes: 1 addition & 1 deletion HasCASL/SubtypeDecl.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ addSuperType t ak p@(i, nAs) =
newSubTypeIdentifier :: Id -> State Env Id
newSubTypeIdentifier i = do
n <- toEnvState inc
return $ simpleIdToId $ Token ("_subtype_" ++ show n) $ posOfId i
return $ simpleIdToId $ Token ("_t" ++ show n) $ posOfId i

rawToKind :: RawKind -> Kind
rawToKind = mapKind (const universeId)
Expand Down
2 changes: 1 addition & 1 deletion HasCASL/Unify.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,7 @@ inc = do
freshVar :: Range -> State Int (Id, Int)
freshVar ps = do
c <- inc
return (simpleIdToId $ Token ("_var_" ++ show c) ps, c)
return (simpleIdToId $ Token ("_v" ++ show c) ps, c)

mkSingleSubst :: (Id, RawKind) -> State Int Type
mkSingleSubst (i, rk) = do
Expand Down
62 changes: 30 additions & 32 deletions HasCASL/test/Alias.hascasl.output
View file
Original file line number Diff line number Diff line change
@@ -1,24 +1,24 @@
var s : Type
type MyPred : Type -> Type := \ s : Type . s_v-1 ->? Unit
type MyAlias : Type -> Type := \ t : Type . t_v-1 ->? Unit
type a1 : Type -> Type -> Type := \ (a : Type)(b : Type) . a_v-1 ->
b_v-2 -> Unit
type a1 : Type -> Type -> Type := \ (a : Type)(b : Type) . a_v-1 ->
b_v-2 -> Unit
type a1 : Type -> Type -> Type := \ (a : Type)(b : Type) . a_v-1 ->
b_v-2 -> Unit
type a2 : Type -> Type -> Type := \ a : Type . a_v-1 -> Unit
type a3 : Type -> Type -> Type := \ a : Type . a_v-1 -> Unit
type a4 : Type -> Type -> Type := \ a : Type . a_v-1 -> Unit
type MyPred : Type -> Type := \ s : Type . s ->? Unit
type MyAlias : Type -> Type := \ t : Type . t ->? Unit
type a1 : Type -> Type -> Type := \ (a : Type)(b : Type) . a ->
b -> Unit
type a1 : Type -> Type -> Type := \ (a : Type)(b : Type) . a ->
b -> Unit
type a1 : Type -> Type -> Type := \ (a : Type)(b : Type) . a ->
b -> Unit
type a2 : Type -> Type -> Type := \ a : Type . a -> Unit
type a3 : Type -> Type -> Type := \ a : Type . a -> Unit
type a4 : Type -> Type -> Type := \ a : Type . a -> Unit
type a5(a : Type)
type a6(a : Type)
type a7 : Type -> Type := \ a : Type . a6 a_v-1 -> Unit
type a7 : Type -> Type := \ a : Type . a6 a -> Unit
%% Type Constructors -----------------------------------------------------
? : +Type -> Type
Logical : Type := ? Unit
MyAlias : Type -> Type := \ t : Type . t_v-1 ->? Unit
MyPred : Type -> Type := \ s : Type . s_v-1 ->? Unit
Pred : -Type -> Type := \ a : -Type . a_v-1 ->? Unit
MyAlias : Type -> Type := \ t : Type . t ->? Unit
MyPred : Type -> Type := \ s : Type . s ->? Unit
Pred : -Type -> Type := \ a : -Type . a ->? Unit
Unit : Type
__*__ : +Type -> +Type -> Type
__*__*__ : +Type -> +Type -> +Type -> Type
Expand All @@ -29,28 +29,26 @@ __-->?__ : -Type -> +Type -> Type < __->?__
__->__ : -Type -> +Type -> Type < __->?__
__->?__ : -Type -> +Type -> Type
a1
: Type -> Type -> Type
:= \ (a : Type)(b : Type) . a_v-1 -> b_v-2 -> Unit
a2 : Type -> Type -> Type := \ a : Type . a_v-1 -> Unit
a3 : Type -> Type -> Type := \ a : Type . a_v-1 -> Unit
a4 : Type -> Type -> Type := \ a : Type . a_v-1 -> Unit
: Type -> Type -> Type := \ (a : Type)(b : Type) . a -> b -> Unit
a2 : Type -> Type -> Type := \ a : Type . a -> Unit
a3 : Type -> Type -> Type := \ a : Type . a -> Unit
a4 : Type -> Type -> Type := \ a : Type . a -> Unit
a5 : Type -> Type
a6 : Type -> Type
a7 : Type -> Type := \ a : Type . a6 a_v-1 -> Unit
a7 : Type -> Type := \ a : Type . a6 a -> Unit
%% Type Variables --------------------------------------------------------
s : Type %(var_1)%
%% Assumptions -----------------------------------------------------------
__/\__ : ? Unit * ? Unit ->? Unit %(fun)%
__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%
__=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%
__=__ : forall a : Type . a * a ->? Unit %(fun)%
__=>__ : ? Unit * ? Unit ->? Unit %(fun)%
__=e=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%
__=e=__ : forall a : Type . a * a ->? Unit %(fun)%
__\/__ : ? Unit * ? Unit ->? Unit %(fun)%
__if__ : ? Unit * ? Unit ->? Unit %(fun)%
__when__else__
: forall a : Type . a_v-1 * ? Unit * a_v-1 ->? a_v-1 %(fun)%
bottom : forall a : Type . a_v-1 %(fun)%
def__ : forall a : Type . a_v-1 ->? Unit %(fun)%
__when__else__ : forall a : Type . a * ? Unit * a ->? a %(fun)%
bottom : forall a : Type . a %(fun)%
def__ : forall a : Type . a ->? Unit %(fun)%
false : Unit %(fun)%
not__ : ? Unit ->? Unit %(fun)%
true : Unit %(fun)%
Expand All @@ -70,21 +68,21 @@ true : Unit %(fun)%
*** Warning 9.15, missing kind for type variable 'a'
*** Warning 9.19, missing kind for type variable 'b'
*** Warning 9.24-9.29, ignoring unused variable(s)
b in 'a_v10 -> Unit'
b in 'a -> Unit'
*** Warning 11.15, missing kind for type variable 'a'
*** Hint 11.19, rebound type variable 'a'
*** Warning 11.24-11.29, ignoring unused variable(s)
a in 'a_v13 -> Unit'
a in 'a -> Unit'
*** Error 11.15, duplicates at '(11,19)' for 'a'
*** Warning 13.9, missing kind for type variable 'a'
*** Hint 13.11, rebound type variable 'a'
*** Warning 13.16-13.21, ignoring unused variable(s)
a in 'a_v15 -> Unit'
a in 'a -> Unit'
*** Error 13.9, duplicates at '(13,11)' for 'a'
*** Warning 15.9, missing kind for type variable 'a'
*** Warning 17.9, missing kind for type variable 'a'
*** Error 17.14-17.22, illegal recursive type synonym 'a5 a_v17 -> Unit'
*** Error 17.14-17.22, illegal recursive type synonym 'a5 a -> Unit'
*** Warning 19.9, missing kind for type variable 'a'
*** Warning 21.9, missing kind for type variable 'a'
*** Warning 23.9, missing kind for type variable 'a'
*** Error 21.14-23.22, illegal recursive type synonym '(a7 a_v20)@(a6 a_v20 -> Unit) -> Unit'
*** Error 21.14-23.22, illegal recursive type synonym 'a7 a -> Unit'
13 changes: 6 additions & 7 deletions HasCASL/test/AsPattern.hascasl.output
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ program (op f : a -> a)(v : a @ (var _ : a)) : a = (var v : a)
%% Type Constructors -----------------------------------------------------
? : +Type -> Type
Logical : Type := ? Unit
Pred : -Type -> Type := \ a : -Type . a_v-1 ->? Unit
Pred : -Type -> Type := \ a : -Type . a ->? Unit
Unit : Type
__*__ : +Type -> +Type -> Type
__*__*__ : +Type -> +Type -> +Type -> Type
Expand All @@ -18,15 +18,14 @@ a : Type
%% Assumptions -----------------------------------------------------------
__/\__ : ? Unit * ? Unit ->? Unit %(fun)%
__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%
__=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%
__=__ : forall a : Type . a * a ->? Unit %(fun)%
__=>__ : ? Unit * ? Unit ->? Unit %(fun)%
__=e=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%
__=e=__ : forall a : Type . a * a ->? Unit %(fun)%
__\/__ : ? Unit * ? Unit ->? Unit %(fun)%
__if__ : ? Unit * ? Unit ->? Unit %(fun)%
__when__else__
: forall a : Type . a_v-1 * ? Unit * a_v-1 ->? a_v-1 %(fun)%
bottom : forall a : Type . a_v-1 %(fun)%
def__ : forall a : Type . a_v-1 ->? Unit %(fun)%
__when__else__ : forall a : Type . a * ? Unit * a ->? a %(fun)%
bottom : forall a : Type . a %(fun)%
def__ : forall a : Type . a ->? Unit %(fun)%
f : a -> a %(op)%
false : Unit %(fun)%
not__ : ? Unit ->? Unit %(fun)%
Expand Down
13 changes: 6 additions & 7 deletions HasCASL/test/B1.hascasl.output
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ h < (c, a)
%% Type Constructors -----------------------------------------------------
? : +Type -> Type
Logical : Type := ? Unit
Pred : -Type -> Type := \ a : -Type . a_v-1 ->? Unit
Pred : -Type -> Type := \ a : -Type . a ->? Unit
Unit : Type
[__] : a -> b
__*__ : +Type -> +Type -> Type
Expand All @@ -46,15 +46,14 @@ y : Type %(var_2)%
%% Assumptions -----------------------------------------------------------
__/\__ : ? Unit * ? Unit ->? Unit %(fun)%
__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%
__=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%
__=__ : forall a : Type . a * a ->? Unit %(fun)%
__=>__ : ? Unit * ? Unit ->? Unit %(fun)%
__=e=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%
__=e=__ : forall a : Type . a * a ->? Unit %(fun)%
__\/__ : ? Unit * ? Unit ->? Unit %(fun)%
__if__ : ? Unit * ? Unit ->? Unit %(fun)%
__when__else__
: forall a : Type . a_v-1 * ? Unit * a_v-1 ->? a_v-1 %(fun)%
bottom : forall a : Type . a_v-1 %(fun)%
def__ : forall a : Type . a_v-1 ->? Unit %(fun)%
__when__else__ : forall a : Type . a * ? Unit * a ->? a %(fun)%
bottom : forall a : Type . a %(fun)%
def__ : forall a : Type . a ->? Unit %(fun)%
false : Unit %(fun)%
not__ : ? Unit ->? Unit %(fun)%
true : Unit %(fun)%
Expand Down
39 changes: 19 additions & 20 deletions HasCASL/test/BasicSpec.hascasl.output
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ pred eq : s * s
type s < ? s
forall x : t; y : t
. %(..)%
((fun __=__[t] : forall a : Type . a_v-1 * a_v-1 ->? Unit) :
((fun __=__[t] : forall a : Type . a * a ->? Unit) :
t * t ->? Unit)
(var x : t, var y : t) :
Unit
Expand Down Expand Up @@ -61,7 +61,7 @@ Data4
::= Cons41 : Data1 * Data2 ->? Data4 (sel1 :? Data1; sel2 :? Data2)
Cons42 : Data2 * Data1 ->? Data4 (sel2 :? Data2; sel1 :? Data1)]%
Logical : Type := ? Unit
Pred : -Type -> Type := \ a : -Type . a_v-1 ->? Unit
Pred : -Type -> Type := \ a : -Type . a ->? Unit
Unit : (TYPE, Type)
__*__ : +Type -> +Type -> Type
__*__*__ : +Type -> +Type -> +Type -> Type
Expand All @@ -83,19 +83,18 @@ Cons41 : Data1 * Data2 ->? Data4 %(construct Data4)%
Cons42 : Data2 * Data1 ->? Data4 %(construct Data4)%
__/\__ : ? Unit * ? Unit ->? Unit %(fun)%
__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%
__=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%
__=__ : forall a : Type . a * a ->? Unit %(fun)%
__=>__ : ? Unit * ? Unit ->? Unit %(fun)%
__=e=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit %(fun)%
__=e=__ : forall a : Type . a * a ->? Unit %(fun)%
__\/__ : ? Unit * ? Unit ->? Unit %(fun)%
__if__ : ? Unit * ? Unit ->? Unit %(fun)%
__when__else__
: forall a : Type . a_v-1 * ? Unit * a_v-1 ->? a_v-1 %(fun)%
__when__else__ : forall a : Type . a * ? Unit * a ->? a %(fun)%
a : Data1 %(construct Data1)%
: ? s %(op)%
b : Data1 %(construct Data1)%
bottom : forall a : Type . a_v-1 %(fun)%
bottom : forall a : Type . a %(fun)%
c : Data1 %(construct Data1)%
def__ : forall a : Type . a_v-1 ->? Unit %(fun)%
def__ : forall a : Type . a ->? Unit %(fun)%
eq : s * s ->? Unit %(pred)%
false : Unit %(fun)%
not__ : ? Unit ->? Unit %(fun)%
Expand Down Expand Up @@ -125,7 +124,7 @@ x : s
y : t
%% Sentences -------------------------------------------------------------
program (pred tt : s) = (\ (var x : s) . ()) : s ->? Unit %(pe_tt)%
((fun __=__[t] : forall a : Type . a_v-1 * a_v-1 ->? Unit) :
((fun __=__[t] : forall a : Type . a * a ->? Unit) :
t * t ->? Unit)
(var x : t, var y : t) :
Unit
Expand All @@ -138,25 +137,25 @@ type Data2
Cons22 : Data2 * Data1 -> Data2 (Data2; Data1)
types Data1 %(ga_Data2)%
forall x_1_1 : Data1; x_1_2 : Data2
. (fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)
. (fun __=__ : forall a : Type . a * a ->? Unit)
((op sel1 : Data3 ->? Data1)
((op Cons31 : Data1 * Data2 -> Data3)
(var x_1_1 : Data1, var x_1_2 : Data2)),
var x_1_1 : Data1) %(ga_select_sel1)%
forall x_1_1 : Data1; x_1_2 : Data2
. (fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)
. (fun __=__ : forall a : Type . a * a ->? Unit)
((op sel2 : Data3 ->? Data2)
((op Cons31 : Data1 * Data2 -> Data3)
(var x_1_1 : Data1, var x_1_2 : Data2)),
var x_1_2 : Data2) %(ga_select_sel2)%
forall x_1_1 : Data2; x_1_2 : Data1
. (fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)
. (fun __=__ : forall a : Type . a * a ->? Unit)
((op sel2 : Data3 ->? Data2)
((op Cons32 : Data2 * Data1 -> Data3)
(var x_1_1 : Data2, var x_1_2 : Data1)),
var x_1_1 : Data2) %(ga_select_sel2)%
forall x_1_1 : Data2; x_1_2 : Data1
. (fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)
. (fun __=__ : forall a : Type . a * a ->? Unit)
((op sel1 : Data3 ->? Data1)
((op Cons32 : Data2 * Data1 -> Data3)
(var x_1_1 : Data2, var x_1_2 : Data1)),
Expand All @@ -166,25 +165,25 @@ type Data3
Cons32 : Data2 * Data1 -> Data3
(sel2 :? Data2; sel1 :? Data1) %(ga_Data3)%
forall x_1_1 : Data1; x_1_2 : Data2
. (fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)
. (fun __=__ : forall a : Type . a * a ->? Unit)
((op sel1 : Data4 ->? Data1)
((op Cons41 : Data1 * Data2 ->? Data4)
(var x_1_1 : Data1, var x_1_2 : Data2)),
var x_1_1 : Data1) %(ga_select_sel1)%
forall x_1_1 : Data1; x_1_2 : Data2
. (fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)
. (fun __=__ : forall a : Type . a * a ->? Unit)
((op sel2 : Data4 ->? Data2)
((op Cons41 : Data1 * Data2 ->? Data4)
(var x_1_1 : Data1, var x_1_2 : Data2)),
var x_1_2 : Data2) %(ga_select_sel2)%
forall x_1_1 : Data2; x_1_2 : Data1
. (fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)
. (fun __=__ : forall a : Type . a * a ->? Unit)
((op sel2 : Data4 ->? Data2)
((op Cons42 : Data2 * Data1 ->? Data4)
(var x_1_1 : Data2, var x_1_2 : Data1)),
var x_1_1 : Data2) %(ga_select_sel2)%
forall x_1_1 : Data2; x_1_2 : Data1
. (fun __=__ : forall a : Type . a_v-1 * a_v-1 ->? Unit)
. (fun __=__ : forall a : Type . a * a ->? Unit)
((op sel1 : Data4 ->? Data1)
((op Cons42 : Data2 * Data1 ->? Data4)
(var x_1_1 : Data2, var x_1_2 : Data1)),
Expand All @@ -207,21 +206,21 @@ type Data4
*** Hint 18.15, rebound variable 'x'
*** Error 20.12, unexpected mixfix token: res
*** Hint 21.1, no type match for: fst
with (maximal) type: _var_4_v4 ->? s
with (maximal) type: _v4 ->? s
known types:

*** Hint 21.1-21.16, untypable application (with result type: s)
'fst(x : s, var y : t)'
*** Error 21.22, no typing for 'program fst(x : s, var y : t) : s = x'
*** Hint 22.1, no type match for: snd
with (maximal) type: _var_5_v5 ->? t
with (maximal) type: _v5 ->? t
known types:

*** Hint 22.1-22.16, untypable application (with result type: t)
'snd(x : s, var y : t)'
*** Error 22.22, no typing for 'program snd(x : s, var y : t) : t = y'
*** Hint 28.9, no type match for: all
with (maximal) type: _var_6_v6 ->? ? Unit
with (maximal) type: _v6 ->? ? Unit
known types:

*** Hint 28.9-28.15, untypable application (with result type: ? Unit)
Expand Down
Loading

0 comments on commit 2986838

Please sign in to comment.