-- Generates rules when loading protocols from S-Expressions.

-- Copyright (c) 2009 The MITRE Corporation
--
-- This program is free software: you can redistribute it and/or
-- modify it under the terms of the BSD License as published by the
-- University of California.

module CPSA.GenRules where

import qualified Data.List as L
-- import CPSA.Lib.SExpr
import CPSA.Signature (Sig)
import CPSA.Algebra
import CPSA.Channel
import CPSA.Protocol
import CPSA.LoadFormulas

{--
import System.IO.Unsafe

z :: Show a => a -> b -> b
z x y = unsafePerformIO (print x >> return y)

zz :: Show a => a -> a
zz x = z x x

zb :: Show a => a -> Bool -> Bool
zb a False = z a False
zb _ b = b

zn :: Show a => a -> Maybe b -> Maybe b
zn x Nothing = z x Nothing
zn _ y = y

zf :: Show a => a -> Bool -> Bool
zf x False = z x False
zf _ y = y

zt :: Show a => a -> Bool -> Bool
zt x True = z x True
zt _ y = y

zl :: Show a => [a] -> [a]
zl a = z (length a) a

--}

-- Protocol Rules

type Conjunction = [AForm]

conjunctionOfConj :: Conj -> Conjunction
conjunctionOfConj = map snd

-- a Renamer is a function that will replace variables within the
-- AForm that should be regarded as universally bound with the
-- variable that will be chosen for the universal quantifier.

-- The loader will in fact read these variables as occurrences of the
-- role parameters
type Renamer = AForm -> AForm

type Conjunctor = Conjunction -> Renamer -> Conjunction
-- Function which, given Conjunction and a fn to plug in new
-- variables, plugs them in to yield a conjunction

-- The loader ensures that when an existential formula's body is
-- loaded, anything that can be read as a local, existentially bound
-- variable will be.  Since these are generated immediately before the
-- body is read, there can be no occurrences of the role parameters
-- present in the body.  Likewise, there can be no occurrences of the
-- local, existentially bound variables outside this body.

-- Hence a renamer for the antecedent may be safely applied here,
-- without capturing variables that should be locally bound.

type Existor = Conjunctor

-- Used to say:   -- Function which, given new
                                        -- variables to bind
                                        -- existentially, plugs them
                                        -- in to yield a conjunctor

ruleOfClauses :: Sig -> Gen -> String ->
                 [Term] ->  -- VarListSpec ->
                 Conjunction ->
                 [([Term],Conjunction)] -> (Gen,Rule)
ruleOfClauses _ g rn fvs antecedent evarDisjuncts = -- sig is vacuous
    let (g', env, uvars) = renamerAndNewVars fvs g in
    let disjuncts =
            map
            (\(evars,c) -> (evars,
                            (map (instantiateAForm env) c)))
            evarDisjuncts in
    (g',
      (Rule { rlname = rn,
              rlgoal =
                  (Goal
                   { uvars = uvars,
                     antec = map (instantiateAForm env) antecedent,
                     consq = disjuncts,
                     concl = map snd disjuncts}),
              rlcomment = [] }))

applyToSoleEntry :: (a -> b) ->  String -> [a] -> b
applyToSoleEntry f _ [a] = f a
applyToSoleEntry _ s _ = error s

applyToThreeEntries :: (a -> a -> a -> b) -> String -> [a] -> b
applyToThreeEntries f _ [a1,a2,a3] = f a1 a2 a3
applyToThreeEntries _ s _ = error s

applyToStrandVarAndParams :: (a -> [a] -> b) -> [a] -> String -> b
applyToStrandVarAndParams _ [] s = error s
applyToStrandVarAndParams f (a : rest) _ = f a rest

-- foldM :: (Foldable t, Monad m) => (b -> a -> m b) -> b -> t a -> m b

neqRules :: Sig -> Gen -> (Gen, [Rule])
neqRules sig g =
    foldr
     (\sortName (g,rs) ->
          let (g', v) = newVar sig g "x" sortName in
          let (g'', r) =
                  (ruleOfClauses sig g' ("neqRl_" ++ sortName)
                   [v]
                   [(AFact "neq" [v,v])]
                   [])       -- false conclusion
          in
            (g'', r : rs))
     (g,[])
     ["indx", "strd", "mesg"]

transRls :: Sig -> Gen -> Role -> [(Int,Int)] -> (Gen, [Rule])
transRls sig g rl =
    L.foldl
     (\(g, rs) pair ->
          let (g', r) = f g pair in
          (g', r : rs))
     (g, [])
     where
       f g (i,j) =
           let (g', z) = newVar sig g "z" "strd" in
           ruleOfClauses sig g' ("trRl_" ++ (rname rl) ++ "-at-" ++ (show i))
             [z]
             [(Length rl z (indxOfInt (j+1)))]
             [                  --one disjunct
              ([],              -- no existentially bound vars
               [(Trans (z, (indxOfInt i)))] -- one conjunct
               )]

lastRecvInCS :: Role -> Int -> Int -> Int
lastRecvInCS rl start end =
    loop start $ drop (start+1) $ rtrace rl
    -- i is always the index before the index of the first entry still
    -- in c.
    where
      loop i ((In (ChMsg ch _)) : c)
           | i < end && isLocn ch       = loop (i+1) c
           | otherwise                  = i
      loop i _                          = i

csRules :: Sig -> Gen -> Role -> [(Int,Int)] -> (Gen, [Rule])
csRules sig g rl =
    L.foldl
     (\(g, rs) (start,end) ->
          (let (g', csRules) = f g start end in
           (g', csRules ++ rs)))
     (g,[])
     where
       f g start end =
           let lastRecv = lastRecvInCS rl start end in
           let (g',rs) = foldr (\ind (g,soFar) ->
                                    let (g',r) = causeRule g rl start ind in
                                    (g', (r : soFar)))
                         (g,[])
                         [start+1..lastRecv] in
           foldr (\ind (g,soFar) ->
                      let (g',r) = effectRule g rl end ind in
                      (g', (r : soFar)))
             (g',rs)
             [lastRecv+1..end-1]

       causeRule g rl start ind =
           let (g',z) = newVar sig g "z" "strd" in
           let (g'', z1) = newVar sig g' "z1" "strd" in
           let (g''', i) = newVar sig g'' "i" "indx" in

           ruleOfClauses sig g'''
             ("cau-" ++ (rname rl) ++ "-" ++ (show ind))
             [z, z1, i]
             [(Length rl z (indxOfInt (ind+1))),
              (Prec (z1,i) (z, (indxOfInt ind)))]

             [([],              -- either z = z1
               [Equals z z1]),
              ([],              -- or z1's i node comes before start
                                -- of critical section
               [(Prec (z1,i) (z,(indxOfInt start)))])]

       effectRule g rl end ind =
           let (g',z) = newVar sig g "z" "strd" in
           let (g'', z1) = newVar sig g' "z1" "strd" in
           let (g''', i) = newVar sig g'' "i" "indx" in

           ruleOfClauses sig g'''
             ("eff-" ++ (rname rl) ++ "-" ++ (show ind))
             [z, z1, i]
             [(Length rl z (indxOfInt (ind+1))),
              (Prec (z, (indxOfInt ind)) (z1,i))]
             [([],              -- either z = z1
               [Equals z z1]),
              ([],              -- or z is long and z1's i node comes
                                -- after end of critical section
               [(Length rl z (indxOfInt (end+1))),
                (Prec (z, (indxOfInt end)) (z1,i))])]

data FoundAt = FoundAt Int
             | Missing Term

-- Return the smallest height in the trace of rl at which all of the
-- vars are found to have occurred, if found, or a missing var if no
-- such height.
varsUsedHeight :: Role -> [Term] -> FoundAt
varsUsedHeight rl vars =
    loop 0 vars
    where
      occ = flip firstOccurs rl -- return *index*
      loop i [] = FoundAt (1+i) -- convert to height
      loop i (v : rest) =
          case occ v of
            Nothing -> Missing v
            Just j -> loop (max i j) rest

boundVarNamesOfVarListSpec :: VarListSpec -> [String]
boundVarNamesOfVarListSpec [] = []
boundVarNamesOfVarListSpec ((_,names) : rest) =
    L.nub $ names ++ boundVarNamesOfVarListSpec rest

{--
freeVarsInExistential :: ([Term],Existor) -> [Term]
freeVarsInExistential (vars,c) =
    let bvns = map varName vars in
    concatMap
    (\a -> filter (not . (flip elem bvns) . varName)
           (aFreeVars [] a))
    (c [])

freeVarsInDisjunction :: [([Term],Existor)] -> [Term]
freeVarsInDisjunction vcs =
    L.nub
     (foldr (\vc acc -> (freeVarsInExistential vc) ++ acc)
      []
      vcs)
--}

freeVarsInConjLists :: [([Term], Conj)] -> [Term]
freeVarsInConjLists [] = []
freeVarsInConjLists ((vars,conj) : rest) =
    ((foldr (\(_,aForm) soFar -> aFreeVars soFar aForm)
                []
                conj)
     L.\\ vars)
    ++ (freeVarsInConjLists rest)

-- Take the subset of fvars that have a name shared with some member
-- of pvars
freeVarsSubsetByName :: [Term] -> [Term] -> [Term]
freeVarsSubsetByName fvars pvars =
    loop fvars []
    where
      pvarNames = map varName pvars
      loop [] soFar = reverse soFar
      loop (fv : rest) soFar
          | (varName fv) `elem` pvarNames =
              loop rest (fv : soFar)
          | otherwise =
              loop rest soFar

--   freeVarsNamedIn [] pvars = []
--   freeVarsNamedIn (fv : rest) pvars =
--       if (varName fv) `elem` (map varName pvars)
--       then fv : freeVarsNamedIn rest pvars
--       else freeVarsNamedIn rest pvars

conclHeight :: Role -> [([Term], Conj)] -> FoundAt
conclHeight _ [] = FoundAt 1
conclHeight rl (disj : rest) =
    case conclHeight rl rest of
      Missing v -> Missing v
      FoundAt j ->
          case varsUsedHeight rl $ freeVarsInConjLists [disj] of
            Missing v -> Missing v
            FoundAt i -> FoundAt (max i j)

renameApart :: String -> [Term] -> String
renameApart prefix vars =
    if not (prefix `elem` vns) then prefix
    else
        loop 0
    where
      vns = map varName vars
      loop :: Int -> String
      loop i =
          let candidate = prefix ++ "-" ++ (show i) in
          if not (candidate `elem` vns) then candidate
          else
              loop (i+1)

{-

Sig -> Gen -> String -> [Term] ->
Conjunction -> [([Term],Conjunction)] -> (Gen,Rule)

--}

ruleOfDisjAtHeight :: Sig -> Gen -> Role -> String -> [([Term],[AForm])] -> Int -> (Gen, Rule)
ruleOfDisjAtHeight sig g rl rulename disj ht =
    let fvs = fvsConsq disj in
    let rvs = L.filter (\t -> L.elem t (rvars rl)) fvs in
    let (g',z) = newVar sig g "z" "strd" in
    (ruleOfClauses
     sig g' rulename
     (fvs ++ [z])
     ((Length rl z (indxOfInt ht)) :
      (map
       (\v ->
            case firstOccurs v rl of
              Nothing -> errorWithMsg v " not found."
              Just i ->
                  if i < ht
                  then (Param rl v (i+1) z v)
                  else errorWithMsg v
                           (" introduced for " ++ (varName v) ++ " too high in role " ++
                            (rname rl) ++": " ++ (show i) ++
                            " not below " ++ (show ht) ++ "in " ++ rulename ++ "."))
       rvs))
     disj)
    where
      errorWithMsg v tail =
          error ("ruleOfDisjAtHeight:  Parameter " ++
                 (varName v) ++ tail)

genOneAssumeRl :: Sig -> Gen -> Role -> Int -> [([Term], Conj)] -> (Gen, Rule)
genOneAssumeRl sig g rl n disjs =
    case conclHeight rl disjs of
      Missing v -> error ("genOneAssumeRl:  Variable not in role " ++ (rname rl)
                         ++ ": " ++ (show v))
      FoundAt ht ->
          let disjuncts = map (\(vs,cs) -> (vs, map snd cs)) disjs in
          ruleOfDisjAtHeight
          sig g rl ("assume-" ++ (rname rl) ++ "-" ++ (show n))
              disjuncts
              ht

genAssumeRls :: Sig -> Gen -> Role -> [[([Term], Conj)]] -> (Gen, [Rule])
genAssumeRls sig g rl disjs =
    (g',rls)
    where
      (g',rls,_) =
          foldr (\ds (g, rs, n) ->
                       (let (g', new_rule) = genOneAssumeRl sig g rl n ds in
                        (g', new_rule : rs, n+1)))
               (g, [], (0 :: Int))
               disjs

genOneRelyGuarRl :: Sig -> Gen -> Role -> Int -> String -> [([Term], Conj)] -> (Gen, Rule)
genOneRelyGuarRl sig g rl ht kind disjs =
    case conclHeight rl disjs of
      Missing v -> error ("genOneRelyGuarRl:  Variable not in role " ++ (rname rl)
                         ++ ": " ++ (show (varName v)))
      FoundAt fndHt
          | fndHt <= ht ->
              let disjuncts = map (\(vs,cs) -> (vs, map snd cs)) disjs in
              (ruleOfDisjAtHeight
               sig g rl (kind ++ "-" ++ (rname rl) ++ "-" ++ (show ht))
               disjuncts ht)
        | otherwise -> error ("genOneRelyGuarRl:  Variable found above ht " ++ (show ht) ++
                              " in " ++ (rname rl))

genStateRls :: Sig -> Gen -> Role -> [Term] -> (Gen, [Rule])
genStateRls sig g rl ts =
    (g',rls)
    where
      (g',rls,_) =
          foldr (\t (g, rs, n) ->
                       (let (g', new_rule) = f g t n in
                        (g', new_rule : rs, n+1)))
               (g, [], (0 :: Int))
               ts

      -- vSpec t = ("strd", ["z"]) : varListSpecOfVars (varsInTerm t)

      f g t n =
          case varsUsedHeight rl (varsInTerm t) of
            Missing v ->
                error ("genStateRls:  In gen-st of "
                       ++ (rname rl) ++ ": no occurrence of "
                              ++ (show (displayTerm (addToContext emptyContext [t]) v)))
            FoundAt ht ->
                (ruleOfDisjAtHeight
                 sig g rl ("gen-st-" ++ (rname rl) ++ "-" ++ (show n))
                 [ -- One disjunct, no existentially bound variables
                   ([],
                   -- One conjunct:
                    [GenStV t])]
                 ht)

genFactRls :: Sig -> Gen -> Role -> [(String,[Term])] -> (Gen, [Rule])
genFactRls sig g rl predarglists =
        (g',rls)
    where
      (g',rls,_) =
          foldr (\(pred,args) (g, rs, n) ->
                     (let (g', new_rule) = f g pred args n in
                      (g', new_rule : rs, n+1)))
                    (g, [], (0 :: Int))
                    predarglists

      -- vSpec t = ("strd", ["z"]) : varListSpecOfVars (varsInTerm t)

      f g pred args n =
          case varsUsedHeight rl (concatMap varsInTerm args) of
            Missing v ->
                error ("genFactRls:  In fact of "
                       ++ (rname rl) ++ ": no occurrence of "
                              ++ (show $ varName v))
            FoundAt ht ->
                (ruleOfDisjAtHeight
                 sig g rl ("fact-" ++ (rname rl) ++ "-" ++ pred ++ (show n))
                 [ -- One disjunct, no existentially bound variables
                   ([],
                   -- One conjunct:
                    [AFact pred args])]
                 ht)

      {--
    (g',rls)
    where
      (g',rls,_) =
          foldr (\(pred,args) (g, rs, n) ->
                       (let (g', new_rule) = f g pred args n in
                        (g', new_rule : rs, n+1)))
               (g, [], (0 :: Integer))
               predarglists

      vSpec args = ("strd", ["z"]) : varListSpecOfVars (varsInArgs args)

      varsInArgs = concatMap varsInTerm

      f g pred args n =
          case varsUsedHeight rl (varsInArgs args) of
            Missing v -> error ("genFactRls:  Unbound variable " ++ (show v)
                               ++ " in fact of " ++ (rname rl) ++ ": "
                               ++ pred ++ (show args))
            FoundAt ht ->
                ruleOfClauses sig g
                  ("fact-" ++ (rname rl) ++ "-" ++ pred ++ (show n))
                  (vSpec args)
                  (\vars ->
                       applyToStrandVarAndParams
                       (\z pvars ->
                            (Length rl z (indxOfInt ht))
                            : (map
                               (\v ->
                                    case paramOfName (varName v) rl of
                                      Nothing -> error ("genFactRls:  Parameter " ++
                                                        (varName v) ++ " not found.")
                                      Just p ->
                                          case firstOccurs p rl of
                                            Nothing -> error ("genFactRls:  Parameter " ++
                                                              (varName v) ++ " not found.")
                                            Just i -> (Param rl p (i+1) z v))
                              pvars))
                       vars
                       "genFactRls:  vars not strand+params?")
                  [([],
                    (\_ vars ->
                         applyToStrandVarAndParams
                         (\_ pvars ->
                              case envsRoleParams rl g [] pvars of
                                [(_,e)] -> [AFact pred (map (instantiate e) args)]
                                _ -> error "genFactRls:  Non-unary matching not implemented")
                         vars
                         "genFactRls:  vars not strand+params?"))]
--}

theVacuousRule :: Rule
theVacuousRule =
    (Rule { rlname = "vacuity",
            rlgoal = Goal {uvars =  [],
                           antec = [],
                           consq = [([], [])], -- no bvs, no conjuncts
                           concl = [[]]},
            rlcomment = [] })

scissorsRule :: Sig -> Gen -> (Gen, Rule)
scissorsRule sig g =
    case sortedVarsOfNames sig g "strd" ["z0","z1","z2"] of
      (g, [z0,z1,z2]) ->
          case sortedVarsOfNames sig g "indx" ["i0","i1","i2"] of
            (g, [i0,i1,i2]) ->
                (g, (Rule { rlname = "scissorsRule",
                        rlgoal =
                            Goal
                            {uvars = [z0,z1,z2,i0,i1,i2],
                             antec = [ -- useful for debugging:
                                       -- (AFact "no-state-split" []),
                                       (Trans (z0,i0)), (Trans (z1,i1)), (Trans (z2,i2)),
                                       (LeadsTo (z0,i0) (z1,i1)), (LeadsTo (z0,i0) (z2,i2)) ],
                             consq = [([],                -- no bvs
                                       [(Equals z1 z2),   -- two eqns
                                        (Equals i1 i2)])],
                             concl = [[(Equals z1 z2),   -- two eqns
                                       (Equals i1 i2)]]},
                        rlcomment = [] }))
            (g, _) -> (g, theVacuousRule)
      (g, _) -> (g, theVacuousRule)

shearsRule :: Sig -> Gen -> (Gen, Rule)
shearsRule sig g =
    case sortedVarsOfNames sig g "strd" ["z0","z1","z2"] of
      (g, [z0,z1,z2]) ->
          case sortedVarsOfNames sig g "indx" ["i0","i1","i2"] of
            (g, [i0,i1,i2]) ->
                (g, (Rule { rlname = "shearsRule",
                        rlgoal =
                            Goal
                            {uvars = [z0,z1,z2,i0,i1,i2],
                             antec = [ -- useful for debugging:
                                       -- (AFact "no-state-split" []),
                                       (Trans (z0,i0)), (Trans (z1,i1)), (Trans (z2,i2)),
                                       (LeadsTo (z0,i0) (z1,i1)), (SameLocn (z0,i0) (z2,i2)),
                                       (Prec (z0,i0) (z2,i2)) ],
                             consq = [([],                -- no bvs
                                       [(Equals z1 z2),   -- two eqns
                                        (Equals i1 i2)]),
                                     ([],                -- no bvs
                                      -- (z1,i1) precedes (z2,i2)
                                       [(Prec (z1, i1) (z2, i2))])],
                             concl = [[(Equals z1 z2),   -- two eqns
                                        (Equals i1 i2)],
                                      -- (z1,i1) precedes (z2,i2)
                                       [(Prec (z1, i1) (z2, i2))]]},
                        rlcomment = [] }))
            (g, _) -> (g, theVacuousRule)
      (g, _) -> (g, theVacuousRule)

invShearsRule :: Sig -> Gen -> (Gen, Rule)
invShearsRule sig g =
    case sortedVarsOfNames sig g "strd" ["z0","z1","z2"] of
      (g, [z0,z1,z2]) ->
          case sortedVarsOfNames sig g "indx" ["i0","i1","i2"] of
            (g, [i0,i1,i2]) ->
                (g, (Rule { rlname = "invShearsRule",
                        rlgoal =
                            Goal
                            {uvars = [z0,z1,z2,i0,i1,i2],
                             antec = [ -- useful for debugging:
                                       -- (AFact "no-state-split" []),
                                       (Trans (z0,i0)), (Trans (z1,i1)),
                                       (SameLocn (z0,i0) (z1,i1)),
                                       (LeadsTo (z1,i1) (z2,i2)), (Prec (z0,i0) (z2,i2)) ],
                             consq = [([],                -- no bvs
                                       [(Equals z0 z1),   -- two eqns
                                        (Equals i0 i1)]),
                                     ([],                -- no bvs
                                      -- (z0, i0) precedes (z1,i1)
                                       [(Prec (z0, i0) (z1, i1))])],
                             concl = [[(Equals z0 z1),   -- two eqns
                                        (Equals i0 i1)],
                                      -- (z0, i0) precedes (z1,i1)
                                       [(Prec (z0, i0) (z1, i1))]]},
                        rlcomment = [] }))
            (g, _) -> (g, theVacuousRule)
      (g, _) -> (g, theVacuousRule)

uninterruptibleRule :: Sig -> Gen -> (Gen, Rule)
uninterruptibleRule sig g =
    case sortedVarsOfNames sig g "strd" ["z0","z1","z2"] of
      (g, [z0,z1,z2]) ->
          case sortedVarsOfNames sig g "indx" ["i0","i1","i2"] of
            (g, [i0,i1,i2]) ->
                (g,
                 (Rule { rlname = "no-interruption",
                         rlgoal =
                             Goal
                             {uvars = [z0,z1,z2,i0,i1,i2],
                              antec = [ (LeadsTo (z0,i0) (z2,i2)), (Trans (z1,i1)),
                                        (SameLocn (z0,i0) (z1,i1)), (Prec (z0,i0) (z1,i1)),
                                        (Prec (z1,i1) (z2,i2)) ],
                              consq = [], -- implies False
                              concl = []},
                         rlcomment = [] }))
            (g, _) -> (g, theVacuousRule)
      (g, _) -> (g, theVacuousRule)

cakeRule :: Sig -> Gen -> (Gen, Rule)
cakeRule sig g =
    case sortedVarsOfNames sig g "strd" ["z0","z1","z2"] of
      (g, [z0,z1,z2]) ->
          case sortedVarsOfNames sig g "indx" ["i0","i1","i2"] of
            (g, [i0,i1,i2]) ->
                (g,
                 (Rule { rlname = "cakeRule",
                         rlgoal =
                             Goal
                             {uvars = [z0,z1,z2,i0,i1,i2],
                              antec = [ (Trans (z0,i0)), (Trans (z1,i1)),
                                        (LeadsTo (z0,i0) (z1,i1)), (LeadsTo (z0,i0) (z2,i2)),
                                        (Prec (z1,i1) (z2,i2)) ],
                              consq = [], -- implies False
                              concl = []},
                         rlcomment = [] }))
            (g, _) -> (g, theVacuousRule)
      (g, _) -> (g, theVacuousRule)