Merge branch 'master' into 1636_hets_performance_issues

.gitignore

@@ -193,3 +193,6 @@ stack.yaml.lock
 consoleHistory.tmp
 /stack.yaml.lock
 /.old.stack-work
+NeSyPatterns/AS.hs
+NeSyPatterns/ATC_NeSyPatterns.der.hs
+NeSyPatterns/ATC_NeSyPatterns.hs

ATC/ATCTest2.hs

@@ -20,6 +20,7 @@ import ATerm.Conversion
 import ATerm.ReadWrite
 import ATerm.Unshared
 import Common.Utils (readMaybe)
+import qualified Control.Monad.Fail as Fail
 import qualified Data.Map as Map
 import Data.List (isPrefixOf)
 
@@ -47,7 +48,7 @@ usage :: String -> FilePath -> IO ()
 usage cmd _ = do
   putStrLn ("unknown command: " ++ cmd)
   putStrLn "Known commands are: ReadWrite, [Check]Big{Map,List}<n>"
-  fail "no known command given"
+  Fail.fail "no known command given"
 
 generateRandomLists :: String -> IO [(Int, Int)]
 generateRandomLists upstr = do

Adl/adl.hs

@@ -16,6 +16,7 @@ import Common.DocUtils (pretty)
 import Common.Parsec ((<<))
 import Common.Result
 import Common.Lib.State
+import qualified Control.Monad.Fail as Fail
 import Text.ParserCombinators.Parsec (parse, eof)
 
 import Adl.As
@@ -56,4 +57,4 @@ process f = do
 #endif
       $ pretty es
       else printDiags 5 ds >> exitFailure
-    Left err -> fail $ show err
+    Left err -> Fail.fail $ show err

CASL/CCC/FreeTypes.hs

@@ -37,6 +37,7 @@ import qualified Common.Lib.MapSet as MapSet
 import qualified Common.Lib.Rel as Rel
 
 import Control.Monad
+import qualified Control.Monad.Fail as Fail
 
 import Data.Either
 import Data.Function
@@ -549,7 +550,7 @@ getNotComplete sig doms fsn constructors =
                     [(p, i)] -> completePatterns sig doms consMap consMap2
                       ([(showId p "", i)]
                       , zip g $ map snd l)
-                    l2 -> fail $ "wrongly grouped leading terms "
+                    l2 -> Fail.fail $ "wrongly grouped leading terms "
                       ++ show l2
          , g)) fsn
 
@@ -582,7 +583,7 @@ completePatterns tsig doms consMap consMap2 (leadingArgs, pas)
     | all (null . snd) pas =
        let fs = checkExhaustive tsig doms $ map fst pas
        in return $ map (\ f -> (showLeadingArgs "" leadingArgs, f)) fs
-    | any (null . snd) pas = fail "wrongly grouped leading terms"
+    | any (null . snd) pas = Fail.fail "wrongly grouped leading terms"
     | otherwise = let hds = map (\ (f, hd : _) -> (f, hd)) pas in
             if all (isVar . snd) hds
             then let
@@ -599,12 +600,12 @@ completePatterns tsig doms consMap consMap2 (leadingArgs, pas)
                 $ map (\ (_, _, os) -> Set.map res_OP_TYPE os) consAppls
               in case filter (not . Set.null . (`MapSet.lookup` consMap))
                      $ Set.toList consSrt of
-                  [] -> fail $
+                  [] -> Fail.fail $
                     "no common result type for constructors found: "
                        ++ showDoc (map snd hds) ""
                   cSrt : _ -> do
                     let allCons = MapSet.lookup cSrt consMap
-                    when (Set.null allCons) . fail
+                    when (Set.null allCons) . Fail.fail
                       $ "no constructors for result type found: " ++ show cSrt
                     let cons_group = map (\ (c, ct) -> (c, ct,
                           filter (\ (_, h : _) -> case unsortedTerm h of

CASL/CCC/TerminationProof.hs

@@ -27,6 +27,7 @@ import Common.Result
 import Common.Utils
 
 import Control.Monad
+import qualified Control.Monad.Fail as Fail
 
 import System.Directory
 
@@ -126,7 +127,7 @@ predSymName :: PRED_SYMB -> String
 predSymName = idStr . predSymbName
 
 -- | create a predicate application
-predAppl :: (Monad m, FormExtension f) => PRED_SYMB -> [TERM f] -> m String
+predAppl :: (Fail.MonadFail m, FormExtension f) => PRED_SYMB -> [TERM f] -> m String
 predAppl p = liftM (predSymName p ++) . termsPA
 
 -- | apply function string to argument string with brackets
@@ -138,7 +139,7 @@ applyBin :: String -> String -> String -> String
 applyBin o t1 t2 = apply o $ t1 ++ "," ++ t2
 
 -- | translate a casl term to a term of TRS(Terme Rewrite Systems)
-term2TRS :: (Monad m, FormExtension f) => TERM f -> m String
+term2TRS :: (Fail.MonadFail m, FormExtension f) => TERM f -> m String
 term2TRS t = case unsortedTerm t of
   Qual_var var _ _ -> return $ tokStr var
   Application o ts _ -> liftM (opSymName o ++) $ termsPA ts
@@ -147,10 +148,10 @@ term2TRS t = case unsortedTerm t of
     c <- axiomSub f
     b2 <- term2TRS t2
     return $ apply "when_else" $ b1 ++ "," ++ c ++ "," ++ b2
-  _ -> fail $ "no support for: " ++ showDoc t ""
+  _ -> Fail.fail $ "no support for: " ++ showDoc t ""
 
 -- | translate a list of casl terms to the patterns of a term in TRS
-termsPA :: (Monad m, FormExtension f) => [TERM f] -> m String
+termsPA :: (Fail.MonadFail m, FormExtension f) => [TERM f] -> m String
 termsPA ts = if null ts then return "" else
     liftM (apply "" . intercalate ",") $ mapM term2TRS ts
 
@@ -159,7 +160,7 @@ a rule without condition is represented by "A -> B" in
 Term Rewrite Systems; if there are some conditions, then
 follow the conditions after the symbol "|".
 For example : "A -> B | C -> D, E -> F, ..." -}
-axiom2TRS :: (FormExtension f, TermExtension f, Ord f, Monad m) => Sign f e
+axiom2TRS :: (FormExtension f, TermExtension f, Ord f, Fail.MonadFail m) => Sign f e
   -> [FORMULA f] -> FORMULA f -> m String
 axiom2TRS sig doms f = case splitAxiom f of
   (cs, f') -> do
@@ -184,7 +185,7 @@ axiom2TRS sig doms f = case splitAxiom f of
         _ -> t
       _ -> t
 
-axiom2Cond :: (FormExtension f, TermExtension f, Ord f, Monad m) => Sign f e
+axiom2Cond :: (FormExtension f, TermExtension f, Ord f, Fail.MonadFail m) => Sign f e
   -> [FORMULA f] -> FORMULA f -> m String
 axiom2Cond sig doms f = let s = liftM (++ " -> true") $ axiomSub f in
   case f of
@@ -206,11 +207,11 @@ isApp t = case unsortedTerm t of
   Application _ ts _ -> all isVar ts
   _ -> False
 
-axiom2Rule :: (Monad m, FormExtension f) => FORMULA f -> m String
+axiom2Rule :: (Fail.MonadFail m, FormExtension f) => FORMULA f -> m String
 axiom2Rule f = case f of
   Negation f' _ -> case f' of
     Quantification {} ->
-      fail "no support for negated quantification"
+      Fail.fail "no support for negated quantification"
     Definedness t _ -> liftM (++ " -> undefined") $ term2TRS t
     _ -> liftM (++ " -> false") $ axiomSub f'
   Definedness {} -> liftM (++ " -> open") $ axiomSub f
@@ -225,7 +226,7 @@ axiom2Rule f = case f of
   _ -> liftM (++ " -> true") $ axiomSub f
 
 -- | translate a casl axiom (without conditions) to a term of TRS,
-axiomSub :: (Monad m, FormExtension f) => FORMULA f -> m String
+axiomSub :: (Fail.MonadFail m, FormExtension f) => FORMULA f -> m String
 axiomSub f = case f of
   Junction j fs@(_ : _) _ -> do
     as <- mapM axiomSub fs
@@ -242,6 +243,6 @@ axiomSub f = case f of
     s1 <- axiomSub f1
     s2 <- axiomSub f2
     return $ applyBin (if c == Equivalence then "equiv" else "implies") s1 s2
-  Quantification {} -> fail "no support for local quantifications"
-  Membership {} -> fail "no support for membership tests"
-  _ -> fail $ "no support for: " ++ showDoc f ""
+  Quantification {} -> Fail.fail "no support for local quantifications"
+  Membership {} -> Fail.fail "no support for membership tests"
+  _ -> Fail.fail $ "no support for: " ++ showDoc f ""

CASL/CompositionTable/ComputeTable.hs

@@ -24,6 +24,7 @@ import Common.IRI (IRI)
 import Common.DocUtils
 import Common.Result
 import qualified Common.Lib.Rel as Rel
+import qualified Control.Monad.Fail as Fail
 
 import Data.Maybe
 import qualified Data.Set as Set
@@ -59,7 +60,7 @@ computeCompTable spName (sig, nsens) = do
   (baseRel, rel) <-
      case map Set.toList $ Rel.topSort $ sortRel sig of
        [[b], [r]] -> return (b, r)
-       _ -> fail errSorts
+       _ -> Fail.fail errSorts
   -- types of operation symbols
   let opTypes = mapSetToList (opMap sig)
       invt = mkTotOpType [baseRel] baseRel
@@ -71,7 +72,7 @@ computeCompTable spName (sig, nsens) = do
   let oplookup typ msg =
         case mlookup typ of
                [op] -> return op
-               ops -> fail (errOps ops msg )
+               ops -> Fail.fail (errOps ops msg )
   cmps <- oplookup cmpt "__cmps__: BaseRel * BaseRel -> Rel"
   _cmpl <- oplookup complt "compl__: Rel -> Rel"
   inv <- oplookup invt "inv__ : BaseRel -> BaseRel"

CASL/CompositionTable/ParseSparQ.hs

@@ -21,6 +21,8 @@ import Common.Parsec
 
 import Data.Char
 
+import qualified Control.Monad.Fail as Fail
+
 parseSparQTableOld :: Parser Table
 parseSparQTableOld = inParens $ do
   calculusName <- parseCalculusName
@@ -33,8 +35,8 @@ parseSparQTableOld = inParens $ do
     [i] -> return $ Table
       (Table_Attrs calculusName i $ rs1 ++ rs2 ++ rs3)
       compt ct (Reflectiontable []) $ Models []
-    [] -> fail "missing identity relation"
-    is -> fail $ "non-unique identity relation " ++ show is
+    [] -> Fail.fail "missing identity relation"
+    is -> Fail.fail $ "non-unique identity relation " ++ show is
 
 parseIdBaOths :: Parser ([Baserel], [Baserel])
 parseIdBaOths = fmap (\ l ->

CASL/CompositionTable/ParseTable2.hs

@@ -25,6 +25,7 @@ import CASL.CompositionTable.Keywords
 import CASL.CompositionTable.ParseSparQ
 import Common.Parsec
 import Common.Utils
+import qualified Control.Monad.Fail as Fail
 
 import qualified Data.IntSet as IntSet
 import qualified Data.IntMap as IntMap
@@ -58,8 +59,8 @@ parseSparQTable = inParens $ do
   (i3, _) <- parseIdBaOths
   case i2 ++ i3 of
     [i] -> return $ Table2 calculusName (lkup i m) ns bs compt ct
-    [] -> fail "missing identity relation"
-    is -> fail $ "non-unique identity relation " ++ show is
+    [] -> Fail.fail "missing identity relation"
+    is -> Fail.fail $ "non-unique identity relation " ++ show is
 
 parseComTab :: BMap -> Parser CmpTbl
 parseComTab m = cKey compositionOperationS

CASL/Morphism.hs

@@ -1,5 +1,7 @@
-{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies
-  , FlexibleInstances, DeriveDataTypeable #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE DeriveDataTypeable #-}
 {- |
 Module      :  ./CASL/Morphism.hs
 Description :  Symbols and signature morphisms for the CASL logic
@@ -82,6 +84,7 @@ import Common.Result
 import Common.Utils (composeMap)
 
 import Control.Monad
+import qualified Control.Monad.Fail as Fail
 
 type SymbolSet = Set.Set Symbol
 type SymbolMap = Map.Map Symbol Symbol
@@ -329,7 +332,7 @@ symbOrMapToRaw sig msig k sm = case sm of
             return [(w, x), (mkS s1, mkS res2)]
           (A_type s1, A_type s2) ->
             return [(w, x), (mkS s1, mkS s2)]
-          _ -> fail $ "profiles '" ++ showDoc t1 "' and '"
+          _ -> Fail.fail $ "profiles '" ++ showDoc t1 "' and '"
                ++ showDoc t2 "' do not match"
         _ -> return [(w, x)]
 
@@ -572,7 +575,7 @@ legalMor mor =
   && isSubOpMap (inducedOpMap sm (op_map mor) $ opMap s1) (opMap s2)
   && isSubMap (inducedPredMap sm (pred_map mor) $ predMap s1) (predMap s2)
   && legalSign s2
-  then legalMorphismExtension mor else fail "illegal CASL morphism"
+  then legalMorphismExtension mor else Fail.fail "illegal CASL morphism"
 
 isInclOpMap :: Op_map -> Bool
 isInclOpMap = all (\ ((i, _), (j, _)) -> i == j) . Map.toList

CASL/OMDocExport.hs

@@ -27,6 +27,7 @@ import Common.Id
 import Common.Result
 import Common.AS_Annotation
 import qualified Common.Lib.Rel as Rel
+import qualified Control.Monad.Fail as Fail
 
 import Common.DocUtils
 
@@ -126,7 +127,7 @@ instance AsOMConstant (String, SymbType) where
     toOMConstant e (n, st) =
         case st of
           SortAsItemType -> toOMConstant e n
-          SubsortAsItemType _ -> fail "AsOMConstant.SubsortAsItemType"
+          SubsortAsItemType _ -> Fail.fail "AsOMConstant.SubsortAsItemType"
           OpAsItemType ot -> toOMConstant e (n, ot)
           PredAsItemType pt -> toOMConstant e (n, pt)
 

CASL/OMDocImport.hs

@@ -32,6 +32,7 @@ import CASL.Sign
 import CASL.OMDoc
 
 import Control.Monad
+import qualified Control.Monad.Fail as Fail
 
 import qualified Data.Map as Map
 import Data.List
@@ -99,15 +100,15 @@ omdocToSym :: Env -> TCElement -> String -> Result Symbol
 omdocToSym e sym@(TCSymbol _ ctp srole _) n =
     case srole of
       Typ | ctp == const_sort -> return $ idToSortSymbol $ nameToId n
-          | otherwise -> fail $ "omdocToSym: No sorttype for " ++ show sym
+          | otherwise -> Fail.fail $ "omdocToSym: No sorttype for " ++ show sym
       Obj -> return $
              case omdocToType e ctp of
                Left ot -> idToOpSymbol (nameToId n) ot
                Right pt -> idToPredSymbol (nameToId n) pt
-      _ -> fail $ concat [ "omdocToSym: only type or object are allowed as"
+      _ -> Fail.fail $ concat [ "omdocToSym: only type or object are allowed as"
                          , " symbol roles, but found: ", show srole ]
 
-omdocToSym _ sym _ = fail $ concat [ "omdocToSym: only TCSymbol is allowed,"
+omdocToSym _ sym _ = Fail.fail $ concat [ "omdocToSym: only TCSymbol is allowed,"
                                    , " but found: ", show sym ]
 
 
@@ -125,7 +126,7 @@ omdocToSen e (TCSymbol _ t sr _) n =
                Theorem -> res False
                _ -> return Nothing
 
-omdocToSen _ sym _ = fail $ concat [ "omdocToSen: only TCSymbol is allowed,"
+omdocToSen _ sym _ = Fail.fail $ concat [ "omdocToSen: only TCSymbol is allowed,"
                                    , " but found: ", show sym ]
 
 

CASL/Qualify.hs

@@ -30,6 +30,7 @@ import Common.Result
 import qualified Common.Lib.MapSet as MapSet
 
 import Control.Monad
+import qualified Control.Monad.Fail as Fail
 import qualified Data.Map as Map
 import qualified Data.Set as Set
 
@@ -94,11 +95,11 @@ inverseMorphism invExt m = do
       ipm = Map.fromList $ map (\ ((i, t), j) ->
                   ((j, mapPredType sm t), i)) $ Map.toList pm
   unless (ss == Set.map (mapSort ism . mapSort sm) ss)
-    $ fail "no injective CASL sort mapping"
+    $ Fail.fail "no injective CASL sort mapping"
   unless (os == inducedOpMap ism iom (inducedOpMap sm om os))
-    $ fail "no injective CASL op mapping"
+    $ Fail.fail "no injective CASL op mapping"
   unless (ps == inducedPredMap ism ipm (inducedPredMap sm pm ps))
-    $ fail "no injective CASL pred mapping"
+    $ Fail.fail "no injective CASL pred mapping"
   return (embedMorphism iExt (imageOfMorphism m) src)
     { sort_map = ism
     , op_map = iom