Changeset 11877

Timestamp:

03.07.2009 18:38:45 (4 months ago)

Author:

maeder

Message:

disallowed explicit pseudo type notation following := (assign)

Location:

trunk/HasCASL

Files:

• ParseItem.hs (modified) (1 diff)
• test/Alias.hascasl (modified) (1 diff)
• test/Alias.hascasl.output (modified) (2 diffs)
• test/ContraVariance.hascasl (modified) (1 diff)
• test/ContraVariance.hascasl.output (modified) (2 diffs)
• test/Graphs.hascasl (modified) (2 diffs)
• test/Graphs.hascasl.output (modified) (1 diff)
• test/Items.hascasl (modified) (1 diff)
• test/Items.hascasl.output (modified) (1 diff)
• test/Prelude.hascasl (modified) (15 diffs)
• test/WrongItems.hascasl (modified) (1 diff)
• test/WrongItems.hascasl.output (modified) (1 diff)

trunk/HasCASL/ParseItem.hs

@@ -127 +127 @@
       <|> typeItemList [p] Plain
 
--- | several 'typeArg's
-typeArgs :: AParser st ([TypeArg], [Token])
-typeArgs = do
-    l <- many1 typeArg
-    return (map fst l, concatMap snd l)
-
-pseudoType :: AParser st TypeScheme
-pseudoType = do
-    l <- asKey lamS
-    (ts, pps) <- typeArgs
-    d <- dotT
-    t <- pseudoType
-    let qs = toRange l pps d
-    case t of
-      TypeScheme ts1 gt ps ->
-          return $ TypeScheme (ts ++ ts1) gt $ appRange qs ps
-  <|> do
-    st <- parseType
-    return $ simpleTypeScheme st
-
 pseudoTypeDef :: TypePattern -> Maybe Kind -> [Token] -> AParser st TypeItem
 pseudoTypeDef t k l = do
     c <- asKey assignS
-    p <- pseudoType
-    return $ AliasType t k p $ catRange $ l ++ [c]
+    p <- parseType
+    return $ AliasType t k (simpleTypeScheme p) $ catRange $ l ++ [c]
 
 -- * parsing datatypes

trunk/HasCASL/test/Alias.hascasl

@@ -6 +6 @@
 
 type a1 a b := a -> b -> Unit
-type a1 := \ (a) (b) .a -> b  -> Unit
-type a1 a := \ b .a -> b  -> Unit
+type a1 (a) (b) := a -> b  -> Unit
 
-type a2 := \ (a) (b) . a -> Unit
+type a2 a b := a -> Unit
 
-type a3 := \ (a) (a) . a -> Unit
+type a3 (a) (a) := a -> Unit
 
 type a4 a a := a -> Unit

trunk/HasCASL/test/Alias.hascasl.output

@@ -4 +4 @@
 type  MyPred s := s ->? Unit
 type  MyAlias t := t ->? Unit
-type  a1 a b := a -> b -> Unit
 type  a1 a b := a -> b -> Unit
 type  a1 a b := a -> b -> Unit
@@ -49 +48 @@
 *** Error 7.9, unknown type variable 'a'
 *** Error 7.11, unknown type variable 'b'
-*** Error 8.15, unknown type variable 'a'
-*** Error 8.19, unknown type variable 'b'
+*** Error 8.10, unknown type variable 'a'
+*** Error 8.14, unknown type variable 'b'
 ### Hint 8.6, redeclared type 'a1'
-*** Error 9.9, unknown type variable 'a'
-*** Error 9.16, unknown type variable 'b'
-### Hint 9.6, redeclared type 'a1'
-*** Error 11.15, unknown type variable 'a'
-*** Error 11.19, unknown type variable 'b'
-*** Error 13.15, unknown type variable 'a'
-*** Error 13.15, duplicates at '(13,19)' for 'a'
-*** Error 15.9, unknown type variable 'a'
-*** Error 15.9, duplicates at '(15,11)' for 'a'
-*** Error 17.9, unknown type variable 'a'
-*** Error 19.9, unknown type variable 'a'
-*** Error 19.14-19.22,
+*** Error 10.9, unknown type variable 'a'
+*** Error 10.11, unknown type variable 'b'
+*** Error 12.10, unknown type variable 'a'
+*** Error 12.10, duplicates at '(12,14)' for 'a'
+*** Error 14.9, unknown type variable 'a'
+*** Error 14.9, duplicates at '(14,11)' for 'a'
+*** Error 16.9, unknown type variable 'a'
+*** Error 18.9, unknown type variable 'a'
+*** Error 18.14-18.22,
 illegal recursive type synonym 'a5 a -> Unit'
-*** Error 21.9, unknown type variable 'a'
-*** Error 23.9, unknown type variable 'a'
-*** Error 25.9, unknown type variable 'a'
-*** Error 23.9-25.22, illegal recursive type synonym 'a7 a -> Unit'
-*** Error 27.6,
+*** Error 20.9, unknown type variable 'a'
+*** Error 22.9, unknown type variable 'a'
+*** Error 24.9, unknown type variable 'a'
+*** Error 22.9-24.22, illegal recursive type synonym 'a7 a -> Unit'
+*** Error 26.6,
 incompatible kind of: a2
   expected: Type -> Type -> Type

trunk/HasCASL/test/ContraVariance.hascasl

@@ -1 @@
-type p := \ (a : +Type) . Pred (Pred a)  %% should be correct
-type p := \ (a : +Type) . Pred a         %% should be wrong
-type m := \ (b : -Type) . b              %% 
-type m := \ (b : +Type) . b              %% both contradict
+var a : +Type
+type p a := Pred (Pred a)  %% should be correct
+type p a := Pred a         %% should be wrong
+type m (b : -Type) := b              %%
+type m (b : +Type) := b              %% both contradict

trunk/HasCASL/test/ContraVariance.hascasl.output

@@ +1 @@
+var   a : +Type
 type  p a := Pred (Pred a)
       %% should be correct
@@ -9 +10 @@
 m := \ b : -Type . b;
 p := \ a : +Type . Pred (Pred a)
-### Hint 2.32, wrong covariance of 'a'
-### Hint 2.32, no kind found for 'a'
-*** Error 2.27-2.32, no kind found for 'Pred a'
-*** Error 4.6,
+var
+a : +Type %(var_1)%
+### Hint 1.5, is type variable 'a'
+### Hint 3.18, wrong covariance of 'a'
+### Hint 3.18, no kind found for 'a'
+*** Error 3.13-3.18, no kind found for 'Pred a'
+*** Error 5.6,
 wrong type of 'm'
   expected: \ b : -Type . b

trunk/HasCASL/test/Graphs.hascasl

@@ -1 +1 @@
  var S,T : Type
   type Bool;
-       Pred := \ (S: -Type) . S ->? Unit ;
-       Set := \ S:Type . S ->? Unit ;
+       Pred (S: -Type) := S ->? Unit ;
+       Set (S:Type) := S ->? Unit ;
   ops True, False : Bool;
 
@@ -14 +14 @@
       __disjointUnion__ :  Set S * Set S -> Set (S*Bool);
       inl,inr : S -> S*Bool;
-  forall x,x':S; y:T; s,s':Set(S); t:Set(T) 
+  forall x,x':S; y:T; s,s':Set(S); t:Set(T)
   . not (x isIn emptySet)
   . (x isIn {x'}) <=> x=x'

trunk/HasCASL/test/Graphs.hascasl.output

@@ -70 +70 @@
 ### Hint 1.6, is type variable 'S'
 ### Hint 1.8, is type variable 'T'
-### Hint 3.19, rebound type variable 'S'
+### Hint 3.14, rebound type variable 'S'
 ### Hint 3.8, redeclared type 'Pred'
-### Hint 4.17, rebound type variable 'S'
+### Hint 4.13, rebound type variable 'S'
 ### Hint 9.18,
 no kind found for 'S'

trunk/HasCASL/test/Items.hascasl

@@ -3 +3 @@
 var {a}: c -> d
 class Monad < Type -> Type
-type a : Monad := \ t . t -> t
+type (a : Monad) t := t -> t
 free type Term ::=  Var Variable | Lam Variable Term | App Term Term
 type WNet={(sys,i,o): T * T * T . i = o }

trunk/HasCASL/test/Items.hascasl.output

@@ -3 +3 @@
 var   {a} : c -> d
 class Monad < Type -> Type
-type  a t := t -> t
+type  (a : Monad) t := t -> t
 free type Term ::= Var Variable | Lam Variable Term | App Term Term
 type  WNet = {(sys, i, o) : T * T * T . i = o}

trunk/HasCASL/test/Prelude.hascasl

@@ -1 @@
-%% predefined universe containing all types, 
+%% predefined universe containing all types,
 %% superclass of all other classes
 
 class Type
 
-var s,t  : Type 
+var s,t  : Type
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -12 +12 @@
 
 %% type aliases
-type Pred __ : Type -> Type := \ t: -Type . t ->? Unit 
-type ? __ := \ t:Type . Unit ->? t
+type Pred __ (t: -Type) := t ->? Unit
+type ? __ (t:Type) := Unit ->? t
 
 pred true, false : Unit
@@ -34 +34 @@
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%% "pred p args = e" abbreviates "op p args :? unit = e"  
+%% "pred p args = e" abbreviates "op p args :? unit = e"
 %% CASL requires "<=>" for pred-defn and disallows "()" as result
 
@@ -40 +40 @@
 var x : s
 
-program def = \x: s . () %% def is also total (identical to tt) 
+program def = \x: s . () %% def is also total (identical to tt)
 
 program tt = \x: s . ()  %% tt is total "op tt(x: s): unit = ()"
@@ -48 +48 @@
 
 %% total function type
-type __->__ : -Type -> +Type -> Type 
+type __->__ : -Type -> +Type -> Type
 
 type __->__ < __ ->? __
@@ -56 +56 @@
 
 %% total functions
-op __res__ (x: s; y: t) : s = x 
-op fst (x: s; y: t) : s = x 
-program snd (x: s, y: t) : t = y 
+op __res__ (x: s; y: t) : s = x
+op fst (x: s; y: t) : s = x
+program snd (x: s, y: t) : t = y
 
 
 %% trivial because its the strict function property
 
-. (\ (x:s, y:t). def (x res y)) =  (\ (x:s, y:t). (def y) und (def x)) 
+. (\ (x:s, y:t). def (x res y)) =  (\ (x:s, y:t). (def y) und (def x))
 . fst = (__ res__)
 
@@ -77 +77 @@
 %% then %def
 
-%% notation "\ ."  abbreviates "\bla:unit." 
+%% notation "\ ."  abbreviates "\bla:unit."
 %% where "bla" is never used, but only "()" instead
 
-%% for type inference 
+%% for type inference
 %% an implicit cast from s to ?s of a term "e" yields the term "\ . e"
 
@@ -93 +93 @@
 program __impl__ (x, y: Pred Unit) : Pred Unit = eq(x, x And y)
 
-program __or__ (x, y: Pred Unit) : Pred Unit = all(\r: Pred Unit. 
+program __or__ (x, y: Pred Unit) : Pred Unit = all(\r: Pred Unit.
                 ((x impl r) und (y impl r)) impl r)
 
@@ -103 +103 @@
 program neg (r: Pred Unit) : Pred Unit = r impl ff
 
-%% the type instance for the first "eq" should be "?t" 
+%% the type instance for the first "eq" should be "?t"
 %% this is explicitely enforced by "\ .f(x)"
 
@@ -109 +109 @@
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%% Recursion (requires "free type nat ::= 0 | Suc(nat)" and "+"  
+%% Recursion (requires "free type nat ::= 0 | Suc(nat)" and "+"
 
 type nat
@@ -124 +124 @@
 
 pred isChain (s: nat -> c) <=> all(\n:nat. s(n) <<= s(Suc(n)))
-pred isBound (x: c; s: nat -> c) <=> all(\n:nat. s(n) <<= x)  
+pred isBound (x: c; s: nat -> c) <=> all(\n:nat. s(n) <<= x)
 
 op sup : (nat -> c) ->? c
@@ -139 +139 @@
 var p : Pcpo
 
-op bottom : p 
-
-. all(\x : p. bottom <<= x)   
+op bottom : p
+
+. all(\x : p. bottom <<= x)
 }
 
 class instance Flatcpo < Cpo
 {
- var f : Flatcpo 
+ var f : Flatcpo
 
  program __<<=[f]__ = eq
@@ -155 +155 @@
 type instance __*__ : +Cpo -> +Cpo -> Cpo
 
-var x1,x2 : c; y1, y2 : d 
-
-program (x1, y1) <<= (x2, y2) = (x1 <<= x2) und (y1 <<= y2) 
-
-
-type instance __*__ : +Pcpo -> +Pcpo -> Pcpo      
+var x1,x2 : c; y1, y2 : d
+
+program (x1, y1) <<= (x2, y2) = (x1 <<= x2) und (y1 <<= y2)
+
+
+type instance __*__ : +Pcpo -> +Pcpo -> Pcpo
 
 type Unit : Pcpo
 
 %% Pcont
-type instance __-->?__ : -Cpo -> +Cpo -> Pcpo 
+type instance __-->?__ : -Cpo -> +Cpo -> Pcpo
 
  type __-->?__ < __->?__
- . __ in c -->? d  = \f : c ->? d . 
+ . __ in c -->? d  = \f : c ->? d .
         all(\(x,y: c). (def (f x) und x <<= y) impl def (f y)) und
-        all(\s: nat -> c. (isChain(s) und def f(sup(s))) impl 
-                ex(\m:nat. def f(s(m)) und 
+        all(\s: nat -> c. (isChain(s) und def f(sup(s))) impl
+                ex(\m:nat. def f(s(m)) und
                         eq(sup(\n:nat.!f(s(n+m))), f(sup(s)))))
 
@@ -179 +179 @@
 type instance __-->__ : -Cpo -> +Cpo -> Cpo
 
- type __-->__ < __-->?__ 
+ type __-->__ < __-->?__
  . __ in c --> d = \f : c -->? d . all(\x:c. def f(x))
 
  var f, g : c --> d
 
- program f <<= g = f <<=[c -->? d] g 
+ program f <<= g = f <<=[c -->? d] g
 
 type instance __-->__ : -Cpo -> +Pcpo -> Pcpo
@@ -195 +195 @@
 var f : p --> p; x : p
 . f(Y(f)) = Y(f)
-. f(x) = x => Y(f) <<= x  
+. f(x) = x => Y(f) <<= x
 
 op undefined : c --> p = Y((\x': c --> p . x') as (c --> p) --> c --> p)

trunk/HasCASL/test/WrongItems.hascasl

@@ -2 +2 @@
 var <
 class a < Type = {x . x < t}
-type t := \ s,r . s -> r
+type t (s,r) := s -> r
 type n (r,s)

trunk/HasCASL/test/WrongItems.hascasl.output

@@ -11 +11 @@
 expecting "[", "%", "->", "{", ";", "sort", "op", "fun", "pred", "type", class, "program", "generated", "free", "var", "forall", dot, "axiom", "internal" or end of input
 
-parse error at 4.17:
+parse error at 4.12:
 unexpected list of type arguments
-expecting "%", "+", "-", ",", ":" or "<"
+expecting casl char, "_", "%", "+", "-", ",", ":" or "<"
 
 parse error at 5.12: