{-# LANGUAGE PatternGuards #-}
module StdPrel(
    preTypes, preClasses, isPreClass, preValues,
    tiArrow, tiSizeOf,
    tiUnit, tiPair, tiMaybe, tiList,
    tiBit, tiBool,
    tiInteger, tiReal, tiString, tiChar,
    tiHandle, tiBufferMode,
    tiFmt,
    tiAction, tiRules,
    tiClock, tiReset, tiInout,
    tiPrimArray,
    tiPosition, tiType, tiName, tiPred, tiSchedPragma
   ) where

import qualified Bag as B
import qualified Data.Set as S

import Util(log2, ordPair, integerSqrt)
import Position
import ErrorUtil(internalError)
import Id
import SymTab
import CType
import Type
import Pred
import PreIds
import CSyntax(anyTExpr)
import Subst(Types(..))
import Unify(mgu)

--import PPrint
--import Debug.Trace

-- -------------------------

v1, v2, v3 :: Id
v1 : v2 : v3 : _ = tmpTyVarIds

tvarh1, tvarh2, tvarh3 :: TyVar
tvarh1 = tVarKind v1 KNum
tvarh2 = tVarKind v2 KNum
tvarh3 = tVarKind v3 KNum

-- instance for p' :=> p
-- avoid mkInst because it does quantification
-- that will introduce unnecessary (and sometimes harmful)
-- fresh type variables
mkImpliedInst :: Pred -> Pred -> Inst
mkImpliedInst p' p = Inst r [] ([pp'] :=> p)
  where pp' = mkPredWithPositions [] p'
        r   = anyTExpr (predToType p' `fn` predToType p)

-- the DVS are the type variables in the concrete type of a type signature
-- (i.e.  without provisos)
-- we only want to drop type variables with a numeric function if:
-- (a) those type variables don't appear in the concrete type
-- (b) the numeric function is determined by type variables in the concrete type
-- multi-step dependencies are handled because we reconsider provisos
-- when an instance-match introduces a substitution
checkDVS :: Types t => [TyVar] -> t -> Bool
checkDVS dvs t = all (flip elem dvs) (tv t)

-- -------------------------

clsAdd :: SymTab -> Class
clsAdd symT = Class {
        name = CTypeclass idAdd,
        csig = [tvarh1, tvarh2, tvarh3],
        super = [],  -- [IsIn clsSize [TVar tvarh1], IsIn clsSize [TVar tvarh2], IsIn clsSize [TVar tvarh3]]
        genInsts = genAddInsts symT,
        tyConOf = TyCon idAdd (Just (Kfun KNum (Kfun KNum (Kfun KNum KStar)))) (TIstruct SClass []),
        funDeps = [[False, False, True], [False, True, False], [True, False, False]],
        funDeps2 = [[Just False, Just False, Just True],
                    [Just False, Just True, Just False],
                    [Just True, Just False, Just False]],
        allowIncoherent = Just False,
        isComm = True
        }

genAddInsts :: SymTab -> [TyVar] -> Maybe [TyVar] -> Pred -> [Inst]

-- (C1, C2, ?) : (C1, C2, C1+C2)
genAddInsts _ _ _ (IsIn c [t1@(TCon (TyNum n1 p1)), t2@(TCon (TyNum n2 _)), _])
        = [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t3]
        t3 = TCon (TyNum (n1+n2) p1)

-- (C1, ?, C3) : (C1, C3-C1, C3)
genAddInsts _ _ _ (IsIn c [t1@(TCon (TyNum i1 p1)), _, t3@(TCon (TyNum i3 _))])
        | i3 >= i1 = [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t3]
        t2 = TCon (TyNum (i3 - i1) p1)

-- (?, C2, C3) : (C3-C2, C2, C3)
genAddInsts _ _ _ (IsIn c [_, t2@(TCon (TyNum i2 p2)), t3@(TCon (TyNum i3 _))])
        | i3 >= i2 = [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t3]
        t1 = TCon (TyNum (i3 - i2) p2)

-- (0, T, ?) : (0, T, T)
genAddInsts _ _ _ (IsIn c [t1@(TCon (TyNum 0 _)), t2, _])
        = [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t2]

-- (T, 0, ?) : (0, T, T)
genAddInsts _ _ _ (IsIn c [t1, t2@(TCon (TyNum 0 _)), _])
        = [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t1]

-- (?, T, T) : (0, T, T)
genAddInsts _ _ _ (IsIn c [_, t2, t3])
        | t2 == t3 = [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t3]
        t1 = TCon (TyNum 0 (getPosition t2))

-- (T, ?, T) : (T, 0, T)
genAddInsts _ _ _ (IsIn c [t1, _, t3])
        | t1 == t3 = [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t3]
        t2 = TCon (TyNum 0 (getPosition t1))

-- (T, T, C) : NumEq(T, C/2) => itself, when C is even
genAddInsts symT _ _ p@(IsIn c [t1, t2, TCon (TyNum n npos)])
    | t1 == t2, even n
    = [ mkImpliedInst (IsIn clsNumEq [t1, TCon (TyNum (n `div` 2) npos)]) p ]
  where
    -- look up the class, rather than construct it, for better sharing
    clsNumEq = mustFindClass symT (CTypeclass idNumEq)

-- (T1, T2, TAdd#(T1,T2)) : itself
-- (T1, T2, TAdd#(T2,T1)) : itself
genAddInsts _ _ _ p@(IsIn c [t1, t2, t3])
    | t3 == cTApplys tAdd [t1, t2] ||
      t3 == cTApplys tAdd [t2, t1] = [ mkInst r ([] :=> p) ]
 where r = anyTExpr (predToType p)

-- (T1, T2, TAdd#(T1, T3)) : NumEq(T2,T3) => itself
-- (T1, T2, TAdd#(T3, T1)) : NumEq(T2,T3) => itself
-- (T1, T2, TAdd#(T2, T3)) : NumEq(T1,T3) => itself
-- (T1, T2, TAdd#(T3, T2)) : NumEq(T1,T3) => itself
genAddInsts symT _ _ p@(IsIn c [t1, t2, t3@(TAp (TAp tc tA) tB)])
    | tc == tAdd,
      t1 == tA
    = [ mkImpliedInst (IsIn clsNumEq [t2, tB]) p ]
    | tc == tAdd,
      t1 == tB
    = [ mkImpliedInst (IsIn clsNumEq [t2, tA]) p ]
    | tc == tAdd,
      t2 == tA
    = [ mkImpliedInst (IsIn clsNumEq [t1, tB]) p ]
    | tc == tAdd,
      t2 == tB
    = [ mkImpliedInst (IsIn clsNumEq [t1, tA]) p ]
  where
    -- look up the class, rather than construct it, for better sharing
    clsNumEq = mustFindClass symT (CTypeclass idNumEq)

-- XXX The above rules are simple cases of this:
genAddInsts symT _ _ p@(IsIn c [t1, t2, t3])
    | not (nullAddTerms b1_b2_intersection) =
        [mkImpliedInst (IsIn clsNumEq [t12',t3']) p]
{-
        -- We can pre-simplify the NumEq, if it is more efficient:
        if (nullAddTerms b1_rem && nullAddTerms b2_rem)
        then let r = anyTExpr (predToType p)
             in  [mkInst r ([] :=> p)]
        else case (fromAddTerms b1_rem) of
               (TAp (TAp tc t1') t2') | tc == tAdd
                 -> [mkImpliedInst (IsIn c [t1',t2',t3']) p]
               t -> [mkImpliedInst (IsIn clsNumEq [t,t3']) p]
-}
  where b1 = toAddTerms (TAp (TAp tAdd t1) t2)
        b2 = toAddTerms t3
        b1_b2_intersection = intersectionAddTerms b1 b2
        b1_rem = differenceAddTerms b1 b1_b2_intersection
        b2_rem = differenceAddTerms b2 b1_b2_intersection
        t12' = fromAddTerms b1_rem
        t3' = fromAddTerms b2_rem
        -- look up the class, rather than construct it, for better sharing
        clsNumEq = mustFindClass symT (CTypeclass idNumEq)

-- when satisfyFV, as a last resort:
-- (T1, T2, V) : (T1, T2, TAdd#(T1,T2))
--   when V is not bound or dependent and T1 and T2 contain only variables
--        which are bound or dependent
genAddInsts _ bvs (Just dvs) (IsIn c [t1,t2, tv@(TVar v)])
    | v `notElem` dvs,
      checkDVS dvs (t1, t2),
      mgu bvs tv t3 /= Nothing =
        --trace ("TAdd " ++ ppReadable (r, p)) $
        [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t3]
        t3 = TAp (TAp tAdd t1) t2

-- when satisfyFV, as a last resort:
-- (T1, V, T3) : (T1, TSub#(T3, T1), T3)
--   when T1 is known to be <= T3, usually because T3 is TMax#(T1,?) or a
--      nested TMax structure containing T1, or because T1 is TMin#(T3, ?)
--      or a nested TMin structure containing T3
--   when V is not bound or dependent
--   and T1 and T2 contain only variables which are bound or dependent
-- and the other permutation:
-- (V, T2, T3) : (TSub#(T3, T2), T2, T3)
--
-- This is safe to do because we know that the TSub will always be non-negative.
-- A general rule from (T1, V, T3) to (T1, TSub#(T3,T1), T3) would cause Add
-- provisos to no longer be required!  But the TSub could fail during elab.
-- This would move numeric checking to elaboration time, which we don't want
-- because we want to catch bugs early.
genAddInsts _ bvs (Just dvs) (IsIn c [t1, tv@(TVar v), t3])
    | t1 `isKnownLTE` t3,
      v `notElem` dvs,
      checkDVS dvs (t1, t3),
      mgu bvs tv t2 /= Nothing =
        --trace ("Add TMax " ++ ppReadable p) $
        [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t3]
        t2 = cTApplys tSub [t3, t1]
genAddInsts _ bvs (Just dvs) (IsIn c [tv@(TVar v), t2, t3])
    | t2 `isKnownLTE` t3,
      v `notElem` dvs,
      checkDVS dvs (t2, t3),
      mgu bvs tv t1 /= Nothing =
        --trace ("Add TMax " ++ ppReadable p) $
        [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t3]
        t1 = cTApplys tSub [t3, t2]

-- else, no instances to match
genAddInsts _ _ _ _ = []

-- -------------------------

-- A bag of non-constant, non-TAdd/TSub terms which have been added;
-- a bag of non-constant, non-TAdd/TSub terms which have been subtracted;
-- and a sum of constant terms
--  * The constant sum may not be needed when the proviso reduces fully;
--    but when the proviso does not reduce, it allows us to make some
--    progress and hopefully report a slightly simpler proviso error.
--    It may also improve efficiency in the fully-reducible case by
--    avoiding having to do multiple steps of reduction.
--  * We will keep the two bags reduced: if a type appears in both,
--    we remove it from both
data AddTerms = AddTerms Integer (B.Bag Type) (B.Bag Type)

unionAddTerms :: AddTerms -> AddTerms -> AddTerms
unionAddTerms (AddTerms i1 add_b1 sub_b1) (AddTerms i2 add_b2 sub_b2) =
    let
        -- cross out any sub terms from one that appear in the other
        (add_b1', sub_b2') = B.removeIntersection add_b1 sub_b2
        (add_b2', sub_b1') = B.removeIntersection add_b2 sub_b1
    in
        AddTerms (i1 + i2)
                 (B.union add_b1' add_b2')
                 (B.union sub_b1' sub_b2')

singletonAddTerms :: Type -> AddTerms
singletonAddTerms (TCon (TyNum { tynum_value = n })) = AddTerms n B.empty B.empty
singletonAddTerms t = AddTerms 0 (B.singleton t) B.empty

invertAddTerms :: AddTerms -> AddTerms
invertAddTerms (AddTerms i add_b sub_b) = (AddTerms (-i) sub_b add_b)

toAddTerms :: Type -> AddTerms
toAddTerms (TAp (TAp tc t1) t2)
    | tc == tAdd = unionAddTerms (toAddTerms t1) (toAddTerms t2)
toAddTerms (TAp (TAp tc t1) t2)
    | tc == tSub = unionAddTerms (toAddTerms t1) (invertAddTerms (toAddTerms t2))
toAddTerms t = singletonAddTerms t

fromAddTerms :: AddTerms -> Type
fromAddTerms (AddTerms 0 add_b sub_b) =
    mkAddType (B.toList add_b) (B.toList sub_b)
fromAddTerms (AddTerms i add_b sub_b) =
    let it = cTNum (abs i) noPosition  -- XXX better position?
    in  if (i > 0)
        then mkAddType (it : B.toList add_b) (B.toList sub_b)
        else mkAddType (B.toList add_b)      (it : B.toList sub_b)

mkAddType :: [Type] -> [Type] -> Type
mkAddType add_ts sub_ts =
    let mkTAdd t1 t2 = TAp (TAp tAdd t1) t2
        mkTSub t1 t2 = TAp (TAp tSub t1) t2
        add_val = case add_ts of
                     [] -> cTNum 0 noPosition  -- XXX better position?
                     ts -> foldr1 mkTAdd add_ts
    in  foldl mkTSub add_val sub_ts

differenceAddTerms :: AddTerms -> AddTerms -> AddTerms
differenceAddTerms big small = unionAddTerms big (invertAddTerms small)

intersectionAddTerms :: AddTerms -> AddTerms -> AddTerms
intersectionAddTerms (AddTerms i1 add_b1 sub_b1) (AddTerms i2 add_b2 sub_b2) =
    AddTerms (min i1 i2)
             (B.intersection add_b1 add_b2)
             (B.intersection sub_b1 sub_b2)

nullAddTerms :: AddTerms -> Bool
nullAddTerms (AddTerms i a s) = (i == 0) && (B.null a) && (B.null s)

-- -------------------------

-- Return whether a type "t1" is known to be less than or equal to type "t2".
-- This is true when the types are equal or when "t2" is a TMax (or nested
-- TMax) containing "t1".  It is also true if "t1" is a TMin (or nested TMin)
-- containing "t2".
isKnownLTE :: Type -> Type -> Bool
isKnownLTE t1 (TAp (TAp tc tA) tB) | tc == tMax =
   (isKnownLTE t1 tA) || (isKnownLTE t1 tB)
isKnownLTE (TAp (TAp tc tA) tB) t2 | tc == tMin =
   (isKnownLTE tA t2) || (isKnownLTE tB t2)
isKnownLTE t1 t2 | t1 == t2 = True
isKnownLTE _ _ = False

-- -------------------------

clsMax :: Class
clsMax = Class {
        name = CTypeclass idMax,
        csig = [tvarh1, tvarh2, tvarh3],
        super = [],  -- [IsIn clsSize [TVar tvarh1], IsIn clsSize [TVar tvarh2], IsIn clsSize [TVar tvarh3]]
        genInsts = genMaxInsts,
        tyConOf = TyCon idMax (Just (Kfun KNum (Kfun KNum (Kfun KNum KStar)))) (TIstruct SClass []),
        funDeps = [[False, False, True]],
        funDeps2 = [[Just False, Just False, Just True]],
        allowIncoherent = Just False,
        isComm = True
        }

genMaxInsts :: [TyVar] -> Maybe [TyVar] -> Pred -> [Inst]

-- (C1, C2, ?) : (C1, C2, max(C1,C2))
genMaxInsts _ _ (IsIn c [t1@(TCon (TyNum n1 p1)), t2@(TCon (TyNum n2 _)), _])
        = [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t3]
        t3 = TCon (TyNum (n1 `max` n2) p1)

-- (0, T, ?) : (0, T, T)
genMaxInsts _ _ (IsIn c [t1@(TCon (TyNum 0 _)), t2, _])
        = [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t2]

-- (T, 0, ?) : (T, 0, T)
genMaxInsts _ _ (IsIn c [t1, t2@(TCon (TyNum 0 _)), _])
        = [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t1]

-- (T1, T2, TMax#(T1,T2)) : itself
-- (T1, T2, TMax#(T2,T1)) : itself
genMaxInsts _ _ (IsIn c [t1, t2, t3])
    | t3 == cTApplys tMax [t1, t2] ||
      t3 == cTApplys tMax [t2, t1] = [ mkInst r ([] :=> p) ]
 where r = anyTExpr (predToType p)
       p = IsIn c [t1, t2, t3]

-- XXX The above rules are a simple case of this
-- Note that this rule only matches if the terms on either side are equal
-- (this rule does not try to reduce the terms to a smaller set)
genMaxInsts _ _ p@(IsIn c [t1, t2, t3]) | equalMaxTerms s1 s2 =
        [ mkInst r ([] :=> p) ]
  where s1 = toMaxTerms (TAp (TAp tMax t1) t2)
        s2 = toMaxTerms t3
        r = anyTExpr (predToType p)

-- when satisfyFV, as a last resort:
-- (T1, T2, V) : (T1, T2, TMax#(T1,T2))
--   when V is not bound or dependent and T1 and T2 contain only variables
--        which are bound or dependent
genMaxInsts bvs (Just dvs) (IsIn c [t1, t2, tv@(TVar v)])
    | v `notElem` dvs,
      checkDVS dvs (t1, t2),
      mgu bvs tv t3 /= Nothing =
        [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t3]
        t3 = TAp (TAp tMax t1) t2

-- else, no instances to match
genMaxInsts _ _ _ = []

-- -------------------------

-- A set of non-constant, non-TMax terms and the max of constant terms
data MaxTerms = MaxTerms Integer (S.Set Type)

unionMaxTerms :: MaxTerms -> MaxTerms -> MaxTerms
unionMaxTerms (MaxTerms i1 s1) (MaxTerms i2 s2) =
    MaxTerms (max i1 i2) (S.union s1 s2)

singletonMaxTerms :: Type -> MaxTerms
singletonMaxTerms (TCon (TyNum { tynum_value = n })) = MaxTerms n S.empty
singletonMaxTerms t = MaxTerms 0 (S.singleton t)

toMaxTerms :: Type -> MaxTerms
toMaxTerms (TAp (TAp tc t1) t2)
    | tc == tMax = unionMaxTerms (toMaxTerms t1) (toMaxTerms t2)
toMaxTerms t = singletonMaxTerms t

equalMaxTerms :: MaxTerms -> MaxTerms -> Bool
equalMaxTerms (MaxTerms i1 s1) (MaxTerms i2 s2) = (i1 == i2) && (s1 == s2)

-- -------------------------

clsMin :: Class
clsMin = Class {
        name = CTypeclass idMin,
        csig = [tvarh1, tvarh2, tvarh3],
        super = [],  -- [IsIn clsSize [TVar tvarh1], IsIn clsSize [TVar tvarh2], IsIn clsSize [TVar tvarh3]]
        genInsts = genMinInsts,
        tyConOf = TyCon idMin (Just (Kfun KNum (Kfun KNum (Kfun KNum KStar)))) (TIstruct SClass []),
        funDeps = [[False, False, True]],
        funDeps2 = [[Just False, Just False, Just True]],
        allowIncoherent = Just False,
        isComm = True
        }

genMinInsts :: [TyVar] -> Maybe [TyVar] -> Pred -> [Inst]

-- (C1, C2, ?) : (C1, C2, min(C1,C2))
genMinInsts _ _ (IsIn c [t1@(TCon (TyNum n1 p1)), t2@(TCon (TyNum n2 _)), _])
        = [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t3]
        t3 = TCon (TyNum (n1 `min` n2) p1)

-- (0, T, ?) : (0, T, 0)
genMinInsts _ _ (IsIn c [t1@(TCon (TyNum 0 _)), t2, _])
        = [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t1]

-- (T, 0, ?) : (T, 0, 0)
genMinInsts _ _ (IsIn c [t1, t2@(TCon (TyNum 0 _)), _])
        = [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t2]

-- (T1, T2, TMin#(T1,T2)) : itself
-- (T1, T2, TMin#(T2,T1)) : itself
genMinInsts _ _ (IsIn c [t1, t2, t3])
    | t3 == cTApplys tMin [t1, t2] ||
      t3 == cTApplys tMin [t2, t1] = [ mkInst r ([] :=> p) ]
 where r = anyTExpr (predToType p)
       p = IsIn c [t1, t2, t3]

-- XXX The above rules are a simple case of this
-- Note that this rule only matches if the terms on either side are equal
-- (this rule does not try to reduce the terms to a smaller set)
genMinInsts _ _ p@(IsIn c [t1, t2, t3]) | equalMinTerms s1 s2 =
        [ mkInst r ([] :=> p) ]
  where s1 = toMinTerms (TAp (TAp tMin t1) t2)
        s2 = toMinTerms t3
        r = anyTExpr (predToType p)

-- when satisfyFV, as a last resort:
-- (T1, T2, V) : (T1, T2, TMin#(T1,T2))
--   when V is not bound or dependent and T1 and T2 contain only variables
--        which are bound or dependent
genMinInsts bvs (Just dvs) (IsIn c [t1, t2, tv@(TVar v)])
    | v `notElem` dvs,
      checkDVS dvs (t1, t2),
      mgu bvs tv t3 /= Nothing =
        [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t3]
        t3 = TAp (TAp tMin t1) t2

-- else, no instances to match
genMinInsts _ _ _ = []

-- -------------------------

-- A set of non-constant, non-TMin terms and the min of constant terms
data MinTerms = MinTerms (Maybe Integer) (S.Set Type)

unionMinTerms :: MinTerms -> MinTerms -> MinTerms
unionMinTerms (MinTerms mi1 s1) (MinTerms mi2 s2) =
    let mi' = case (mi1, mi2) of
                (Nothing, _) -> mi2
                (_, Nothing) -> mi1
                (Just i1, Just i2) -> Just (min i1 i2)
    in  MinTerms mi' (S.union s1 s2)

singletonMinTerms :: Type -> MinTerms
singletonMinTerms (TCon (TyNum { tynum_value = n })) = MinTerms (Just n) S.empty
singletonMinTerms t = MinTerms Nothing (S.singleton t)

toMinTerms :: Type -> MinTerms
toMinTerms (TAp (TAp tc t1) t2)
    | tc == tMin = unionMinTerms (toMinTerms t1) (toMinTerms t2)
toMinTerms t = singletonMinTerms t

equalMinTerms :: MinTerms -> MinTerms -> Bool
equalMinTerms (MinTerms i1 s1) (MinTerms i2 s2) = (i1 == i2) && (s1 == s2)

-- -------------------------

clsLog :: Class
clsLog = Class {
        name = CTypeclass idLog,
        csig = [tvarh1, tvarh2],
        super = [],  -- [IsIn clsSize [TVar tvarh1], IsIn clsSize [TVar tvarh2], IsIn clsSize [TVar tvarh3]]
        genInsts = genLogInsts,
        tyConOf = TyCon idLog (Just (Kfun KNum (Kfun KNum KStar))) (TIstruct SClass []),
        funDeps = [[False, True]],
        funDeps2 = [[Just False, Just True]],
        allowIncoherent = Just False,
        isComm = False
        }

genLogInsts :: [TyVar] -> Maybe [TyVar] -> Pred -> [Inst]

-- (0, ?) : no instance
genLogInsts _ _ (IsIn c [t1@(TCon (TyNum i1 p1)), _])
        | i1 == 0 = []

-- (C, ?) : (C, log(C))
genLogInsts _ _ (IsIn c [t1@(TCon (TyNum i1 p1)), _])
        | i1 > 0 = [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2]
        t2 = TCon (TyNum (log2 i1) p1)

-- For most C, there are multiple X for which Log#(X,C) is an instance.
-- This code produces only one instance, and it would only match if the
-- first type is the exact TyNum, which would have been caught by the
-- above case arm.  So this case arm is useless:
{-
-- (?, C) : (2^C, C)
genLogInsts _ _ (IsIn c [_, t2@(TCon (TyNum i2 p2))])
        | i2 >= 0 = [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2]
        t1 = TCon (TyNum (2 ^ i2) p2)
-}

-- (T, TLog#(T)) : itself
-- (TExp#(T), T) : itself
genLogInsts _ _ p@(IsIn c [t1, t2])
    | (tcon, [arg]) <- splitTAp t2,
      tcon == tLog, arg == t1 = [ mkInst r ([] :=> p) ]
    | (tcon, [arg]) <- splitTAp t1,
      tcon == tExp, arg == t2 = [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)

-- XXX Add this?
-- (TExp#(T1), T2) : NumEq(T1,T2) => itself

{-
-- XXX Consider removing this:
-- when satisfyFV, as a last resort:
-- (V, T) : (TExp#(T), V)
--   when V is not bound or dependent and T contains only variables
--        which are bound or dependent
-- XXX Log a b does not have b -> a fundep
-- YYY This should be OK because (in theory)
-- if we get here v is "otherwise unconstrained"
-- otherwise we'd have learned something before
-- dvs reduction kicks in (at the second satisfyFV)
genLogInsts bvs (Just dvs) (IsIn c [tv@(TVar v),t2])
    | v `notElem` dvs,
      checkDVS dvs t2,
      mgu bvs tv t1 /= Nothing =
        [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2]
        t1 = TAp tExp t2
-}

-- when satisfyFV, as a last resort:
-- (T, V) : (T, TLog#(T))
--   when V is not bound or dependent and T contains only variables
--        which are bound or dependent
-- XXX Should this also introduce a NotZero#(T) proviso?
genLogInsts bvs (Just dvs) (IsIn c [t1,tv@(TVar v)])
    | v `notElem` dvs,
      checkDVS dvs t1,
      mgu bvs tv t2 /= Nothing =
        [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2]
        t2 = TAp tLog t1

-- else, no instances to match
genLogInsts _ _ _ = []

-- -------------------------

clsMul :: SymTab -> Class
clsMul symT = Class {
        name = CTypeclass idMul,
        csig = [tvarh1, tvarh2, tvarh3],
        super = [],  -- [IsIn clsSize [TVar tvarh1], IsIn clsSize [TVar tvarh2], IsIn clsSize [TVar tvarh3]]
        genInsts = genMulInsts symT,
        tyConOf = TyCon idMul (Just (Kfun KNum (Kfun KNum (Kfun KNum KStar)))) (TIstruct SClass []),
        funDeps = [[False, False, True], [False, True, False], [True, False, False]],
        funDeps2 = [[Just False, Just False, Just True],
                    [Just False, Just True, Just False],
                    [Just True, Just False, Just False]],
        allowIncoherent = Just False,
        isComm = True
        }

genMulInsts :: SymTab -> [TyVar] -> Maybe [TyVar] -> Pred -> [Inst]

-- (C1, C2, ?) : (C1, C2, C1*C2)
genMulInsts _ _ _ (IsIn c [t1@(TCon (TyNum n1 p1)), t2@(TCon (TyNum n2 _)), _])
        = [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t3]
        t3 = TCon (TyNum (n1 * n2) p1)

-- (C1, ?, C3) : (C1, C3/C1, C3) when C3/C1 has no remainder (and C1 is not 0)
genMulInsts _ _ _ (IsIn c [t1@(TCon (TyNum i1 p1)), _, t3@(TCon (TyNum i3 _))])
        | i1 /= 0 && i3 `mod` i1 == 0 = [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t3]
        t2 = TCon (TyNum (i3 `div` i1) p1)

-- (?, C2, C3) : (C3/C2, C2, C3) when C3/C2 has no remainder (and C2 is not 0)
genMulInsts _ _ _ (IsIn c [_, t2@(TCon (TyNum i2 p2)), t3@(TCon (TyNum i3 _))])
        | i2 /= 0 && i3 `mod` i2 == 0 = [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t3]
        t1 = TCon (TyNum (i3 `div` i2) p2)

-- (1, T, ?) : (1, T, T)
genMulInsts _ _ _ (IsIn c [t1@(TCon (TyNum 1 _)), t2, _])
        = [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t2]

-- (0, T, ?) : (0, T, 0)
genMulInsts _ _ _ (IsIn c [t1@(TCon (TyNum 0 _)), t2, _])
        = [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t1]

-- (T, 1, ?) : (T, 1, T)
genMulInsts _ _ _ (IsIn c [t1, t2@(TCon (TyNum 1 _)), _])
        = [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t1]

-- (T, 0, ?) : (T, 0, 0)
genMulInsts _ _ _ (IsIn c [t1, t2@(TCon (TyNum 0 _)), _])
        = [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t2]

-- (?, T, T) : (1, T, T)
genMulInsts _ _ _ (IsIn c [_, t2, t3])
        | t2 == t3 = [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t3]
        t1 = TCon (TyNum 1 (getPosition t2))

-- (T, ?, T) : (T, 1, T)
genMulInsts _ _ _ (IsIn c [t1, _, t3])
        | t1 == t3 = [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t3]
        t2 = TCon (TyNum 1 (getPosition t1))

-- (T, T, C) : NumEq(T, sqrt(C)) => itself, when C is a perfect square
genMulInsts symT _ _ p@(IsIn c [t1, t2, TCon (TyNum n npos)])
    | t1 == t2, (Just sqrt_n) <- integerSqrt n
    = [ mkImpliedInst (IsIn clsNumEq [t1, TCon (TyNum sqrt_n npos)]) p ]
  where
    -- look up the class, rather than construct it, for better sharing
    clsNumEq = mustFindClass symT (CTypeclass idNumEq)

-- (T1, T2, TMul#(T1,T2)) : itself
-- (T1, T2, TMul#(T2,T1)) : itself
genMulInsts _ _ _ p@(IsIn c [t1, t2, t3])
    | t3 == cTApplys tMul [t1, t2] ||
      t3 == cTApplys tMul [t2, t1] = [ mkInst r ([] :=> p) ]
 where r = anyTExpr (predToType p)

-- XXX The above rules are simple cases of this:
genMulInsts symT _ _ p@(IsIn c [t1, t2, t3])
    | (equalMulTerms b1 b2) = [ mkInst r ([] :=> p) ]
 where b1 = toMulTerms (TAp (TAp tMul t1) t2)
       b2 = toMulTerms t3
       r = anyTExpr (predToType p)

-- (T1, T1, TMul#(T2, T2)) : NumEq(T1,T2) => itself
genMulInsts symT _ _ p@(IsIn c [t1,t1',t3])
    | t1 == t1', (tcon, [tA, tA']) <- splitTAp t3,
      tcon == tMul, tA == tA'
    = [ mkImpliedInst (IsIn clsNumEq [t1, tA]) p ]
  where
    -- look up the class, rather than construct it, for better sharing
    clsNumEq = mustFindClass symT (CTypeclass idNumEq)

-- XXX Not sure this is useful without a NotZero class
{-
-- (T1, T2, TMul#(T1,T3)) : NumEq(T2,T3) => itself
-- (T1, T2, TMul#(T3,T1)) : NumEq(T2,T3) => itself
--   when T1 /= 0, which can be expressed now as a condition on the structure
--        of T1 (e.g. it's a TyNum that is not 0) but later could be expressed
--        with a NotZero superclass
-- (T1, T2, TMul#(T2,T3)) : NumEq(T1,T3) => itself
-- (T1, T2, TMul#(T3,T1)) : NumEq(T1,T3) => itself
--   when T2 /= 0, which can be expressed now as a condition on the structure
--        of T1 (e.g. it's a TyNum that is not 0) but later could be expressed
--        with a NotZero superclass
genMulInsts symT _ _ p@(IsIn c [t1, t2, t3@(TAp (TAp tc tA) tB)])
    | tc == tMul,
      t1 == tA,
      -- when not zero
      isTNum t1, getTNum t1 /= 0
    = [ mkImpliedInst (IsIn clsNumEq [t2, tB]) p ]
    | tc == tMul,
      t1 == tB,
      -- when not zero
      isTNum t1, getTNum t1 /= 0
    = [ mkImpliedInst (IsIn clsNumEq [t2, tA]) p ]
    | tc == tMul,
      t2 == tA,
      -- when not zero
      isTNum t2, getTNum t2 /= 0
    = [ mkImpliedInst (IsIn clsNumEq [t1, tB]) p ]
    | tc == tMul,
      t2 == tB,
      -- when not zero
      isTNum t2, getTNum t2 /= 0
    = [ mkImpliedInst (IsIn clsNumEq [t1, tA]) p ]
  where
    -- look up the class, rather than construct it, for better sharing
    clsNumEq = mustFindClass symT (CTypeclass idNumEq)
-}

-- XXX The above and below rules could be generalized using MulTerms
-- XXX but we'd have to be careful about non-commutativity of TDiv and
-- XXX non-zeroness when crossing out TMul terms.
-- XXX For now, we settle for just reducing the constant terms.
genMulInsts symT _ _ p@(IsIn c [t1, t2, t3])
    | common_divisor > 1
    = [ mkImpliedInst (IsIn clsNumEq [t12',t3']) p]
 where b1 = toMulTerms (TAp (TAp tMul t1) t2)
       b2 = toMulTerms t3
       common_divisor = constIntersectionMulTerms b1 b2
       b1_rem = constDifferenceMulTerms b1 common_divisor
       b2_rem = constDifferenceMulTerms b2 common_divisor
       t12' = fromMulTerms b1_rem
       t3' = fromMulTerms b2_rem
       -- look up the class, rather than construct it, for better sharing
       clsNumEq = mustFindClass symT (CTypeclass idNumEq)

-- when satisfyFV, as a last resort, though, we can ignore the NotZero
-- requirement and see if things satisfy:
-- (T1, T2, TMul#(T1,T3)) : NumEq(T2,T3) => itself
-- (T1, T2, TMul#(T3,T1)) : NumEq(T2,T3) => itself
-- (T1, T2, TMul#(T2,T3)) : NumEq(T1,T3) => itself
-- (T1, T2, TMul#(T3,T1)) : NumEq(T1,T3) => itself
genMulInsts symT _ (Just _) p@(IsIn c [t1, t2, t3@(TAp (TAp tc tA) tB)])
    | tc == tMul,
      t1 == tA
    = [ mkImpliedInst (IsIn clsNumEq [t2, tB]) p ]
    | tc == tMul,
      t1 == tB
    = [ mkImpliedInst (IsIn clsNumEq [t2, tA]) p ]
    | tc == tMul,
      t2 == tA
    = [ mkImpliedInst (IsIn clsNumEq [t1, tB]) p ]
    | tc == tMul,
      t2 == tB
    = [ mkImpliedInst (IsIn clsNumEq [t1, tA]) p ]
  where
    -- look up the class, rather than construct it, for better sharing
    clsNumEq = mustFindClass symT (CTypeclass idNumEq)

-- when satisfyFV, as a last resort:
-- (T1, T2, V) : (T1, T2, TMul#(T1,T2))
--   when V is not bound or dependent and T1 and T2 contain only variables
--        which are bound or dependent
genMulInsts _ bvs (Just dvs) (IsIn c [t1,t2,tv@(TVar v)])
    | v `notElem` dvs,
      checkDVS dvs (t1, t2),
      mgu bvs tv t3 /= Nothing =
        [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t3]
        t3 = TAp (TAp tMul t1) t2

{-
genMulInsts (Just dvs) (IsIn c [t1,TVar v,t3]) | v `notElem` dvs =
        [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t3]
        t2 = TAp (TAp tDiv t3) t1

genMulInsts (Just dvs) (IsIn c [TVar v,t2,t3]) | v `notElem` dvs =
        [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t3]
        t1 = TAp (TAp tDiv t3) t2
-}

-- else, no instances to match
genMulInsts _ _ _ _ = []

-- -------------------------

-- Basic commutativity rules for Mul/TMul (similar to Add/TAdd).
-- However, since Div/TDiv round, they are not commutative, and are
-- therefore not included in this analysis (like Sub/TSub with Add/TAdd).

-- A bag of non-constant, non-TMul terms which have been multiplied;
-- and a product of constant terms
--  * The constant product may not be needed when the proviso reduces fully;
--    but when the proviso does not reduce, it allows us to make some
--    progress and hopefully report a slightly simpler proviso error.
--    It may also improve efficiency in the fully-reducible case by
--    avoiding having to do multiple steps of reduction.
data MulTerms = MulTerms Integer (B.Bag Type)

unionMulTerms :: MulTerms -> MulTerms -> MulTerms
unionMulTerms (MulTerms i1 mul_b1) (MulTerms i2 mul_b2) =
    MulTerms (i1 * i2) (B.union mul_b1 mul_b2)

singletonMulTerms :: Type -> MulTerms
singletonMulTerms (TCon (TyNum { tynum_value = n })) = MulTerms n B.empty
singletonMulTerms t = MulTerms 1 (B.singleton t)

toMulTerms :: Type -> MulTerms
toMulTerms (TAp (TAp tc t1) t2)
    | tc == tMul = unionMulTerms (toMulTerms t1) (toMulTerms t2)
toMulTerms t = singletonMulTerms t

fromMulTerms :: MulTerms -> Type
fromMulTerms (MulTerms 1 mul_b) =
    mkMulType (B.toList mul_b)
fromMulTerms (MulTerms i mul_b) =
    let it = cTNum i noPosition  -- XXX better position?
    in  mkMulType (it : B.toList mul_b)

mkMulType :: [Type] -> Type
mkMulType [] = cTNum 1 noPosition  -- XXX better position?
mkMulType mul_ts =
    let mkTMul t1 t2 = TAp (TAp tMul t1) t2
    in  foldr1 mkTMul mul_ts

equalMulTerms :: MulTerms -> MulTerms -> Bool
equalMulTerms (MulTerms i1 mul_b1) (MulTerms i2 mul_b2) =
    (i1 == i2) && (mul_b1 == mul_b2)

constIntersectionMulTerms :: MulTerms -> MulTerms -> Integer
constIntersectionMulTerms (MulTerms i1 _) (MulTerms i2 _) =
    gcd i1 i2

constDifferenceMulTerms :: MulTerms -> Integer -> MulTerms
constDifferenceMulTerms (MulTerms i mul_b) c =
    -- doesn't check that the constant is an integral divisor
    MulTerms (i `div` c) mul_b

-- -------------------------

clsDiv :: Class
clsDiv = Class {
        name = CTypeclass idDiv,
        csig = [tvarh1, tvarh2, tvarh3],
        super = [],  -- [IsIn clsSize [TVar tvarh1], IsIn clsSize [TVar tvarh2], IsIn clsSize [TVar tvarh3]]
        genInsts = genDivInsts,
        tyConOf = TyCon idDiv (Just (Kfun KNum (Kfun KNum (Kfun KNum KStar)))) (TIstruct SClass []),
        funDeps = [[False, False, True]],
        funDeps2 = [[Just False, Just False, Just True]],
        allowIncoherent = Just False,
        isComm = False
        }

genDivInsts :: [TyVar] -> Maybe [TyVar] -> Pred -> [Inst]

-- (C1, C2, ?) : (C1, C2, C1/C2)
genDivInsts _ _ (IsIn c [t1@(TCon (TyNum i1 pos)), t2@(TCon (TyNum i2 _)), _])
        = [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t3]
        t3 = TCon (TyNum ((i1+i2-1) `div` i2) pos)

-- (T, 1, ?) : (T, 1, T)
genDivInsts _ _ (IsIn c [t1, t2@(TCon (TyNum 1 _)), _])
        = [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t1]

-- XXX Add this?
-- (0, T, ?) : (0, T, 0)

-- (T1, T2, TDiv#(T1,T2)) : itself
genDivInsts _ _ (IsIn c [t1, t2, t3])
    | t3 == cTApplys tDiv [t1, t2] = [ mkInst r ([] :=> p) ]
 where r = anyTExpr (predToType p)
       p = IsIn c [t1, t2, t3]

-- when satisfyFV, as a last resort:
-- (T1, T2, V) : (T1, T2, TDiv#(T1,T2))
--   when V is not bound or dependent and T1 and T2 contain only variables
--        which are bound or dependent
-- XXX need t2 /= 0 as well
genDivInsts bvs (Just dvs) (IsIn c [t1,t2,tv@(TVar v)])
    | v `notElem` dvs,
      checkDVS dvs (t1, t2),
      mgu bvs tv t3 /= Nothing =
        [ mkInst r ([] :=> p) ]
  where r = anyTExpr (predToType p)
        p = IsIn c [t1, t2, t3]
        t3 = TAp (TAp tDiv t1) t2

-- else, no instances to match
genDivInsts _ _ _ = []

-- -------------------------

clsNumEq :: SymTab -> Class
clsNumEq symT =
       Class {
            name = CTypeclass idNumEq,
            csig = [tvarh1, tvarh2],
            super = [],
            genInsts = genNumEqInsts symT,
            tyConOf = TyCon idNumEq (Just kNNS) (TIstruct SClass []),
            funDeps  = [[False, True], [True, False]],
            funDeps2 = [[Just False, Just True], [Just True, Just False]],
            allowIncoherent = Just False,
            isComm = True
            }

genNumEqInsts :: SymTab ->  [TyVar] -> Maybe [TyVar] -> Pred -> [Inst]
-- safe base-case if t1 and t2 are syntactically equal
genNumEqInsts symT _ _ p@(IsIn c [t1, t2])
    | t1 == t2 = [ mkInst r ([] :=> p) ]
  where p = IsIn c [t1, t1]
        r = anyTExpr (predToType p)

-- reduce a requested equality to a simpler provisos
-- (i.e. fewer type functions)
genNumEqInsts symT _ _ p@(IsIn c [t, t'])
    | tcon == tAdd, [t1, t2] <- args = [ mkImpliedInst (IsIn clsAdd' [t1, t2, tB]) p ]
    | tcon == tSub, [t1, t2] <- args = [ mkImpliedInst (IsIn clsAdd' [t2, tB, t1]) p ]
    | tcon == tMul, [t1, t2] <- args = [ mkImpliedInst (IsIn clsMul' [t1, t2, tB]) p ]
    | tcon == tDiv, [t1, t2] <- args = [ mkImpliedInst (IsIn clsDiv [t1, t2, tB]) p ]
    | tcon == tMax, [t1, t2] <- args = [ mkImpliedInst (IsIn clsMax [t1, t2, tB]) p ]
    | tcon == tMin, [t1, t2] <- args = [ mkImpliedInst (IsIn clsMin [t1, t2, tB]) p ]
    | tcon == tLog, [t1] <- args     = [ mkImpliedInst (IsIn clsLog [t1, tB])     p ]
    -- we do NumEq (TExp a) (TExp b) ==> NumEq a b because more is tricky
    | tcon == tExp, [t1] <- args,
      (tcon2, args2) <- splitTAp tB,
      tcon2 == tExp, [t2] <- args2   = [ mkImpliedInst (IsIn c [t1, t2])       p ]
    | tcon == tSizeOf, [t1] <- args  = [ mkImpliedInst (IsIn clsBits [t1, tB]) p ]
  where clsBits = mustFindClass symT (CTypeclass idBits)
        -- look up the class, rather than construct it, for better sharing
        clsAdd' = mustFindClass symT (CTypeclass idAdd)
        clsMul' = mustFindClass symT (CTypeclass idMul)
        -- tA should have more structure since TAp sorts first
        (tA, tB) = ordPair (t, t')
        (tcon, args) = splitTAp tA

-- If one is a variable and the other has no tyvars, it's safe to unify them
genNumEqInsts _ _ _ (IsIn c [TVar {}, t2]) | null (tv t2)
    = [ mkInst r ([] :=> p) ]
  where p = IsIn c [t2, t2]
        r = anyTExpr (predToType p)
genNumEqInsts symT _ _ (IsIn c [t1, TVar {}]) | null (tv t1)
    = [ mkInst r ([] :=> p) ]
  where p = IsIn c [t1, t1]
        r = anyTExpr (predToType p)

-- reduce away a generated type variable
genNumEqInsts symT bvs (Just dvs) (IsIn c [t1, t2])
    | TVar v <- tB, checkDVS dvs tA, mgu bvs tB tA /= Nothing,
      let p = IsIn c [tA, tA], let r = anyTExpr (predToType p) =
        --trace ("NumEq " ++ ppReadable (r, p)) $
        [ mkInst r ([] :=> p) ]
  where (tA, tB) = ordPair (t1, t2)

genNumEqInsts _ _ _ _ = []

-- -------------------------

tiArrow, tiBit, tiSizeOf, tiInteger, tiReal :: TISort
tiArrow   = TIabstract
tiBit     = TIabstract
tiSizeOf  = TIabstract
tiInteger = TIabstract
tiReal    = TIabstract

tiClock, tiReset, tiInout, tiPrimArray :: TISort
tiClock   = TIabstract -- XXX TIstruct SInterface ... ?
tiReset   = TIabstract -- XXX TIstruct or Bit 1 ?
tiInout   = TIabstract
tiPrimArray = TIabstract

tiPair, tiBool, tiAction, tiRules, tiString, tiChar :: TISort
tiPair    = TIstruct SStruct [idPrimFst, idPrimSnd]
tiBool    = tiEnum [idFalse, idTrue]
tiAction  = TIabstract
tiRules   = TIabstract
tiString  = TIabstract
tiChar    = TIabstract

tiHandle, tiBufferMode, tiMaybe, tiList, tiFmt :: TISort
tiHandle  = TIabstract
tiBufferMode = tiEnum [idNoBuffering, idLineBuffering, idBlockBuffering]
tiMaybe   = tiData [idInvalid, idValid]
tiList    = tiData [idNil noPosition, idCons noPosition]
tiFmt     = TIabstract

tiUnit, tiPosition, tiType, tiName, tiPred, tiSchedPragma :: TISort
tiUnit    = TIstruct SStruct []
tiPosition = TIabstract
tiType = TIabstract
tiName = TIabstract
tiPred = TIabstract
tiSchedPragma = TIabstract

tyiArrow :: TypeInfo
tyiArrow   = TypeInfo (Just (idArrow noPosition)) (Kfun KStar (Kfun KStar KStar)) [] tiArrow
{-
tyiBit     = TypeInfo (Just idBit) (Kfun KNum KStar) [] tiBit
tyiInteger = TypeInfo (Just idInteger) KStar [] tiInteger
-}

-- -------------------------

-- all preTypes should have identifiers (i.e. be non-numeric, non-string) because the usage in MakeSymTab.hs depends on this
preTypes :: [TypeInfo]
preTypes = [
        tyiArrow,
{-
        tyiBit,
        tyiInteger,
        TypeInfo  idString KStar              [] TIabstract,
        TypeInfo  idSizeOf (Kfun KStar KNum)  [] TIabstract,
-}
        TypeInfo (Just idAdd) (Kfun KNum (Kfun KNum (Kfun KNum KStar))) [v1, v2, v3] (TIstruct SClass []),
        TypeInfo (Just idMax) (Kfun KNum (Kfun KNum (Kfun KNum KStar))) [v1, v2, v3] (TIstruct SClass []),
        TypeInfo (Just idMin) (Kfun KNum (Kfun KNum (Kfun KNum KStar))) [v1, v2, v3] (TIstruct SClass []),
        TypeInfo (Just idMul) (Kfun KNum (Kfun KNum (Kfun KNum KStar))) [v1, v2, v3] (TIstruct SClass []),
        TypeInfo (Just idDiv) (Kfun KNum (Kfun KNum (Kfun KNum KStar))) [v1, v2, v3] (TIstruct SClass []),
        TypeInfo (Just idLog) (Kfun KNum (Kfun KNum KStar)) [v1, v2] (TIstruct SClass []),
        TypeInfo (Just idNumEq) (Kfun KNum (Kfun KNum KStar)) [v1, v2] (TIstruct SClass [])
        ]

preClasses :: SymTab -> [Class]
preClasses symT = [clsNumEq symT,
                   clsAdd symT,
                   clsMax,
                   clsMin,
                   clsLog,
                   clsMul symT,
                   clsDiv ]

isPreClass :: Class -> Bool
isPreClass cl =
    let preClassNames = map name (preClasses (internalError "isPreClass"))
    in  (name cl) `elem` preClassNames

preValues :: [(Id, VarInfo)]
preValues = [
--        (idValueOf, VarInfo VarPrim (idValueOf :>: Forall [KNum] ([] :=> (TGen noPosition 0 `fn` tInteger))) Nothing)
        ]

-- -------------------------