{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}

{- |

Module : ./HasCASL/MatchingWithDefinitions.hs

Description : matching of terms modulo definition expansion

Copyright : (c) Ewaryst Schulz, DFKI Bremen 2010

License : GPLv2 or higher, see LICENSE.txt

Maintainer : ewaryst.schulz@dfki.de

Stability : experimental

Portability : non-portable (see extensions)

Matching of terms modulo constant definition expansion and constraints

-}

module HasCASL.MatchingWithDefinitions where

import HasCASL.Subst

import HasCASL.PrintSubst

import HasCASL.As

import HasCASL.Le

import HasCASL.PrintAs ()

import Common.Id

import Common.ConvertGlobalAnnos ()

import Common.Doc

import Common.DocUtils

import qualified Data.Map as Map

import qualified Data.Set as Set

-- For candidate generation and DG navigation

import Data.List

import Data.Maybe

import Static.DGNavigation

import Logic.Grothendieck

import Logic.Coerce

import HasCASL.Logic_HasCASL

{- | We need two classes:

1. A class for lookup definitions and checking for good functions

2. A class for storing the match (substitution plus constraints)

-}

class DefStore a where

isGood :: a -> Term -> Bool

isMapable :: a -> (Id, TypeScheme) -> Bool

getDefinition :: a -> (Id, TypeScheme) -> Maybe Term

getEnv :: a -> Env

logMsg :: a -> Doc -> IO ()

class Match a where

addMatch :: a -> SubstConst -> Term -> a

addConstraint :: a -> Term -> Term -> a

newtype DefinitionStore = DefinitionStore (Env, Set.Set Symbol)

initialDefStore :: Env -> Set.Set Symbol -> DefinitionStore

initialDefStore e syms = DefinitionStore (e, syms)

instance DefStore DefinitionStore where

isGood _ _ = True

isMapable (DefinitionStore (_, syms)) (opid, typ) =

Set.member (idToOpSymbol opid typ) syms

getDefinition (DefinitionStore (e, _)) = getOpDefinition e

getEnv (DefinitionStore (e, _)) = e

-- logMsg _ _ = return ()

logMsg def d = let e = getEnv def

in appendFile "/tmp/matcher.out" $ (++ "\n") $ show

$ useGlobalAnnos (globAnnos e) d

newtype MatchResult = MatchResult (Subst, [(Term, Term)]) deriving Show

getMatchResult :: MatchResult -> (Subst, [(Term, Term)])

getMatchResult (MatchResult x) = x

emptyMatchResult :: MatchResult

emptyMatchResult = MatchResult (emptySubstitution, [])

instance PrettyInEnv MatchResult where

prettyInEnv e (MatchResult (sb, ctrts)) =

vcat [ prettyInEnv e sb

, if null ctrts then empty else text "Constraints"

, prettyTermMapping e ctrts ]

instance Match MatchResult where

addMatch mr@(MatchResult (sb, ctrts)) sc t =

case lookupContent sb sc of

Just t' | t == t' -> mr

| otherwise ->

addConstraint mr t t'

_ -> MatchResult (addTerm sb sc t, ctrts)

addConstraint (MatchResult (sb, ctrts)) t1 t2 = MatchResult (sb, (t1, t2) : ctrts)

{- | The rules of matching:

f,g are functions

c is a constant

v is a variable

t1, t2 are arbitrary terms

"good" functions are the list-constructor, the solidworks datatype constructors and all other constructors.

f != g

1a. f(x_i) f(y_i) -> match x_i y_i, if f is a "good" function

AddConstraint f(x_i) = f(y_i), otherwise

1b. f(...) g(...) -> AddConstraint f(...) = g(...)

2a. c t2 -> match t1 t2, if c is defined by term t1

AddMatch c t2, if c is mapable

AddConstraint c = t2, otherwise

2b. t1 c -> match t1 t2, if c is defined by term t2

AddConstraint t1 = c, otherwise

3. v t2 -> AddMatch v t2

-}

match :: (DefStore d, Match a) => d -> a -> Term -> Term -> IO (Either String a)

match def mtch t1 t2 =

case (t1, t2) of

-- handle the 'skip-cases' first

(TypedTerm term _ _ _, _) -> match' term t2 -- logg "typed1" $ match' term t2

(_, TypedTerm term _ _ _) -> match' t1 term -- logg "typed2" $ match' t1 term

-- check for clash, handle constraints and definition expansion

(ApplTerm f1 a1 _, _) ->

case t2 of

ApplTerm f2 a2 _

-- 1a1.

| f1 == f2 && isGood def f1 -> logg msg1a1 $ match' a1 a2

-- 1a2., 1b.

| otherwise -> logg msg1a21b addLocalConstraint

-- eventually 2b.

_ -> logg msg2b tryDefExpand2

(TupleTerm l _, _) ->

case t2 of

TupleTerm l' _ | length l == length l' ->

logg msg1aT $ matchfold mtch $ zip l l'

| otherwise ->

logg "tclash" tupleClash

-- eventually 2b.

_ -> logg msg2bT tryDefExpand2

-- 3.: add the mapping v->t2 to output

(QualVar v, _) -> logg "mapped" $ addMapping v

-- 2a.: follow the definition of pattern

(QualOp _ (PolyId opid _ _) typ _ _ _, _) ->

logg msg2a $ tryDefExpand1 (opid, typ)

-- all other terms are not expected and accepted here

_ -> return $ Left "match: unhandled term"

where match' = match def mtch

{- The definition expansion application case

(for ApplTerm and TupleTerm) is handled uniformly -}

tryDefExpand1 oi = case getTermDef t1 of

Just t1' -> match' t1' t2

_ | isMapable def oi -> addMapping oi

| otherwise -> addLocalConstraint

tryDefExpand2 = case getTermDef t2 of

Just t2' -> match' t1 t2'

_ -> addLocalConstraint

getTermDef t = getTermOp t >>= getDefinition def

addLocalConstraint

-- Do not add constraints for equal terms

| t1 == t2 = return $ Right mtch

| otherwise = return $ Right $ addConstraint mtch t1 t2

addMapping t = return $ Right $ addMatch mtch (toSC t) t2

matchfold mtch' (x : l) = do

res <- uncurry (match def mtch') x

case res of

Right mtch'' -> matchfold mtch'' l

err -> return err

matchfold mtch' [] = return $ Right mtch'

-- clash = return $ Left $ "match: Clash for " ++ show (pretty (t1,t2))

tupleClash = return $ Left $ "match: Clash for tuples "

++ show (pretty (t1, t2))

-- Logging stuff

logg s a = do

let e = getEnv def

logMsg def $ text "Log" <+> text s

$++$ text "t1:" $+$ prettyInEnv e t1 $++$ text "t2:"

$+$ prettyInEnv e t2 $++$ text "==============="

a

msg1a1 = "1a1: good same function"

msg1a21b = "1a2, 1b: not good or not same function"

msg1aT = "1aT: tuple: same tuple"

msg2bT = "2bT:"

msg2a = "2a: pattern constant"

msg2b = "2b: term constant"

-- ----------------------- term tools -------------------------

getTermOp :: Term -> Maybe (Id, TypeScheme)

getTermOp (QualOp _ (PolyId opid _ _) typ _ _ _) = Just (opid, typ)

getTermOp _ = Nothing

getOpInfo :: Env -> (Id, TypeScheme) -> Maybe OpInfo

getOpInfo e (opid, typ) =

case Map.lookup opid (assumps e) of

Just soi ->

let fs = Set.filter f soi

in if Set.null fs then Nothing

else Just $ Set.findMin fs

_ -> Nothing

where

f oi = opType oi == typ

getOpDefinition :: Env -> (Id, TypeScheme) -> Maybe Term

getOpDefinition e t =

case fmap opDefn $ getOpInfo e t of

Just (Definition _ t') -> Just t'

_ -> Nothing

-- * Match Candidates

-- ** 1. Injections

newtype Injection a b = Injection [(a, b)]

instance (Show a, Show b) => Show (Injection a b) where

show (Injection l) = "{" ++ intercalate ", " (map sf l) ++ "}"

where sf (x, y) = show x ++ " --> " ++ show y

toList :: Injection a b -> [(a, b)]

toList (Injection l) = l

insertMapping :: (a, b) -> Injection a b -> Injection a b

insertMapping p (Injection l) = Injection (p : l)

combine :: Injection a b -> Injection a b -> Injection a b

combine (Injection l) (Injection l') = Injection (l ++ l')

singleton :: (a, b) -> Injection a b

singleton p = Injection [p]

-- Build all injections from source list to target list

injections :: [a] -> [b] -> [Injection a b]

injections l l'

| length l > length l' = []

| otherwise =

case l of

[] -> [Injection []]

[x] -> [ singleton (x, y) | y <- l' ]

x : xl -> f [] l'

where

f a (y : b) = f (y : a) b ++

map (insertMapping (x, y)) (injections xl $ a ++ b)

f _ [] = []

crossInjs :: [[Injection a b]] -> [Injection a b]

crossInjs = crosscombine combine

-- Build all combinations from the list of lists

crosscombine :: (a -> a -> a) -> [[a]] -> [a]

crosscombine _ [] = []

crosscombine _ [x] = x

crosscombine f cl@(x : l)

| any null cl = []

| otherwise = [ f a b | a <- x, b <- crosscombine f l ]

-- ** 2. Candidates from operators

{- | Candidate generation

a. For a symbol set make a map from Types to 'MatchOp'-lists: 'typePartition'

b. From two such maps make a list of 'Injection's, each injection is a candidate

(a list of 'MatchOp' pairs, wich will be matched using their definitions):

'candidatesAux'

-}

type MatchOp = (Id, TypeScheme, Term)

instance PrettyInEnv MatchOp where

prettyInEnv e (opid, typ, t) = pretty opid <> text ":" <+> pretty typ

<+> text "=" <+> prettyInEnv e t

candType :: MatchOp -> TypeScheme

candType (_, typ, _) = typ

candTerm :: MatchOp -> Term

candTerm (_, _, t) = t

-- *** a.

typePartition :: ((Id, TypeScheme) -> Maybe Term) -- ^ Definiens extractor

-> (TypeScheme -> Bool) -- ^ Filter predicate for types

-> Set.Set Symbol -- ^ MatchOp symbol set

-> Map.Map TypeScheme [MatchOp]

typePartition df tPred s =

Map.fromListWith (++) $ mapMaybe g $ Set.toList s

where f x = let typ = candType x

in if tPred typ then Just (typ, [x]) else Nothing

g x = candFromSymbol df x >>= f

candFromSymbol :: ((Id, TypeScheme) -> Maybe Term) -- ^ Definiens extractor

-> Symbol -> Maybe MatchOp

candFromSymbol df (Symbol {symName = opid, symType = OpAsItemType typ}) =

fmap ((,,) opid typ) $ df (opid, typ)

candFromSymbol _ _ = Nothing

-- *** b.

candidatesAux :: Map.Map TypeScheme [MatchOp]

-> Map.Map TypeScheme [MatchOp]

-> [Injection MatchOp MatchOp]

candidatesAux patMap cMap = crossInjs $ Map.foldWithKey f [] patMap where

f typ l injL = let l' = Map.findWithDefault err typ cMap

err = error $ "candidates: No concrete ops for type: "

++ show (pretty typ)

in injections l l' : injL

candidates :: ((Id, TypeScheme) -> Maybe Term) -- ^ Definiens extractor

-> (TypeScheme -> Bool) -- ^ Filter predicate for types

-> Set.Set Symbol -> Set.Set Symbol -> [[(MatchOp, MatchOp)]]

candidates df tPred s1 s2 = map toList $ candidatesAux tp1 tp2

where (tp1, tp2) = (typePartition df tPred s1, typePartition df tPred s2)

-- ** 3. Matching of candidates

matchCandidate :: (DefStore d) => d -> [(MatchOp, MatchOp)]

-> IO (Either String MatchResult)

matchCandidate def = f emptyMatchResult where

f mtch [] = return $ Right mtch

f mtch ((pat, c) : l) = do

let e = getEnv def

logMsg def $ text "Matching Candidate Pattern"

$+$ prettyInEnv e pat $+$ text " with" $+$ prettyInEnv e c

res <- match def mtch (candTerm pat) $ candTerm c

case res of

Right mtch' -> f mtch' l

x -> return x

matchCandidates :: (DefStore d) => d -> [[(MatchOp, MatchOp)]]

-> IO (Either String MatchResult, [[(MatchOp, MatchOp)]])

matchCandidates _ [] = return (Left "matchCandidates: Out of candidates", [])

matchCandidates def (cand : l) = do

res <- matchCandidate def cand

case res of

Left _ -> matchCandidates def l

x -> return (x, l)

getCandidates :: (DefStore d, DevGraphNavigator nav) =>

d -> nav

-> (TypeScheme -> Bool) -- ^ Filter predicate for types

-> String -- ^ Name of pattern spec

-> String -- ^ Name of concrete spec

-> Maybe [[(MatchOp, MatchOp)]]

getCandidates def dgnav tFilter patN cN =

let

-- g s dgnav' = getInLibEnv dgnav' lookupLocalNodeByName s

g = getNamedSpec

f s = fromSearchResult (g s) getLocalSyms dgnav

mGp = f patN

mGc = f cN

pSyms = Set.map gsymToSym $ fromJust mGp

cSyms = Set.map gsymToSym $ fromJust mGc

cands = candidates (getDefinition def) tFilter pSyms cSyms

in if isJust mGp && isJust mGc then Just cands else Nothing

-- | Utility function for symbol conversion

gsymToSym :: G_symbol -> Symbol

gsymToSym (G_symbol lid sym) = coerceSymbol lid HasCASL sym

{- | The main matching function using specifications:

The pattern specification is expected to be a parameterized specification

containing the constants to be mapped in the actual parameter specification.

The candidates for the matching stem from those operators which have a

definition and a certain type satisfying the given type predicate.

A typical such predicate is:

'(flip elem ["typename1", "typename2", ...]) . show . pretty'

Only operators with the same type can be matched, and all possible

combinations of matching candidates are computed.

With the given Number (> 0) you can constrain the number of candidates to

try before giving up the matching (0 means all candidates).

If one candidate gives a correct match result the following candidates are

not tried and the 'MatchResult' is returned together with the list of non

tried candidates.

-}

matchSpecs :: (DefStore d, DevGraphNavigator nav) =>

d -> nav

-> (TypeScheme -> Bool) -- ^ Filter predicate for types

-> Int -- ^ Number of candidates to try

-> String -- ^ Name of pattern spec

-> String -- ^ Name of concrete spec

-> IO (Either String MatchResult, [[(MatchOp, MatchOp)]])

matchSpecs def dgnav tFilter n patN cN =

case getCandidates def dgnav tFilter patN cN of

Nothing -> return (Left "matchSpecs: specs not found.", [])

Just cl

| null cl ->

return (Left "matchSpecs: no candidates available.", [])

| otherwise -> do

let (cands, remC) = if n > 0 then splitAt n cl else (cl, [])

(mr, l) <- matchCandidates def cands

return (mr, l ++ remC)