From c7ed12eb8a885ae5f9c5be727550702402f93fe6 Mon Sep 17 00:00:00 2001 From: mscodescu Date: Fri, 11 May 2018 08:26:34 +0200 Subject: [PATCH 1/5] first try to see how this would work --- Logic/Logic.hs | 3 +++ OWL2/AS.hs | 3 +++ OWL2/Logic_OWL2.hs | 1 + Static/AnalysisLibrary.hs | 12 ++++++--- Static/AnalysisStructured.hs | 44 ++++++++++++++++++++++++++++-- Syntax/AS_Library.der.hs | 50 +++++++++++++++++++++++++++++++++++ Syntax/AS_Structured.der.hs | 1 + Syntax/Print_AS_Structured.hs | 1 + 8 files changed, 110 insertions(+), 5 deletions(-) diff --git a/Logic/Logic.hs b/Logic/Logic.hs index 4695d4088b..0071806bb7 100644 --- a/Logic/Logic.hs +++ b/Logic/Logic.hs @@ -387,6 +387,9 @@ class (Language lid, Category sign morphism, Ord sentence, -- | combine two symbols into another one pair_symbols :: lid -> symbol -> symbol -> Result symbol pair_symbols lid _ _ = error $ "pair_symbols nyi for logic " ++ show lid + -- | rename a symbol + rename_symbol :: lid -> symbol -> Id -> symbol + rename_symbol lid _ _ = error $ "symbol renaming nyi for logic " ++ show lid -- | makes a singleton list from the given value singletonList :: a -> [a] diff --git a/OWL2/AS.hs b/OWL2/AS.hs index 21aaa41e7c..fc3a8079be 100644 --- a/OWL2/AS.hs +++ b/OWL2/AS.hs @@ -354,6 +354,9 @@ mkEntity = Entity Nothing mkEntityLbl :: String -> EntityType -> IRI -> Entity mkEntityLbl = Entity . Just +renEntity :: Entity -> Id -> Entity +renEntity e i = e{cutIRI = idToIRI i} + instance Ord Entity where compare (Entity _ ek1 ir1) (Entity _ ek2 ir2) = compare (ek1, ir1) (ek2, ir2) diff --git a/OWL2/Logic_OWL2.hs b/OWL2/Logic_OWL2.hs index 83615b503d..c19b6d1694 100644 --- a/OWL2/Logic_OWL2.hs +++ b/OWL2/Logic_OWL2.hs @@ -108,6 +108,7 @@ instance Sentences OWL2 Axiom Sign OWLMorphism Entity where symKind OWL2 = takeWhile isAlpha . showEntityType . entityKind symsOfSen OWL2 _ = Set.toList . symsOfAxiom pair_symbols OWL2 = pairSymbols + rename_symbol OWL2 = renEntity inducedFromToMor :: Map.Map RawSymb RawSymb -> ExtSign Sign Entity -> diff --git a/Static/AnalysisLibrary.hs b/Static/AnalysisLibrary.hs index 2564176bc8..ff0822ba95 100644 --- a/Static/AnalysisLibrary.hs +++ b/Static/AnalysisLibrary.hs @@ -159,10 +159,16 @@ anaStringAux mln lgraph opts topLns initDG mt file posFileName (_, libenv) $ concatMap (getSpecDef . item) is' declNs = Set.fromList . map expnd $ concatMap (getDeclSpecNames . item) is' - missNames = Set.toList $ spNs Set.\\ declNs + -- all missing names + missNames' = spNs Set.\\ declNs + -- if a missing name appears as argument of a generic spec, mark it as unsolved iri + (unsolvedNames, is'') = foldl (\(nl, il) li -> let (n, i') = getGenSpecArgNames $ item li + in (n:nl, il ++ [li{item = i'}])) ([],[]) is' + -- the missing names that are not unsolved iris must be solved as downloads + missNames = Set.toList $ missNames' Set.\\ (Set.fromList $ concat unsolvedNames) unDecls = map (addDownload True) $ filter (isNothing . (`lookupGlobalEnvDG` initDG)) missNames - is = unDecls ++ is' + is = unDecls ++ is'' spN = convertFileToLibStr file noLibName = getLibId pln == nullIRI nIs = case is of @@ -376,7 +382,7 @@ expCurieT ga eo = liftR . expCurieR ga eo anaLibItem :: LogicGraph -> HetcatsOpts -> LNS -> LibName -> LibEnv -> DGraph -> ExpOverrides -> LIB_ITEM -> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides) -anaLibItem lg opts topLns currLn libenv dg eo itm = +anaLibItem lg opts topLns currLn libenv dg eo itm = case itm of Spec_defn spn2 gen asp pos -> do let spn' = if null (iriToStringUnsecure spn2) then diff --git a/Static/AnalysisStructured.hs b/Static/AnalysisStructured.hs index b841b96448..0a9b8f2261 100644 --- a/Static/AnalysisStructured.hs +++ b/Static/AnalysisStructured.hs @@ -523,7 +523,7 @@ anaSpecAux conser addSyms optNodes lg anaSpecTop conser addSyms lg libEnv ln dg nsig name opts eo (item asp) rg return (Group (replaceAnnoted sp' asp) pos, nsig', dg') - Spec_inst spname' afitargs mImp pos0 -> do + s@(Spec_inst spname' afitargs mImp pos0) -> do spname <- expCurieR (globalAnnos dg) eo spname' let pos = if null afitargs then iriPos spname else pos0 adjustPos pos $ case lookupGlobalEnvDG spname dg of @@ -1117,8 +1117,12 @@ anaAllFitArgs lg libEnv opts eo ln dg nsig name spname gs@(ExtGenSig (GenSig imps params _) _) afitargs = do let fitargs = map item afitargs + -- first solve Unsolved_IRIs: for now, always generate specs. Have to think how to call analysis of download_items from this level. + fitargs'' <- solveIRIs lg libEnv opts eo ln dg nsig name spname gs $ zip params fitargs + -- there is a duplication: during solveIRIs we actually do the analysis of the argument and then we analyze again the generated spec + -- but this was the simplest way to try if things work (fitargs', dg', args, _) <- foldM (anaFitArgs lg libEnv opts eo ln spname imps) - ([], dg, [], extName "Actuals" name) (zip params fitargs) + ([], dg, [], extName "Actuals" name) (zip params fitargs'') let actualargs = reverse args (gsigma', morDelta) <- applyGS lg gs actualargs gsigmaRes <- gsigUnionMaybe lg True nsig gsigma' @@ -1128,6 +1132,42 @@ anaAllFitArgs lg libEnv opts eo ln dg nsig name spname return ( zipWith replaceAnnoted (reverse fitargs') afitargs, dg3 , (morDelta, gsigma', ns)) +solveIRIs :: LogicGraph -> LibEnv -> HetcatsOpts -> ExpOverrides -> LibName -> DGraph + -> MaybeNode + -> NodeName -> IRI -> ExtGenSig -> [(NodeSig, FIT_ARG)] -> Result [FIT_ARG] +solveIRIs lg libEnv opts eo ln dg nsig name spname gs args = do -- TODO: remove unneeded arguments + fitargs <- mapM (solveIRI lg libEnv opts eo ln dg nsig name spname gs) args + return fitargs + +solveIRI :: LogicGraph -> LibEnv -> HetcatsOpts -> ExpOverrides -> LibName -> DGraph + -> MaybeNode + -> NodeName -> IRI -> ExtGenSig -> (NodeSig, FIT_ARG) -> Result FIT_ARG +solveIRI lg libEnv opts eo ln dg nsig name spname gs (par, arg) = + case arg of + Fit_spec aspec [] r-> + case item aspec of + Unsolved_IRI x -> do + let gsig = getSig par + gn = getNode par + case gsig of + G_sign lid (ExtSign sig _) _ -> do + let sset = symset_of lid sig + case Set.toList sset of + [sym] -> do + let rsym1 = symbol_to_raw lid sym + rsym2 = symbol_to_raw lid $ rename_symbol lid sym $ iriPath x -- TODO: better conversion from IRI to Id? + fitmor <- induced_from_morphism lid (Map.fromList [(rsym1, rsym2)]) sig + fsens <- case dgn_theory $ labDG dg gn of -- computeTheory libEnv ln gn does not work as the libEnv is empty + G_theory lid1 _ _ _ tsens _ -> coerceThSens lid1 lid "Static.AnalysisStructured.solveIRI" tsens + let tsig = cod fitmor + bspec = case convertTheory lid of + Just f -> f (tsig, toNamedList fsens) + Nothing -> error $ "cannot convert theory to basic spec in logic " ++ show lid + return $ Fit_spec aspec{item = Basic_spec (G_basic_spec lid bspec) nullRange} [] r + _ -> fail $ "try to instantiate a formal parameter with more than one symbol with a single-symbol spec:" ++ show x + _ -> return arg + _ -> return arg + parLink :: LogicGraph -> MaybeNode -> DGLinkOrigin -> NodeSig -> DGraph -> NodeSig -> Result DGraph parLink lg nsig orig (NodeSig node gsigma') dg (NodeSig nA_i sigA_i) = diff --git a/Syntax/AS_Library.der.hs b/Syntax/AS_Library.der.hs index 5a8d050886..39a4bf47c9 100644 --- a/Syntax/AS_Library.der.hs +++ b/Syntax/AS_Library.der.hs @@ -177,6 +177,56 @@ getDeclSpecNames li = case li of Download_items _ di _ -> getImportNames di _ -> [] +getGenSpecArgNames :: LIB_ITEM -> ([IRI], LIB_ITEM) +getGenSpecArgNames li = case li of + Spec_defn sn g as r -> let (iris, s') = getActualParams $ item as + in (iris, Spec_defn sn g as{item = s'} r) + _ -> ([], li) + +getActualParams :: SPEC -> ([IRI], SPEC) +getActualParams sp = + let f c aspec r = let (iris, sp') = getActualParams $ item aspec + in (iris, c aspec{item = sp'} r) + fs c aspecs r = let resl = map (getActualParams.item) aspecs + iris = concat $ map fst resl + aspecs' = map (\(as, s) -> as {item = s}) $ zip aspecs $ map snd resl + in (iris, c aspecs' r) + in case sp of + Extraction aspec r -> f Extraction aspec r + Translation aspec r -> f Translation aspec r + Reduction aspec r -> f Reduction aspec r + Approximation aspec r -> f Approximation aspec r + Minimization aspec r -> f Minimization aspec r + Filtering aspec r -> f Filtering aspec r + Bridge aspec1 rens aspec2 r -> let (iris1, sp1) = getActualParams $ item aspec1 + (iris2, sp2) = getActualParams $ item aspec2 + aspec1' = aspec1{item = sp1} + aspec2' = aspec2{item = sp2} + in (iris1 ++ iris2, Bridge aspec1' rens aspec2' r) + Union aspecs r -> fs Union aspecs r + Intersection aspecs r -> fs Intersection aspecs r + Extension aspecs r -> fs Extension aspecs r + Free_spec aspec r -> f Free_spec aspec r + Cofree_spec aspec r -> f Cofree_spec aspec r + Minimize_spec aspec r -> f Minimize_spec aspec r + Closed_spec aspec r -> f Closed_spec aspec r + Group aspec r -> f Group aspec r + Qualified_spec ld aspec r -> f (Qualified_spec ld) aspec r + Data l1 l2 aspec1 aspec2 r -> let (iris1, sp1) = getActualParams $ item aspec1 + (iris2, sp2) = getActualParams $ item aspec2 + aspec1' = aspec1{item = sp1} + aspec2' = aspec2{item = sp2} + in (iris1 ++ iris2, Data l1 l2 aspec1' aspec2' r) + Spec_inst sn aargs miri r -> let + resL = map (\p -> case p of + Fit_spec aspec [] r' -> + case item aspec of + Spec_inst x [] Nothing _ -> ([x], Fit_spec (aspec{item=Unsolved_IRI x}) [] r') + _ -> ([], p) + _ -> ([],p)) $ map item aargs + in (concat $ map fst resL, Spec_inst sn (map (\(as, s) -> as {item = s}) $ zip aargs $ map snd resL) miri r) + _-> ([], sp) + getImportNames :: DownloadItems -> [IRI] getImportNames di = case di of ItemMaps im -> map (\ (ItemNameMap i mi) -> fromMaybe i mi) im diff --git a/Syntax/AS_Structured.der.hs b/Syntax/AS_Structured.der.hs index f8b2cc376f..d4d8ecdf64 100644 --- a/Syntax/AS_Structured.der.hs +++ b/Syntax/AS_Structured.der.hs @@ -75,6 +75,7 @@ data SPEC = Basic_spec G_basic_spec Range -- pos: "combine" | Apply IRI G_basic_spec Range -- pos: "apply", use a basic spec parser to parse a sentence + | Unsolved_IRI IRI deriving (Show, Typeable) data Network = Network [LABELED_ONTO_OR_INTPR_REF] [IRI] Range diff --git a/Syntax/Print_AS_Structured.hs b/Syntax/Print_AS_Structured.hs index f85f7ec772..561195e0ed 100644 --- a/Syntax/Print_AS_Structured.hs +++ b/Syntax/Print_AS_Structured.hs @@ -120,6 +120,7 @@ printSPEC lg spec = case spec of sep [keyword "apply" <+> pretty i, prettyLG lg $ Basic_spec bs nullRange] Bridge s1 rs s2 _ -> fsep $ [condBraces lg s1, keyword "bridge"] ++ map pretty rs ++ [condBraces lg s2] + Unsolved_IRI i -> keyword "unsolved iri"<+>pretty i instance Pretty Network where pretty (Network cs es _) = fsep $ ppWithCommas cs From c2dbd9065315cfe2e9c3d9a31d8e67345fcc1239 Mon Sep 17 00:00:00 2001 From: mscodescu Date: Fri, 8 Jun 2018 17:40:28 +0200 Subject: [PATCH 2/5] handle compound identifiers --- Common/IRI.hs | 114 +++++++++++++------------- Static/AnalysisLibrary.hs | 164 ++++++++++++++++++++------------------ Syntax/AS_Library.der.hs | 113 +++++++++++++++----------- 3 files changed, 211 insertions(+), 180 deletions(-) diff --git a/Common/IRI.hs b/Common/IRI.hs index 961a186a45..0d42215540 100644 --- a/Common/IRI.hs +++ b/Common/IRI.hs @@ -49,7 +49,7 @@ module Common.IRI , iriParser , angles , iriCurie - , compoundIriCurie + , compoundIriCurie , parseCurie , parseIRICurie , parseIRIReference @@ -64,7 +64,7 @@ module Common.IRI , simpleIdToIRI , deleteQuery , setAngles - + -- * methods from OWL2.AS , isNullIRI , iRIRange @@ -73,30 +73,30 @@ module Common.IRI , showIRIFull , dummyIRI , mkIRI - , idToIRI + , idToIRI , setPrefix ) where -import Text.ParserCombinators.Parsec +import Text.ParserCombinators.Parsec -import Data.Char -import Data.Data -import Data.Ord (comparing) -import Data.Map as Map (Map, lookup) -import Data.Maybe -import Data.List -import qualified Data.Map as Map +import Data.Char +import Data.Data +import Data.List +import Data.Map as Map (Map, lookup) +import qualified Data.Map as Map +import Data.Maybe +import Data.Ord (comparing) -import Control.Monad (when) +import Control.Monad (when) -import OWL2.ColonKeywords -import OWL2.Keywords +import OWL2.ColonKeywords +import OWL2.Keywords -import Common.Id as Id -import Common.Lexer -import Common.Parsec -import Common.Percent -import Common.Token (mixId, comps) +import Common.Id as Id +import Common.Lexer +import Common.Parsec +import Common.Percent +import Common.Token (comps, mixId) -- * The IRI datatype @@ -119,23 +119,23 @@ or the simple IRI data IRI = IRI - { iriScheme :: String -- ^ @foo:@ + { iriScheme :: String -- ^ @foo:@ , iriAuthority :: Maybe IRIAuth -- ^ @\/\/anonymous\@www.haskell.org:42@ - , iriPath :: Id -- ^ local part @\/ghc@ - , iriQuery :: String -- ^ @?query@ - , iriFragment :: String -- ^ @#frag@ - , prefixName :: String -- ^ @prefix@ - , isAbbrev :: Bool -- ^ is the IRI a CURIE or not? - , isBlankNode :: Bool -- ^ is the IRI a blank node? - , hasAngles :: Bool -- ^ IRI in angle brackets - , iriPos :: Range -- ^ position + , iriPath :: Id -- ^ local part @\/ghc@ + , iriQuery :: String -- ^ @?query@ + , iriFragment :: String -- ^ @#frag@ + , prefixName :: String -- ^ @prefix@ + , isAbbrev :: Bool -- ^ is the IRI a CURIE or not? + , isBlankNode :: Bool -- ^ is the IRI a blank node? + , hasAngles :: Bool -- ^ IRI in angle brackets + , iriPos :: Range -- ^ position } deriving (Typeable, Data) -- | Type for authority value within a IRI data IRIAuth = IRIAuth { iriUserInfo :: String -- ^ @anonymous\@@ - , iriRegName :: String -- ^ @www.haskell.org@ - , iriPort :: String -- ^ @:42@ + , iriRegName :: String -- ^ @www.haskell.org@ + , iriPort :: String -- ^ @:42@ } deriving (Eq, Ord, Show, Typeable, Data) -- | Blank IRI @@ -213,7 +213,7 @@ setIRIRange r i = i { iriPos = r } -- | checks if a string (bound to be localPart of an IRI) contains \":\/\/\" cssIRI :: String -> String -cssIRI i +cssIRI i | isInfixOf "://" i = "Full" | otherwise = "Abbreviated" @@ -225,7 +225,7 @@ iRIRange i = let Range rs = iriPos i in case rs of _ -> rs showIRI :: IRI -> String -showIRI i +showIRI i | hasFullIRI i = showIRIFull i | otherwise = showIRICompact i @@ -247,9 +247,9 @@ showIRIFull i = iriToStringFull id i "" -- this should behave like show, and there we use id --- | a default ontology name +-- | a default ontology name dummyIRI :: IRI -dummyIRI = nullIRI { +dummyIRI = nullIRI { iriScheme = "http:" , iriAuthority = Just IRIAuth { iriUserInfo = "" @@ -299,7 +299,7 @@ parseIRICurie = parseIRIAny iriCurie -- Helper function for turning a string into a IRI parseIRIAny :: IRIParser () IRI -> String -> Maybe IRI parseIRIAny parser iristr = case parse (parser << eof) "" iristr of - Left _ -> Nothing + Left _ -> Nothing Right u -> Just u { iriPos = nullRange } -- * IRI parser body based on Parsec elements and combinators @@ -342,10 +342,10 @@ iriWithPos parser = do -- | Parses an IRI reference enclosed in '<', '>' or a CURIE iriCurie :: IRIParser st IRI -iriCurie = angles iriParser <|> curie +iriCurie = angles iriParser <|> curie compoundIriCurie :: IRIParser st IRI -compoundIriCurie = angles iriParser <|> compoundCurie +compoundIriCurie = angles iriParser <|> compoundCurie angles :: IRIParser st IRI -> IRIParser st IRI angles p = char '<' >> fmap (\ i -> i { hasAngles = True }) p << char '>' @@ -388,10 +388,10 @@ referenceAux allowEmpty = iriWithPos $ do { iriPath = stringToId up , iriQuery = uq , iriFragment = uf - , isAbbrev = True + , isAbbrev = True } return iri - + {- | Prefix part of CURIE in @prefix_part:reference@ -} ncname :: GenParser Char st String @@ -590,7 +590,7 @@ iisegment-nz-nc = 1*( iunreserved / pct-encoded / sub-delims / "@" -} idParser :: IRIParser st Id -idParser = mixId ([],[]) ([],[]) +idParser = mixId ([],[]) ([],[]) ipathAbEmpty :: IRIParser st Id ipathAbEmpty = do @@ -605,7 +605,7 @@ ipathAbEmpty1 slash = do Left s -> do char '/' i <- ipathAbEmpty1 False return $ prependString s i - <|> do return $ stringToId "" + <|> do return $ stringToId "" Right i -> return i isegmentorId :: String -> IRIParser st (Either String Id) @@ -614,7 +614,7 @@ isegmentorId lead = return (Left ('/':s)) -- <|> do id <- idParser -- return (Right (prependString "/" id)) - + ipathAbs :: IRIParser st Id ipathAbs = do s <- char '/' <:> option "" ipathRootLess @@ -797,7 +797,7 @@ iriToStringFull iuserinfomap (IRI { iriScheme = scheme , iriQuery = query , iriFragment = fragment , hasAngles = b - }) s = + }) s = (if b then "<" else "") ++ scheme ++ iriAuthToString iuserinfomap authority "" ++ show path ++ query ++ fragment ++ (if b then ">" else "") ++ s @@ -847,11 +847,11 @@ relativeTo ref base just_isegments ref | isJust ( iriAuthority ref ) = just_isegments ref { iriScheme = iriScheme base } - | isDefined $ getFstString $ iriPath ref = + | isDefined $ getFstString $ iriPath ref = just_isegments ref { iriScheme = iriScheme base , iriAuthority = iriAuthority base - , iriPath = if head (getFstString $ iriPath ref) == '/' + , iriPath = if head (getFstString $ iriPath ref) == '/' then iriPath ref else stringToId $ mergePaths base ref } @@ -869,9 +869,9 @@ relativeTo ref base , iriQuery = iriQuery base } where - getFstString anId = case getTokens anId of + getFstString anId = case getTokens anId of (Token s _):_ -> s - _ -> error $ "can't get first string from an empty id" + _ -> error $ "can't get first string from an empty id" just_isegments u = Just $ u { iriPath = removeDotSegments (iriPath u) } mergePaths b r @@ -888,13 +888,13 @@ relativeTo ref base removeDotSegments :: Id -> Id removeDotSegments i = case getTokens i of [] -> error $ "Common/IRI.hs: Cannot remove dots from empty id:" ++ show i - (Token s r):_ -> let + (Token s r):_ -> let t' = Token (removeDotSegmentsString s) r - in simpleIdToId t' + in simpleIdToId t' removeDotSegmentsString :: String -> String removeDotSegmentsString ('/' : ps) = '/' : elimDots ps [] -removeDotSegmentsString ps = elimDots ps [] +removeDotSegmentsString ps = elimDots ps [] -- Second arg accumulates isegments processed so far in reverse order elimDots :: String -> [String] -> String @@ -913,7 +913,7 @@ nextSegment :: String -> (String, String) nextSegment ps = case break (== '/') ps of (r, '/' : ps1) -> (r ++ "/", ps1) - (r, _) -> (r, []) + (r, _) -> (r, []) -- Split last (name) isegment from path, returning (path,name) splitLast :: String -> (String, String) @@ -953,8 +953,8 @@ relativeFrom uabs base i1 = iriPath uabs i2 = iriPath base in case (getTokens i1, getTokens i2) of - ((Token s1 _):_ , (Token s2 _):_) -> - stringToId $ relPathFrom + ((Token s1 _):_ , (Token s2 _):_) -> + stringToId $ relPathFrom (removeBodyDotSegments s1) (removeBodyDotSegments s2) _ -> error $ "empty id:" ++ show i1 ++ " " ++ show i2 @@ -1036,7 +1036,7 @@ This function operates under the invariant that the supplied value of sabs is the desired path relative to the beginning of base. Thus, when base is empty, the desired path has been found. -} difSegsFrom :: String -> String -> String -difSegsFrom sabs "" = sabs +difSegsFrom sabs "" = sabs difSegsFrom sabs base = difSegsFrom ("../" ++ sabs) (snd $ nextSegment base) -- * Other normalization functions @@ -1045,7 +1045,7 @@ difSegsFrom sabs base = difSegsFrom ("../" ++ sabs) (snd $ nextSegment base) to the prefix of @c@ or the concatenation of @i@ and @iriPath c@ is not a valid IRI. -} expandCurie :: Map String IRI -> IRI -> Maybe IRI -expandCurie prefixMap c = +expandCurie prefixMap c = if hasFullIRI c then Just c else case Map.lookup (filter (/= ':') $ prefixName c) prefixMap of Nothing -> Nothing @@ -1074,7 +1074,7 @@ deleteQuery :: IRI -> IRI deleteQuery i = i { iriQuery = "" } addSuffixToIRI :: String -> IRI -> IRI -addSuffixToIRI s i = if not $ null $ iriQuery i +addSuffixToIRI s i = if not $ null $ iriQuery i then i{iriQuery = iriQuery i ++ s} - else + else i{iriPath = appendId (iriPath i) (stringToId s)} diff --git a/Static/AnalysisLibrary.hs b/Static/AnalysisLibrary.hs index ff0822ba95..2dd0741125 100644 --- a/Static/AnalysisLibrary.hs +++ b/Static/AnalysisLibrary.hs @@ -22,61 +22,61 @@ module Static.AnalysisLibrary , LNS ) where -import Logic.Logic -import Logic.Grothendieck -import Logic.Coerce -import Logic.Prover - -import Syntax.AS_Structured -import Syntax.Print_AS_Structured -import Syntax.Print_AS_Library () -import Syntax.AS_Library - -import Static.GTheory -import Static.DevGraph -import Static.DgUtils -import Static.ComputeTheory -import Static.AnalysisStructured -import Static.AnalysisArchitecture -import Static.ArchDiagram (emptyExtStUnitCtx) - -import Common.AS_Annotation hiding (isAxiom, isDef) -import Common.Consistency -import Common.GlobalAnnotations -import Common.ConvertGlobalAnnos -import Common.AnalyseAnnos -import Common.ExtSign -import Common.Result -import Common.ResultT -import Common.LibName -import Common.Id -import Common.IRI -import Common.DocUtils -import qualified Common.Unlit as Unlit -import Common.Utils - -import Driver.Options -import Driver.ReadFn -import Driver.ReadLibDefn -import Driver.WriteLibDefn - -import qualified Data.Map as Map -import qualified Data.Set as Set -import Data.Either (lefts, rights) -import Data.List -import Data.Maybe - -import Control.Monad -import Control.Monad.Trans - -import System.Directory -import System.FilePath - -import LF.Twelf2DG -import Framework.Analysis - -import MMT.Hets2mmt (mmtRes) -import Proofs.ComputeColimit +import Logic.Coerce +import Logic.Grothendieck +import Logic.Logic +import Logic.Prover + +import Syntax.AS_Library +import Syntax.AS_Structured +import Syntax.Print_AS_Library () +import Syntax.Print_AS_Structured + +import Static.AnalysisArchitecture +import Static.AnalysisStructured +import Static.ArchDiagram (emptyExtStUnitCtx) +import Static.ComputeTheory +import Static.DevGraph +import Static.DgUtils +import Static.GTheory + +import Common.AnalyseAnnos +import Common.AS_Annotation hiding (isAxiom, isDef) +import Common.Consistency +import Common.ConvertGlobalAnnos +import Common.DocUtils +import Common.ExtSign +import Common.GlobalAnnotations +import Common.Id +import Common.IRI +import Common.LibName +import Common.Result +import Common.ResultT +import qualified Common.Unlit as Unlit +import Common.Utils + +import Driver.Options +import Driver.ReadFn +import Driver.ReadLibDefn +import Driver.WriteLibDefn + +import Data.Either (lefts, rights) +import Data.List +import qualified Data.Map as Map +import Data.Maybe +import qualified Data.Set as Set + +import Control.Monad +import Control.Monad.Trans + +import System.Directory +import System.FilePath + +import Framework.Analysis +import LF.Twelf2DG + +import MMT.Hets2mmt (mmtRes) +import Proofs.ComputeColimit -- a set of library names to check for cyclic imports type LNS = Set.Set LibName @@ -95,7 +95,7 @@ anaSource mln lg opts topLns libenv initDG origName = ResultT $ do fname = tryToStripPrefix "file://" mName syn = case defSyntax opts of "" -> Nothing - s -> Just $ simpleIdToIRI $ mkSimpleId s + s -> Just $ simpleIdToIRI $ mkSimpleId s lgraph = setSyntax syn $ setCurLogic (defLogic opts) lg fname' <- getContentAndFileType opts fname dir <- getCurrentDirectory @@ -137,7 +137,7 @@ anaString mln lgraph opts topLns libenv initDG input file mr = do let realFileName = curDir file posFileName = case mln of Just gLn | useLibPos opts -> libToFileName gLn - _ -> if checkUri file then file else realFileName + _ -> if checkUri file then file else realFileName lift $ putIfVerbose opts 2 $ "Reading file " ++ file libdefns <- readLibDefn lgraph opts mr file posFileName input when (null libdefns) . fail $ "failed to read contents of file: " ++ file @@ -145,7 +145,7 @@ anaString mln lgraph opts topLns libenv initDG input file mr = do (error "Static.AnalysisLibrary.anaString", libenv) $ case analysis opts of Skip -> [last libdefns] - _ -> libdefns + _ -> libdefns -- | calling static analysis for parsed library-defn anaStringAux :: Maybe LibName -- ^ suggested library name @@ -160,12 +160,20 @@ anaStringAux mln lgraph opts topLns initDG mt file posFileName (_, libenv) declNs = Set.fromList . map expnd $ concatMap (getDeclSpecNames . item) is' -- all missing names - missNames' = spNs Set.\\ declNs - -- if a missing name appears as argument of a generic spec, mark it as unsolved iri - (unsolvedNames, is'') = foldl (\(nl, il) li -> let (n, i') = getGenSpecArgNames $ item li - in (n:nl, il ++ [li{item = i'}])) ([],[]) is' + missNames' = spNs Set.\\ declNs + -- if a missing name appears as argument of a generic spec, + -- mark it as unsolved iri + (unsolvedNames, is'') = foldl (\(nl, il) li -> + let (n, i') = getGenSpecArgNames $ item li + in (n:nl, il ++ [li{item = i'}])) ([],[]) is' -- the missing names that are not unsolved iris must be solved as downloads - missNames = Set.toList $ missNames' Set.\\ (Set.fromList $ concat unsolvedNames) + missIds = concat $ map (\anIri -> getTokens $ iriPath anIri) $ + Set.toList $ missNames' + unsolvedIds = concat $ map (\anIri -> (getTokens $ iriPath anIri) ++ + ( concatMap getTokens $ getComps $ iriPath anIri)) + $ concat unsolvedNames + missNames = map simpleIdToIRI $ + filter (\x -> not $ x `elem` unsolvedIds) missIds unDecls = map (addDownload True) $ filter (isNothing . (`lookupGlobalEnvDG` initDG)) missNames is = unDecls ++ is'' @@ -302,7 +310,7 @@ shortcutUnions dgraph = let spNs = getGlobNodes $ globalEnv dgraph in _ -> False) innNs && case nodeInfo nl of DGNode DGUnion _ -> True - _ -> False + _ -> False -> foldM (\ dg' (s, _, el) -> do newMor <- composeMorphisms (dgl_morphism el) $ dgl_morphism et return $ insLink dg' newMor @@ -382,7 +390,7 @@ expCurieT ga eo = liftR . expCurieR ga eo anaLibItem :: LogicGraph -> HetcatsOpts -> LNS -> LibName -> LibEnv -> DGraph -> ExpOverrides -> LIB_ITEM -> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides) -anaLibItem lg opts topLns currLn libenv dg eo itm = +anaLibItem lg opts topLns currLn libenv dg eo itm = case itm of Spec_defn spn2 gen asp pos -> do let spn' = if null (iriToStringUnsecure spn2) then @@ -452,7 +460,7 @@ anaLibItem lg opts topLns currLn libenv dg eo itm = analyzing opts $ "unit spec " ++ usstr l <- lookupCurrentLogic "Unit_spec_defn" lg (rSig, dg', usp') <- - liftR $ anaUnitSpec lg libenv currLn dg opts eo + liftR $ anaUnitSpec lg libenv currLn dg opts eo usn' (EmptyNode l) Nothing usp unitSig <- liftR $ getUnitSigFromRef rSig let usd' = Unit_spec_defn usn usp' pos @@ -467,7 +475,7 @@ anaLibItem lg opts topLns currLn libenv dg eo itm = rn <- expCurieT (globalAnnos dg) eo rn' let rnstr = iriToStringUnsecure rn l <- lookupCurrentLogic "Ref_spec_defn" lg - (_, _, _, rsig, dg', rsp') <- liftR $ + (_, _, _, rsig, dg', rsp') <- liftR $ anaRefSpec True lg libenv currLn dg opts eo (EmptyNode l) rn emptyExtStUnitCtx Nothing rsp analyzing opts $ "ref spec " ++ rnstr @@ -502,7 +510,7 @@ anaLibItem lg opts topLns currLn libenv dg eo itm = let (cNodes, cEdges) = networkDiagram dg cItems eItems diag = makeDiagram dg cNodes cEdges genv = globalEnv dg - if Map.member nn genv + if Map.member nn genv then liftR $ plain_error (itm, dg, libenv, lg, eo) (alreadyDefined nnstr) pos @@ -546,7 +554,7 @@ anaLibItem lg opts topLns currLn libenv dg eo itm = let is = Map.keys $ globalEnv dg' ks = case is of [_] -> is - _ -> filter (== getLibId ln') is + _ -> filter (== getLibId ln') is in case ks of [j] -> case expCurie (globalAnnos dg) eo i of Nothing -> ([], [prefixErrorIRI i], [i]) @@ -597,14 +605,14 @@ symbolsOf lg gs1@(G_sign l1 (ExtSign sig1 sys1) _) , filter (\ sy -> matches l2 sy r2) $ Set.toList sys2) of ([s1], [s2]) -> return (G_symbol l1 s1, G_symbol l2 s2) - (ll1, ll2) -> + (ll1, ll2) -> plain_error (G_symbol l1 $ head ll1, G_symbol l2 $ head ll2) -- this is a hack! - ("Missing or non-unique symbol match " ++ - "for correspondence\nMatches for first symbol: " ++ + ("Missing or non-unique symbol match " ++ + "for correspondence\nMatches for first symbol: " ++ showDoc rs1 "\n" ++ - showDoc ll1 "\nMatches for second symbol: " ++ + showDoc ll1 "\nMatches for second symbol: " ++ showDoc rs2 "\n" ++ - showDoc ll2 "\n") + showDoc ll2 "\n") nullRange _ -> fail $ "non-unique raw symbols" ps <- symbolsOf lg gs1 gs2 corresps' @@ -624,10 +632,10 @@ anaEntailmentDefn lg ln libEnv dg opts eo en et pos = do spT = item asp2 name = makeName en l <- lookupCurrentLogic "ENTAIL_DEFN" lg - (_spSrc', srcNsig, dg') <- anaSpec False True lg libEnv ln + (_spSrc', srcNsig, dg') <- anaSpec False True lg libEnv ln dg (EmptyNode l) (extName "Source" name) opts eo spS $ getRange spS - (_spTgt', tgtNsig, dg'') <- anaSpec True True lg libEnv ln + (_spTgt', tgtNsig, dg'') <- anaSpec True True lg libEnv ln dg' (EmptyNode l) (extName "Target" name) opts eo spT $ getRange spT incl <- ginclusion lg (getSig tgtNsig) (getSig srcNsig) @@ -910,7 +918,7 @@ anaItemNameOrMap1 libenv ln refDG (genv, dg) (old, new) = do maybeToResult (iriPos new) (iriToStringUnsecure new ++ " already used") $ case Map.lookup new genv of Nothing -> Just () - Just _ -> Nothing + Just _ -> Nothing case entry of SpecEntry extsig -> return $ snd $ refExtsigAndInsert libenv ln refDG (genv, dg) new extsig @@ -990,7 +998,7 @@ expandCurieItemNameMap fn newFn (ItemNameMap i1 mi2) = Nothing -> Right $ ItemNameMap i mi2 Just j -> case expandCurieByPath newFn j of Nothing -> Left $ prefixErrorIRI j - mj -> Right $ ItemNameMap i mj + mj -> Right $ ItemNameMap i mj Nothing -> Left $ prefixErrorIRI i1 itemNameMapsToIRIs :: [ItemNameMap] -> [IRI] diff --git a/Syntax/AS_Library.der.hs b/Syntax/AS_Library.der.hs index 39a4bf47c9..4b02fdef0d 100644 --- a/Syntax/AS_Library.der.hs +++ b/Syntax/AS_Library.der.hs @@ -19,22 +19,22 @@ module Syntax.AS_Library where -- DrIFT command: {-! global: GetRange !-} -import Common.Id -import Common.IRI -import Common.AS_Annotation -import Common.LibName +import Common.AS_Annotation +import Common.Id +import Common.IRI +import Common.LibName -import Data.Maybe -import Data.Typeable +import Data.Maybe +import Data.Typeable -import Logic.Grothendieck -import Logic.Logic +import Logic.Grothendieck +import Logic.Logic -import Syntax.AS_Architecture -import Syntax.AS_Structured +import Syntax.AS_Architecture +import Syntax.AS_Structured -import Framework.AS -import Framework.ATC_Framework () +import Framework.AS +import Framework.ATC_Framework () data LIB_DEFN = Lib_defn LibName [Annoted LIB_ITEM] Range [Annotation] {- pos: "library" @@ -103,8 +103,8 @@ addDownloadAux unique j = let libPath = deleteQuery j query = iriQuery j -- this used to be the fragment i = case query of - "" -> j - "?" -> libPath + "" -> j + "?" -> libPath _ : r -> fromMaybe libPath $ parseIRICurie r in Download_items (iriLibName i) (if unique then UniqueItem i else ItemMaps [ItemNameMap i Nothing]) @@ -149,9 +149,9 @@ data ENTAIL_TYPE = Entail_type OmsOrNetwork OmsOrNetwork Range showAlignArity :: ALIGN_ARITY -> String showAlignArity ar = case ar of - AA_InjectiveAndTotal -> "1" - AA_Injective -> "?" - AA_Total -> "+" + AA_InjectiveAndTotal -> "1" + AA_Injective -> "?" + AA_Total -> "+" AA_NeitherInjectiveNorTotal -> "*" data ItemNameMap = @@ -173,23 +173,25 @@ fromBasicSpec ln sn gbs = getDeclSpecNames :: LIB_ITEM -> [IRI] getDeclSpecNames li = case li of - Spec_defn sn _ _ _ -> [sn] + Spec_defn sn _ _ _ -> [sn] Download_items _ di _ -> getImportNames di - _ -> [] + _ -> [] getGenSpecArgNames :: LIB_ITEM -> ([IRI], LIB_ITEM) getGenSpecArgNames li = case li of - Spec_defn sn g as r -> let (iris, s') = getActualParams $ item as - in (iris, Spec_defn sn g as{item = s'} r) + Spec_defn sn g as r -> + let (iris, s') = getActualParams $ item as + in (iris, Spec_defn sn g as{item = s'} r) _ -> ([], li) getActualParams :: SPEC -> ([IRI], SPEC) -getActualParams sp = +getActualParams sp = let f c aspec r = let (iris, sp') = getActualParams $ item aspec in (iris, c aspec{item = sp'} r) fs c aspecs r = let resl = map (getActualParams.item) aspecs iris = concat $ map fst resl - aspecs' = map (\(as, s) -> as {item = s}) $ zip aspecs $ map snd resl + aspecs' = map (\(as, s) -> as {item = s}) + $ zip aspecs $ map snd resl in (iris, c aspecs' r) in case sp of Extraction aspec r -> f Extraction aspec r @@ -197,12 +199,13 @@ getActualParams sp = Reduction aspec r -> f Reduction aspec r Approximation aspec r -> f Approximation aspec r Minimization aspec r -> f Minimization aspec r - Filtering aspec r -> f Filtering aspec r - Bridge aspec1 rens aspec2 r -> let (iris1, sp1) = getActualParams $ item aspec1 - (iris2, sp2) = getActualParams $ item aspec2 - aspec1' = aspec1{item = sp1} - aspec2' = aspec2{item = sp2} - in (iris1 ++ iris2, Bridge aspec1' rens aspec2' r) + Filtering aspec r -> f Filtering aspec r + Bridge aspec1 rens aspec2 r -> + let (iris1, sp1) = getActualParams $ item aspec1 + (iris2, sp2) = getActualParams $ item aspec2 + aspec1' = aspec1{item = sp1} + aspec2' = aspec2{item = sp2} + in (iris1 ++ iris2, Bridge aspec1' rens aspec2' r) Union aspecs r -> fs Union aspecs r Intersection aspecs r -> fs Intersection aspecs r Extension aspecs r -> fs Extension aspecs r @@ -212,29 +215,49 @@ getActualParams sp = Closed_spec aspec r -> f Closed_spec aspec r Group aspec r -> f Group aspec r Qualified_spec ld aspec r -> f (Qualified_spec ld) aspec r - Data l1 l2 aspec1 aspec2 r -> let (iris1, sp1) = getActualParams $ item aspec1 - (iris2, sp2) = getActualParams $ item aspec2 - aspec1' = aspec1{item = sp1} - aspec2' = aspec2{item = sp2} - in (iris1 ++ iris2, Data l1 l2 aspec1' aspec2' r) - Spec_inst sn aargs miri r -> let - resL = map (\p -> case p of - Fit_spec aspec [] r' -> - case item aspec of - Spec_inst x [] Nothing _ -> ([x], Fit_spec (aspec{item=Unsolved_IRI x}) [] r') - _ -> ([], p) - _ -> ([],p)) $ map item aargs - in (concat $ map fst resL, Spec_inst sn (map (\(as, s) -> as {item = s}) $ zip aargs $ map snd resL) miri r) - _-> ([], sp) + Data l1 l2 aspec1 aspec2 r -> + let (iris1, sp1) = getActualParams $ item aspec1 + (iris2, sp2) = getActualParams $ item aspec2 + aspec1' = aspec1{item = sp1} + aspec2' = aspec2{item = sp2} + in (iris1 ++ iris2, Data l1 l2 aspec1' aspec2' r) + Spec_inst sn aargs miri r -> let + resL = map (\p -> case p of + Fit_spec aspec [] r' -> + case item aspec of + Spec_inst x [] Nothing _ -> + ([x], Fit_spec (aspec{item=Unsolved_IRI x}) [] r') + Spec_inst x aargs' Nothing _ -> + let argSpecs = map (\(Fit_spec aspec' _ _) -> item aspec') $ + map item aargs' + argNames = map (\as -> case as of + Spec_inst y [] Nothing _ -> Just y + _ -> Nothing) argSpecs + in if Nothing `elem` argNames then ([],p) + else + let + iriToToken anIri = idToSimpleId $ iriPath anIri + compId = Id [iriToToken x] + (map (iriPath . fromJust) argNames) + nullRange + cIRI = idToIRI compId + in ([cIRI], + Fit_spec (aspec{item=Unsolved_IRI cIRI}) [] r') + _ -> ([], p) + _ -> ([],p)) $ map item aargs + in (concat $ map fst resL, + Spec_inst sn (map (\(as, s) -> as {item = s}) $ + zip aargs $ map snd resL) miri r) + _-> ([], sp) getImportNames :: DownloadItems -> [IRI] getImportNames di = case di of - ItemMaps im -> map (\ (ItemNameMap i mi) -> fromMaybe i mi) im + ItemMaps im -> map (\ (ItemNameMap i mi) -> fromMaybe i mi) im UniqueItem i -> [i] getOms :: OmsOrNetwork -> [SPEC] getOms o = case o of - MkOms s -> [item s] + MkOms s -> [item s] MkNetwork _ -> [] getSpecDef :: LIB_ITEM -> [SPEC] From 675f43660a08c17d3bcb8705758f552dd1404a52 Mon Sep 17 00:00:00 2001 From: mscodescu Date: Thu, 12 Jul 2018 13:16:45 +0200 Subject: [PATCH 3/5] fixed second issue --- Static/AnalysisLibrary.hs | 17 ++++++++++---- Syntax/AS_Library.der.hs | 49 +++++++++++++++++++++++++-------------- 2 files changed, 43 insertions(+), 23 deletions(-) diff --git a/Static/AnalysisLibrary.hs b/Static/AnalysisLibrary.hs index 2dd0741125..178904f04d 100644 --- a/Static/AnalysisLibrary.hs +++ b/Static/AnalysisLibrary.hs @@ -22,6 +22,8 @@ module Static.AnalysisLibrary , LNS ) where +import Debug.Trace + import Logic.Coerce import Logic.Grothendieck import Logic.Logic @@ -160,20 +162,25 @@ anaStringAux mln lgraph opts topLns initDG mt file posFileName (_, libenv) declNs = Set.fromList . map expnd $ concatMap (getDeclSpecNames . item) is' -- all missing names - missNames' = spNs Set.\\ declNs + missNames' = trace ("declNs:" ++ show declNs) $ spNs Set.\\ declNs -- if a missing name appears as argument of a generic spec, -- mark it as unsolved iri (unsolvedNames, is'') = foldl (\(nl, il) li -> - let (n, i') = getGenSpecArgNames $ item li + let (n, i') = getGenSpecArgNames (Set.toList declNs) $ item li in (n:nl, il ++ [li{item = i'}])) ([],[]) is' -- the missing names that are not unsolved iris must be solved as downloads - missIds = concat $ map (\anIri -> getTokens $ iriPath anIri) $ + missIds = trace ("unsolvedNames:" ++ show unsolvedNames) $ + trace ("missNames':" ++ show missNames') $ + concat $ map (\anIri -> getTokens $ iriPath anIri) $ Set.toList $ missNames' unsolvedIds = concat $ map (\anIri -> (getTokens $ iriPath anIri) ++ ( concatMap getTokens $ getComps $ iriPath anIri)) $ concat unsolvedNames - missNames = map simpleIdToIRI $ - filter (\x -> not $ x `elem` unsolvedIds) missIds + missNames = trace ("unsolvedIds:" ++ show unsolvedIds) $ + trace ("missIds:" ++ show missIds) $ + trace ("unsolvedNames:" ++ show unsolvedNames) $ + map simpleIdToIRI $ + filter (\x -> (not $ x `elem` unsolvedIds) && (not $ (simpleIdToIRI x) `elem` declNs)) missIds unDecls = map (addDownload True) $ filter (isNothing . (`lookupGlobalEnvDG` initDG)) missNames is = unDecls ++ is'' diff --git a/Syntax/AS_Library.der.hs b/Syntax/AS_Library.der.hs index 4b02fdef0d..6125fb3403 100644 --- a/Syntax/AS_Library.der.hs +++ b/Syntax/AS_Library.der.hs @@ -19,6 +19,8 @@ module Syntax.AS_Library where -- DrIFT command: {-! global: GetRange !-} +import Debug.Trace + import Common.AS_Annotation import Common.Id import Common.IRI @@ -177,18 +179,18 @@ getDeclSpecNames li = case li of Download_items _ di _ -> getImportNames di _ -> [] -getGenSpecArgNames :: LIB_ITEM -> ([IRI], LIB_ITEM) -getGenSpecArgNames li = case li of +getGenSpecArgNames :: [IRI] -> LIB_ITEM -> ([IRI], LIB_ITEM) +getGenSpecArgNames knownSpecs li = case li of Spec_defn sn g as r -> - let (iris, s') = getActualParams $ item as + let (iris, s') = getActualParams knownSpecs $ item as in (iris, Spec_defn sn g as{item = s'} r) _ -> ([], li) -getActualParams :: SPEC -> ([IRI], SPEC) -getActualParams sp = - let f c aspec r = let (iris, sp') = getActualParams $ item aspec +getActualParams :: [IRI] -> SPEC -> ([IRI], SPEC) +getActualParams knownSpecs sp = + let f c aspec r = let (iris, sp') = getActualParams knownSpecs $ item aspec in (iris, c aspec{item = sp'} r) - fs c aspecs r = let resl = map (getActualParams.item) aspecs + fs c aspecs r = let resl = map ((getActualParams knownSpecs).item) aspecs iris = concat $ map fst resl aspecs' = map (\(as, s) -> as {item = s}) $ zip aspecs $ map snd resl @@ -201,8 +203,8 @@ getActualParams sp = Minimization aspec r -> f Minimization aspec r Filtering aspec r -> f Filtering aspec r Bridge aspec1 rens aspec2 r -> - let (iris1, sp1) = getActualParams $ item aspec1 - (iris2, sp2) = getActualParams $ item aspec2 + let (iris1, sp1) = getActualParams knownSpecs $ item aspec1 + (iris2, sp2) = getActualParams knownSpecs $ item aspec2 aspec1' = aspec1{item = sp1} aspec2' = aspec2{item = sp2} in (iris1 ++ iris2, Bridge aspec1' rens aspec2' r) @@ -216,23 +218,34 @@ getActualParams sp = Group aspec r -> f Group aspec r Qualified_spec ld aspec r -> f (Qualified_spec ld) aspec r Data l1 l2 aspec1 aspec2 r -> - let (iris1, sp1) = getActualParams $ item aspec1 - (iris2, sp2) = getActualParams $ item aspec2 + let (iris1, sp1) = getActualParams knownSpecs $ item aspec1 + (iris2, sp2) = getActualParams knownSpecs $ item aspec2 aspec1' = aspec1{item = sp1} aspec2' = aspec2{item = sp2} in (iris1 ++ iris2, Data l1 l2 aspec1' aspec2' r) Spec_inst sn aargs miri r -> let - resL = map (\p -> case p of - Fit_spec aspec [] r' -> + resL = map (\p -> trace ("p:" ++ show p) $ case p of + Fit_spec aspec [] r' -> trace ("item aspec:" ++ show (item aspec)) $ case item aspec of Spec_inst x [] Nothing _ -> - ([x], Fit_spec (aspec{item=Unsolved_IRI x}) [] r') - Spec_inst x aargs' Nothing _ -> + if x `elem` knownSpecs then ([],p) + else ([x], Fit_spec (aspec{item=Unsolved_IRI x}) [] r') + Spec_inst x aargs' Nothing _ -> let argSpecs = map (\(Fit_spec aspec' _ _) -> item aspec') $ map item aargs' - argNames = map (\as -> case as of - Spec_inst y [] Nothing _ -> Just y - _ -> Nothing) argSpecs + argNames = concatMap (\as -> case as of + Spec_inst y [] Nothing _ -> [Just y] + {-Spec_inst y aargs'' Nothing _ -> + let argSpecs' = map (\(Fit_spec aspec' _ _) -> item aspec') $ + map item aargs'' + argNames' = map (\as' -> case as' of + Spec_inst z [] Nothing _ -> Just z + _ -> Nothing) argSpecs' + in if Nothing `elem` argNames' + then [Nothing] + else [Just $ idToIRI $ Id [idToSimpleId $ iriPath y] (map (iriPath . fromJust) argNames') nullRange]-} + _ -> [Nothing]) + argSpecs in if Nothing `elem` argNames then ([],p) else let From 6d81409688205fa0ac106dc8a6b4d4f573b785c1 Mon Sep 17 00:00:00 2001 From: mscodescu Date: Fri, 13 Jul 2018 14:37:03 +0200 Subject: [PATCH 4/5] fixed first issue --- Syntax/AS_Library.der.hs | 46 +++++++++++++++++++++------------------- 1 file changed, 24 insertions(+), 22 deletions(-) diff --git a/Syntax/AS_Library.der.hs b/Syntax/AS_Library.der.hs index 6125fb3403..70df16d0a8 100644 --- a/Syntax/AS_Library.der.hs +++ b/Syntax/AS_Library.der.hs @@ -224,30 +224,31 @@ getActualParams knownSpecs sp = aspec2' = aspec2{item = sp2} in (iris1 ++ iris2, Data l1 l2 aspec1' aspec2' r) Spec_inst sn aargs miri r -> let - resL = map (\p -> trace ("p:" ++ show p) $ case p of + resL = map (handleArg knownSpecs) $ map item aargs + in (concat $ map fst resL, + Spec_inst sn (map (\(as, s) -> as {item = s}) $ + zip aargs $ map snd resL) miri r) + _-> ([], sp) + +handleArg :: [IRI] -> FIT_ARG -> ([SPEC_NAME], FIT_ARG) +handleArg knownSpecs p = case p of Fit_spec aspec [] r' -> trace ("item aspec:" ++ show (item aspec)) $ case item aspec of Spec_inst x [] Nothing _ -> if x `elem` knownSpecs then ([],p) else ([x], Fit_spec (aspec{item=Unsolved_IRI x}) [] r') - Spec_inst x aargs' Nothing _ -> - let argSpecs = map (\(Fit_spec aspec' _ _) -> item aspec') $ - map item aargs' - argNames = concatMap (\as -> case as of - Spec_inst y [] Nothing _ -> [Just y] - {-Spec_inst y aargs'' Nothing _ -> - let argSpecs' = map (\(Fit_spec aspec' _ _) -> item aspec') $ - map item aargs'' - argNames' = map (\as' -> case as' of - Spec_inst z [] Nothing _ -> Just z - _ -> Nothing) argSpecs' - in if Nothing `elem` argNames' - then [Nothing] - else [Just $ idToIRI $ Id [idToSimpleId $ iriPath y] (map (iriPath . fromJust) argNames') nullRange]-} - _ -> [Nothing]) - argSpecs + Spec_inst x [aarg] Nothing r'' -> trace "here" $ + let argSpec = (\(Fit_spec aspec' _ _) -> item aspec') $ item aarg + argNames = case argSpec of + Spec_inst y [] Nothing _ -> [Just y] + _ -> [Nothing] in if Nothing `elem` argNames then ([],p) else + if x `elem` knownSpecs then let + [y] = map fromJust argNames + unsolvedAnnoFitSpec = Annoted (Fit_spec (Annoted (Unsolved_IRI y) nullRange [] []) [] nullRange) nullRange [] [] + in ([y], Fit_spec(aspec{item = Spec_inst x [unsolvedAnnoFitSpec] Nothing r''}) [] r') + else let iriToToken anIri = idToSimpleId $ iriPath anIri compId = Id [iriToToken x] @@ -256,12 +257,13 @@ getActualParams knownSpecs sp = cIRI = idToIRI compId in ([cIRI], Fit_spec (aspec{item=Unsolved_IRI cIRI}) [] r') + Spec_inst x aargs' Nothing r -> + let aSpecs = map item aargs' + hSpecs = map (handleArg knownSpecs) aSpecs + in (concatMap fst hSpecs, + Fit_spec (Annoted (Spec_inst x (map (\sp -> Annoted (snd sp) nullRange [] []) hSpecs) Nothing r) nullRange [] []) [] r') _ -> ([], p) - _ -> ([],p)) $ map item aargs - in (concat $ map fst resL, - Spec_inst sn (map (\(as, s) -> as {item = s}) $ - zip aargs $ map snd resL) miri r) - _-> ([], sp) + _ -> ([],p) getImportNames :: DownloadItems -> [IRI] getImportNames di = case di of From 4113b1a1c58647a42d3814347a526e4dbf831d19 Mon Sep 17 00:00:00 2001 From: mscodescu Date: Fri, 13 Jul 2018 14:45:31 +0200 Subject: [PATCH 5/5] removed tracing --- Static/AnalysisLibrary.hs | 15 ++++++++------- Syntax/AS_Library.der.hs | 6 +++--- 2 files changed, 11 insertions(+), 10 deletions(-) diff --git a/Static/AnalysisLibrary.hs b/Static/AnalysisLibrary.hs index 178904f04d..f94de99597 100644 --- a/Static/AnalysisLibrary.hs +++ b/Static/AnalysisLibrary.hs @@ -22,7 +22,7 @@ module Static.AnalysisLibrary , LNS ) where -import Debug.Trace +-- import Debug.Trace import Logic.Coerce import Logic.Grothendieck @@ -162,23 +162,24 @@ anaStringAux mln lgraph opts topLns initDG mt file posFileName (_, libenv) declNs = Set.fromList . map expnd $ concatMap (getDeclSpecNames . item) is' -- all missing names - missNames' = trace ("declNs:" ++ show declNs) $ spNs Set.\\ declNs + missNames' = -- trace ("declNs:" ++ show declNs) $ + spNs Set.\\ declNs -- if a missing name appears as argument of a generic spec, -- mark it as unsolved iri (unsolvedNames, is'') = foldl (\(nl, il) li -> let (n, i') = getGenSpecArgNames (Set.toList declNs) $ item li in (n:nl, il ++ [li{item = i'}])) ([],[]) is' -- the missing names that are not unsolved iris must be solved as downloads - missIds = trace ("unsolvedNames:" ++ show unsolvedNames) $ - trace ("missNames':" ++ show missNames') $ + missIds = -- trace ("unsolvedNames:" ++ show unsolvedNames) $ + -- trace ("missNames':" ++ show missNames') $ concat $ map (\anIri -> getTokens $ iriPath anIri) $ Set.toList $ missNames' unsolvedIds = concat $ map (\anIri -> (getTokens $ iriPath anIri) ++ ( concatMap getTokens $ getComps $ iriPath anIri)) $ concat unsolvedNames - missNames = trace ("unsolvedIds:" ++ show unsolvedIds) $ - trace ("missIds:" ++ show missIds) $ - trace ("unsolvedNames:" ++ show unsolvedNames) $ + missNames = -- trace ("unsolvedIds:" ++ show unsolvedIds) $ + -- trace ("missIds:" ++ show missIds) $ + -- trace ("unsolvedNames:" ++ show unsolvedNames) $ map simpleIdToIRI $ filter (\x -> (not $ x `elem` unsolvedIds) && (not $ (simpleIdToIRI x) `elem` declNs)) missIds unDecls = map (addDownload True) $ filter diff --git a/Syntax/AS_Library.der.hs b/Syntax/AS_Library.der.hs index 70df16d0a8..42fcb0735d 100644 --- a/Syntax/AS_Library.der.hs +++ b/Syntax/AS_Library.der.hs @@ -19,7 +19,7 @@ module Syntax.AS_Library where -- DrIFT command: {-! global: GetRange !-} -import Debug.Trace +-- import Debug.Trace import Common.AS_Annotation import Common.Id @@ -232,12 +232,12 @@ getActualParams knownSpecs sp = handleArg :: [IRI] -> FIT_ARG -> ([SPEC_NAME], FIT_ARG) handleArg knownSpecs p = case p of - Fit_spec aspec [] r' -> trace ("item aspec:" ++ show (item aspec)) $ + Fit_spec aspec [] r' -> -- trace ("item aspec:" ++ show (item aspec)) $ case item aspec of Spec_inst x [] Nothing _ -> if x `elem` knownSpecs then ([],p) else ([x], Fit_spec (aspec{item=Unsolved_IRI x}) [] r') - Spec_inst x [aarg] Nothing r'' -> trace "here" $ + Spec_inst x [aarg] Nothing r'' -> let argSpec = (\(Fit_spec aspec' _ _) -> item aspec') $ item aarg argNames = case argSpec of Spec_inst y [] Nothing _ -> [Just y]