{- |
Module      :  ./CASL/Induction.hs
Description :  Derive induction schemes from sort generation constraints
Copyright   :  (c) Till Mossakowski, Rainer Grabbe and Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

We provide both second-order induction schemes as well as their
instantiation to specific first-order formulas.
-}

module CASL.Induction (inductionScheme, inductionSentence, generateInductionLemmas, substitute) where

import CASL.AS_Basic_CASL
import CASL.Sign
import CASL.Fold
import CASL.Quantification (flatVAR_DECLs)
import CASL.ToDoc

import Common.AS_Annotation as AS_Anno
import Common.Id
import Common.Utils (combine, number)

import qualified Data.Set as Set
import Data.List
import Data.Maybe

{- | derive a second-order induction scheme from a sort generation constraint
the second-order predicate variables are represented as predicate
symbols P[s], where s is a sort -}
inductionScheme :: FormExtension f => [Constraint] -> FORMULA f
inductionScheme :: [Constraint] -> FORMULA f
inductionScheme constrs :: [Constraint]
constrs = FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f
unpackSentence (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ [Constraint] -> FORMULA f
forall f. FormExtension f => [Constraint] -> FORMULA f
inductionSentence [Constraint]
constrs
  where unpackSentence :: FORMULA f -> FORMULA f
unpackSentence (QuantPred _ _ f :: FORMULA f
f) = FORMULA f -> FORMULA f
unpackSentence FORMULA f
f
        unpackSentence f :: FORMULA f
f = FORMULA f
f

inductionSentence :: FormExtension f => [Constraint] -> FORMULA f
inductionSentence :: [Constraint] -> FORMULA f
inductionSentence constrs :: [Constraint]
constrs =
  (FORMULA f -> (PRED_NAME, PRED_TYPE) -> FORMULA f)
-> FORMULA f -> [(PRED_NAME, PRED_TYPE)] -> FORMULA f
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl FORMULA f -> (PRED_NAME, PRED_TYPE) -> FORMULA f
forall f. FORMULA f -> (PRED_NAME, PRED_TYPE) -> FORMULA f
quantifyPred ([(Constraint, TERM f -> FORMULA f)] -> FORMULA f
forall f.
FormExtension f =>
[(Constraint, TERM f -> FORMULA f)] -> FORMULA f
induction [(Constraint, TERM f -> FORMULA f)]
forall f. [(Constraint, TERM f -> FORMULA f)]
constrSubstr) [(PRED_NAME, PRED_TYPE)]
predSymbs
    where
        quantifyPred :: FORMULA f -> (PRED_NAME, PRED_TYPE) -> FORMULA f
quantifyPred f :: FORMULA f
f (pName :: PRED_NAME
pName, pType :: PRED_TYPE
pType) = PRED_NAME -> PRED_TYPE -> FORMULA f -> FORMULA f
forall f. PRED_NAME -> PRED_TYPE -> FORMULA f -> FORMULA f
QuantPred PRED_NAME
pName PRED_TYPE
pType FORMULA f
f
        (constrSubstr :: [(Constraint, TERM f -> FORMULA f)]
constrSubstr, predSymbs :: [(PRED_NAME, PRED_TYPE)]
predSymbs) = [((Constraint, TERM f -> FORMULA f), (PRED_NAME, PRED_TYPE))]
-> ([(Constraint, TERM f -> FORMULA f)], [(PRED_NAME, PRED_TYPE)])
forall a b. [(a, b)] -> ([a], [b])
unzip ([((Constraint, TERM f -> FORMULA f), (PRED_NAME, PRED_TYPE))]
 -> ([(Constraint, TERM f -> FORMULA f)], [(PRED_NAME, PRED_TYPE)]))
-> [((Constraint, TERM f -> FORMULA f), (PRED_NAME, PRED_TYPE))]
-> ([(Constraint, TERM f -> FORMULA f)], [(PRED_NAME, PRED_TYPE)])
forall a b. (a -> b) -> a -> b
$ (Constraint
 -> ((Constraint, TERM f -> FORMULA f), (PRED_NAME, PRED_TYPE)))
-> [Constraint]
-> [((Constraint, TERM f -> FORMULA f), (PRED_NAME, PRED_TYPE))]
forall a b. (a -> b) -> [a] -> [b]
map Constraint
-> ((Constraint, TERM f -> FORMULA f), (PRED_NAME, PRED_TYPE))
forall f.
Constraint
-> ((Constraint, TERM f -> FORMULA f), (PRED_NAME, PRED_TYPE))
predSubst [Constraint]
constrs
        sorts :: [PRED_NAME]
sorts = (Constraint -> PRED_NAME) -> [Constraint] -> [PRED_NAME]
forall a b. (a -> b) -> [a] -> [b]
map Constraint -> PRED_NAME
newSort [Constraint]
constrs
        injective :: Bool
injective = [PRED_NAME] -> Bool
forall a. Ord a => [a] -> Bool
isInjectiveList [PRED_NAME]
sorts
        predSubst :: Constraint
-> ((Constraint, TERM f -> FORMULA f), (PRED_NAME, PRED_TYPE))
predSubst constr :: Constraint
constr =
          ((Constraint
constr, \ t :: TERM f
t -> PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication PRED_SYMB
predSymb [TERM f
t] Range
nullRange), (PRED_NAME
ident, PRED_TYPE
typ))
          where
          predSymb :: PRED_SYMB
predSymb = PRED_NAME -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name PRED_NAME
ident PRED_TYPE
typ Range
nullRange
          Id ts :: [Token]
ts cs :: [PRED_NAME]
cs ps :: Range
ps =
              if Bool
injective then Constraint -> PRED_NAME
newSort Constraint
constr else Constraint -> PRED_NAME
origSort Constraint
constr
          ident :: PRED_NAME
ident = [Token] -> [PRED_NAME] -> Range -> PRED_NAME
Id [String -> Token
mkSimpleId (String -> Token) -> String -> Token
forall a b. (a -> b) -> a -> b
$ String
genNamePrefix String -> String -> String
forall a. [a] -> [a] -> [a]
++ "P_"
                          String -> String -> String
forall a. [a] -> [a] -> [a]
++ PRED_NAME -> String -> String
showId ([Token] -> [PRED_NAME] -> Range -> PRED_NAME
Id [Token]
ts [] Range
ps) ""] [PRED_NAME]
cs Range
ps
          typ :: PRED_TYPE
typ = [PRED_NAME] -> Range -> PRED_TYPE
Pred_type [Constraint -> PRED_NAME
newSort Constraint
constr] Range
nullRange

{- | Function for derivation of first-order instances of sort generation
constraints.
Given a list of formulas with a free sorted variable, instantiate the
sort generation constraint for this list of formulas
It is assumed that the (original) sorts of the constraint
match the sorts of the free variables -}
instantiateSortGen :: FormExtension f
  => [(Constraint, (FORMULA f, (VAR, SORT)))] -> FORMULA f
instantiateSortGen :: [(Constraint, (FORMULA f, (Token, PRED_NAME)))] -> FORMULA f
instantiateSortGen phis :: [(Constraint, (FORMULA f, (Token, PRED_NAME)))]
phis =
  [(Constraint, TERM f -> FORMULA f)] -> FORMULA f
forall f.
FormExtension f =>
[(Constraint, TERM f -> FORMULA f)] -> FORMULA f
induction (((Constraint, (FORMULA f, (Token, PRED_NAME)))
 -> (Constraint, TERM f -> FORMULA f))
-> [(Constraint, (FORMULA f, (Token, PRED_NAME)))]
-> [(Constraint, TERM f -> FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map (Constraint, (FORMULA f, (Token, PRED_NAME)))
-> (Constraint, TERM f -> FORMULA f)
forall f a.
FormExtension f =>
(a, (FORMULA f, (Token, PRED_NAME))) -> (a, TERM f -> FORMULA f)
substFormula [(Constraint, (FORMULA f, (Token, PRED_NAME)))]
phis)
  where substFormula :: (a, (FORMULA f, (Token, PRED_NAME))) -> (a, TERM f -> FORMULA f)
substFormula (c :: a
c, (phi :: FORMULA f
phi, (v :: Token
v, s :: PRED_NAME
s))) = (a
c, \ t :: TERM f
t -> Token -> PRED_NAME -> TERM f -> FORMULA f -> FORMULA f
forall f.
FormExtension f =>
Token -> PRED_NAME -> TERM f -> FORMULA f -> FORMULA f
substitute Token
v PRED_NAME
s TERM f
t FORMULA f
phi)

-- | substitute a term for a variable in a formula
substitute :: FormExtension f => VAR -> SORT -> TERM f -> FORMULA f -> FORMULA f
substitute :: Token -> PRED_NAME -> TERM f -> FORMULA f -> FORMULA f
substitute v :: Token
v s :: PRED_NAME
s t :: TERM f
t = Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f
forall f a b. Record f a b -> FORMULA f -> a
foldFormula
 ((f -> f) -> Record f (FORMULA f) (TERM f)
forall f g. (f -> g) -> Record f (FORMULA g) (TERM g)
mapRecord f -> f
forall a. a -> a
id) { foldQual_var :: TERM f -> Token -> PRED_NAME -> Range -> TERM f
foldQual_var = \ t2 :: TERM f
t2 v2 :: Token
v2 s2 :: PRED_NAME
s2 _ ->
                  if Token
v Token -> Token -> Bool
forall a. Eq a => a -> a -> Bool
== Token
v2 Bool -> Bool -> Bool
&& PRED_NAME
s PRED_NAME -> PRED_NAME -> Bool
forall a. Eq a => a -> a -> Bool
== PRED_NAME
s2 then TERM f
t else TERM f
t2
                , foldQuantification :: FORMULA f
-> QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
foldQuantification = \ t2 :: FORMULA f
t2 q :: QUANTIFIER
q vs :: [VAR_DECL]
vs p :: FORMULA f
p r :: Range
r ->
                  if (Token, PRED_NAME) -> [(Token, PRED_NAME)] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (Token
v, PRED_NAME
s) ([(Token, PRED_NAME)] -> Bool) -> [(Token, PRED_NAME)] -> Bool
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> [(Token, PRED_NAME)]
flatVAR_DECLs [VAR_DECL]
vs
                  then FORMULA f
t2 else QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q [VAR_DECL]
vs FORMULA f
p Range
r
                }

{- | derive an induction scheme from a sort generation constraint
using substitutions as induction predicates -}
induction :: FormExtension f => [(Constraint, TERM f -> FORMULA f)] -> FORMULA f
induction :: [(Constraint, TERM f -> FORMULA f)] -> FORMULA f
induction constrSubsts :: [(Constraint, TERM f -> FORMULA f)]
constrSubsts =
   let mkVar :: a -> Token
mkVar i :: a
i = String -> Token
mkSimpleId ("x_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i)
       sortInfo :: [(TERM f -> FORMULA f, (Token, PRED_NAME))]
sortInfo = (((Constraint, TERM f -> FORMULA f), Int)
 -> (TERM f -> FORMULA f, (Token, PRED_NAME)))
-> [((Constraint, TERM f -> FORMULA f), Int)]
-> [(TERM f -> FORMULA f, (Token, PRED_NAME))]
forall a b. (a -> b) -> [a] -> [b]
map (\ ((cs :: Constraint
cs, sub :: TERM f -> FORMULA f
sub), i :: Int
i) -> (TERM f -> FORMULA f
sub, (Int -> Token
forall a. Show a => a -> Token
mkVar Int
i, Constraint -> PRED_NAME
newSort Constraint
cs)))
         ([((Constraint, TERM f -> FORMULA f), Int)]
 -> [(TERM f -> FORMULA f, (Token, PRED_NAME))])
-> [((Constraint, TERM f -> FORMULA f), Int)]
-> [(TERM f -> FORMULA f, (Token, PRED_NAME))]
forall a b. (a -> b) -> a -> b
$ [(Constraint, TERM f -> FORMULA f)]
-> [((Constraint, TERM f -> FORMULA f), Int)]
forall a. [a] -> [(a, Int)]
number [(Constraint, TERM f -> FORMULA f)]
constrSubsts
       mkConclusion :: (TERM f -> FORMULA f, (Token, PRED_NAME)) -> FORMULA f
mkConclusion (subst :: TERM f -> FORMULA f
subst, v :: (Token, PRED_NAME)
v) =
         [VAR_DECL] -> FORMULA f -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [(Token -> PRED_NAME -> VAR_DECL) -> (Token, PRED_NAME) -> VAR_DECL
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Token -> PRED_NAME -> VAR_DECL
mkVarDecl (Token, PRED_NAME)
v] (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ TERM f -> FORMULA f
subst (TERM f -> FORMULA f) -> TERM f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ (Token -> PRED_NAME -> TERM f) -> (Token, PRED_NAME) -> TERM f
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Token -> PRED_NAME -> TERM f
forall f. Token -> PRED_NAME -> TERM f
mkVarTerm (Token, PRED_NAME)
v
       inductionConclusion :: FORMULA f
inductionConclusion = [FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
conjunct ([FORMULA f] -> FORMULA f) -> [FORMULA f] -> FORMULA f
forall a b. (a -> b) -> a -> b
$ ((TERM f -> FORMULA f, (Token, PRED_NAME)) -> FORMULA f)
-> [(TERM f -> FORMULA f, (Token, PRED_NAME))] -> [FORMULA f]
forall a b. (a -> b) -> [a] -> [b]
map (TERM f -> FORMULA f, (Token, PRED_NAME)) -> FORMULA f
forall f f. (TERM f -> FORMULA f, (Token, PRED_NAME)) -> FORMULA f
mkConclusion [(TERM f -> FORMULA f, (Token, PRED_NAME))]
sortInfo
       inductionPremises :: [[FORMULA f]]
inductionPremises = ((Constraint, TERM f -> FORMULA f) -> [FORMULA f])
-> [(Constraint, TERM f -> FORMULA f)] -> [[FORMULA f]]
forall a b. (a -> b) -> [a] -> [b]
map ([TERM f -> FORMULA f]
-> (Constraint, TERM f -> FORMULA f) -> [FORMULA f]
forall f.
FormExtension f =>
[TERM f -> FORMULA f]
-> (Constraint, TERM f -> FORMULA f) -> [FORMULA f]
mkPrems ([TERM f -> FORMULA f]
 -> (Constraint, TERM f -> FORMULA f) -> [FORMULA f])
-> [TERM f -> FORMULA f]
-> (Constraint, TERM f -> FORMULA f)
-> [FORMULA f]
forall a b. (a -> b) -> a -> b
$ ((Constraint, TERM f -> FORMULA f) -> TERM f -> FORMULA f)
-> [(Constraint, TERM f -> FORMULA f)] -> [TERM f -> FORMULA f]
forall a b. (a -> b) -> [a] -> [b]
map (Constraint, TERM f -> FORMULA f) -> TERM f -> FORMULA f
forall a b. (a, b) -> b
snd [(Constraint, TERM f -> FORMULA f)]
constrSubsts) [(Constraint, TERM f -> FORMULA f)]
constrSubsts
       inductionPremise :: FORMULA f
inductionPremise = [FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
conjunct ([FORMULA f] -> FORMULA f) -> [FORMULA f] -> FORMULA f
forall a b. (a -> b) -> a -> b
$ [[FORMULA f]] -> [FORMULA f]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[FORMULA f]]
inductionPremises
   in FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl FORMULA f
inductionPremise FORMULA f
inductionConclusion

{- | construct premise set for the induction scheme
for one sort in the constraint -}
mkPrems :: FormExtension f => [TERM f -> FORMULA f]
  -> (Constraint, TERM f -> FORMULA f) -> [FORMULA f]
mkPrems :: [TERM f -> FORMULA f]
-> (Constraint, TERM f -> FORMULA f) -> [FORMULA f]
mkPrems substs :: [TERM f -> FORMULA f]
substs (constr :: Constraint
constr, sub :: TERM f -> FORMULA f
sub) = ((OP_SYMB, [Int]) -> FORMULA f)
-> [(OP_SYMB, [Int])] -> [FORMULA f]
forall a b. (a -> b) -> [a] -> [b]
map ([TERM f -> FORMULA f]
-> (TERM f -> FORMULA f) -> (OP_SYMB, [Int]) -> FORMULA f
forall f.
FormExtension f =>
[TERM f -> FORMULA f]
-> (TERM f -> FORMULA f) -> (OP_SYMB, [Int]) -> FORMULA f
mkPrem [TERM f -> FORMULA f]
substs TERM f -> FORMULA f
sub) (Constraint -> [(OP_SYMB, [Int])]
opSymbs Constraint
constr)

-- | construct a premise for the induction scheme for one constructor
mkPrem :: FormExtension f => [TERM f -> FORMULA f] -> (TERM f -> FORMULA f)
  -> (OP_SYMB, [Int]) -> FORMULA f
mkPrem :: [TERM f -> FORMULA f]
-> (TERM f -> FORMULA f) -> (OP_SYMB, [Int]) -> FORMULA f
mkPrem substs :: [TERM f -> FORMULA f]
substs subst :: TERM f -> FORMULA f
subst (opSym :: OP_SYMB
opSym@(Qual_op_name _ (Op_type _ argTypes :: [PRED_NAME]
argTypes _ _) _), idx :: [Int]
idx) =
  [VAR_DECL] -> FORMULA f -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL]
qVars FORMULA f
phi
  where
  qVars :: [VAR_DECL]
qVars = ((PRED_NAME, Int) -> VAR_DECL) -> [(PRED_NAME, Int)] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map (\ (a :: PRED_NAME
a, i :: Int
i) -> String -> PRED_NAME -> VAR_DECL
mkVarDeclStr ("y_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i) PRED_NAME
a) ([(PRED_NAME, Int)] -> [VAR_DECL])
-> [(PRED_NAME, Int)] -> [VAR_DECL]
forall a b. (a -> b) -> a -> b
$ [PRED_NAME] -> [(PRED_NAME, Int)]
forall a. [a] -> [(a, Int)]
number [PRED_NAME]
argTypes
  phi :: FORMULA f
phi = if [FORMULA f] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FORMULA f]
indHyps then FORMULA f
indConcl
           else FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl ([FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
conjunct [FORMULA f]
indHyps) FORMULA f
indConcl
  indConcl :: FORMULA f
indConcl = TERM f -> FORMULA f
subst (TERM f -> FORMULA f) -> TERM f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ OP_SYMB -> [TERM f] -> TERM f
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl OP_SYMB
opSym ([TERM f] -> TERM f) -> [TERM f] -> TERM f
forall a b. (a -> b) -> a -> b
$ (VAR_DECL -> TERM f) -> [VAR_DECL] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar [VAR_DECL]
qVars
  indHyps :: [FORMULA f]
indHyps = ((VAR_DECL, Int) -> Maybe (FORMULA f))
-> [(VAR_DECL, Int)] -> [FORMULA f]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (VAR_DECL, Int) -> Maybe (FORMULA f)
indHyp ([VAR_DECL] -> [Int] -> [(VAR_DECL, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [VAR_DECL]
qVars [Int]
idx)
  indHyp :: (VAR_DECL, Int) -> Maybe (FORMULA f)
indHyp (v1 :: VAR_DECL
v1, i :: Int
i) =
    if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0 then Maybe (FORMULA f)
forall a. Maybe a
Nothing -- leave out sorts from outside the constraint
     else FORMULA f -> Maybe (FORMULA f)
forall a. a -> Maybe a
Just (FORMULA f -> Maybe (FORMULA f)) -> FORMULA f -> Maybe (FORMULA f)
forall a b. (a -> b) -> a -> b
$ ([TERM f -> FORMULA f]
substs [TERM f -> FORMULA f] -> Int -> TERM f -> FORMULA f
forall a. [a] -> Int -> a
!! Int
i) (TERM f -> FORMULA f) -> TERM f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
v1
mkPrem _ _ (opSym :: OP_SYMB
opSym, _) =
  String -> FORMULA f
forall a. HasCallStack => String -> a
error ("CASL.Induction. mkPrems: "
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ "unqualified operation symbol occuring in constraint: "
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ OP_SYMB -> String
forall a. Show a => a -> String
show OP_SYMB
opSym)

-- | for goals try to generate additional implications based on induction
generateInductionLemmas :: FormExtension f => Bool
  -> (Sign f e, [Named (FORMULA f)]) -> (Sign f e, [Named (FORMULA f)])
generateInductionLemmas :: Bool
-> (Sign f e, [Named (FORMULA f)])
-> (Sign f e, [Named (FORMULA f)])
generateInductionLemmas b :: Bool
b (sig :: Sign f e
sig, sens :: [Named (FORMULA f)]
sens) = let
   sortGens :: [[Constraint]]
sortGens = (Named (FORMULA f) -> [[Constraint]] -> [[Constraint]])
-> [[Constraint]] -> [Named (FORMULA f)] -> [[Constraint]]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ s :: Named (FORMULA f)
s cs :: [[Constraint]]
cs -> case Named (FORMULA f) -> FORMULA f
forall s a. SenAttr s a -> s
sentence Named (FORMULA f)
s of
     Sort_gen_ax c :: [Constraint]
c _ -> [Constraint]
c [Constraint] -> [[Constraint]] -> [[Constraint]]
forall a. a -> [a] -> [a]
: [[Constraint]]
cs
     _ -> [[Constraint]]
cs) [] [Named (FORMULA f)]
axs
   (axs :: [Named (FORMULA f)]
axs, goals :: [Named (FORMULA f)]
goals) = (Named (FORMULA f) -> Bool)
-> [Named (FORMULA f)]
-> ([Named (FORMULA f)], [Named (FORMULA f)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Named (FORMULA f) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom [Named (FORMULA f)]
sens
   in (Sign f e
sig, (if Bool
b then [Named (FORMULA f)]
sens else [Named (FORMULA f)]
axs)
       [Named (FORMULA f)] -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. [a] -> [a] -> [a]
++ Bool
-> [[Constraint]] -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall f.
FormExtension f =>
Bool
-> [[Constraint]] -> [Named (FORMULA f)] -> [Named (FORMULA f)]
generateInductionLemmasAux Bool
b [[Constraint]]
sortGens [Named (FORMULA f)]
goals)

generateInductionLemmasAux
  :: FormExtension f => Bool
  -- ^ if True create additional implication otherwise replace goals
  -> [[Constraint]] -- ^ the constraints of a theory
  -> [AS_Anno.Named (FORMULA f)] -- ^ all goals of a theory
  -> [AS_Anno.Named (FORMULA f)]
{- ^ all the generated induction lemmas
and the labels are derived from the goal-names -}
generateInductionLemmasAux :: Bool
-> [[Constraint]] -> [Named (FORMULA f)] -> [Named (FORMULA f)]
generateInductionLemmasAux b :: Bool
b sort_gen_axs :: [[Constraint]]
sort_gen_axs goals :: [Named (FORMULA f)]
goals = let
    findVar :: t -> [(p, t)] -> p
findVar s :: t
s [] = String -> p
forall a. HasCallStack => String -> a
error ("CASL.generateInductionLemmas:\n"
                       String -> String -> String
forall a. [a] -> [a] -> [a]
++ "No VAR found of SORT " String -> String -> String
forall a. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "!")
    findVar s :: t
s ((vl :: p
vl, sl :: t
sl) : lst :: [(p, t)]
lst) = if t
s t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
sl then p
vl else t -> [(p, t)] -> p
findVar t
s [(p, t)]
lst
    removeVarsort :: Token -> PRED_NAME -> FORMULA f -> FORMULA f
removeVarsort v :: Token
v s :: PRED_NAME
s f :: FORMULA f
f = case FORMULA f
f of
      Quantification Universal varDecls :: [VAR_DECL]
varDecls formula :: FORMULA f
formula rng :: Range
rng ->
        let vd' :: [VAR_DECL]
vd' = [VAR_DECL] -> [VAR_DECL]
newVarDecls [VAR_DECL]
varDecls
        in if [VAR_DECL] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VAR_DECL]
vd' then FORMULA f
formula
            else QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
Universal [VAR_DECL]
vd' FORMULA f
formula Range
rng
      _ -> FORMULA f
f
      where
        newVarDecls :: [VAR_DECL] -> [VAR_DECL]
newVarDecls = (VAR_DECL -> Bool) -> [VAR_DECL] -> [VAR_DECL]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Var_decl vs :: [Token]
vs _ _) -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Token] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Token]
vs) ([VAR_DECL] -> [VAR_DECL])
-> ([VAR_DECL] -> [VAR_DECL]) -> [VAR_DECL] -> [VAR_DECL]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
            (VAR_DECL -> VAR_DECL) -> [VAR_DECL] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map (\ var_decl :: VAR_DECL
var_decl@(Var_decl vars :: [Token]
vars varsort :: PRED_NAME
varsort r :: Range
r) ->
                   if PRED_NAME
varsort PRED_NAME -> PRED_NAME -> Bool
forall a. Eq a => a -> a -> Bool
== PRED_NAME
s
                     then [Token] -> PRED_NAME -> Range -> VAR_DECL
Var_decl ((Token -> Bool) -> [Token] -> [Token]
forall a. (a -> Bool) -> [a] -> [a]
filter (Token -> Token -> Bool
forall a. Eq a => a -> a -> Bool
/= Token
v) [Token]
vars) PRED_NAME
s Range
r
                     else VAR_DECL
var_decl)
    (uniQuantGoals :: [(Named (FORMULA f), [(Token, PRED_NAME)])]
uniQuantGoals, restGoals :: [Named (FORMULA f)]
restGoals) =
            (Named (FORMULA f)
 -> ([(Named (FORMULA f), [(Token, PRED_NAME)])],
     [Named (FORMULA f)])
 -> ([(Named (FORMULA f), [(Token, PRED_NAME)])],
     [Named (FORMULA f)]))
-> ([(Named (FORMULA f), [(Token, PRED_NAME)])],
    [Named (FORMULA f)])
-> [Named (FORMULA f)]
-> ([(Named (FORMULA f), [(Token, PRED_NAME)])],
    [Named (FORMULA f)])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ( \ goal :: Named (FORMULA f)
goal (ul :: [(Named (FORMULA f), [(Token, PRED_NAME)])]
ul, rl :: [Named (FORMULA f)]
rl) -> case Named (FORMULA f) -> FORMULA f
forall s a. SenAttr s a -> s
sentence Named (FORMULA f)
goal of
                     Quantification Universal varDecl :: [VAR_DECL]
varDecl _ _ ->
                         ((Named (FORMULA f)
goal, [VAR_DECL] -> [(Token, PRED_NAME)]
flatVAR_DECLs [VAR_DECL]
varDecl) (Named (FORMULA f), [(Token, PRED_NAME)])
-> [(Named (FORMULA f), [(Token, PRED_NAME)])]
-> [(Named (FORMULA f), [(Token, PRED_NAME)])]
forall a. a -> [a] -> [a]
: [(Named (FORMULA f), [(Token, PRED_NAME)])]
ul, [Named (FORMULA f)]
rl)
                     _ -> ([(Named (FORMULA f), [(Token, PRED_NAME)])]
ul, Named (FORMULA f)
goal Named (FORMULA f) -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. a -> [a] -> [a]
: [Named (FORMULA f)]
rl)) ([], []) [Named (FORMULA f)]
goals

    {- For each constraint we get a list of goals out of uniQuantGoals
    which contain the constraint's newSort. Afterwards all combinations
    are created. -}
    constraintGoals :: [Constraint] -> [[(Named (FORMULA f), [(Token, PRED_NAME)])]]
constraintGoals = [[(Named (FORMULA f), [(Token, PRED_NAME)])]]
-> [[(Named (FORMULA f), [(Token, PRED_NAME)])]]
forall a. [[a]] -> [[a]]
combine
      ([[(Named (FORMULA f), [(Token, PRED_NAME)])]]
 -> [[(Named (FORMULA f), [(Token, PRED_NAME)])]])
-> ([Constraint] -> [[(Named (FORMULA f), [(Token, PRED_NAME)])]])
-> [Constraint]
-> [[(Named (FORMULA f), [(Token, PRED_NAME)])]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Constraint -> [(Named (FORMULA f), [(Token, PRED_NAME)])])
-> [Constraint] -> [[(Named (FORMULA f), [(Token, PRED_NAME)])]]
forall a b. (a -> b) -> [a] -> [b]
map (\ c :: Constraint
c -> ((Named (FORMULA f), [(Token, PRED_NAME)]) -> Bool)
-> [(Named (FORMULA f), [(Token, PRED_NAME)])]
-> [(Named (FORMULA f), [(Token, PRED_NAME)])]
forall a. (a -> Bool) -> [a] -> [a]
filter (((Token, PRED_NAME) -> Bool) -> [(Token, PRED_NAME)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Constraint -> PRED_NAME
newSort Constraint
c PRED_NAME -> PRED_NAME -> Bool
forall a. Eq a => a -> a -> Bool
==) (PRED_NAME -> Bool)
-> ((Token, PRED_NAME) -> PRED_NAME) -> (Token, PRED_NAME) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Token, PRED_NAME) -> PRED_NAME
forall a b. (a, b) -> b
snd) ([(Token, PRED_NAME)] -> Bool)
-> ((Named (FORMULA f), [(Token, PRED_NAME)])
    -> [(Token, PRED_NAME)])
-> (Named (FORMULA f), [(Token, PRED_NAME)])
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named (FORMULA f), [(Token, PRED_NAME)]) -> [(Token, PRED_NAME)]
forall a b. (a, b) -> b
snd)
                                 [(Named (FORMULA f), [(Token, PRED_NAME)])]
uniQuantGoals)
    combis :: [([Constraint], [(Named (FORMULA f), [(Token, PRED_NAME)])])]
combis =
         {- returns big list containing tuples of constraints and a matching
         combination (list) of goals. -}
         ([Constraint]
 -> [([Constraint], [(Named (FORMULA f), [(Token, PRED_NAME)])])])
-> [[Constraint]]
-> [([Constraint], [(Named (FORMULA f), [(Token, PRED_NAME)])])]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ c :: [Constraint]
c -> ([(Named (FORMULA f), [(Token, PRED_NAME)])]
 -> ([Constraint], [(Named (FORMULA f), [(Token, PRED_NAME)])]))
-> [[(Named (FORMULA f), [(Token, PRED_NAME)])]]
-> [([Constraint], [(Named (FORMULA f), [(Token, PRED_NAME)])])]
forall a b. (a -> b) -> [a] -> [b]
map (\ combi :: [(Named (FORMULA f), [(Token, PRED_NAME)])]
combi -> ([Constraint]
c, [(Named (FORMULA f), [(Token, PRED_NAME)])]
combi)) ([[(Named (FORMULA f), [(Token, PRED_NAME)])]]
 -> [([Constraint], [(Named (FORMULA f), [(Token, PRED_NAME)])])])
-> [[(Named (FORMULA f), [(Token, PRED_NAME)])]]
-> [([Constraint], [(Named (FORMULA f), [(Token, PRED_NAME)])])]
forall a b. (a -> b) -> a -> b
$ [Constraint] -> [[(Named (FORMULA f), [(Token, PRED_NAME)])]]
constraintGoals [Constraint]
c)
          [[Constraint]]
sort_gen_axs
    singleDts :: [Constraint]
singleDts = ([Constraint] -> Constraint) -> [[Constraint]] -> [Constraint]
forall a b. (a -> b) -> [a] -> [b]
map [Constraint] -> Constraint
forall a. [a] -> a
head ([[Constraint]] -> [Constraint]) -> [[Constraint]] -> [Constraint]
forall a b. (a -> b) -> a -> b
$ ([Constraint] -> Bool) -> [[Constraint]] -> [[Constraint]]
forall a. (a -> Bool) -> [a] -> [a]
filter [Constraint] -> Bool
forall a. [a] -> Bool
isSingle [[Constraint]]
sort_gen_axs
    indSorts :: Set PRED_NAME
indSorts = [PRED_NAME] -> Set PRED_NAME
forall a. Ord a => [a] -> Set a
Set.fromList ([PRED_NAME] -> Set PRED_NAME) -> [PRED_NAME] -> Set PRED_NAME
forall a b. (a -> b) -> a -> b
$ (Constraint -> PRED_NAME) -> [Constraint] -> [PRED_NAME]
forall a b. (a -> b) -> [a] -> [b]
map Constraint -> PRED_NAME
newSort [Constraint]
singleDts
    (simpleIndGoals :: [(Named (FORMULA f), (Token, PRED_NAME), Constraint)]
simpleIndGoals, rest2 :: [Named (FORMULA f)]
rest2) = ((Named (FORMULA f), [(Token, PRED_NAME)])
 -> ([(Named (FORMULA f), (Token, PRED_NAME), Constraint)],
     [Named (FORMULA f)])
 -> ([(Named (FORMULA f), (Token, PRED_NAME), Constraint)],
     [Named (FORMULA f)]))
-> ([(Named (FORMULA f), (Token, PRED_NAME), Constraint)],
    [Named (FORMULA f)])
-> [(Named (FORMULA f), [(Token, PRED_NAME)])]
-> ([(Named (FORMULA f), (Token, PRED_NAME), Constraint)],
    [Named (FORMULA f)])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (gs :: Named (FORMULA f)
gs, vs :: [(Token, PRED_NAME)]
vs) (ul :: [(Named (FORMULA f), (Token, PRED_NAME), Constraint)]
ul, rl :: [Named (FORMULA f)]
rl) ->
       case ((Token, PRED_NAME) -> Bool)
-> [(Token, PRED_NAME)] -> [(Token, PRED_NAME)]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Bool -> Bool
not (Bool -> Bool)
-> ((Token, PRED_NAME) -> Bool) -> (Token, PRED_NAME) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PRED_NAME -> Set PRED_NAME -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set PRED_NAME
indSorts) (PRED_NAME -> Bool)
-> ((Token, PRED_NAME) -> PRED_NAME) -> (Token, PRED_NAME) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Token, PRED_NAME) -> PRED_NAME
forall a b. (a, b) -> b
snd) [(Token, PRED_NAME)]
vs of
         [] -> ([(Named (FORMULA f), (Token, PRED_NAME), Constraint)]
ul, Named (FORMULA f)
gs Named (FORMULA f) -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. a -> [a] -> [a]
: [Named (FORMULA f)]
rl)
         (v :: Token
v, s :: PRED_NAME
s) : _ -> case (Constraint -> Bool) -> [Constraint] -> Maybe Constraint
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((PRED_NAME -> PRED_NAME -> Bool
forall a. Eq a => a -> a -> Bool
== PRED_NAME
s) (PRED_NAME -> Bool)
-> (Constraint -> PRED_NAME) -> Constraint -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraint -> PRED_NAME
newSort) [Constraint]
singleDts of
           Nothing -> ([(Named (FORMULA f), (Token, PRED_NAME), Constraint)]
ul, Named (FORMULA f)
gs Named (FORMULA f) -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. a -> [a] -> [a]
: [Named (FORMULA f)]
rl)
           Just c :: Constraint
c -> ((Named (FORMULA f)
gs, (Token
v, PRED_NAME
s), Constraint
c) (Named (FORMULA f), (Token, PRED_NAME), Constraint)
-> [(Named (FORMULA f), (Token, PRED_NAME), Constraint)]
-> [(Named (FORMULA f), (Token, PRED_NAME), Constraint)]
forall a. a -> [a] -> [a]
: [(Named (FORMULA f), (Token, PRED_NAME), Constraint)]
ul, [Named (FORMULA f)]
rl)) ([], []) [(Named (FORMULA f), [(Token, PRED_NAME)])]
uniQuantGoals
    toIndPrem :: (SenAttr (FORMULA f) a, (Token, PRED_NAME), Constraint)
-> SenAttr (FORMULA f) a
toIndPrem (gs :: SenAttr (FORMULA f) a
gs, (v :: Token
v, s :: PRED_NAME
s), c :: Constraint
c) =
      let f :: FORMULA f
f = Token -> PRED_NAME -> FORMULA f -> FORMULA f
forall f. Token -> PRED_NAME -> FORMULA f -> FORMULA f
removeVarsort Token
v PRED_NAME
s (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ SenAttr (FORMULA f) a -> FORMULA f
forall s a. SenAttr s a -> s
sentence SenAttr (FORMULA f) a
gs
          sb :: TERM f -> FORMULA f
sb t :: TERM f
t = Token -> PRED_NAME -> TERM f -> FORMULA f -> FORMULA f
forall f.
FormExtension f =>
Token -> PRED_NAME -> TERM f -> FORMULA f -> FORMULA f
substitute Token
v PRED_NAME
s TERM f
t FORMULA f
f
          ps :: [FORMULA f]
ps = [TERM f -> FORMULA f]
-> (Constraint, TERM f -> FORMULA f) -> [FORMULA f]
forall f.
FormExtension f =>
[TERM f -> FORMULA f]
-> (Constraint, TERM f -> FORMULA f) -> [FORMULA f]
mkPrems [TERM f -> FORMULA f
sb] (Constraint
c, TERM f -> FORMULA f
sb)
      in SenAttr (FORMULA f) a
gs { sentence :: FORMULA f
sentence = [FORMULA f] -> FORMULA f
forall f. [FORMULA f] -> FORMULA f
conjunct [FORMULA f]
ps }
    in if Bool
b then
    (([Constraint], [(Named (FORMULA f), [(Token, PRED_NAME)])])
 -> Named (FORMULA f))
-> [([Constraint], [(Named (FORMULA f), [(Token, PRED_NAME)])])]
-> [Named (FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (cons :: [Constraint]
cons, formulas :: [(Named (FORMULA f), [(Token, PRED_NAME)])]
formulas) ->
            let formula :: FORMULA f
formula = [(Constraint, (FORMULA f, (Token, PRED_NAME)))] -> FORMULA f
forall f.
FormExtension f =>
[(Constraint, (FORMULA f, (Token, PRED_NAME)))] -> FORMULA f
instantiateSortGen
                    ([(Constraint, (FORMULA f, (Token, PRED_NAME)))] -> FORMULA f)
-> [(Constraint, (FORMULA f, (Token, PRED_NAME)))] -> FORMULA f
forall a b. (a -> b) -> a -> b
$ ((Constraint, (Named (FORMULA f), [(Token, PRED_NAME)]))
 -> (Constraint, (FORMULA f, (Token, PRED_NAME))))
-> [(Constraint, (Named (FORMULA f), [(Token, PRED_NAME)]))]
-> [(Constraint, (FORMULA f, (Token, PRED_NAME)))]
forall a b. (a -> b) -> [a] -> [b]
map (\ (c :: Constraint
c, (f :: Named (FORMULA f)
f, varsorts :: [(Token, PRED_NAME)]
varsorts)) ->
                       let s :: PRED_NAME
s = Constraint -> PRED_NAME
newSort Constraint
c
                           vs :: Token
vs = PRED_NAME -> [(Token, PRED_NAME)] -> Token
forall t p. (Show t, Eq t) => t -> [(p, t)] -> p
findVar PRED_NAME
s [(Token, PRED_NAME)]
varsorts
                       in (Constraint
c, (Token -> PRED_NAME -> FORMULA f -> FORMULA f
forall f. Token -> PRED_NAME -> FORMULA f -> FORMULA f
removeVarsort Token
vs PRED_NAME
s (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ Named (FORMULA f) -> FORMULA f
forall s a. SenAttr s a -> s
sentence Named (FORMULA f)
f, (Token
vs, PRED_NAME
s))))
                    ([(Constraint, (Named (FORMULA f), [(Token, PRED_NAME)]))]
 -> [(Constraint, (FORMULA f, (Token, PRED_NAME)))])
-> [(Constraint, (Named (FORMULA f), [(Token, PRED_NAME)]))]
-> [(Constraint, (FORMULA f, (Token, PRED_NAME)))]
forall a b. (a -> b) -> a -> b
$ [Constraint]
-> [(Named (FORMULA f), [(Token, PRED_NAME)])]
-> [(Constraint, (Named (FORMULA f), [(Token, PRED_NAME)]))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Constraint]
cons [(Named (FORMULA f), [(Token, PRED_NAME)])]
formulas

                sName :: String
sName = String -> String
forall a. [a] -> [a]
tail (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ ((Named (FORMULA f), [(Token, PRED_NAME)]) -> String)
-> [(Named (FORMULA f), [(Token, PRED_NAME)])] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (('_' Char -> String -> String
forall a. a -> [a] -> [a]
:) (String -> String)
-> ((Named (FORMULA f), [(Token, PRED_NAME)]) -> String)
-> (Named (FORMULA f), [(Token, PRED_NAME)])
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named (FORMULA f) -> String
forall s a. SenAttr s a -> a
senAttr (Named (FORMULA f) -> String)
-> ((Named (FORMULA f), [(Token, PRED_NAME)]) -> Named (FORMULA f))
-> (Named (FORMULA f), [(Token, PRED_NAME)])
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named (FORMULA f), [(Token, PRED_NAME)]) -> Named (FORMULA f)
forall a b. (a, b) -> a
fst) [(Named (FORMULA f), [(Token, PRED_NAME)])]
formulas
                        String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_induction"
            in String -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed String
sName FORMULA f
formula
         ) [([Constraint], [(Named (FORMULA f), [(Token, PRED_NAME)])])]
combis
    else ((Named (FORMULA f), (Token, PRED_NAME), Constraint)
 -> Named (FORMULA f))
-> [(Named (FORMULA f), (Token, PRED_NAME), Constraint)]
-> [Named (FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map (Named (FORMULA f), (Token, PRED_NAME), Constraint)
-> Named (FORMULA f)
forall f a.
FormExtension f =>
(SenAttr (FORMULA f) a, (Token, PRED_NAME), Constraint)
-> SenAttr (FORMULA f) a
toIndPrem [(Named (FORMULA f), (Token, PRED_NAME), Constraint)]
simpleIndGoals [Named (FORMULA f)] -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. [a] -> [a] -> [a]
++ [Named (FORMULA f)]
rest2 [Named (FORMULA f)] -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. [a] -> [a] -> [a]
++ [Named (FORMULA f)]
restGoals