content: module TiPropStruct where
  import PropSyntax hiding (Q(..))
  import qualified PropSyntax as P(Q(..))
  import PropSyntaxStruct(Prop,prop)
  import TI hiding (TI)
  --import TiHsName
  --import TiT(kcStar,kcPred)
  import TiE(tcLambda')
  import TiPrelude(pt)
  import SrcLoc
  import TypedIds(HasIdTy)
  import MUtils
  import Monad(unless)
  import PrettySymbols(el)
  import PrettyPrint hiding (var)
  import SimpleGraphs(reachable')
  
  -- For debugging:
  --import IOExts(trace)
  
  -- I wish there was an easier way to declare instances in Haskell...
  
  instance (TypeCheck i be e,TypeCheck i pe e) => TypeCheck i (Prop be pe) e where
    tc = prop tc tc
  {-
  instance (Printable bd,Printable pd,
            TypeCheckDecl i bd d,TypeCheckDecl i pd d)
         => TypeCheckDecl i (Prop bd pd) d where
    tcDecl bs d = --trace (pp d)  $
                  prop (tcDecl bs) (tcDecl bs) d
  
  instance (Fresh i,TypeId i,ValueId i,TypeVar i,HasSrcLoc i,--HasIdTy i,
            Printable i,Printable pa,Printable pp,
            TypeCheck i pa (Typed i pa2),
            TypeCheck i pp (Typed i pp2),
  	  HasDef ds2 d2,
  	  HasPropStruct d2 (PD i pa2 pp2))
        => TypeCheckDecl i (PD i pa pp) ds2
    where tcDecl = tcPD
  -}
  instance (TypeId i,ValueId i,Fresh i,HasSrcLoc i,HasIdTy x i,
            Printable i,Printable e1,--Printable t,
  	  TypeCheck i e1 (Typed i e2),
  	  TypeCheck i pa1 (Typed i pa2),
  	  TypeCheck i pp1 (Typed i pp2),
  	  HasTypeAnnot i e2,HasId i e2,
  	  HasPropStruct r (PA i e2 (HsQualTypeI i) pa2 pp2))
        => TypeCheck i (PA i e1 (HsQualTypeI i) pa1 pp1) (Typed i r)
    where tc = tcPA
  
  instance (TypeId i,ValueId i,Fresh i,HasSrcLoc i,HasIdTy x i,
            Printable t,Printable e1,Printable p1,
  	  Printable pa1,Printable pp1,PrintableOp i,
  	  DefinedNames i p1,
            TypeCheck i e1 (Typed i e2),
            TypeCheck i p1 (Typed i p2),
  	  TypeCheck i pa1 (Typed i pa2),
  	  TypeCheck i pp1 (Typed i pp2),
  	  HasId i e2,
  	  HasBaseStruct t (TI i t'),
  	  HasPropStruct r (PP i e2 p2 (P.Q [t] (Type i)) pa2 pp2)) =>
           TypeCheck i (PP i e1 p1 (P.Q [t] (Type i)) pa1 pp1) (Typed i r)
    where tc = tcPP
  
  {-
  predAp i [] = predId i
  predAp i as = predApp i as
  -}
  targs vs = map (([]P.:=>).tyvar) vs
  
  tcPP p =
    case p of
  --  PredId q -> do t <- propinst q
  --		   predId q>:t
  {-
      PredId q -> do (_,ds):>:t <- propinst_loc q -- add type params!!
                     predAp q (map Left ds)>:t
  -}
      PredApp i [] es -> do ((sc,vs),ds):>:ti <- propinst_loc i
  		          es':>:ts <- unzipTyped # mapM tcArg es
  		          v <- pfresh
  		          ti=:=funT (ts++[v])
  		          tpredApp i (targs vs) (map Left ds++es') >: v
      PredArrow p1 p2 -> do p1':>:t1 <- tcPred p1
  			  p2':>:t2 <- tcPred p2
  			  predArrow p1' p2'>:tPred (funT [t1,t2])
      PredInfixApp p1 i p2 -> do ((sc,vs),ds):>:ti <- propinst_loc i
                                 p1':>:t1 <- tc p1
  			       p2':>:t2 <- tc p2
  		               v <- pfresh
  		               ti=:=funT [t1,t2,v]
  			       let p' = if null ds && null vs
  			                then predInfixApp p1' i p2'
  				        else tpredApp i (targs vs) (map Left ds++map Right [p1',p2'])
  			       p'>:v
      PredNeg optt p -> do p':>:t <- tc p
  			 checkOptT optt t
  		         predNeg (Just ([]P.:=>t)) p'>:t
      PredOp op optt p1 p2 -> tcBinPred (predOp op) optt p1 p2
      PredLfp i optt p -> tcFp predLfp' i optt p
      PredGfp i optt p -> tcFp predGfp' i optt p
      PredNil -> do v<-tfresh
  		  listType <- getListType
                    predNil>:tPred (listType v)
      PredLifted e -> do e':>:t <- tc e
  		       v <- tfresh
  		       tBool <- getBoolType
  		       t=:=funT [v,tBool]
  		       predLifted e'>:tPred v
      PredStrong p -> do p':>:t <- tc p
  		       isPred t
  		       predStrong p'>:t
  
      PredParen p -> emap predParen # tc p
      PredComp pts a -> do let (ps,ts) = unzip pts
  		             --ts' = ts -- repeat Nothing -- hmm!!
  		         (ps',a') :>: (tps,t') <- tcLambda' ps a
  			 isProp t'
  			 let tps' = [Just ([]P.:=>tp)|tp<-tps]
  			 {- No rank 2 polymorphism: type variables in the
  			    type signatures are treated as free type variables
  			    that can be unified with other types. The type
  			    signature can only be used to make the
  			    inferred type more specific, not more general. -}
  			 sequence_ [tp=:=t|(tp,Just (_ P.:=>t))<-zip tps ts]--hm
  			 predComp (zip ps' tps') a'>:tPredn tps
      _ -> error (pp p)
  
  tcArg a = either (\e->emap Left # tc e) (\p->emap Right # tc p) a
  
  tcFp f i optt p =
      do --v <- pfresh -- too general (ok if proper kind checking is done)
         vv <- tfresh
         let v = tPred vv -- restricted to unary predicates
         p':>:t <-extend1 (HsCon i) (mono v) (tc p)
         t=:=v
         checkOptT optt v
         let qv= []P.:=>vv -- vv is more appropriate than v in the Alfa transl
         f i qv p'>:t
  
  checkOptT optt v =
      case optt of
        Nothing -> done
        Just ([]P.:=>ta) -> ta=:=v
        _ -> fail "qualified type annotation not supported"
  
  
  ----
  
  tProp :: TypeCon i => Type i
  tProp = pt "Prop"
  tPred v = funT [v,tProp]
  tPredn ts = funT (ts++[tProp])
  
  isProp t = t=:=tProp
  
  tcProp a = do a':>:t <- tc a
                isProp t
  	      return a'
  
  tcPred a = do ta@(a':>:t) <- tc a
                t'<-isPred t
  	      a'>:t' -- hmm
  
  isPred t = do v <- tfresh
                t=:=tPred v
  	      return v
  
  tcBinProp op a1 a2 = do p' <- propOp op # tcProp a1 <# tcProp a2
  		        p'>:tProp
  
  tcBinPred op optt p1 p2 = do p1':>:t1 <- tc p1
  			     p2':>:t2 <- tc p2
  			     t1=:=t2
  			     checkOptT optt t1 -- hmm
  			     op (Just ([]P.:=>t1)) p1' p2'>:t1
  
  propAp i [] = propId i
  propAp i es = propApp i es
  
  tcPA pa =
    case pa of
      Quant q i optt pa ->
         do t <- tfresh
  	  let bs = [HsVar i:>:t]
  	  --bs <- intro [HsVar i]
  	  check t optt
            pa' <- extendts ((map.fmap) mono bs) $ tcProp pa
            --quant q i optt pa' >: tProp
  	  quant q i (Just ([] P.:=> t)) pa' >: tProp
        where
         check t (Just (_ P.:=>t')) = t=:=t' -- !!
         check _ _ = return ()
  
  --  PropId q -> do t <- propinst q
  --		   propId q>:t
  {-
      PropId q -> do (_,ds):>:t <- propinst_loc q -- add type params!!
                     propAp q ds>:t
  -}
      PropApp i [] es -> do ((sc,vs),ds):>:ti <- propinst_loc i
  		          es':>:ts <- unzipTyped # mapM tcArg es
  		          v <- pfresh
  		          ti=:=funT (ts++[v])
  		          tpropApp i (targs vs) (map Left ds++es') >: v
      PropNeg a -> do a' <- tcProp a; propNeg a' >: tProp
      PropOp op a1 a2 -> tcBinProp op a1 a2
      PropEqual e1 e2 -> do e1':>:t1 <- tc e1
  			  e2':>:t2 <- tc e2
  			  t1=:=t2
  			  propEqual (typeAnnot e1' t1) e2' >: tProp
      PropHas e p -> do e':>:te <- tc e
  		      p':>:tp <- tc p
  		      tp=:=funT [te,tProp]
  		      propHas e' p' >: tProp
      PropParen a -> emap propParen # tc a
  
  tcPD bs d =
    case d of
      HsAssertion s optn pa ->
         posContext' s "in assertion" $
         do pa' <- tcProp pa
  	  maybe done (isProp @@ coninst' bs) optn
  	  return $ oneDef $ hsAssertion s optn pa'
      HsPropDecl s n ns pp ->
         do lbs <- ptintro ns
  	  tn <- coninst' bs n
  	  pp':>:t <- extendts ((map.fmap) mono lbs) $ tc pp
  	  tn=:=funT ([ t | _:>:t<-lbs]++[t])
            return $ oneDef $ hsPropDecl s n ns pp'
  
  ptintro xs = do ts <- freshlist (length xs)
  		let lbs = zipTyped (xs:>:ts)
  	        addptypes lbs
  	        return lbs
  
  addptypes ts = mapM_ addptype ts
  addptype (HsVar _:>:t) = addtype t
  addptype (HsCon _:>:t) = addprop t
  
  coninst' bs n =
    case [ t | HsCon x:>:t<-bs,x==n] of
      t:_ -> return t
      _ -> fail$"Type checker bug: no type introduced for: "++pp n
  
  {-
  propinst x =
    do s <- sch (HsCon x)
       ctx :=> t <- sinst s
       unless (null ctx) $
         fail.pp $
  	 sep [srcLoc x<+>"overloaded predicates are not supported (yet):",
  	      nest 4 (x<+>el<+>s)]
       return (toPredType (isCon x) t)
  -}
  
  propinst_loc x = propinst_loc' (Just (srcLoc x)) x
  propinst_loc' s x =
    do sc@(Forall ags gs qt) <- sch (HsCon x)
       vs <- freshvars gs
       let ctx:=> t = freshen' vs (tdom gs) qt
       ds <- newdicts s ctx
       ((sc,{-map tyvar-} vs),map var ds) >: toPredType (isCon x) t
  
  toPredType False = id
  toPredType True  = liftCon
  
  liftCon x = funT . map tPred . flatFunT $ x
  
  flatFunT t =
    case isFunT t of
      Just (t1,t2) -> t1:flatFunT t2
      _ -> [t]
  
  pfresh = do t <- fresh
  	    addprop t
  	    return t
  
  addprop t = addkinst (t:>:kprop)
  
  {-+
  Predicate definition can not use explicit recursion. The Gfp & Lfp operators
  have to be used instead.
  -}
  checkPredicateRec ds =
      unless (null recpreds) $ 
        declContext recpreds $
          fail "Recursive predicates"
    where
      recpreds = [pred|(pred,_)<-g,pred `elem` reachable' g [pred]]
      g = [(i,free) | Just d@(HsPropDecl {})<-map propstruct ds,
  	            let free=freeValueNames d,
  	            i<-definedValueNames d]
  