{-# LANGUAGE TypeSynonymInstances, Rank2Types #-}

{- |

Module : $Header$

Description : Test functions for MatchingWithDefinitions

Copyright : (c) Ewaryst Schulz, DFKI Bremen 2010

License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

Maintainer : ewaryst.schulz@dfki.de

Stability : experimental

Portability : portable

Test functions for MatchingWithDefinitions

-}

module HasCASL.InteractiveTests where

import HasCASL.Subst

import HasCASL.PrintSubst

import HasCASL.MatchingWithDefinitions ( initialDefStore

, gsymToSym

, matchSpecs

, matchCandidates

, getCandidates

, getMatchResult

, MatchResult (..)

, DefinitionStore

-- , DefStore(..)

)

import HasCASL.As

import HasCASL.Le

import HasCASL.Logic_HasCASL

import Common.AS_Annotation

import qualified Data.Set as Set

import qualified Data.Map as Map

import Data.Maybe

import Data.List

-- global part imports

import Static.SpecLoader (getSigSensComplete, SigSens (..))

import Data.Time.Clock

import Control.Monad

import Control.Monad.Trans (MonadIO (..))

import Driver.Options

import Common.Utils (getEnvDef)

import Common.Doc

import Common.DocUtils

-- For Navigation

import qualified Data.Graph.Inductive.Graph as Graph

import Static.PrintDevGraph ()

import Static.DevGraph

import Static.DGNavigation

{- testruns:

-- Use this for new testing:

(sigs, dgn) <- env "HasCASL/Real3D/SolidWorks/flange.het" "Component"

sigs <- siggy 4

-- match the concrete design to the pattern

testnewM sigs "FlangePattern" "BoltHole" "Durchgangsloch"

testSpecMatchM sigs "FlangePattern" "Component"

fromSigsNiceL sigs "FlangePattern" "Component" allMatches

fromSigsNice sigs "FlangePattern" "Component" (findMatch noConstraints)

-- shortcut for the above statement

matchDesign "/tmp/flange.het" "Match" "FlangePattern" "Component"

-- get the actual parameter spec of FlangePattern

navi sigs $ getActualParameterSpec "FlangePattern"

-- get the local symbols for the actual parameter spec of FlangePattern

naviGen sigs (show . pretty) $ (\ a -> getLocalSyms a $ fst $ fromJust $ getActualParameterSpec "FlangePattern" a)

(res, m1) <- getMatchMap "/tmp/flange.het" "Match" "FlangePattern" "Component"

tmpl <- readFile "/home/ewaryst/Hets-lib/EnCL/flangeExported.het"

writeFile "/tmp/f1.het" $ processTemplate (\ k v -> " . " ++ k ++ " := " ++ show (v * 1000)) m1 tmpl

-}

help :: IO ()

help = do

s <- readFile "HasCASL/InteractiveTests.hs"

let l = lines s

startP = ("{- testruns:" /=)

endP = ("-}" /=)

putStrLn $ unlines $ takeWhile endP $ dropWhile startP l

-- ----------------------- Global DG functions -------------------------

-- * Point evaluator

type RealType = Double

{-

type EvalEnv = Map.Map String

evalInSubst :: Subst -> Term -> RealType

evalInSubst s t =

case t of

lookupS :: Subst -> a -> Maybe (SRule b)

ruleContent :: SRule a -> a

-}

data Point = P (RealType, RealType, RealType) deriving (Read, Show)

data Vector = V (RealType, RealType, RealType) deriving (Read, Show)

diff :: (Point, Point) -> Vector

diff (p, q) = V (c1 p - c1 q, c2 p - c2 q, c3 p - c3 q)

prod :: (Vector, Vector) -> RealType

prod (V (x1, y1, z1), V (x2, y2, z2)) = x1 * x2 + y1 * y2 + z1 * z2

dist :: (Point, Point) -> RealType

dist (p, q) = sqrt $ prod (diff (p, q), diff (p, q))

diam :: (Point, Point) -> RealType

diam (p, q) = 2 * dist (p, q)

c1 :: Point -> RealType

c1 (P (x, _, _)) = x

c2 :: Point -> RealType

c2 (P (_, x, _)) = x

c3 :: Point -> RealType

c3 (P (_, _, x)) = x

type EvalEnv = Map.Map String EvalTerm

data ETBinFun = ETdiff | ETdiam | ETprod | ETdist deriving Show

data EvalTerm = ETbinary ETBinFun EvalTerm EvalTerm | ETpoint Point

| ETvector Vector | ETreal RealType | ETconst String deriving Show

toEvalTerm :: Env -> Term -> Maybe EvalTerm

toEvalTerm e t =

let s = show $ prettyWithAnnos e t

realL = reads s :: [(RealType, String)]

pointL = reads s :: [(Point, String)]

mT | not (null realL) = Just $ ETreal $ fst $ head realL

| not (null pointL) = Just $ ETpoint $ fst $ head pointL

| otherwise = Nothing

in mT

envFromSubst :: Env -> Subst -> EvalEnv

envFromSubst e (Subst (m, _, _)) = Map.fromList $ mapMaybe f $ Map.toList m

where f (sc, sr) = fmap ((,) $ scName sc) $ toEvalTerm e $ ruleContent sr

etPoint :: EvalTerm -> Point

etPoint (ETpoint p) = p

etPoint et = error $ "etPoint: no point: " ++ show et

etVector :: EvalTerm -> Vector

etVector (ETvector p) = p

etVector et = error $ "etVector: no vector: " ++ show et

etReal :: EvalTerm -> RealType

etReal (ETreal p) = p

etReal et = error $ "etReal: no real: " ++ show et

evalInEnv :: EvalEnv -> EvalTerm -> EvalTerm

evalInEnv e (ETbinary bf t1 t2) =

let t1' = evalInEnv e t1

t2' = evalInEnv e t2

in case bf of

ETprod -> ETreal $ prod (etVector t1', etVector t2')

ETdiam -> ETreal $ diam (etPoint t1', etPoint t2')

ETdist -> ETreal $ dist (etPoint t1', etPoint t2')

ETdiff -> ETvector $ diff (etPoint t1', etPoint t2')

evalInEnv e (ETconst s) =

Map.findWithDefault (error $ "evalInEnv: lookup failure for " ++ s) s e

evalInEnv _ x = x

getRconsts :: Env -> Subst -> Map.Map String RealType

getRconsts e s = getRealConstMap e s constsForEval

getRealConstMap :: Env -> Subst -> [(String, EvalTerm)] -> Map.Map String RealType

getRealConstMap e sbst l = Map.fromList $ map f l where

ee = envFromSubst e sbst

f (s, et) = (s, etReal $ evalInEnv ee et)

evalInSubst :: Env -> Subst -> EvalTerm -> EvalTerm

evalInSubst e s = evalInEnv (envFromSubst e s)

constsForEval :: [(String, EvalTerm)]

constsForEval =

[ ("d_0", ETbinary ETdiam (ETconst "BoundaryTube") (ETconst "Offset"))

, ("d_3", ETbinary ETdiam (ETconst "BoltOffset") (ETconst "Offset"))

, ("d_4", ETbinary ETdiam (ETconst "BoundaryRing") (ETconst "Offset"))

, ("d_5", ETbinary ETdiam (ETconst "BoltBoundary") (ETconst "BoltOffset"))

, ("e_F", ETconst "RingHeight") ]

-- ----------------------- Global DG functions -------------------------

-- * DG Navigation

mkDGNav :: SigSens Env Sentence -> DGNav

mkDGNav s = makeDGNav (sigsensLibenv s) (sigsensDG s) []

prettyEdge :: DGraph -> Graph.LEdge DGLinkLab -> Doc

prettyEdge dg (n1, n2, dgl) =

pretty (dgl_id dgl) <> text ":" <+> text (getNameOfNode n1 dg) <+> text "->"

<+> text (getNameOfNode n2 dg)

prettyNode :: DGraph -> Graph.LNode DGNodeLab -> Doc

prettyNode _ (n, lbl) =

pretty n <> text ":" <+> text (getDGNodeName lbl)

-- | get all ancestor nodes and output them

collectNodes :: DGraph -> [Graph.Node] -> IO ()

collectNodes _ [] = return ()

collectNodes dg nds = do

let ledgs = concatMap (innDG dg) nds

newnds = map linkSource ledgs

showl = map f ledgs

f (x, _, lbl) = show x ++ ":" ++ show (pretty $ dgl_origin lbl)

print showl

collectNodes dg newnds

navi :: SigSens Env Sentence

-> (forall a . DevGraphNavigator a => a -> Maybe (Graph.LNode DGNodeLab))

-> IO ()

navi s = naviGen s pf

where pf x = case x of

Just dgn -> show $ prettyNode (sigsensDG s) dgn

_ -> error "navi: No result."

naviGen :: SigSens Env Sentence -> (b -> String)

-> (forall a . DevGraphNavigator a => a -> b) -> IO ()

naviGen s pf sf =

putStrLn $ pf $ sf $ mkDGNav s

-- removing the additional new dgnavigator from the result

naviSimplify :: (a -> Maybe (b, c)) -> a -> Maybe c

naviSimplify f = fmap snd . f

naviTest :: SigSens Env Sentence -> String -> IO ()

naviTest sigs s =

navi sigs $ naviSimplify $ getActualParameterSpec s

-- collectNodes (sigsensDG sigs) [sigsensNode sigs]

-- ** Spec extraction

testspecs :: [(Int, (String, String))]

testspecs =

[ (1, ("HasCASL/Real3D/SolidWorks/Matchtest.het", "Matching1"))

, (2, ("HasCASL/Real3D/SolidWorks/Matchtest2.het", "Matching0"))

, (3, ("HasCASL/Real3D/SolidWorks/Matchtest2.het", "Matching1"))

, (4, ("HasCASL/Real3D/SolidWorks/flange.het", "Match"))

]

env :: String -> String -> IO (SigSens Env Sentence, DGNav)

env lb sp = do

sigs <- sigsensGen lb sp

return (sigs, mkDGNav sigs)

sigsensGen :: String -> String -> IO (SigSens Env Sentence)

sigsensGen lb sp = do

hlib <- getEnvDef "HETS_LIB" $ error "Missing HETS_LIB environment variable"

let fp = if head lb == '/' then lb else hlib ++ "/" ++ lb

ho = defaultHetcatsOpts { libdirs = [hlib]

, verbose = 0 }

res <- getSigSensComplete False ho HasCASL fp sp

-- putStrLn "\n"

return res { sigsensSignature = (sigsensSignature res) { globAnnos = sigsensGlobalAnnos res } }

siggy :: Int -> IO (SigSens Env Sentence)

siggy = uncurry sigsensGen . libFP

libFP :: Int -> (String, String)

libFP i = fromMaybe (error "libFP: no such spec") $ Prelude.lookup i testspecs

sigsens :: Int -> IO (Env, [Named Sentence])

sigsens i = do

res <- siggy i

return ( sigsensSignature res, sigsensNamedSentences res )

sig :: Int -> IO Env

sig = fmap fst . sigsens

-- Check if the order is broken or not!

sens :: Int -> IO [Named Sentence]

sens = fmap snd . sigsens

cmds :: Int -> IO [Sentence]

cmds = fmap (map sentence) . sens

-- time measurement, pendant of the time shell command

time :: MonadIO m => m a -> m a

time p = do

t <- liftIO getCurrentTime

res <- p

t' <- liftIO getCurrentTime

liftIO $ putStrLn "Time"

liftIO $ print $ diffUTCTime t' t

liftIO $ putStrLn ""

return res

times :: MonadIO m => m a -> m ()

times p = time p >> return ()

-- nice output

niceOut :: Env -> Doc -> IO ()

-- niceOut e = putStrLn . show . useGlobalAnnos (globAnnos e) . pretty

niceOut e x = do

let ga = globAnnos e

{- putStrLn "Global Annotations:"

putStrLn $ show $ pretty $ ga

putStrLn "======================================================================" -}

print $ useGlobalAnnos ga x

prettyWithAnnos :: PrettyInEnv a => Env -> a -> Doc

prettyWithAnnos e = useGlobalAnnos (globAnnos e) . prettyInEnv e

prettyInSigs :: PrettyInEnv a => SigSens Env Sentence -> a -> Doc

prettyInSigs sigs = prettyWithAnnos (sigsensSignature sigs)

nice :: (MonadIO m, PrettyInEnv a) => SigSens Env Sentence -> m a -> m ()

nice sigs x = do

y <- time x

let e = sigsensSignature sigs

liftIO $ niceOut e $ prettyInEnv e y

niceL :: (MonadIO m, PrettyInEnv a) => SigSens Env Sentence -> m [a] -> m ()

niceL sigs l = do

l' <- time l

let e = sigsensSignature sigs

liftIO $ niceOut e $ prettyInEnvList e l'

prettyInEnvList :: PrettyInEnv a => Env -> [a] -> Doc

prettyInEnvList e = vsep . map (prettyInEnv e)

-- ----------------------- New Testsuite -------------------------

typeFilter :: TypeScheme -> Bool

typeFilter = flip elem ["SWExtrusion", "SWCut"] . show . pretty

fromSigsNice :: (PrettyInEnv a) => SigSens Env Sentence -> String -> String

-> (DefinitionStore -> DGNav -> String -> String -> IO a) -> IO ()

fromSigsNice sigs s1 s2 f = nice sigs $ fromSigs sigs s1 s2 f

fromSigsNiceL :: (PrettyInEnv a) => SigSens Env Sentence -> String -> String

-> (DefinitionStore -> DGNav -> String -> String -> IO [a]) -> IO ()

fromSigsNiceL sigs s1 s2 f = niceL sigs $ fromSigs sigs s1 s2 f

fromSigs :: SigSens Env Sentence -> String -> String ->

(DefinitionStore -> DGNav -> String -> String -> IO a) -> IO a

fromSigs sigs s1 s2 f =

case prepareDefStore sigs s1 of

Nothing -> fail $ "Pattern spec " ++ s1 ++ " not found."

Just (def, dgnav) -> f def dgnav s1 s2

-- TODO: use actually not the actual parameter here, but the formal parameter! add to DGNavigation

prepareDefStore :: SigSens Env Sentence -> String -> Maybe (DefinitionStore, DGNav)

prepareDefStore sigs patN =

let e = sigsensSignature sigs

dgnav = mkDGNav sigs

mGsyms = fromSearchResult (getActualParameterSpec patN) getLocalSyms dgnav

f syms = (initialDefStore e $ Set.map gsymToSym syms, dgnav)

in fmap f mGsyms

allMatches :: DefinitionStore -> DGNav

-> String

-> String

-> IO [MatchResult]

allMatches def dgnav patN cN =

let err = error "allMatches: no candidates found."

g [] = return []

g l = do

(res, l') <- matchCandidates def l

case res of

Right mr -> fmap (mr :) $ g l'

_ -> return []

in g $ fromMaybe err $ getCandidates def dgnav typeFilter patN cN

findMatch :: (MatchResult -> Bool) -> DefinitionStore -> DGNav

-> String

-> String

-> IO MatchResult

findMatch p def dgnav patN cN =

let err = error "findMatch: no candidates found."

err' = error "findMatch: no match satisfies predicate."

g [] = err'

g l = do

(res, l') <- matchCandidates def l

case res of

Right mr -> if p mr then return mr else g l'

_ -> err'

in g $ fromMaybe err $ getCandidates def dgnav typeFilter patN cN

noConstraints :: MatchResult -> Bool

noConstraints (MatchResult (_, l)) = null l

testSpecMatchM :: SigSens Env Sentence

-> String

-> String

-> IO ()

testSpecMatchM sigs patN cN =

case prepareDefStore sigs patN of

Nothing -> fail $ "Pattern spec " ++ patN ++ " not found."

Just (def, dgnav) -> do

(res, l) <- matchSpecs def dgnav typeFilter 1 patN cN

(res2, l') <- matchCandidates def l

case res of

Right mr ->

do

putStrLn $ "Non tried elements: " ++ show (length l)

nice sigs $ return mr

Left s ->

unless (null l) $ error "Not all tried!"

putStrLn s

putStrLn "------------------------------"

case res2 of

Right mr ->

do

putStrLn $ "Non tried elements: " ++ show (length l')

nice sigs $ return mr

Left s ->

unless (null l') $ error "Not all tried!"

putStrLn s

-- ----------------------- Template filler -------------------------

processTemplate :: (String -> a -> String) -> Map.Map String a -> String -> String

processTemplate f m s = unlines $ map g $ lines s where

l = Map.toList m

g ln = h ln l

h ln [] = ln

h ln ((k, v) : l')

| isInfixOf k ln = f k v

| otherwise = h ln l'

-- ----------------------- Shortcuts -------------------------

matchDesign :: String -- ^ The filename of the library containing the specs to match

-> String -- ^ The specname importing the specs to match

-> String -- ^ The pattern specname

-> String -- ^ The concrete design specname

-> IO String

matchDesign lb sp patN cN = do

sigs <- sigsensGen lb sp

res <- fromSigs sigs patN cN (findMatch noConstraints)

return $ show $ prettyInSigs sigs res

matchTranslate :: String -- ^ The filename of the library containing the specs to match

-> String -- ^ The specname importing the specs to match

-> String -- ^ The pattern specname

-> String -- ^ The concrete design specname

-> IO String

matchTranslate lb sp patN cN = do

(_, m) <- getMatchMap lb sp patN cN

hlib <- getEnvDef "HETS_LIB" $ error "Missing HETS_LIB environment variable"

tmpl <- readFile $ hlib ++ "/EnCL/flangeExported.het"

let f k v = " . " ++ k ++ " := " ++ show (v * 1000)

return $ processTemplate f m tmpl

getMatchMap :: String -- ^ The filename of the library containing the specs to match

-> String -- ^ The specname importing the specs to match

-> String -- ^ The pattern specname

-> String -- ^ The concrete design specname

-> IO (MatchResult, Map.Map String RealType)

getMatchMap lb sp patN cN = do

sigs <- sigsensGen lb sp

res <- fromSigs sigs patN cN (findMatch noConstraints)

let (sbst, _) = getMatchResult res

rcm = getRconsts (sigsensSignature sigs) sbst

return (res, rcm)

{-

(sigs, dgn) <- env "HasCASL/Real3D/SolidWorks/flange.het" "Component"

pretty $ linkSource $ snd $ fromJust $ searchLink (isJust . dglPredActualParam "FlangePattern") dgn

liftM (pretty . linkSource . snd . fromJust . searchLink (isJust . dglPredActualParam "FlangePattern") . snd) $ env "HasCASL/Real3D/SolidWorks/flange.het" "Component"

Temp -}

printDG :: String -> String -> IO ()

printDG lb sp = sigsensGen lb sp >>= putStrLn . printGE . globalEnv . sigsensDG

printGE :: GlobalEnv -> String

-- printGE = show . pretty

printGE = unlines . map f . Map.toList where

f (s, ge) = show $ pretty s <> text ":" <+> infoEntry ge

infoEntry :: GlobalEntry -> Doc

infoEntry ge = case ge of

SpecEntry egs -> text "SpecEntry" <+> parens (infoEGS egs)

ViewOrStructEntry b evs -> text $ (if b then "View" else "Struct")

++ "Entry"

UnitEntry us -> text "UnitEntry"

ArchOrRefEntry b rs -> text $ (if b then "Arch" else "Ref")

++ "Entry"

infoEGS :: ExtGenSig -> Doc

infoEGS (ExtGenSig gs ns) = sepBySemis [infoGS gs, infoNS ns]

infoGS :: GenSig -> Doc

infoGS (GenSig mn1 nsl mn2) = sepByCommas [infoMN mn1, parens $ sepBySemis $ map infoNS nsl, infoMN mn2]

infoNS :: NodeSig -> Doc

infoNS = pretty . getNode

infoMN :: MaybeNode -> Doc

infoMN (JustNode ns) = infoNS ns

infoMN (EmptyNode _) = text "EmptyNode"

{-

infoEGS :: DevGraphNavigator a => a -> ExtGenSig -> (a, Doc)

infoEGS dgn (ExtGenSig gs ns) = sepBySemis [infoGS gs, infoNS ns]

infoGS :: DevGraphNavigator a => a -> GenSig -> (a, Doc)

infoGS dgn (GenSig mn1 nsl mn2) =

(dgn', dl1) = mapAccumL infoMN dgn [mn1, mn2]

sepByCommas [infoMN mn1, parens $ sepBySemis $ map infoNS nsl, infoMN mn2]

infoNS :: DevGraphNavigator a => a -> NodeSig -> (a, Doc)

infoNS dgn = pretty . getNode

infoMN :: DevGraphNavigator a => a -> MaybeNode -> (a, Doc)

infoMN dgn (JustNode ns) = infoNS ns

infoMN dgn (EmptyNode _) = (dgn, text "EmptyNode")

-- | import, formal parameters and united signature of formal params

data GenSig = GenSig MaybeNode [NodeSig] MaybeNode deriving Show

-- | genericity and body

data ExtGenSig = ExtGenSig GenSig NodeSig deriving Show

-}