import Prelude ()
import Dessy
import CollectionTools ( to_list, foldr, foldl )
import String ( unlines )

{--

Determining Variances for Generic Conformance - A Literate Program
------------------------------------------------------------------

This file contains a type checker for some typing rules that have been
proposed first by Cook later by myself, but have never been
formalised.

The problem is, whether in an object-oriented language a generic type
FOO[A, ..] conforms to FOO[B, ..] and under what conditions.  Eiffel
has the rule that this conformance holds if and only if A, .. conform
to B, .. .  This is intuitive in some cases, but generally it is
unsound and unfoundable.

Some other languages (e.g., OCaml, I think) allow the conformance by
regarding the individual structure of the types FOO[A, ..] and FOO[B,
..].  I have claimed that this look at the structure of each type can
be replaced by a look at some simple extra information in the class
interface on which both types are based.  Already Cook pointed out,
that it suffices to declare each of the class' formal generics as
covariant (or not) and contravariant (or not).  He left implicit how
this information could be derived from the class interface.  However,
it now turns out, that in general -- due to recursions between classes
-- all class interfaces of the system have to be considered together.

However, the final part of this program shows how this restriction can
be considerably weakened.

-}


-- Minimal data type declaration: 
-- Class Interfaces, Signatures and Types.

data ClassInterface = ClassInterface { class_name :: String,
				       num_generics :: Int,
				       features :: [ExportedFeature]
				     } deriving (Eq, Ord)

-- instance Eq ClassInterface where
--    c == d  =  class_name c == class_name d

data ExportedFeature = Query { arguments :: [Type], result :: Type }
		     | Command { arguments :: [Type] }
		       deriving (Eq, Ord)

data Type = LikeCurrent
	  | ClassType { base_class :: String, actual_generics :: [Type] }
	  | FormalGeneric { generic_num :: Int }
	    deriving (Eq, Ord)

-- Invariants of the data types.

valid_class c = all (valid_feature [1..num_generics c]) (features c)

valid_feature gens (Query args res) = all (valid_type gens) (res:args)
valid_feature gens (Command args)   = all (valid_type gens) args

valid_type gens (LikeCurrent)         = True
valid_type gens (FormalGeneric n)     = n # gens
valid_type gens (ClassType n actuals) = classes `has_key` n
				     && length actuals == num_generics (classes `at` n)
				     && all (valid_type gens) actuals

check_classes = -- all valid_class $ range classes
                fold True (valid_class.snd) (&&) classes

-- Printing of the data structures.

instance Show ClassInterface where
    show c = "class " ++ class_name c ++ show_formals (num_generics c)
             ++ " signatures \n" 
	     ++ (unlines $ apply (\x -> "\t" ++ show x) $ features c)
	     ++ "end" 

show_formals 0 = ""
show_formals n = "[G1" ++ s n ++ "]"
    where s 1 = ""; s n = s (n-1) ++ ", G" ++ show n

instance Show ExportedFeature where
    show (Query args res) = show_args args ++ ":" ++ show res
    show (Command args)   = show_args args

show_args [] = ""
show_args xs = "(" ++ fold1 show comm xs ++ ")"
    where 
    comm a b = a ++ ", " ++ b

instance Show Type where
    show LikeCurrent = "like Current"
    show (FormalGeneric n) = "G" ++ show n
    show (ClassType name actuals) = name ++ show_actuals (apply show actuals)

show_actuals [] = ""
show_actuals (x:xs) = "[" ++ x ++ s xs ++ "]"
    where s [] = ""; s (x:xs) = ", " ++ x ++ s xs

unparagraph :: Sequence seq String => 
               seq String -> String
unparagraph = concat_apply (++"\n\n")

-- print_classes = putStr $ unparagraph $ apply show $ range classes
{--
  unparagraph $ apply show $ range classes
= concat_apply (++"\n\n") $ apply show $ apply' snd $ classes
= concat_apply ((++"\n\n").show.snd) classes
= concat_apply ( \ (_, x) -> shows x "\n\n" ) classes
= fold "" ( \ (_, x) ->  shows x "\n\n" ) (++) classes
= fold id ( \ (_, x) -> shows x . ("\n\n"++) ) (.) classes ""
--}
print_classes = putStr $ foldr ( \ (_, x) -> shows x . ("\n\n"++) ) "" classes
-- The deforested and closured version is particularly nice, isn't it? ;-)

-- Example Classes.

class_integer = ClassInterface { 
   class_name = "INTEGER", num_generics = 0,
   features =
   [ Query [ClassType "INTEGER" []] (ClassType "INTEGER" []),  -- plus/minus/...
     Query [] (ClassType "INTEGER" []),                        -- abs
     Query [] (ClassType "BOOLEAN" [])                         -- is_positive
   ] }

class_sequence = ClassInterface 
   { class_name = "SEQUENCE", num_generics = 1,
     features =
     [ Query [] (ClassType "INTEGER" []),                 -- length
       Query [] (FormalGeneric 1),                        -- head
       Query [] (ClassType "SEQUENCE" [FormalGeneric 1])  -- tail
     ] }
   
class_list = ClassInterface
   { class_name = "LIST", num_generics = 1,
     features = [Command [ClassType "LIST" [FormalGeneric 1]]] -- append
   }

class_pair = ClassInterface
   { class_name = "PAIR", num_generics = 2,
     features =
     [ Query [] (FormalGeneric 1),   -- first
       Query [] (FormalGeneric 2),   -- second
       Query [] (ClassType "PAIR" [FormalGeneric 2, FormalGeneric 1]) -- swapped
     ] }

class_a = ClassInterface
   { class_name = "A", num_generics = 1,
     features =
     [ Query [] (ClassType "B" [FormalGeneric 1])
     ]  }
     
class_b = ClassInterface
   { class_name = "B", num_generics = 1,
     features =
     [ Command [ClassType "A" [FormalGeneric 1]]
     ]  }
     
class_a1 = ClassInterface
   { class_name = "A1", num_generics = 1,
     features =
     [ Query [] (ClassType "B1" [FormalGeneric 1]),
       Query [] (FormalGeneric 1)
     ]  }
     
class_b1 = ClassInterface
   { class_name = "B1", num_generics = 1,
     features =
     [ Command [ClassType "A1" [FormalGeneric 1]]
     ]  }
     

classes :: Map String ClassInterface
classes = map_by class_name
	  [ClassInterface "BOOLEAN" 0 [],
	   class_integer,
	   class_sequence,
	   class_list,
	   class_pair,
	   class_a, class_b, class_a1, class_b1
	  ]

{-- Now to the concept of variance.

Definition:
-----------

An occurrence of a type in a class interface is in covariant context,
if and only if

 - it is an actual generic of a covariant formal generic of a class
   type (see definition below) that occurs in (recursively) covariant
   context, or

 - it is an actual generic of a contravariant formal generic of a
   class type that occurs in contravariant context, or

 - it is the type of a query result.

An occurrence of a type in a class interface is in contravariant
context, if and only if

 - it is an actual generic of a covariant formal generic of a class
   type (see definition below) that occurs in (recursively)
   contravariant context, or

 - it is an actual generic of a contravariant formal generic of a
   class type that occurs in covariant context, or

 - it is the type of a formal routine argument.

A class is covariant in a formal generic, if and only if the formal
generic does always occur in covariant context in the class interface.
A class is contravariant in a formal generic, if and only if the
formal generic does always occur in a contravariant context in the
class interface.

A class is called to be novariant in a formal generic if it is neither
co- nor contravariant in that generic, and fullvariant if it is both
co- and contravariant in the generic.

Since these definitions are recursive, they are actually ambiguous!
For example the variance of the generics of the recursive classes
LIST, SEQUENCE and others above cannot be determined using the rules.
The solution to this ambiguity can be explained easily after
formalising the above definitions.

-}

type Variance = (Bool, Bool)
is_covariant = fst
is_contravariant = snd

covariant     = (True, False)
contravariant = (False, True)
novariant     = (False, False)
fullvariant   = (True, True)

-- The variance- determining algorithm will for each formal generic
-- traverse a class interface and take into account the context of
-- where it occurs.  Different contexts are combined via a logical
-- "and" corresponding to the implicit universal quantification with
-- "always" in the above definition.

infix 2 &+ -- like ||
infix 3 &* -- like &&

(co, con) &+ (co', con') = (co&&co', con&&con')
and_var coll = reduce fullvariant (&+) coll -- named like the function `and`

-- As an example: "covariant &+ contravariant == novariant".

-- The following operator "lifts" a context through the application of
-- a formal generic.

(co, con) &* (cco, ccon) = ((co && cco)||(con&&ccon), (con&&cco)||(co&&ccon))

-- As an example: "covariant &* contravariant == contravariant".

type VarId    = (String, Int)  -- class_name, formal_generic
type Mapping = Map VarId Variance

-- Now we can define a function, that takes a mapping with given
-- variances and a formal generic, and calculates the formal generic's
-- variance resorting to the given mapping in all recursive cases:

var_class :: Mapping -> VarId -> Variance
var_class mapping (c, v) 
   = and_var $ apply (var_sig mapping (c, v)) $ features $ classes `at` c

var_sig :: Mapping -> VarId -> ExportedFeature -> Variance
var_sig mapping v (Query args res) 
   = and_var ( var_type mapping v covariant res : 
	      apply (var_type mapping v contravariant) args )
var_sig mapping v (Command args) 
   = and_var ( apply (var_type mapping v contravariant) args )

var_type :: Mapping -> VarId -> Variance -> Type -> Variance
var_type mapping (_, v) context (FormalGeneric i) 
   = if i == v then context else fullvariant
var_type mapping v context (ClassType name actuals) 
   = and_var [ var_type mapping v (mapping `at` (name, i) &* context) act
	      | (i, act) <- zip [1..] actuals ]
var_type mapping (c, v) context LikeCurrent 
   = mapping `at` (c, v) &* context

-- The last case is a combination and simplification of the other two.
-- We know that there is exactly one occurrence of the formal generic,
-- namely in its "own position".  Therefore the 'if' and the list
-- treatment disappear.


-- Now we can take the list of all formal generics and calculate the
-- variance for them.

generics :: Set VarId
generics = set [ (n, v) | (n, c) <- to_list classes
                        , v      <- [1..num_generics c]
	       ]

var_step mapping = fun_map generics (var_class mapping)
              -- = map [ (v, var_class mapping v) | v <- generics ]
              -- = map $ zip generics $ apply (var_class mapping) generics

{-- This function calculates a mapping of variances, but still needs
such a mapping given to account for the recursive references.  (This
could not be implemented via recursive calls, since the references can
be cyclic.)

Such a mapping of formal generics to their variances complies to the
rules stated and formalised above if and only if it fulfils the
equation "var_step mapping == mapping".  But we are not interested in
a predicate to characterise such mappings, but instead in a function
to calculate us one.  And still we haven't said which of those
mappings should be the one that is made part of the class interfaces.
Concerning that question we should be generous and specify the weakest
mapping, that is the one, that makes as many generics as possible co-
and contravariant.

But does such a mapping exist?  Or may there be cases where a generic
can be covariant or contravariant, but not both?  In such a case none
of the two mappings would be weaker than the other, and so there would
be no weakest.  However, such cases do not exist and there is indeed
always a weakest solution, because the rules are monotonic: there is
no place where a variance must be false (i.e., not co- or
contravariant) in order to make another variance true (i.e. make the
generic co- or contravariant).  

Because of this property, we can also calculate the weakest solution
(weakest fix point) by a simple iteration:

-}
    
iter f x = let x' = f x in
	   if x' == x then x else iter f x'

-- Our final mapping of variances is then simply:

variances :: Mapping
variances = iter var_step all_true
    where all_true = fun_map generics (const fullvariant)
		-- = map [ (v, fullvariant) | v <- to_list generics ] 

-- By the way this iteration terminates, because the mapping has only
-- a finite state space (two booleans for every class).

print_variances = putStr $ show_FM_table $ variances

show_FM_table fm = unlines [ show a ++ "\t" ++ show b | (a, b) <- to_list fm ]


-- Optimising it.

depends_on :: VarId -> Set VarId
depends_on (c, v) = union $ apply (dep_sig (c, v)) $ features $ classes `at` c

dep_sig v (Query args res) = union $ apply (dep_type v) $ res:args
dep_sig v (Command args)   = union $ apply (dep_type v) $ args

dep_type v      (LikeCurrent)         
    = set [v]
dep_type (c, v) (ClassType n actuals) 
    = set [ (n, i) | (i, a) <- zip [1..] actuals, occurs v a ] 
   \/ (union $ apply (dep_type (c, v)) actuals)
dep_type _      (FormalGeneric _)
    = empty

occurs v LikeCurrent           = True
occurs v (ClassType _ actuals) = or $ apply (occurs v) actuals
occurs v (FormalGeneric g)     = v == g 

-- Specification of topological sort:

spec_sorted_generics 
   = union sorted_generics == set generics -- contains all
  && size (union sorted_generics) == sum (apply size sorted_generics)
                                           -- no duplicates
  && depends_on_earlier sorted_generics
-- Still lacking: is the "best possible sort", 
--                otherwise they could all be in one group.

depends_on_earlier [] 
   = True
depends_on_earlier (x:xs) 
   = (union $ apply depends_on $ to_list x) `subset` (union xs)
  && depends_on_earlier xs

-- Then the iteration becomes:

new_step finished mapping 
   = map_apply (\ (v, _) -> var_class (finished <+> mapping) v ) mapping
-- = map [ (v, var_class (finished <+> mapping) v) | v <- domain mapping ]

new_variances :: Mapping
new_variances = foldr nv empty sorted_generics
    where
    nv generics finished = iter (new_step finished) (all_true generics)
    all_true generics = fun_map generics (const fullvariant)

sorted_generics :: [Set VarId]
sorted_generics = undefined -- simple standard algorithm left as exercise

{-- This algorithm unifies two advantages: First, it works for all
systems of classes, whatever their recursiveness, and it is still
considerably efficient (quadratic in the size of a recursive cycle,
which is optimal, I think).  Second, if their are no cycles each
variable (or each class, see ex. 1. below) is treated alone, this is
perfect for incremental updates.

The second point is especially important, because I have not yet found
a practical example, where a cycle spans more than one class!

--}

{-- Further optimisations as exercises 
    (work on simple and topological version):

1. Do traversal of class interface for all formal generics of the
   class at the same time.  "var_class, var_sig, var_type" will return
   mappings with domain [1..num_generics] and the operator &+ has to
   be lifted to this type.  (&* works on contexts only and doesn't
   need to be changed.)  To let this work with topological sort, the
   latter has to be lifted to class level, too.

2. If the step function is implemented imperatively, instead of
   calling `var_class` independently for each generic, the calls can
   update the mapping and later calls can already use the updated
   version.  

Both optimisations only yield a constant factor in improvement, and
since run-time should be very low anyway, I think they are not worth
being implemented.

--}


var_class' :: Mapping -> VarId -> Variance
var_class' mapping (c, v) 
   = let feats = features $ classes `at` c
	 mapping' = put mapping (c, v) fullvariant
     in ( foldl (var_sig' (c, v)) mapping' feats ) `at` (c, v)

var_sig' :: VarId -> Mapping -> ExportedFeature -> Mapping
var_sig' v mapping (Query args res) 
   = let mapping' = foldl (var_type' v contravariant) mapping args
     in var_type' v covariant mapping' res
var_sig' v mapping (Command args) 
   = foldl (var_type' v contravariant) mapping args

var_type' :: VarId -> Variance -> Mapping -> Type -> Mapping
var_type' (c, v) context mapping (FormalGeneric i) 
   = if i == v then update mapping (c, v) (&+ context) else mapping
var_type' v context mapping (ClassType name actuals) 
   = foldl (\mapping (i, act) ->
	      var_type' v (var_rec (name, i) &* context) mapping act)
	   mapping
	   (zip [1..] actuals :: [(Int, Type)])
    where var_rec v | mapping `has_key` v = mapping `at` v
		    | otherwise           = var_class mapping v
var_type' (c, v) context mapping LikeCurrent 
   = update mapping (c, v) (&+ (mapping `at` (c, v) &* context))

variances' :: Mapping
variances' = fun_map generics (var_class' empty)

print_variances' = putStr $ show_FM_table $ variances'

{-- This last algorithm doesn't work.  To correctly implement its
idea, we would have to calculate each of the two components of a
variant separately, that is, have one function that calculates whether
a generic is covariant and another for the contravariance.  The reason
is that to calculate one component we can assume for recursive calls
that this component is True, but we cannot assume, that the other is
also True (and neither that it is False).  (The classes A1 and B1
illustrate this.)  This is also why the function `var_class' doesn't
return the mapping that it calculated, but it returns only one
variance.  Actually it should only return one component of a
variance. --}

-- For GHC 5.00:
main = print_variances