{-

Open Source Fixedpoint Model-Checker version 2009c

(C) Copyright IBM Corp. 2009
(C) Copyright ETH Zurich (Swiss Federal Institute of Technology) 2003,2007

All Rights Reserved.

-}

module Translator where
import Ast
import Msg
import MsgPat
import Data.List
import Data.Maybe
import AnBOnP

--------- Facts, Rules, and the Translation State ---------------

data Fact = State Ident [MsgPat]
     	  | FPState Ident [Msg]
          | Iknows Msg
	  | Fact Ident [Msg]
	  deriving (Eq,Show)

type Rule = ([Fact],Eqs,[Ident],[Fact])
lhs (l,_,_) = l
rhs (_,_,r) = r
frv (_,f,_) = f

identsF :: Fact -> [Ident]
identsF (State _ msgs) = error "identsf of state"
identsF (FPState _ msgs) = nub (concatMap idents msgs)
identsF (Iknows msg) = nub (idents msg)
identsF (Fact _ msgs) = nub (concatMap idents msgs)

identsFL m = nub (concatMap identsF m)

type Rule' = (Rule,ProtocolState,ProtocolState)

type Eqs = [(Msg,Msg)]

type Role = (Ident,[Rule'])

data ProtocolTranslationState = PTS { protocol :: Protocol,
     			      	      options  :: AnBOptsAndPars,
				      roles    :: [Role],
				      rules    :: [Rule],
				      initial  :: String }

mkPTS :: Protocol -> AnBOptsAndPars -> ProtocolTranslationState
mkPTS protocol options = PTS { protocol = protocol, options = options, roles=[], rules=[],initial="" }
				       

---- Translation Stage 1: Creating Rules 
----------------------------------------

createRules :: ProtocolTranslationState -> ProtocolTranslationState
createRules pts =
  let (p@(_,types,knowledge,abstractions,actions,goals)) = protocol pts
      frMsg = fresh p 
      pks = concatMap snd ((filter (\ (x,y) -> x==PublicKey)) types)
      roles = 
       (snd . head . 
        (filter (\ x -> case (fst x) of Agent _ _ ->True;_ -> False))) 
	types 
  in pts {rules = manageRules 0 frMsg (\x -> initialState (lookupL x knowledge)) actions pks}

manageRules step fresh states actions pks =
        --- about step number (=list index+1)
        --- initially 0: there is no incoming message
        --- finally (length actions): there is no outgoing message
	let ((a,ctin,b,min,minp,minzk),(b',ctout,c,mout,_,_))
             = if step == (length actions) 
	       then (toJust (Just (last actions)),toJust Nothing) else 
	       if step == 0
	       then (toJust Nothing, toJust (Just (head actions))) else
	       (toJust (Just (actions !! (step-1))), 
	        toJust (Just (actions !! step)))
            thisfresh = case mout of 
			Nothing -> []
			Just (_,_,_,mout',_) -> 
			  intersect fresh (idents mout')
            freshpks = intersect pks thisfresh
            ub = if b==Nothing 
	         then if b'==Nothing 
		      then error ("Undefined Receiver in step"++(show step))
		      else fromJust b'
                 else if b'==Nothing 
		      then fromJust b
		      else if b/=b' 
			   then error ("Receiver: "++(show b)++
				       " and Sender/NextMsg is "++(show b'))
			   else fromJust b
	    (rule,state')=createRule thisfresh freshpks ub (states ub) min mout in
  	   rule:
	   (if step == (length actions) then [] else
	    manageRules (step+1) (fresh \\ thisfresh) 
	    (\x -> if x==ub then state' else states x) actions pks)

createRule fresh freshpks role state incomin outgoin = 
       let (state1,msg1) = 
             case incomin of
             Nothing -> (state,Atom "i")
	     Just (sender,ct,receiver,recm,Nothing) -> 
              let st = (receiveMsg recm state) in
	      (st,chtrafo False sender ct receiver (snd (last st)))
	     Just (sender,ct,receiver,recm,Just recmp) -> 
              let st = (receiveMsgPat (recm,recmp) state) in
	      (st,chtrafo False sender ct receiver (snd (last st)))
           (state2,msg2) = 
             case outgoin of
             Nothing -> (state1,Atom "i")
	     Just (sender,ct,receiver,sndm,_) ->
              let state1'=peertrafo receiver msg1 state1
		  st = sendMsg sndm (state1'++(map (\x -> (Atom x,Atom x)) fresh)++(map (\x -> (Comp Inv [Atom x],Comp Inv [Atom x])) freshpks))
	      in (st,chtrafo True sender ct receiver (snd (last st)))
       in  
       (((State role 
          (((nubBy eqSnd) . (\x -> (Atom role, Atom role):(x++[(Atom "SID",Atom "SID")])) . 
	    (take (length state))) state1)):
         (if msg1==(Atom "i") then [] else [Iknows msg1]),[],
	 fresh,
	 (State role
          (((nubBy eqSnd)  . (\x -> (Atom role,Atom role):(x++[(Atom "SID",Atom "SID")]))) state2)):
	 (if msg2==(Atom "i") then [] else [Iknows msg2])),state2)

eqSnd (_,a) (_,b) = a==b

fresh :: Protocol -> [Ident]
fresh (_,_,knowl,_,actions,_) =
  let longterm = concatMap ((concatMap idents) . snd) knowl
      all = concatMap (\ (_,m,_,_) -> idents m) actions
            --- here we don't count sender/receiver names (can't be fresh)
  in  nub ((nub all) \\ (nub longterm))


toJust :: Maybe Action -> 
	  (Maybe Ident,ChannelType,Maybe Ident,
	   Maybe(Peer,ChannelType,Peer,Msg,Maybe Msg),
	   Maybe Msg,Maybe Msg)
toJust Nothing = (Nothing,Secure,Nothing,Nothing,Nothing,Nothing)
toJust (Just ((sp@(a,_,_),ct,rp@(b,_,_)),m,mp,zk)) = 
       (Just a,Secure,Just b,Just (sp,ct,rp,m,mp),mp,zk)

---------- Channel Transformation ---------

chtrafo :: Bool -> Peer -> ChannelType -> Peer -> Msg -> Msg

chtrafo isSender (sender,psender,Just _) ct (receiver,preceiver,_) msg = 
  error "Not yet implemented: custom pseudos in protocol."
chtrafo isSender (sender,psender,_) ct (receiver,preceiver,Just _) msg = 
  error "Not yet implemented: custom pseudos in protocol."

chtrafo isSender (sp@(sender,psender,Nothing)) ct (rp@(receiver,preceiver,Nothing)) msg = 
  case ct of
   Insecure ->
    if psender then
      let id = if isSender then peerToMsgKnwn sp
	                   else peerToMsgUKnwn sp in
        (Comp Cat 
	 [id,msg])
    else
	 msg
   Authentic -> 
    if psender then
      let id = if isSender then peerToMsgKnwn sp
	                   else peerToMsgUKnwn sp in
        (Comp Cat 
	 [id,
	  Comp Crypt 
	  [Comp Inv
	   [Comp Apply 
	    [Atom "authChCr",id]],
           msg]])
    else
     (Comp Crypt [Comp Inv [Comp Apply [Atom "authChCr",Atom sender]],msg])
   Confidential ->
    if preceiver then 
      let id = if isSender then peerToMsgUKnwn rp
			   else peerToMsgKnwn rp in
        (Comp Crypt [Comp Apply [Atom "confChCr",id],msg])

    else
    (Comp Crypt [Comp Apply [Atom "confChCr",Atom receiver],msg])
   Secure ->
    if psender then 
      let ids = if isSender then peerToMsgKnwn sp
	                    else peerToMsgUKnwn sp in
      if preceiver then error "Secure channel with mutual pseudonymity..."
      else 
       Comp Cat
       [ids,
        Comp Scrypt 
        [Comp Apply 
	 [Atom "secChCr",
	  Comp Cat
	  [ids,
	   Atom receiver]],
	 msg]]
    else if preceiver then
      let idr = if isSender then peerToMsgUKnwn rp
			    else peerToMsgKnwn rp in
        Comp Scrypt 
        [Comp Apply 
	 [Atom "secChCr",
	  Comp Cat 
	  [Atom sender,
	   idr]],
	 msg]
    else
    Comp Scrypt 
    [Comp Apply [Atom "secChCr",Comp Cat [Atom sender,Atom receiver]],
     msg]

peertrafo :: Peer -> Msg -> ProtocolState -> ProtocolState
peertrafo (receiver,ispseudo,Just _) inmsg protostate = 
  error "Not yet implemented: alternative pseudos in protocol."
peertrafo (receiver,ispseudo,Nothing) inmsg protostate =  
  let pseus = (nub . (filter (isPrefixOf "Pseudonym")) .
	       idents) inmsg in
  if (length pseus)>1 then error ("Too much pseudo in inmsgs="++
				  (show inmsg)++" namely "++(show pseus))
  else if (length pseus)==0 then 
	  if ispseudo then error ("Contact pseudo!"++(show inmsg)) else
	  protostate
       else
	let [pseu]=pseus in
	if (Atom pseu) `elem` (map snd protostate) then protostate
	else protostate++[(Atom pseu,Atom pseu)]

peerToMsgKnwn :: Peer -> Msg
peerToMsgKnwn (a,False,_) = Atom a
peerToMsgKnwn (a,True,Nothing)  = Comp Apply [Atom "pseudonym",Atom a]
peerToMsgKnwn (a,True,Just _)  = error "N/A"
peerToMsgUKnwn :: Peer -> Msg
peerToMsgUKnwn (a,False,_) = Atom a
peerToMsgUKnwn (a,True,Just _)  = error "N/A"
peerToMsgUKnwn (a,True,Nothing)  = Atom ("Pseudonym"++a)


lookupL :: Ident -> Knowledge -> [Msg]
lookupL x [] = error ("Initial knowledge of role "++(show x)++" not specified.")
lookupL x ((y,k):ys) = if x==y then k else lookupL x ys


----- Translation Stage 2: add steps
------------------------------------

rulesAddSteps :: ProtocolTranslationState -> ProtocolTranslationState
rulesAddSteps pts = 
  let counter inc (State role (player:ids)) (facts,db) = 
       ((State role (player:(((\x -> (x,x)) . Atom . show) (db role)):ids)):facts,
        \x -> if x==role then (db role)+inc else db x)
      counter inc fact (facts,db) = (fact:facts,db)
      adds [] db = []
      adds ((l,[],f,r):xs) db =
       let (l',db') = foldr (counter 1) ([],db) l
           (r',db'') = foldr (counter 0) ([],db') r
       in (l',[],f,r'):(adds xs db'')
  in pts {rules = adds (rules pts) (\x -> 0)}

---- Translation Stage 3: adding goals
---------------------------------------

addGoals :: ProtocolTranslationState -> ProtocolTranslationState
addGoals pts =
 let rs = rules pts
 in 
  if lversion then pts else
  let (_,_,_,_,_,goals) = protocol pts
      folder (ChGoal ((speer@(sender,_,_)), channeltype, (rpeer@(receiver,_,_))) msg) rs =
        let (i,pattern) = findFirstKnow rs sender msg 1
	    pre = take (i-1) rs
	    post = drop (i-1) rs
	    (l,[],f,r) = head post
	    newfacts = 
	      (if channeltype==Secure || channeltype==Confidential 
	      	  || channeltype==FreshSecure
	       then [Fact "secret" [pattern,
				    goalpeer False
				        rpeer (head post)]]
	       else [])++
	      (if channeltype==Secure || channeltype==Authentic 
	      || channeltype==FreshAuthentic || channeltype==FreshSecure
	       then [Fact "witness" 
		     [goalpeer True -- peerToMsgKnwn 
		      speer (head post),
		      goalpeer False -- peerToMsgUKnwn 
		      rpeer (head post),
		      mkPurpose (Comp Cat [goalpeer True rpeer (head post2),
                                                          goalpeer False speer (head post2),
                                                          msg]),pattern]]
               else [])
	    rs' = pre++[(l,[],f,newfacts++r)]++(tail post)
	    (i2,pat) = findLastKnow rs' receiver msg 1 Nothing
	    pre2 = take (i2-1) rs'
	    post2 = drop (i2-1) rs'
	    (l2,[],f2,r2) = head post2
	    newfacts' =
	      (if channeltype==FreshSecure || channeltype==FreshAuthentic
	       then [Fact "request" [goalpeer True -- peerToMsgKnwn 
				     rpeer (head post2),
				     goalpeer False -- peerToMsgUKnwn 
				     speer (head post2),
				     mkPurpose (Comp Cat [goalpeer True rpeer (head post2),
                                                          goalpeer False speer (head post2),
                                                          msg]),pat,Atom "SID"]]
               else 
	       if channeltype==Secure || channeltype==Authentic
	       then [Fact "wrequest" [goalpeer True -- peerToMsgKnwn 
				      rpeer (head post2),
				      goalpeer False -- peerToMsgUKnwn 
				      speer (head post2),
				      mkPurpose (Comp Cat [goalpeer True rpeer (head post2),
                                                          goalpeer False speer (head post2),
                                                          msg]),pat]]
		else [])
	    rs2' = pre2++[(l2,[],f2,newfacts'++r2)]++(tail post2)
	in rs2' 
      folder (Secret msg peers) rs =
        foldr (folder2 (Secret msg peers)) rs peers
      folder2 (Secret msg (peers::[Peer])) (peer@(pee,_,_)::Peer) rs =
        let (i,pattern) = findLastKnow rs pee msg 1 Nothing
	    pre = take (i-1) rs
	    post = drop (i-1) rs
	    (l,[],f,r) = head post
            secrecyset = Comp Apply [Atom "secrecyset", Comp Cat [goalpeer False peer (head post), Atom "SID", mkPurpose msg]]
	    newfacts = 
	      ((Fact "secrets" [pattern, secrecyset]): --- was: Atom ("secrecyset(SID)")]):
	       [Fact "contains" [secrecyset, -- was: Atom "secrecyset(SID)",
	        goalpeer False p (head post)]
	       | p <- peers])
	    rs' = pre++[(l,[],f,newfacts++r)]++(tail post)
	in rs'
  in pts {rules = foldr folder rs goals}

mkPurpose :: Msg -> Msg
mkPurpose m = Comp Apply [Atom "typePurpose", let (Atom s)= mkname m in (Atom $ "p"++(tail s))]
---mkPurpose (Atom m) = Comp Apply [Atom "typePurpose", Atom ("purpose"++m)]
---mkPurpose m = Comp Apply [Atom "typePurpose", Atom "purpose"]
  


goalpeer :: Bool -> Peer -> Rule -> Msg
goalpeer isKnown (a,False,Nothing) (_,[],_,r) = Atom a
goalpeer isKnown (a,True,Nothing) _ = 
	 if isKnown then (Comp Apply [Atom "pseudonym",Atom a])
	 else Atom ("Pseudonym"++a)
goalpeer isKnown (a,True,Just msg) (_,_,_,r) = 
  let (State role msgs) = head r in
  if msg `elem` (map snd msgs) then msg
  else let msg' = mkname msg
       in if msg' `elem` (map snd msgs) then msg'
	  else error "Pseudo not found!"



getKnow :: [Fact] -> Ident -> Maybe [MsgPat]
getKnow [] ident = Nothing
getKnow ((State player know):facts) ident =
  if (player==ident) then Just know
  else getKnow facts ident
getKnow (f:fs) ident = getKnow fs ident

findFirstKnow :: [Rule] -> Ident -> Msg -> Int -> (Int,Msg)
findFirstKnow [] ident msg i = 
  error ((ppMsg Pretty msg)++" is never known by "++(ppId ident))
findFirstKnow ((l,[],f,r):rules) ident msg i = 
  case getKnow r ident of
  Nothing -> findFirstKnow rules ident msg (i+1)
  Just know -> maybe (findFirstKnow rules ident msg (i+1)) (\x->(i,x))(synthesisPattern know msg) 

findLastKnow :: [Rule] -> Ident -> Msg -> Int -> Maybe (Int,Msg) -> (Int,Msg)
findLastKnow [] ident msg i Nothing = 
  error ((ppMsg Pretty msg)++" is never known by "++(ppId ident))
findLastKnow [] ident msg i (Just (n,pat))=(n,pat)
findLastKnow ((l,[],f,r):rules) ident msg i maybe_n_pat = 
  case getKnow r ident of
  Nothing -> findLastKnow rules ident msg (i+1) maybe_n_pat
  Just know -> 
    maybe (findLastKnow rules ident msg (i+1) maybe_n_pat)
    	  (\ x -> findLastKnow rules ident msg (i+1) (Just (i,x)))
	  (synthesisPattern know msg)

subtermList :: Msg -> [Msg] -> Bool
subtermList m = any (subterm m)

subterm :: Msg -> Msg -> Bool
subterm m1 m2 =
  if m1==m2 then True
  else case m2 of
        Atom _ -> False
	Comp f xs -> subtermList m1 xs






--- Stage 4: Adding the initial state
-------------------------------------

addInit :: ProtocolTranslationState -> ProtocolTranslationState
addInit pts=
  let (_,typdec,knowledge,_,_,_)=protocol pts
      args = options pts
      absInit = getinitials (rules pts) knowledge
      jn = numSess args
      n::Int
      n = if (jn==Nothing) 
	  then error "Unbounded sessions currently not supported." 
	  else fromJust jn
      (facts0,honest,aglili,agents0,ik0) = instantiate n absInit
      facts = facts0++
              ik0++(getCrypto agents0)
      agents = ((++) ["i","A","B"]) agents0
  in
  pts { 
   initial = 
    (if typed args then 
       ("section types:\n"++
        (ppIdList agents)++":agent\n"++
     	(printTypes typdec)++"\n")
     else "")++
    "section inits:\n"++
    " initial_state init1 :=\n"++
    (ppFactList IF facts)++
    (concatMap (\x -> " & "++(ppId x)++"/=i") honest)++
---    (concatMap (\ (x,y) -> " & "++(ppId x)++"/="++(ppId y)) [(x,y) | x<-agents0, y<-agents0, x/=y])++
---    (error $ (show aglili) ++ (show (concatMap (\ (x,y) -> " & "++(ppId x)++"/="++(ppId y)) [(x,y) | l<-aglili, x<-l, y<-l, x/=y])))++ 
    "\n\n"++
    "section rules:\n"}
  
getCrypto :: [Ident]->[Fact]
getCrypto agents =
  map Iknows 
  ((Atom "confChCr"):(Atom "authChCr"):
   (Comp Inv [Comp Apply [Atom "authChCr",Atom "i"]]):
   (Comp Inv [Comp Apply [Atom "confChCr",Atom "i"]]):
   [Comp Apply [Atom "secChCr",Comp Cat [Atom "i",Atom other]]
   | other <- agents\\["i"]]++
   [Comp Apply [Atom "secChCr",Comp Cat [Atom other,Atom "i"]]
   | other <- agents\\["i"]]++
   [Comp Apply [Atom "secChCr",Comp Cat [Atom "i",Comp Apply [Atom "pseudonym",Comp Cat [Atom other]]]]
   | other <- agents\\["i"]]++
   [Comp Apply [Atom "secChCr",Comp Cat [Comp Apply [Atom "pseudonym",Comp Cat [Atom other]],Atom "i"]]
   | other <- agents\\["i"]])


printTypes :: Types -> String
printTypes = 
 let f (Agent _ _,ids) = (ppIdList ids)++":agent\n"
     f (Number,ids) = (ppIdList ids)++":text\n"
     f (PublicKey,ids) =  (ppIdList ids)++":public_key\n"
     f (SymmetricKey,ids) =  (ppIdList ids)++":symmetric_key\n"
     f (Function,ids) = (ppIdList ids)++":function\n"
     f (Untyped,ids) = ""
 in concatMap f 

getIK0 :: [Fact] -> [Fact]
getIK0 states =
   let f (Atom a) = 
	if (isVariable a) && (a/="SID")
	then Atom "i"
	else Atom a
       f (Comp o as) = Comp o (map f as)
   in  ((map (Iknows . f)) . 
        nub . 
	(concatMap getMsgs) . 
        (filter (\ (State role msgs) -> isVariable role)))
       states


getMsgs :: Fact -> [Msg]
getMsgs (State role msgs) = map snd msgs 
getMsgs (FPState role msgs) =  msgs 
getMsgs (Iknows msg) = [msg]
getMsgs (Fact _ msgs) = msgs


getinitials :: [Rule] -> Knowledge -> [Fact]
getinitials rules =
  map (\ (x,y) -> State x (map (\z-> (z,z)) ((Atom x):(Atom "0"):(((analysis y)\\[Atom x])++[Atom "SID"]))))

instantiate :: Int -> [Fact] -> ([Fact],[Ident],[[Ident]],[Ident],[Fact])
instantiate n states = 
  let nstates = zip states [1..]
      inst0 i n (State role msgs) = 
        let f (Atom a) = 
	      if (isVariable a) && (a/="SID")
	      then Atom (a++"_"++(show i)++"_"++(show n))
	      else Atom a
	    f (Comp o as) = Comp o (map f as)
	    varcheck =  (nub (concatMap vars (map snd msgs))) \\ (nub (filter isVariable (map (\ (Atom x) -> x) (filter isAtom (map snd msgs)))))
        in if varcheck==[]
	   then insSid n (State role (map (\ (x,y) -> (f x,f y))msgs))
	   else error 
	   	("Currently not supported:\n "++
		 " role "++role++" does not know "++(show varcheck)++"\n"++
		 " but functions of "++(show varcheck)++"\n.")
      ik0 i n (State role msgs) = 
        let f (Atom a) = 
	      if (isVariable a) && (a/="SID")
	      then if a==role then (Atom "i")
	      	   else Atom (a++"_"++(show i)++"_"++(show n))
	      else Atom a
	    f (Comp o as) = Comp o (map f as)
        in if isVariable role 
	   then map (Iknows . f) (map snd msgs)
	   else []
      ik = nub (concat [ik0 i k f|  k<-[1..n], (f,i)<-nstates])
      insSid i (State r m) =
        State r ((init m)++(map (\x->(x,x)) [Atom (show (2*i))]))
      instfacts = [inst0 i k f|  k<-[1..n], (f,i)<-nstates]
      aglili =  [ nub [name++"_"++(show ( i))++"_"++(show k)  | k<-[1..n]]
		   | (State r msgs,i)<-nstates,
		     name <- ((filter ((/=) "SID")).
		                     (filter isVariable).
				     (concatMap idents).
				     (concatMap getMsgs)) [(State r msgs)],
		      isVariable name]
      honestNames = 
               nub 
                    [ name++"_"++(show ( i))++"_"++(show k) 
		    | (State _ ((_,Atom name):_),i)<-nstates, k<-[1..n],
		      isVariable name]
      allNames = (nub.
		  (filter ((/=) "SID")).
		  (filter isVariable).
	          (concatMap idents).
		  (concatMap getMsgs)) instfacts
  in (instfacts,
      honestNames,
      aglili,
      allNames,
      ik )

initstr protocol args= 
  "section types:\n"++
  "\n"++
  "A,B,B2,a,b,i: agent\n"++
  "\n"++
  "section inits:\n"++
  " initial_state init1 :=\n"++
  " state_rA(A,0,B,inv(apply(pk,A)),pk,1).\n"++
  " state_rB(B2,0,inv(apply(pk,B2)),pk,  1).\n"++
  " iknows(a).iknows(b).iknows(i).iknows(pk).iknows(inv(apply(pk,i)))\n"++
  " & A/=B & A/=i & B2 /=i\n\n"++
  "section rules:\n"

--- Stage 5: printing the rules
--------------------------------

ruleList :: ProtocolTranslationState -> String
ruleList pts =
  ruleListIF (initial pts, rules pts)


ruleListIF :: (String,[Rule]) -> String
ruleListIF (init,rules) =
 let ruleIF [] n = ""
     ruleIF (x:xs) n = "step trans"++(show n)++":=\n"++
		       (ppRule IF x)++"\n"++(ruleIF xs (n+1))
 in init ++ (ruleIF rules 0)




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

endstr = 
  "section attack_states:\n"++
  "  attack_state secrecy :=\n"++
  "    secret(M,A).\n"++
  "    iknows(M)\n"++
  "    & A/=i\n\n"++
  "  attack_state weak_auth :=\n"++
  "    request(A,B,PURP,MSG,SID)\n"++
  "    & not(witness(B,A,PURP,MSG))\n"++
  "    & A/=B & B/=i\n\n"++
  "  attack_state weak_auth :=\n"++
  "    wrequest(A,B,PURP,MSG)\n"++
  "    & not(witness(B,A,PURP,MSG))\n"++
  "    & B/=i\n\n"++
  "  attack_state strong_auth :=\n"++
  "    request(A,B,PURP,MSG,SID).\n"++
  "    request(A,B,PURP,MSG,SID2)\n"++
  "    & SID/=SID2\n"++
  "    & B/=i\n"++
  "  attack_state secrets :=\n"++
  "    secrets(M,SET).\n"++
  "    iknows(M)\n"++
  "    & not(contains(SET,i))"
---------------------------------


-------- 

isntIknowsFunction (Iknows msg) = isntFunction msg
isntIknowsFunction _ = True

isIknows (Iknows _) = True
isIknows _ = False

ppFact Isa (State role msgs) = error "State-Fact in ISA mode" 
ppFact Isa (FPState role msgs) = "State (r"++(ppId role)++",["++(ppMsgList Isa (filter isntFunction msgs))++"])"

ppFact outf (State role msgs) = "state_r"++(ppId role)++"("++(ppMsgList outf (map snd msgs))++")"
ppFact outf (FPState role msgs) = "state_r"++(ppId role)++"("++(ppMsgList outf msgs)++")"
ppFact outf (Iknows msg) = "iknows("++(ppMsg outf msg)++")"
ppFact outf (Fact i m) = (ppId i)++"("++(ppMsgList outf m)++")"

ppFactList outf = (ppXList (ppFact outf) ".\n") . (filter isntIknowsFunction)

ppEq outf (x,y) = (ppMsg outf x)++"/="++(ppMsg outf y)

ppRule Isa (l,eq,f,r) 
 = (ppXList (ppFact Isa) ";\n" (filter isntIknowsFunction l))++"\n"++
   (if eq==[] then "" else " | "++(ppXList (ppEq Isa) ";\n" eq))++"\n"++ 
   (if f==[] then "=>" else error "fresh variable remaining")++"\n"++
   (ppXList (ppFact Isa) ";\n" (filter isntIknowsFunction r))++"\n"

ppRule outf (l,[],f,r) = (ppFactList outf l)++"\n"++
                     (if f==[] then "=>" else "=[exists "++(ppIdList f)++"]=>")++"\n"++
		     (ppFactList outf r)++"\n"

ppRuleList Isa list =
  let ppRL Isa (x:xs) c = "step rule_"++(show c)++":\n"++(ppRule Isa x)++"\n"++(ppRL Isa xs (c+1))
      ppRL Isa [] _ = "" 
  in ppRL Isa list 0

ppRuleList outf list = ppXList (ppRule outf) "\n" list

ppInit str ot list =
  let ppFP0 ot (x:xs) c = str++"_"++(show c)++": "++(ppFact ot x)++";\n"++(ppFP0 ot xs (c+1))
      ppFP0 ot [] _ = "" 
  in ppFP0 ot (filter isntIknowsFunction list) 0

ppFP str ot list =
  let ppFP0 ot (x:xs) c = str++"_"++(show c)++": "++(ppFact ot x)++";\n"++(ppFP0 ot xs (c+1))
      ppFP0 ot [] _ = "" 
  in ppFP0 ot list 0

subfact :: Substitution -> Fact -> Fact
subfact sub (FPState r msgs) = FPState r (map sub msgs)
subfact sub (State r msgs) = State r (map (\ (x,y)-> (sub x,sub y)) msgs)
subfact sub (Iknows msg) = Iknows (sub msg)
subfact sub (Fact ident msgs) = Fact ident (map sub msgs)

subrule sub (l,eq,f,r) = (map (subfact sub) l, 
	    	       	  map (\ (x,y) -> (sub x,sub y)) eq,
			  f, 
			  map (subfact sub) r)
