content: {-+
  The various auxiliary operations required by the extensible type checker
  are defined here.
  -}
  module TiPropInstances where
  import List(partition)
  import Maybe(isJust)
  --import Maybe(mapMaybe)
  
  import HasBaseStruct
  import PropSyntax
  import TI hiding (Subst,Qual(..))
  --import TiD(DeclInfo(..),HasMethodSigs(..))
  --import TiHsName
  --import TiBaseStruct(pApp)
  import TiBase()
  --import TiPrelude(pt)
  import HsPropStruct
  import MUtils
  import DefinedNamesProp()
  import FreeNamesProp()
  import Substitute
  import SubstituteProp
  
  instance HasId i (HsExpI i) where
    ident = base . ident
    isId = isId @@ basestruct
  
  --instance HasLit (HsExpI i) where lit = hsLit loc0
  ----instance HasLit (HsPatI i) where lit = hsPLit
  
  instance HasCoreSyntax i (HsExpI i) where
    app e1 e2 = hsApp e1 e2
    tuple = hsTuple
    list = hsList
  
  instance HasAbstr i (HsExpI i) where
    abstract = hsLambda . map var
  {-
  instance HasId i (HsPatI i) where
    ident = base . ident
    isId = isId @@ basestruct
  
  instance HasCoreSyntax i (HsPatI i) where
    app (Pat (Base p1)) p2 = base $ pApp p1 p2 -- hmm
    tuple = hsPTuple
    list = hsPList
  -}
  
  instance HasAbstr i (HsDeclI i) where
    abstract is = mapRec (mapProp (abstract is) id) -- !!
  
  instance HasAbstr i pa => HasAbstr i (PD i pa pp) where
    abstract is pd =
      case pd of
        HsAssertion s optn pa -> HsAssertion s optn (abstract is pa)
        HsPropDecl s n ns pp -> HsPropDecl s n (map HsVar is++ns) pp
  
  --instance HasAbstr i (AssertionI i) where
  --  abstract is pa = foldr propLambda pa is
  
  instance Eq i => HasLocalDef i (HsExpI i) (HsDeclI i) where
    letvar xt e = mapRec (mapProp (letvar xt e) id) -- !!
  
  instance (FreeNames i pa,MapExp e pa,HasAbstr i pa,
  	  HasLocalDef i e pa,
  	  FreeNames i pp,MapExp e pp,
  	  HasId i e,Subst i e)
        => HasLocalDef i e (PD i pa pp) where
    letvar xt@(i:>:t) e pd =
      case pd of
        HsPropDecl s n ns pp ->
  	  if HsVar i `elem` freeVars pp
            then if isJust (isId e)
  	       then HsPropDecl s n ns (esubst1 var e i pp)
  	       else --pd -- hmm!!
                      HsPropDecl s n ns (esubst1 var e i pp) --code duplication...
                      
  	  else pd
        HsAssertion s optn pa -> 
  	  if HsVar i `elem` freeVars pa
            then if isJust (isId e)
  	       then HsAssertion s optn (esubst1 var e i pa)
  	       else HsAssertion s optn (letvar xt e pa)
  	  else pd
  
  instance AddDeclsType i [HsDeclI i]
  
  instance HasDef [HsDeclI i] (HsDeclI i) where
    nullDef = null
    noDef = []
    consDef = (:)
    appendDef = (++)
    toDefs = id
    filterDefs = filter
  
  instance (ValueId i,TypeVar i) => DeclInfo i (HsDeclI i) where
    explicitlyTyped kenv tinfo ctx =
        recprop (explicitlyTyped kenv tinfo ctx) (explicitlyTyped kenv tinfo ctx)
    --isTypeDecl = isBase isTypeDecl . struct
    isUnrestricted expl = recprop (isUnrestricted expl) (isUnrestricted expl)
    keepAmbigTypes = recprop keepAmbigTypes keepAmbigTypes
  
  instance DeclInfo i (PD i pa pp) where
    explicitlyTyped _ _ _ pd =
      case pd of
        --HsAssertion s (Just n) pa -> ([],[HsCon n:>:mono (pt "Prop")])
        _ -> ([],[]) -- no explitit type info here...
    isUnrestricted _ _ = True
    keepAmbigTypes pd =
      case pd of
        HsAssertion {} -> True
        _ -> False
  
  
  --- Dummy instances ---
  -- Need something sensible when decorating the syntax tree with types...
  instance TypeVar i => Types i (HsDeclI i)    where tmap f = id; tv d = []
  instance TypeVar i => Types i (AssertionI i) where tmap f = id; tv d = []
  instance TypeVar i => Types i (PredicateI i) where tmap f = id; tv d = []
  
  instance HasTypeApp i (HsExpI i) where spec x _ ts = ident x
  --instance HasTypeApp i (HsPatI i) where spec x _ ts = ident x
  
  instance HasTypeAnnot i (HsExpI i)
  
  instance HasMethodSigs [HsDeclI i] where
    splitMethodSigs = partition isSig
      where
        isSig (Dec (Base (HsTypeSig {}))) = True
        --isSig (Dec (Prop (HsAssertion _ (Just _) _))) = True
        isSig _                           = False
  {-
  instance GetSigs i [Pred i] (Type i) [HsDeclI i] where
    getSigs = mapMaybe getSig
      where
        getSig (Dec (Base (HsTypeSig s is c tp))) = Just (s,is,c,tp)
        getSig _                                  = Nothing
  -}
  