Induction.hs revision 3d3889e0cefcdce9b3f43c53aaa201943ac2e895
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul BryanModule : $Header$
9414015dda290f99570edc01b6dbe98f0f4c49c7Laszlo HordosDescription : Derive induction schemes from sort generation constraints
9414015dda290f99570edc01b6dbe98f0f4c49c7Laszlo HordosCopyright : (c) Till Mossakowski, Rainer Grabbe and Uni Bremen 2002-2006
e0a79e452974c14e353e70a43b5beb1afba5342fJason VincentLicense : GPLv2 or higher, see LICENSE.txt
9414015dda290f99570edc01b6dbe98f0f4c49c7Laszlo HordosMaintainer : till@informatik.uni-bremen.de
9414015dda290f99570edc01b6dbe98f0f4c49c7Laszlo HordosStability : provisional
9414015dda290f99570edc01b6dbe98f0f4c49c7Laszlo HordosPortability : portable
9414015dda290f99570edc01b6dbe98f0f4c49c7Laszlo HordosWe provide both second-order induction schemes as well as their
9414015dda290f99570edc01b6dbe98f0f4c49c7Laszlo Hordosinstantiation to specific first-order formulas.
9414015dda290f99570edc01b6dbe98f0f4c49c7Laszlo Hordosmodule CASL.Induction (inductionScheme, generateInductionLemmas) where
9414015dda290f99570edc01b6dbe98f0f4c49c7Laszlo Hordosimport CASL.Quantification (flatVAR_DECLs)
9414015dda290f99570edc01b6dbe98f0f4c49c7Laszlo Hordosimport Common.Utils (combine, number)
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryanimport qualified Data.Set as Set
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan{- | derive a second-order induction scheme from a sort generation constraint
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryanthe second-order predicate variables are represented as predicate
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryansymbols P[s], where s is a sort -}
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo HordosinductionScheme :: FormExtension f => [Constraint] -> FORMULA f
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo HordosinductionScheme constrs =
935bb442e75e8d04a4eda0aca0cfa24cf4c6af6eLaszlo Hordos induction $ map predSubst constrs
e37f4f387b578ba6a967cc9a8b7d79d2ab3508a6omebold where sorts = map newSort constrs
935bb442e75e8d04a4eda0aca0cfa24cf4c6af6eLaszlo Hordos injective = isInjectiveList sorts
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan predSubst constr =
52ac627fd3ec7d31990e454143b1a476284fb3d5Jason Lemay (constr, \ t -> Predication predSymb [t] nullRange)
e0a79e452974c14e353e70a43b5beb1afba5342fJason Vincent predSymb = Qual_pred_name ident typ nullRange
52ac627fd3ec7d31990e454143b1a476284fb3d5Jason Lemay Id ts cs ps =
10a9be648c010204b8ba63b283aa177749227e11Paul Bryan if injective then newSort constr else origSort constr
10a9be648c010204b8ba63b283aa177749227e11Paul Bryan ident = Id [mkSimpleId $ genNamePrefix ++ "P_"
e0a79e452974c14e353e70a43b5beb1afba5342fJason Vincent ++ showId (Id ts [] ps) ""] cs ps
10a9be648c010204b8ba63b283aa177749227e11Paul Bryan typ = Pred_type [newSort constr] nullRange
e0a79e452974c14e353e70a43b5beb1afba5342fJason Vincent{- | Function for derivation of first-order instances of sort generation
b18b5daa8da6584a68cb16eecaa6c4b12ec68fbaBrendan MmillerGiven a list of formulas with a free sorted variable, instantiate the
7523c7f44ed55a9882212a3925629e54c1295daePaul Bryansort generation constraint for this list of formulas
7523c7f44ed55a9882212a3925629e54c1295daePaul BryanIt is assumed that the (original) sorts of the constraint
2ae41f94c30465830758177491494f918a7a79bcLaszlo Hordosmatch the sorts of the free variables -}
7523c7f44ed55a9882212a3925629e54c1295daePaul BryaninstantiateSortGen :: FormExtension f
c843c9cfeb1566e1a4e4ebf0dc019e931dab5182Andi Egloff => [(Constraint, (FORMULA f, (VAR, SORT)))] -> FORMULA f
621b48669f6acb49c11a34c1e93a0e680a88582aChad KienleinstantiateSortGen phis =
e0a79e452974c14e353e70a43b5beb1afba5342fJason Vincent induction (map substFormula phis)
621b48669f6acb49c11a34c1e93a0e680a88582aChad Kienle where substFormula (c, (phi, (v, s))) = (c, \ t -> substitute v s t phi)
e0a79e452974c14e353e70a43b5beb1afba5342fJason Vincent-- | substitute a term for a variable in a formula
100c3de960445a33612602ff02a07eef71963486Phill Cunningtonsubstitute :: FormExtension f => VAR -> SORT -> TERM f -> FORMULA f -> FORMULA f
e0a79e452974c14e353e70a43b5beb1afba5342fJason Vincentsubstitute v s t = foldFormula
93f381e5d31053932f4ffbf07d97b6d8dce32caeJason Vincent (mapRecord id) { foldQual_var = \ t2 v2 s2 _ ->
93f381e5d31053932f4ffbf07d97b6d8dce32caeJason Vincent if v == v2 && s == s2 then t else t2
93f381e5d31053932f4ffbf07d97b6d8dce32caeJason Vincent , foldQuantification = \ t2 q vs p r ->
93f381e5d31053932f4ffbf07d97b6d8dce32caeJason Vincent if elem (v, s) $ flatVAR_DECLs vs
621b48669f6acb49c11a34c1e93a0e680a88582aChad Kienle then t2 else Quantification q vs p r
c843c9cfeb1566e1a4e4ebf0dc019e931dab5182Andi Egloff{- | derive an induction scheme from a sort generation constraint
9c8c2c05a3d08f94d29b4a42b8a0506a4e97e4faLaszlo Hordosusing substitutions as induction predicates -}
9c8c2c05a3d08f94d29b4a42b8a0506a4e97e4faLaszlo Hordosinduction :: FormExtension f => [(Constraint, TERM f -> FORMULA f)] -> FORMULA f
9c8c2c05a3d08f94d29b4a42b8a0506a4e97e4faLaszlo Hordosinduction constrSubsts =
b7dc48d3b8b0550ab1e178408299bed5185ab4a1Bruno Lavit let mkVar i = mkSimpleId ("x_" ++ show i)
9c8c2c05a3d08f94d29b4a42b8a0506a4e97e4faLaszlo Hordos sortInfo = map (\ ((cs, sub), i) -> (sub, (mkVar i, newSort cs)))
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos $ number constrSubsts
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos mkConclusion (subst, v) =
2df9b9c4ff87e7ac55d076945ff1a9922870b4ddAndi Egloff mkForall [uncurry mkVarDecl v] $ subst $ uncurry mkVarTerm v
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos inductionConclusion = conjunct $ map mkConclusion sortInfo
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos inductionPremises = map (mkPrems $ map snd constrSubsts) constrSubsts
2df9b9c4ff87e7ac55d076945ff1a9922870b4ddAndi Egloff inductionPremise = conjunct $ concat inductionPremises
d591ab7a9428501f88bdb3456151ab9018c646e9Laszlo Hordos in mkImpl inductionPremise inductionConclusion
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos{- | construct premise set for the induction scheme
d591ab7a9428501f88bdb3456151ab9018c646e9Laszlo Hordosfor one sort in the constraint -}
904cb62bed9852642ea1d7699cb0515f4f62794aJon BranchmkPrems :: FormExtension f => [TERM f -> FORMULA f]
904cb62bed9852642ea1d7699cb0515f4f62794aJon Branch -> (Constraint, TERM f -> FORMULA f) -> [FORMULA f]
904cb62bed9852642ea1d7699cb0515f4f62794aJon BranchmkPrems substs (constr, sub) = map (mkPrem substs sub) (opSymbs constr)
904cb62bed9852642ea1d7699cb0515f4f62794aJon Branch-- | construct a premise for the induction scheme for one constructor
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo HordosmkPrem :: FormExtension f => [TERM f -> FORMULA f] -> (TERM f -> FORMULA f)
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos -> (OP_SYMB, [Int]) -> FORMULA f
aa26d20912b59f80d1b06b9c0a34c2d4de507a4fLaszlo HordosmkPrem substs subst (opSym@(Qual_op_name _ (Op_type _ argTypes _ _) _), idx) =
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos mkForall qVars phi
aa26d20912b59f80d1b06b9c0a34c2d4de507a4fLaszlo Hordos qVars = map (\ (a, i) -> mkVarDeclStr ("y_" ++ show i) a) $ number argTypes
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan phi = if null indHyps then indConcl
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos else mkImpl (conjunct indHyps) indConcl
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan indConcl = subst $ mkAppl opSym $ map toQualVar qVars
aa26d20912b59f80d1b06b9c0a34c2d4de507a4fLaszlo Hordos indHyps = mapMaybe indHyp (zip qVars idx)
660a40ad15749d74efa0dd4ef12cb8781c570e22Laszlo Hordos indHyp (v1, i) =
aa26d20912b59f80d1b06b9c0a34c2d4de507a4fLaszlo Hordos if i < 0 then Nothing -- leave out sorts from outside the constraint
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan else Just $ (substs !! i) $ toQualVar v1
0bfa6b040942fa10868f2a7c82555652b605a280Travis HallmkPrem _ _ (opSym, _) =
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos error ("CASL.Induction. mkPrems: "
d591ab7a9428501f88bdb3456151ab9018c646e9Laszlo Hordos ++ "unqualified operation symbol occuring in constraint: "
aa26d20912b59f80d1b06b9c0a34c2d4de507a4fLaszlo Hordos ++ show opSym)
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos-- | for goals try to generate additional implications based on induction
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo HordosgenerateInductionLemmas :: FormExtension f => Bool
9c4d05edc8e0887d3aad788027d46d5afedb3ee0Travis Hall -> (Sign f e, [Named (FORMULA f)]) -> (Sign f e, [Named (FORMULA f)])
aa26d20912b59f80d1b06b9c0a34c2d4de507a4fLaszlo HordosgenerateInductionLemmas b (sig, sens) = let
aa26d20912b59f80d1b06b9c0a34c2d4de507a4fLaszlo Hordos sortGens = foldr (\ s cs -> case sentence s of
aa26d20912b59f80d1b06b9c0a34c2d4de507a4fLaszlo Hordos Sort_gen_ax c _ -> c : cs
9c4d05edc8e0887d3aad788027d46d5afedb3ee0Travis Hall _ -> cs) [] axs
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan (axs, goals) = partition isAxiom sens
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos in (sig, (if b then sens else axs)
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos ++ generateInductionLemmasAux b sortGens goals)
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo HordosgenerateInductionLemmasAux
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan :: FormExtension f => Bool
aa26d20912b59f80d1b06b9c0a34c2d4de507a4fLaszlo Hordos -- ^ if True create additional implication otherwise replace goals
aa26d20912b59f80d1b06b9c0a34c2d4de507a4fLaszlo Hordos -> [[Constraint]] -- ^ the constraints of a theory
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan -> [AS_Anno.Named (FORMULA f)] -- ^ all goals of a theory
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos -> [AS_Anno.Named (FORMULA f)]
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos{- ^ all the generated induction lemmas
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryanand the labels are derived from the goal-names -}
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul BryangenerateInductionLemmasAux b sort_gen_axs goals = let
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan findVar s [] = error ("CASL.generateInductionLemmas:\n"
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos ++ "No VAR found of SORT " ++ show s ++ "!")
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos findVar s ((vl, sl) : lst) = if s == sl then vl else findVar s lst
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan removeVarsort v s f = case f of
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan Quantification Universal varDecls formula rng ->
154001a7695db48f5e59bd2978bf3254210feed4Jason Vincent let vd' = newVarDecls varDecls
154001a7695db48f5e59bd2978bf3254210feed4Jason Vincent in if null vd' then formula
154001a7695db48f5e59bd2978bf3254210feed4Jason Vincent else Quantification Universal vd' formula rng
52ac627fd3ec7d31990e454143b1a476284fb3d5Jason Lemay newVarDecls = filter (\ (Var_decl vs _ _) -> not $ null vs) .
52ac627fd3ec7d31990e454143b1a476284fb3d5Jason Lemay map (\ var_decl@(Var_decl vars varsort r) ->
52ac627fd3ec7d31990e454143b1a476284fb3d5Jason Lemay if varsort == s
52ac627fd3ec7d31990e454143b1a476284fb3d5Jason Lemay then Var_decl (filter (/= v) vars) s r
52ac627fd3ec7d31990e454143b1a476284fb3d5Jason Lemay else var_decl)
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan (uniQuantGoals, restGoals) =
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan foldr ( \ goal (ul, rl) -> case sentence goal of
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan Quantification Universal varDecl _ _ ->
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos ((goal, flatVAR_DECLs varDecl) : ul, rl)
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos _ -> (ul, goal : rl)) ([], []) goals
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos {- For each constraint we get a list of goals out of uniQuantGoals
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos which contain the constraint's newSort. Afterwards all combinations
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos are created. -}
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos constraintGoals = combine
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos . map (\ c -> filter (any ((newSort c ==) . snd) . snd)
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos uniQuantGoals)
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos {- returns big list containing tuples of constraints and a matching
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos combination (list) of goals. -}
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos concatMap (\ c -> map (\ combi -> (c, combi)) $ constraintGoals c)
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos singleDts = map head $ filter isSingle sort_gen_axs
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos indSorts = Set.fromList $ map newSort singleDts
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos (simpleIndGoals, rest2) = foldr (\ (gs, vs) (ul, rl) ->
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan case dropWhile (not . (`Set.member` indSorts) . snd) vs of
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan [] -> (ul, gs : rl)
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan (v, s) : _ -> case find ((== s) . newSort) singleDts of
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan Nothing -> (ul, gs : rl)
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan Just c -> ((gs, (v, s), c) : ul, rl)) ([], []) uniQuantGoals
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan toIndPrem (gs, (v, s), c) =
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan let f = removeVarsort v s $ sentence gs
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan sb t = substitute v s t f
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan ps = mkPrems [sb] (c, sb)
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan in gs { sentence = conjunct ps }
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan in if b then
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan map (\ (cons, formulas) ->
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan let formula = instantiateSortGen
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan $ map (\ (c, (f, varsorts)) ->
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan let s = newSort c
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan vs = findVar s varsorts
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan in (c, (removeVarsort vs s $ sentence f, (vs, s))))
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan $ zip cons formulas
47196c962e3caf7cdf7ea5d00ccdefc9f208bdceLaszlo Hordos sName = tail $ concatMap (('_' :) . senAttr . fst) formulas
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan ++ "_induction"
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan in makeNamed sName formula
d3bd4c99b4d249234086d3e694d9c8fb649dcc3ePaul Bryan else map toIndPrem simpleIndGoals ++ rest2 ++ restGoals