forall to forAll (tamarin-prover#549)

* Changing the forall occurence to forAll

* remplacing all foreall function occurence by forAll on Haskell file

lib/accountability/src/Accountability/Generation.hs

@@ -59,7 +59,7 @@ freesSubsetCorrupt vars = foldl1 (.&&.) corrupted
         corrupt var = quantifyVars exists [tempVar "i"] $ protoFactFormula "Corrupted" [varTerm $ Free var] (tempTerm "i")
 
 corruptSubsetFrees :: [LVar] -> SyntacticLNFormula
-corruptSubsetFrees vars = quantifyVars forall [msgVar "a", tempVar "i"] $
+corruptSubsetFrees vars = quantifyVars forAll [msgVar "a", tempVar "i"] $
                             (protoFactFormula "Corrupted" [msgTerm "a"] (tempTerm "i") .==>. isElem (msgVar "a") vars)
 
 isElem :: LVar -> [LVar] -> SyntacticLNFormula
@@ -91,7 +91,7 @@ singleMatch :: MonadFresh m => SyntacticLNFormula -> m SyntacticLNFormula
 singleMatch t = do
     t1 <- rename t
     t2 <- rename t
-    return $ t1 .&&. quantifyVars forall (frees t2) (t2 .==>. varsEq (frees t2) (frees t1))
+    return $ t1 .&&. quantifyVars forAll (frees t2) (t2 .==>. varsEq (frees t2) (frees t1))
 
 caseTestFormulasExcept :: AccLemma -> CaseTest -> [SyntacticLNFormula]
 caseTestFormulasExcept accLemma caseTest = map (L.get cFormula) (filter (\c -> L.get cName caseTest /= L.get cName c) (L.get aCaseTests accLemma))
@@ -173,23 +173,23 @@ verifiabilityEmpty accLemma = return $ toLemma accLemma AllTraces name formula
         taus = map (L.get cFormula) (L.get aCaseTests accLemma)
         lhs = Not $ foldConn (.||.) $ map (quantifyFrees exists) taus
         phi = L.get aFormula accLemma
-        formula = quantifyFrees forall $ lhs .==>. phi
+        formula = quantifyFrees forAll $ lhs .==>. phi
 
 verifiabilityNonEmpty :: MonadFresh m => AccLemma -> CaseTest -> m (ProtoLemma SyntacticLNFormula ProofSkeleton)
 verifiabilityNonEmpty accLemma caseTest = return $ toLemma accLemma AllTraces name (toIntermediate formula)
     where
         name = "_" ++ L.get cName caseTest ++ "_verif_nonempty"
         tau = L.get cFormula caseTest
         phi = L.get aFormula accLemma
-        formula = quantifyFrees forall $ tau .==>. Not phi
+        formula = quantifyFrees forAll $ tau .==>. Not phi
 
 minimality :: MonadFresh m => AccLemma -> CaseTest -> m (ProtoLemma SyntacticLNFormula ProofSkeleton)
 minimality accLemma caseTest = do
     t1 <- rename tau
     tts <- mapM rename taus
 
     let rhs = map (\t -> Not (quantifyVars exists (frees t) $ t .&&. strictSubsetOf (frees t) (frees t1))) tts
-    let formula = quantifyFrees forall $ t1 .==>. foldConn (.&&.) rhs
+    let formula = quantifyFrees forAll $ t1 .==>. foldConn (.&&.) rhs
 
     return $ toLemma accLemma AllTraces name (toIntermediate formula)
     where
@@ -202,15 +202,15 @@ uniqueness accLemma caseTest = return $ toLemma accLemma AllTraces name (toInter
     where
         name = "_" ++ L.get cName caseTest ++ "_uniq"
         tau = L.get cFormula caseTest
-        formula = quantifyFrees forall (tau .==>. freesSubsetCorrupt (frees tau))
+        formula = quantifyFrees forAll (tau .==>. freesSubsetCorrupt (frees tau))
 
 -- | :TODO: : Avoid duplicates
 injective :: MonadFresh m => AccLemma -> CaseTest -> m (ProtoLemma SyntacticLNFormula ProofSkeleton)
 injective accLemma caseTest = return $ toLemma accLemma AllTraces name (toIntermediate formula)
     where
         name = "_" ++ L.get cName caseTest ++ "_inj"
         tau = L.get cFormula caseTest
-        formula = quantifyFrees forall (tau .==>. foldl (.&&.) (TF True) [ Not $ varsEq [x] [y] | x <- frees tau, y <- frees tau, x /= y ])
+        formula = quantifyFrees forAll (tau .==>. foldl (.&&.) (TF True) [ Not $ varsEq [x] [y] | x <- frees tau, y <- frees tau, x /= y ])
 
 singlematched :: MonadFresh m => AccLemma -> CaseTest -> m (ProtoLemma SyntacticLNFormula ProofSkeleton)
 singlematched accLemma caseTest = do

lib/sapic/src/Sapic/Basetranslation.hs

@@ -257,7 +257,7 @@ baseTransComb c an p tildex
         in
         let fa = Conn Imp (Ato (EqE (fmapTerm (fmap Free) t1) (fmapTerm (fmap Free) t2))) (TF False) in
         let tildexl =  freeset t1or `union` tildex in
-        let faN = fold (hinted forall) fa freevars in
+        let faN = fold (hinted forAll) fa freevars in
         let pos = p++[1] in
         if elsBranch then
           ([

lib/sapic/src/Sapic/ProgressTranslation.hs

@@ -165,7 +165,7 @@ progressRestr anP restrictions  = do
             mapM (\tos -> return $ Restriction (name tos) (formula tos))  (toList toss)
             where
                 name tos = "Progress_" ++ prettyPosition pos ++ "_to_" ++ List.intercalate "_or_" (map prettyPosition $ toList tos)
-                formula tos = hinted forall pvar $ hinted forall t1var $ antecedent .==>. conclusion tos
+                formula tos = hinted forAll pvar $ hinted forAll t1var $ antecedent .==>. conclusion tos
                 pvar = msgVarProgress pos
                 t1var = LVar "t" LSortNode 1
                 t2var = LVar "t" LSortNode 2

lib/theory/src/Theory/Model/Formula.hs

@@ -51,7 +51,7 @@ module Theory.Model.Formula (
   , (.==>.)
   , (.<=>.)
   , exists
-  , forall
+  , forAll
   , hinted
 
   -- ** General Transformations
@@ -338,14 +338,14 @@ quantify x =
               | otherwise = Free v
 
 -- | Create a universal quantification with a sort hint for the bound variable.
-forall :: (Ord c, Ord v, Functor syn) => s -> v -> ProtoFormula syn s c v -> ProtoFormula syn s c v
-forall hint' x = Qua All hint' . quantify x
+forAll :: (Ord c, Ord v, Functor syn) => s -> v -> ProtoFormula syn s c v -> ProtoFormula syn s c v
+forAll hint' x = Qua All hint' . quantify x
 
 -- | Create a existential quantification with a sort hint for the bound variable.
 exists :: (Ord c, Ord v, Functor syn) => s -> v -> ProtoFormula syn s c v -> ProtoFormula syn s c v
 exists hint' x = Qua Ex hint' . quantify x
 
--- | Transform @forall@ and @exists@ into functions that operate on logical variables or other variables
+-- | Transform @forAll@ and @exists@ into functions that operate on logical variables or other variables
 --   that have hasHint
 hinted :: Hinted v => ((String, LSort) -> v -> a) -> v -> a
 hinted f v = f (hint v) v

lib/theory/src/Theory/Model/Restriction.hs

@@ -143,7 +143,7 @@ fromRuleRestriction rname f =
                 -- and varnow
                 mkRestriction f' = Restriction
                                         (restrPrefix ++ rname)
-                                        (foldr (hinted forall) f'' (frees f''))
+                                        (foldr (hinted forAll) f'' (frees f''))
                                         where
                                             f'' = Ato (Action timepoint fact) .==>. f'
                                             timepoint = varTerm $ Free varNow

lib/theory/src/Theory/Text/Parser/Formula.hs

@@ -71,7 +71,7 @@ fatom varp nodep = asum
   ]
   where
     quantification = do
-        q <- (forall <$ opForall) <|> (exists <$ opExists)
+        q <- (forAll <$ opForall) <|> (exists <$ opExists)
         vs <- many1 (try varp <|> nodep)  <* dot
         f  <- iff varp nodep
         return $ foldr (hinted q) f vs