diff --git a/Common/Lexer.hs b/Common/Lexer.hs index cfdb27d95e..56362ece35 100644 --- a/Common/Lexer.hs +++ b/Common/Lexer.hs @@ -291,6 +291,10 @@ commaT = asSeparator "," semiT :: CharParser st Token semiT = pToken $ string ";" << notFollowedBy (char ';') +-- a double colon +doubleColonT :: CharParser st Token +doubleColonT = pToken $ string "::" << notFollowedBy (char ':') + oBraceT :: CharParser st Token oBraceT = asSeparator "{" diff --git a/Common/Token.hs b/Common/Token.hs index 2c1e243b41..8a7b57b28e 100644 --- a/Common/Token.hs +++ b/Common/Token.hs @@ -113,14 +113,15 @@ criticalKeywords = terminatingKeywords ++ startingKeywords terminatingKeywords :: [String] terminatingKeywords = [ andS, endS, extractS, fitS, forgetS, hideS, keepS, rejectS, removeS, - revealS, selectS, thenS, withS, withinS, ofS, forS, toS, intersectS] + revealS, selectS, thenS, withS, withinS, ofS, forS, toS, intersectS, + ";", "::"] -- | keywords starting a library item startingKeywords :: [String] startingKeywords = [ archS, fromS, logicS, newlogicS, refinementS, specS, unitS, viewS , ontologyS, alignmentS, networkS, equivalenceS, newcomorphismS - , interpretationS, entailmentS ] + , interpretationS, entailmentS, "pattern" ] -- | keywords that may follow a defining equal sign otherStartKeywords :: [String] diff --git a/Driver/WriteFn.hs b/Driver/WriteFn.hs index ffa16e38dd..eb5af303e1 100644 --- a/Driver/WriteFn.hs +++ b/Driver/WriteFn.hs @@ -302,7 +302,7 @@ writeTheory ins nam opts filePrefix ga (printTheory ms OWL2 $ OWL2.prepareBasicTheory th2) "\n" showDiags opts ds when (null sy) - $ case parse (OWL2.basicSpec Map.empty >> eof) f owltext of + $ case parse ((OWL2.basicSpec True) Map.empty >> eof) f owltext of Left err -> putIfVerbose opts 0 $ show err _ -> putIfVerbose opts 3 $ "reparsed: " ++ f writeVerbFile opts f owltext diff --git a/Logic/ExtSign.hs b/Logic/ExtSign.hs index da50967e16..1a7becca6f 100644 --- a/Logic/ExtSign.hs +++ b/Logic/ExtSign.hs @@ -21,7 +21,6 @@ import Common.DocUtils import Common.ExtSign import Logic.Logic - ext_sym_of :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree @@ -154,7 +153,7 @@ ext_induced_from_to_morphism l r s@(ExtSign p sy) t = do checkExtSign l "from" s checkExtSign l "to" t checkRawMap l r p - checkRawSyms l (Map.elems r) $ nonImportedSymbols t + -- checkRawSyms l (Map.elems r) $ nonImportedSymbols t mor <- induced_from_to_morphism l r s t let sysI = Set.toList $ Set.difference (symset_of l p) sy morM = symmap_of l mor diff --git a/Logic/Logic.hs b/Logic/Logic.hs index 4695d4088b..2a74886bfa 100644 --- a/Logic/Logic.hs +++ b/Logic/Logic.hs @@ -257,6 +257,9 @@ class (Language lid, PrintTypeConv basic_spec, GetRange basic_spec, Just p -> makeDefault (p, pretty) -- | parser for basic specifications parse_basic_spec :: lid -> Maybe (PrefixMap -> AParser st basic_spec) + -- | parser for macros + parse_macro :: lid -> Maybe (PrefixMap -> AParser st basic_spec) + parse_macro _ = Nothing -- | parser for a single symbol returned as list parseSingleSymbItem :: lid -> Maybe (AParser st symb_items) -- | parser for symbol lists @@ -277,6 +280,10 @@ basicSpecParser :: Syntax lid basic_spec symbol symb_items symb_map_items => Maybe IRI -> lid -> Maybe (PrefixMap -> AParser st basic_spec) basicSpecParser sm = fmap fst . parserAndPrinter sm +macroParser :: Syntax lid basic_spec symbol symb_items symb_map_items + => Maybe IRI -> lid -> Maybe (PrefixMap -> AParser st basic_spec) +macroParser _ = parse_macro + basicSpecPrinter :: Syntax lid basic_spec symbol symb_items symb_map_items => Maybe IRI -> lid -> Maybe (basic_spec -> Doc) basicSpecPrinter sm = fmap snd . parserAndPrinter sm @@ -372,6 +379,9 @@ class (Language lid, Category sign morphism, Ord sentence, -- | symbols have a name, see CASL RefMan p. 192 sym_name :: lid -> symbol -> Id sym_name l _ = statError l "sym_name" + -- | allow to change name + rename_symbol :: lid -> symbol -> Id -> symbol + rename_symbol lid _ _ = error $ "symbol renaming nyi for logic " ++ show lid -- | some symbols have a label for better readability sym_label :: lid -> symbol -> Maybe String sym_label _ _ = Nothing @@ -387,6 +397,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 + -- | create symbol from a name and a kind + new_symbol :: lid -> IRI -> String -> symbol + new_symbol _ _ _ = error "new_symbol nyi" -- | makes a singleton list from the given value singletonList :: a -> [a] @@ -481,6 +494,10 @@ class ( Syntax lid basic_spec symbol symb_items symb_map_items convertTheory :: lid -> Maybe ((sign, [Named sentence]) -> basic_spec) convertTheory _ = Nothing + -- | convert a pair of symbols to symb_map_items + convertSymbols :: lid -> Maybe(symbol -> symbol -> symb_map_items) + convertSymbols _ = Nothing + {- ----------------------- amalgamation --------------------------- Computation of colimits of signature diagram. Indeed, it suffices to compute a cocone that is weakly amalgamable @@ -625,6 +642,70 @@ class ( Syntax lid basic_spec symbol symb_items symb_map_items extract_module :: lid -> [IRI] -> (sign, [Named sentence]) -> Result (sign, [Named sentence]) extract_module _ _ = return + -- solving symbols in patterns + solve_symbols :: lid -> Set.Set symbol -> PatternVarMap -> basic_spec -> Result basic_spec + solve_symbols _ _ _ = error "solve_symbols nyi" + -- instantiating macros + instantiate_macro :: lid -> PatternVarMap -> GSubst -> basic_spec -> Result basic_spec + instantiate_macro _ _ _ _ = error "instantiate_macro nyi" + -- delete all occurences of a set of symbols in a solved macro + delete_symbols_macro :: lid -> Set.Set symbol -> basic_spec -> Result basic_spec + delete_symbols_macro _ _ _ = error "delete_symbols_macro nyi" + + +type GSubst = Map.Map (IRI, String) GSubstVal -- TODO: use GSubstVal instead of IRI! + +data GSubstVal = PlainVal IRI | + ListVal String [IRI] -- the string stores the kind! + deriving (Eq, Show) + +getIRIVal :: GSubstVal -> IRI +getIRIVal v = case v of + PlainVal x -> x + _ -> error $ "expecting plain value but got list:" ++ show v + +-- instantiate paramerized names +-- p[X] becomes p[V] if subst maps X to V +-- the string argument is the kind + +instParamName :: GSubst -> IRI -> IRI +instParamName subst p = + p{iriPath = solveId subst (iriPath p)} + +solveId :: GSubst -> Id -> Id +solveId subst t = + case getComps t of + [] -> let tIRI = idToIRI t + k = let tSubsts = filter (\(x,_) -> x == tIRI) $ Map.keys subst + in case tSubsts of + [(_,b)] -> b + []-> "Class" -- does not matter + (_, b):_ -> b + in iriPath $ getIRIVal $ Map.findWithDefault (PlainVal tIRI) (tIRI,k) subst + cs -> let its' = map (solveToken subst) $ getTokens t + ts' = concatMap getTokens its' + cs'' = concatMap getComps its' + cs' = map (solveId subst) cs + in t{getTokens = ts', getComps = cs'' ++ cs'} + +solveToken :: GSubst -> Token -> Id +solveToken subst tok = + let tIRI = idToIRI $ mkId [tok] + k = let tSubsts = filter (\(x,_) -> x == tIRI) $ Map.keys subst + in case tSubsts of + [(_,b)] -> b + []-> "Class" -- does not matter + (_,b):_ -> b + idVal = iriPath $ getIRIVal $ Map.findWithDefault (PlainVal tIRI) (tIRI,k) subst + in idVal --case getComps idVal of + -- [] -> head $ getTokens idVal + -- _ -> error $ "expecting simple id but got a composed one: " ++ show idVal + +type PatternVarMap = Map.Map IRI (Bool, String) +-- Bool is true for list- and false for non-list variables +-- TODO: ideally we should have logic-dependent kinds, but strings will do +-- TODO: this does not allow to have same name for different kinds. +-- One idea would be to work with lists of strings. Future work, should be easy. -- | print a whole theory printTheory :: StaticAnalysis lid basic_spec sentence symb_items symb_map_items diff --git a/OWL2/AS.hs b/OWL2/AS.hs index 21aaa41e7c..6245a006bd 100644 --- a/OWL2/AS.hs +++ b/OWL2/AS.hs @@ -348,6 +348,14 @@ data Entity = Entity , cutIRI :: IRI } deriving (Show, Typeable, Data) +newSymbol :: IRI -> String -> Entity +newSymbol i s = + case s of + "Class" -> mkEntity Class i + "ObjectProperty" -> mkEntity ObjectProperty i + "Individual" -> mkEntity NamedIndividual i + _ -> error $ "nyi:" ++ show s + mkEntity :: EntityType -> IRI -> Entity mkEntity = Entity Nothing @@ -371,6 +379,7 @@ data EntityType = | DataProperty | AnnotationProperty | NamedIndividual + | UnsolvedEntity deriving (Enum, Bounded, Show, Read, Eq, Ord, Typeable, Data) showEntityType :: EntityType -> String @@ -385,6 +394,9 @@ showEntityType e = case e of entityTypes :: [EntityType] entityTypes = [minBound .. maxBound] +renameSymbol :: Entity -> Id -> Entity +renameSymbol e i = e {cutIRI = idToIRI i} + pairSymbols :: Entity -> Entity -> Result Entity -- TODO: improve! pairSymbols (Entity lb1 k1 i1) (Entity lb2 k2 i2) = if k1 /= k2 then @@ -409,7 +421,7 @@ pairSymbols (Entity lb1 k1 i1) (Entity lb2 k2 i2) = data TypedOrUntyped = Typed Datatype | Untyped (Maybe LanguageTag) deriving (Show, Eq, Ord, Typeable, Data) -data Literal = Literal LexicalForm TypedOrUntyped | NumberLit FloatLit +data Literal = Literal LexicalForm TypedOrUntyped | NumberLit FloatLit | LiteralVar IRI deriving (Show, Eq, Ord, Typeable, Data) -- | non-negative integers given by the sequence of digits @@ -515,12 +527,15 @@ type InverseObjectProperty = ObjectPropertyExpression data ObjectPropertyExpression = ObjectProp ObjectProperty | ObjectInverseOf InverseObjectProperty + | ObjectPropertyVar Bool IRI + | UnsolvedObjProp IRI deriving (Show, Eq, Ord, Typeable, Data) objPropToIRI :: ObjectPropertyExpression -> Individual objPropToIRI opExp = case opExp of ObjectProp u -> u ObjectInverseOf objProp -> objPropToIRI objProp + _ -> error "nyi" type DataPropertyExpression = DataProperty @@ -533,10 +548,12 @@ data DataRange = | DataOneOf [Literal] deriving (Show, Eq, Ord, Typeable, Data) --- * CLASS EXPERSSIONS +-- * CLASS EXPRESSIONS data ClassExpression = Expression Class + | UnsolvedClass IRI + | VarExpression MVarOrTerm | ObjectJunction JunctionType [ClassExpression] | ObjectComplementOf ClassExpression | ObjectOneOf [Individual] @@ -549,6 +566,19 @@ data ClassExpression = | DataCardinality (Cardinality DataPropertyExpression DataRange) deriving (Show, Eq, Ord, Typeable, Data) +data MVarOrTerm = MVar Bool IRI | MUnion IRI IRI + -- the name of the head and the name of the tail TODO: should be extended with other terms + -- True for lists! + deriving (Show, Eq, Ord, Typeable, Data) + +-- * INDIVIDUAL EXPRESSIONS + +data IndExpression = + IndAsExpression Individual + | UnsolvedInd IRI + | IndVar IRI + deriving (Show, Eq, Ord, Typeable, Data) + -- * ANNOTATIONS data Annotation = Annotation [Annotation] AnnotationProperty AnnotationValue diff --git a/OWL2/DMU2OWL2.hs b/OWL2/DMU2OWL2.hs index 244b798fa3..1459a4b534 100644 --- a/OWL2/DMU2OWL2.hs +++ b/OWL2/DMU2OWL2.hs @@ -81,7 +81,7 @@ runOntoDMU str = if null str then return "" else do return out readOWL :: Monad m => String -> m (Sign, [Named Axiom]) -readOWL str = case runParser (liftM2 const (basicSpec Map.empty) eof) () "" str of +readOWL str = case runParser (liftM2 const ((basicSpec True) Map.empty) eof) () "" str of Left er -> fail $ show er Right ontoFile -> let newont = function Expand (StringMap $ prefixDeclaration ontoFile) ontoFile diff --git a/OWL2/Function.hs b/OWL2/Function.hs index 2206c0254d..306952ee2b 100644 --- a/OWL2/Function.hs +++ b/OWL2/Function.hs @@ -134,6 +134,7 @@ instance Function ObjectPropertyExpression where function t s opr = case opr of ObjectProp op -> ObjectProp $ cutWith ObjectProperty t s op ObjectInverseOf op -> ObjectInverseOf $ function t s op + _ -> error $ show opr instance Function DataRange where function t s dra = case dra of @@ -162,6 +163,7 @@ instance Function ClassExpression where $ function t s l DataCardinality (Cardinality ct i dp mdr) -> DataCardinality $ Cardinality ct i (cutWith DataProperty t s dp) $ maybeDo t s mdr + _ -> error $ show cle instance Function Annotation where function t s (Annotation al ap av) = Annotation (map (function t s) al) diff --git a/OWL2/Logic_OWL2.hs b/OWL2/Logic_OWL2.hs index 27dc614f50..1c0d4e009b 100644 --- a/OWL2/Logic_OWL2.hs +++ b/OWL2/Logic_OWL2.hs @@ -57,6 +57,9 @@ import OWL2.Symbols import OWL2.Taxonomy import OWL2.Theorem import OWL2.ExtractModule +-- import OWL2.Macros + +import Debug.Trace data OWL2 = OWL2 @@ -86,9 +89,10 @@ instance Monoid OntologyDocument where OntologyDocument (Map.union p1 p2) $ mappend o1 o2 instance Syntax OWL2 OntologyDocument Entity SymbItems SymbMapItems where - parsersAndPrinters OWL2 = addSyntax "Ship" (basicSpec, ppShipOnt) - $ addSyntax "Manchester" (basicSpec, pretty) - $ makeDefault (basicSpec, pretty) + parsersAndPrinters OWL2 = addSyntax "Ship" (basicSpec True, ppShipOnt) + $ addSyntax "Manchester" (basicSpec True, pretty) + $ makeDefault (basicSpec True, pretty) + parse_macro OWL2 = Just (basicSpec False) parseSingleSymbItem OWL2 = Just symbItem parse_symb_items OWL2 = Just symbItems parse_symb_map_items OWL2 = Just symbMapItems @@ -100,6 +104,7 @@ instance Sentences OWL2 Axiom Sign OWLMorphism Entity where sym_of OWL2 = singletonList . symOf symmap_of OWL2 = symMapOf sym_name OWL2 = entityToId + rename_symbol OWL2 = renameSymbol sym_label OWL2 = label fullSymName OWL2 s = let i = cutIRI s @@ -108,6 +113,7 @@ instance Sentences OWL2 Axiom Sign OWLMorphism Entity where symKind OWL2 = takeWhile isAlpha . showEntityType . entityKind symsOfSen OWL2 _ = Set.toList . symsOfAxiom pair_symbols OWL2 = pairSymbols + new_symbol OWL2 = newSymbol inducedFromToMor :: Map.Map RawSymb RawSymb -> ExtSign Sign Entity -> @@ -138,7 +144,7 @@ inducedFromToMorphismAux :: Map.Map RawSymb RawSymb -> ExtSign Sign Entity -> ExtSign Sign Entity -> Result OWLMorphism -inducedFromToMorphismAux rm s@(ExtSign ssig _) t@(ExtSign tsig _) = do +inducedFromToMorphismAux rm s@(ExtSign ssig _) t@(ExtSign tsig _) = do -- trace ("\n aux ssig:" ++ show ssig ++ "\ntsig:" ++ show tsig ++ "\nrm:" ++ show rm) $ do mor <- inducedFromMor rm ssig let csig = cod mor incl <- inclusion OWL2 csig tsig @@ -153,6 +159,7 @@ instance StaticAnalysis OWL2 OntologyDocument Axiom stat_symb_items OWL2 s = return . statSymbItems s stat_symb_map_items OWL2 = statSymbMapItems convertTheory OWL2 = Just convertBasicTheory + convertSymbols OWL2 = Just convertEntities empty_signature OWL2 = emptySign signature_union OWL2 = uniteSign intersection OWL2 = intersectSign @@ -173,9 +180,13 @@ instance StaticAnalysis OWL2 OntologyDocument Axiom corresp2th OWL2 = corr2theo equiv2cospan OWL2 = addEquiv extract_module OWL2 = extractModule + solve_symbols OWL2 = solveSymbols + instantiate_macro OWL2 = instantiateMacro + delete_symbols_macro OWL2 = deleteSymbolsMacro #ifdef UNI_PACKAGE theory_to_taxonomy OWL2 = onto2Tax #endif + instance Logic OWL2 ProfSub OntologyDocument Axiom SymbItems SymbMapItems Sign OWLMorphism Entity RawSymb ProofTree where diff --git a/OWL2/MS.hs b/OWL2/MS.hs index 09d37088f3..b51bd167f2 100644 --- a/OWL2/MS.hs +++ b/OWL2/MS.hs @@ -35,6 +35,7 @@ data Extended = | ClassEntity ClassExpression | ObjectEntity ObjectPropertyExpression | SimpleEntity Entity + | IndividualVar IRI deriving (Show, Eq, Ord, Typeable, Data) -- | frames with annotated lists diff --git a/OWL2/ManchesterParser.hs b/OWL2/ManchesterParser.hs index a02134c880..30f8309ef9 100644 --- a/OWL2/ManchesterParser.hs +++ b/OWL2/ManchesterParser.hs @@ -28,6 +28,8 @@ import qualified Common.GlobalAnnotations as GA (PrefixMap) import Text.ParserCombinators.Parsec import qualified Data.Map as Map +-- import Debug.Trace + optAnnos :: CharParser st a -> CharParser st (Annotations, a) optAnnos p = do as <- optionalAnnos @@ -43,8 +45,8 @@ annotations = do fmap (map $ \ (as, (i, v)) -> Annotation as i v) . sepByComma . optAnnos $ pair uriP annotationValue -descriptionAnnotatedList :: CharParser st [(Annotations, ClassExpression)] -descriptionAnnotatedList = sepByComma $ optAnnos description +descriptionAnnotatedList :: Bool -> CharParser st [(Annotations, ClassExpression)] +descriptionAnnotatedList flag = sepByComma $ optAnnos (description flag) makeFrame :: Extended -> [FrameBit] -> Frame makeFrame ext fbl = Frame ext @@ -85,45 +87,45 @@ datatypeBit = do Just (ans, dr) -> [AnnFrameBit ans $ DatatypeBit dr] ++ map (`AnnFrameBit` AnnotationFrameBit Assertion) as2 -classFrame :: CharParser st Frame -classFrame = do +classFrame :: Bool -> CharParser st Frame +classFrame flag = do pkeyword classC - i <- description - plain <- many classFrameBit + i <- description flag + plain <- many (classFrameBit flag) -- ignore Individuals: ... ! optional $ pkeyword individualsC >> sepByComma individual return $ makeFrame (ClassEntity i) plain -classFrameBit :: CharParser st FrameBit -classFrameBit = do +classFrameBit :: Bool -> CharParser st FrameBit +classFrameBit flag = do pkeyword subClassOfC - ds <- descriptionAnnotatedList + ds <- descriptionAnnotatedList flag return $ ListFrameBit (Just SubClass) $ ExpressionBit ds <|> do e <- equivOrDisjoint - ds <- descriptionAnnotatedList + ds <- descriptionAnnotatedList flag return $ ListFrameBit (Just $ EDRelation e) $ ExpressionBit ds <|> do pkeyword disjointUnionOfC as <- optionalAnnos - ds <- sepByComma description + ds <- sepByComma (description flag) return $ AnnFrameBit as $ ClassDisjointUnion ds <|> do pkeyword hasKeyC as <- optionalAnnos - o <- sepByComma objectPropertyExpr + o <- sepByComma (objectPropertyExpr flag) return $ AnnFrameBit as $ ClassHasKey o [] <|> do as <- annotations return $ AnnFrameBit as $ AnnotationFrameBit Assertion -objPropExprAList :: CharParser st [(Annotations, ObjectPropertyExpression)] -objPropExprAList = sepByComma $ optAnnos objectPropertyExpr +objPropExprAList :: Bool -> CharParser st [(Annotations, ObjectPropertyExpression)] +objPropExprAList flag = sepByComma $ optAnnos (objectPropertyExpr flag) -objectFrameBit :: CharParser st FrameBit -objectFrameBit = do +objectFrameBit :: Bool -> CharParser st FrameBit +objectFrameBit flag = do r <- domainOrRange - ds <- descriptionAnnotatedList + ds <- descriptionAnnotatedList flag return $ ListFrameBit (Just $ DRRelation r) $ ExpressionBit ds <|> do characterKey @@ -131,39 +133,39 @@ objectFrameBit = do return $ ListFrameBit Nothing $ ObjectCharacteristics ds <|> do subPropertyKey - ds <- objPropExprAList + ds <- objPropExprAList flag return $ ListFrameBit (Just SubPropertyOf) $ ObjectBit ds <|> do e <- equivOrDisjoint - ds <- objPropExprAList + ds <- objPropExprAList flag return $ ListFrameBit (Just $ EDRelation e) $ ObjectBit ds <|> do pkeyword inverseOfC - ds <- objPropExprAList + ds <- objPropExprAList flag return $ ListFrameBit (Just InverseOf) $ ObjectBit ds <|> do pkeyword subPropertyChainC as <- optionalAnnos - os <- sepBy1 objectPropertyExpr (keyword oS) + os <- sepBy1 (objectPropertyExpr flag) (keyword oS) return $ AnnFrameBit as $ ObjectSubPropertyChain os <|> do as <- annotations return $ AnnFrameBit as $ AnnotationFrameBit Assertion -objectPropertyFrame :: CharParser st Frame -objectPropertyFrame = do +objectPropertyFrame :: Bool -> CharParser st Frame +objectPropertyFrame flag = do pkeyword objectPropertyC - ouri <- objectPropertyExpr - as <- many objectFrameBit + ouri <- objectPropertyExpr flag + as <- many (objectFrameBit flag) return $ makeFrame (ObjectEntity ouri) as dataPropExprAList :: CharParser st [(Annotations, DataPropertyExpression)] dataPropExprAList = sepByComma $ optAnnos uriP -dataFrameBit :: CharParser st FrameBit -dataFrameBit = do +dataFrameBit :: Bool -> CharParser st FrameBit +dataFrameBit flag = do pkeyword domainC - ds <- descriptionAnnotatedList + ds <- descriptionAnnotatedList flag return $ ListFrameBit (Just (DRRelation ADomain)) $ ExpressionBit ds <|> do pkeyword rangeC @@ -186,15 +188,15 @@ dataFrameBit = do as <- annotations return $ AnnFrameBit as $ AnnotationFrameBit Assertion -dataPropertyFrame :: CharParser st Frame -dataPropertyFrame = do +dataPropertyFrame :: Bool -> CharParser st Frame +dataPropertyFrame flag = do pkeyword dataPropertyC duri <- uriP - as <- many dataFrameBit + as <- many (dataFrameBit flag) return $ makeFrame (SimpleEntity $ mkEntity DataProperty duri) as -fact :: CharParser st Fact -fact = do +fact :: Bool -> CharParser st Fact +fact flag = do pn <- option Positive $ keyword notS >> return Negative u <- uriP do @@ -202,12 +204,13 @@ fact = do return $ DataPropertyFact pn u c <|> do t <- individual - return $ ObjectPropertyFact pn (ObjectProp u) t + let ope = if flag then ObjectProp u else UnsolvedObjProp u + return $ ObjectPropertyFact pn ope t -iFrameBit :: CharParser st FrameBit -iFrameBit = do +iFrameBit :: Bool -> CharParser st FrameBit +iFrameBit flag = do pkeyword typesC - ds <- descriptionAnnotatedList + ds <- descriptionAnnotatedList flag return $ ListFrameBit (Just Types) $ ExpressionBit ds <|> do s <- sameOrDifferent @@ -215,30 +218,32 @@ iFrameBit = do return $ ListFrameBit (Just $ SDRelation s) $ IndividualSameOrDifferent is <|> do pkeyword factsC - fs <- sepByComma $ optAnnos fact + fs <- sepByComma $ optAnnos (fact flag) return $ ListFrameBit Nothing $ IndividualFacts fs <|> do a <- annotations return $ AnnFrameBit a $ AnnotationFrameBit Assertion -individualFrame :: CharParser st Frame -individualFrame = do +individualFrame :: Bool -> CharParser st Frame +individualFrame flag = do pkeyword individualC iuri <- individual - as <- many iFrameBit - return $ makeFrame (SimpleEntity $ mkEntity NamedIndividual iuri) as + as <- many (iFrameBit flag) + let ent = if flag then SimpleEntity $ mkEntity NamedIndividual iuri + else SimpleEntity $ mkEntity UnsolvedEntity iuri + return $ makeFrame ent as -misc :: CharParser st Frame -misc = do +misc :: Bool -> CharParser st Frame +misc flag = do e <- equivOrDisjointKeyword classesC as <- optionalAnnos - ds <- sepByComma description + ds <- sepByComma (description flag) return $ Frame (Misc as) [ListFrameBit (Just $ EDRelation e) $ ExpressionBit $ emptyAnnoList ds] <|> do e <- equivOrDisjointKeyword propertiesC as <- optionalAnnos - es <- sepByComma objectPropertyExpr + es <- sepByComma (objectPropertyExpr flag) -- indistinguishable from dataProperties return $ Frame (Misc as) [ListFrameBit (Just $ EDRelation e) $ ObjectBit $ emptyAnnoList es] @@ -249,24 +254,29 @@ misc = do return $ Frame (Misc as) [ListFrameBit (Just $ SDRelation s) $ IndividualSameOrDifferent $ emptyAnnoList is] -frames :: CharParser st [Frame] -frames = many $ datatypeBit <|> classFrame - <|> objectPropertyFrame <|> dataPropertyFrame <|> individualFrame - <|> annotationPropertyFrame <|> misc +frames :: Bool -> CharParser st [Frame] +frames flag = + many $ datatypeBit <|> classFrame flag + <|> objectPropertyFrame flag <|> dataPropertyFrame flag <|> individualFrame flag + <|> annotationPropertyFrame <|> misc flag -basicSpec :: GA.PrefixMap -> CharParser st OntologyDocument -basicSpec pm = do +-- the Bool flag is true for ontologies and false for macros +basicSpec :: Bool -> GA.PrefixMap -> CharParser st OntologyDocument +basicSpec flag pm = do nss <- many nsEntry ou <- option nullIRI $ pkeyword ontologyC >> option nullIRI uriP ie <- many importEntry ans <- many annotations - as <- frames + as <- frames flag if null nss && null ie && null ans && null as && ou == nullIRI then fail "empty ontology" - else return $ OntologyDocument - (Map.union (Map.fromList $ map (\ (p, q) -> (p, showIRICompact q)) nss) - (convertPrefixMap pm)) - (emptyOntology as) - { imports = ie - , ann = ans - , name = ou } + else do + let o = OntologyDocument + (Map.union (Map.fromList $ map (\ (p, q) -> (p, showIRICompact q)) nss) + (convertPrefixMap pm)) + (emptyOntology as) + { imports = ie + , ann = ans + , name = ou } + -- trace ("o:" ++ show o) $ + return o diff --git a/OWL2/Parse.hs b/OWL2/Parse.hs index 0fa3dc19ea..9c78ac7bc5 100644 --- a/OWL2/Parse.hs +++ b/OWL2/Parse.hs @@ -329,15 +329,15 @@ keyword :: String -> CharParser st String keyword s = keywordNotFollowedBy s (alphaNum <|> char '_') -- base OWLClass excluded -atomic :: CharParser st ClassExpression -atomic = parensP description +atomic :: Bool -> CharParser st ClassExpression +atomic flag = parensP (description flag) <|> fmap ObjectOneOf (bracesP $ sepByComma individual) -objectPropertyExpr :: CharParser st ObjectPropertyExpression -objectPropertyExpr = do +objectPropertyExpr :: Bool -> CharParser st ObjectPropertyExpression +objectPropertyExpr flag = do keyword inverseS - fmap ObjectInverseOf objectPropertyExpr - <|> fmap ObjectProp uriP + fmap ObjectInverseOf (objectPropertyExpr flag) + <|> fmap (if flag then ObjectProp else UnsolvedObjProp) uriP -- creating the facet-value pairs facetValuePair :: CharParser st (ConstrainingFacet, RestrictionValue) @@ -416,23 +416,23 @@ individualOrConstantList = do Right c -> fmap (Right . (c :)) $ optionL $ commaP >> sepByComma literal -primaryOrDataRange :: CharParser st (Either ClassExpression DataRange) -primaryOrDataRange = do +primaryOrDataRange :: Bool -> CharParser st (Either ClassExpression DataRange) +primaryOrDataRange flag = do ns <- many $ keyword notS -- allows multiple not before primary ed <- do u <- datatypeUri - fmap Left (restrictionAny $ ObjectProp u) + fmap Left ((restrictionAny flag) $ ObjectProp u) <|> fmap (Right . DataType u) (bracketsP $ sepByComma facetValuePair) <|> return (if isDatatypeKey u then Right $ DataType u [] - else Left $ Expression u) -- could still be a datatypeUri + else Left $ (if flag then Expression else UnsolvedClass) u) -- could still be a datatypeUri <|> do e <- bracesP individualOrConstantList return $ case e of Left us -> Left $ ObjectOneOf us Right cs -> Right $ DataOneOf cs - <|> fmap Left restrictionOrAtomic + <|> fmap Left (restrictionOrAtomic flag) return $ if even (length ns) then ed else case ed of Left d -> Left $ ObjectComplementOf d @@ -444,8 +444,8 @@ mkObjectJunction ty ds = case nubOrd ds of [x] -> x ns -> ObjectJunction ty ns -restrictionAny :: ObjectPropertyExpression -> CharParser st ClassExpression -restrictionAny opExpr = do +restrictionAny :: Bool -> ObjectPropertyExpression -> CharParser st ClassExpression +restrictionAny flag opExpr = do keyword valueS e <- individualOrConstant case e of @@ -458,7 +458,7 @@ restrictionAny opExpr = do return $ ObjectHasSelf opExpr <|> do -- sugar keyword onlysomeS - ds <- bracketsP $ sepByComma description + ds <- bracketsP $ sepByComma (description flag) let as = map (ObjectValuesFrom SomeValuesFrom opExpr) ds o = ObjectValuesFrom AllValuesFrom opExpr $ mkObjectJunction UnionOf ds @@ -469,7 +469,7 @@ restrictionAny opExpr = do return $ ObjectValuesFrom SomeValuesFrom opExpr $ ObjectOneOf [iu] <|> do v <- someOrOnly - pr <- primaryOrDataRange + pr <- primaryOrDataRange flag case pr of Left p -> return $ ObjectValuesFrom v opExpr p Right r -> case opExpr of @@ -477,7 +477,7 @@ restrictionAny opExpr = do _ -> unexpected $ "dataRange after " ++ showQuantifierType v <|> do (c, n) <- card - mp <- optionMaybe primaryOrDataRange + mp <- optionMaybe (primaryOrDataRange flag) case mp of Nothing -> return $ ObjectCardinality $ Cardinality c n opExpr Nothing Just pr -> case pr of @@ -488,34 +488,44 @@ restrictionAny opExpr = do return $ DataCardinality $ Cardinality c n dpExpr $ Just r _ -> unexpected $ "dataRange after " ++ showCardinalityType c -restriction :: CharParser st ClassExpression -restriction = objectPropertyExpr >>= restrictionAny +restriction :: Bool -> CharParser st ClassExpression +restriction flag = (objectPropertyExpr flag) >>= (restrictionAny flag) -restrictionOrAtomic :: CharParser st ClassExpression -restrictionOrAtomic = do - opExpr <- objectPropertyExpr - restrictionAny opExpr <|> case opExpr of - ObjectProp euri -> return $ Expression euri +restrictionOrAtomic :: Bool -> CharParser st ClassExpression +restrictionOrAtomic flag = do + opExpr <- objectPropertyExpr flag + (restrictionAny flag) opExpr <|> case opExpr of + ObjectProp euri -> return $ (if flag then Expression else UnsolvedClass) euri + UnsolvedObjProp euri -> return $ UnsolvedClass euri _ -> unexpected "inverse object property" - <|> atomic + <|> atomic flag optNot :: (a -> a) -> CharParser st a -> CharParser st a optNot f p = (keyword notS >> fmap f p) <|> p -primary :: CharParser st ClassExpression -primary = optNot ObjectComplementOf restrictionOrAtomic - -conjunction :: CharParser st ClassExpression -conjunction = do - curi <- fmap Expression $ try (owlClassUri << keyword thatS) - rs <- sepBy1 (optNot ObjectComplementOf restriction) $ keyword andS +primary :: Bool -> CharParser st ClassExpression +primary flag = optNot ObjectComplementOf (restrictionOrAtomic flag) + +conjunction :: Bool -> CharParser st ClassExpression +conjunction flag = do + _ <- keyword andS + _ <- oParenT + hd <- uriP + _ <- commaT + tl <- uriP + _ <- cParenT + return $ VarExpression $ MUnion hd tl + <|> do + curi <- fmap (if flag then Expression else UnsolvedClass) + $ try (owlClassUri << keyword thatS) + rs <- sepBy1 (optNot ObjectComplementOf (restriction flag)) $ keyword andS return $ mkObjectJunction IntersectionOf $ curi : rs <|> fmap (mkObjectJunction IntersectionOf) - (sepBy1 primary $ keyword andS) + (sepBy1 (primary flag) $ keyword andS) -description :: CharParser st ClassExpression -description = - fmap (mkObjectJunction UnionOf) $ sepBy1 conjunction $ keyword orS +description :: Bool -> CharParser st ClassExpression +description flag = + fmap (mkObjectJunction UnionOf) $ sepBy1 (conjunction flag) $ keyword orS entityType :: CharParser st EntityType entityType = choice $ map (\ f -> keyword (show f) >> return f) diff --git a/OWL2/Print.hs b/OWL2/Print.hs index 87a6f01520..aad92a8abf 100644 --- a/OWL2/Print.hs +++ b/OWL2/Print.hs @@ -119,6 +119,7 @@ instance Pretty Literal where Nothing -> empty Just tag2 -> text asP <> text tag2 NumberLit f -> text (show f) + _ -> error "nyi" instance Pretty ObjectPropertyExpression where pretty = printObjPropExp @@ -127,6 +128,8 @@ printObjPropExp :: ObjectPropertyExpression -> Doc printObjPropExp obExp = case obExp of ObjectProp ou -> pretty ou ObjectInverseOf iopExp -> keyword inverseS <+> printObjPropExp iopExp + ObjectPropertyVar _ ou -> text "var" <+> pretty ou + UnsolvedObjProp ou -> text "unsolved" <+> pretty ou printFV :: (ConstrainingFacet, RestrictionValue) -> Doc printFV (facet, restValue) = pretty (fromCF facet) <+> pretty restValue @@ -159,6 +162,7 @@ printDataRange dr = case dr of instance Pretty ClassExpression where pretty desc = case desc of Expression ocUri -> printIRI ocUri + UnsolvedClass anIri -> text "unsolved" <+> printIRI anIri ObjectJunction ty ds -> let (k, p) = case ty of UnionOf -> (orS, pretty) diff --git a/OWL2/StaticAnalysis.hs b/OWL2/StaticAnalysis.hs index 50499cbf14..54a1cfc4de 100644 --- a/OWL2/StaticAnalysis.hs +++ b/OWL2/StaticAnalysis.hs @@ -32,12 +32,15 @@ import Common.GlobalAnnotations hiding (PrefixMap) import Common.ExtSign import Common.Lib.State import Common.IRI --(iriToStringUnsecure, setAngles) +import Common.Id import Common.SetColimit import Control.Monad import Logic.Logic +import Debug.Trace + -- | Error messages for static analysis failMsg :: Entity -> ClassExpression -> Result a failMsg (Entity _ ty e) desc = @@ -49,7 +52,7 @@ failMsg (Entity _ ty e) desc = -- | checks if an entity is in the signature checkEntity :: Sign -> Entity -> Result () checkEntity s t@(Entity _ ty e) = - let errMsg = mkError ("unknown " ++ showEntityType ty) e + let errMsg = mkError ("unknown " ++ showEntityType ty ++ " in " ++ show s) e in case ty of Datatype -> unless (Set.member e (datatypes s) || isDatatypeKey e) errMsg Class -> unless (Set.member e (concepts s) || isThing e) errMsg @@ -96,7 +99,8 @@ checkObjPropList s ol = do unless (and ls) $ fail $ "undeclared object properties:\n" ++ showDoc (map (\o -> case o of ObjectProp _ -> o - ObjectInverseOf x -> x) ol) "" + ObjectInverseOf x -> x + _ -> error "unsolved string or variable") ol) "" checkDataPropList :: Sign -> [DataPropertyExpression] -> Result () checkDataPropList s dl = do @@ -181,6 +185,7 @@ checkClassExpression s desc = Nothing -> return desc Just d -> checkDataRange s d >> return desc else datErr dExp + _ -> error "unsolved string or class variable" checkFact :: Sign -> Fact -> Result () checkFact s f = case f of @@ -400,9 +405,9 @@ generateLabelMap sig = foldr (\ (Frame ext fbl) -> case ext of -- | adding annotations for theorems anaAxiom :: Axiom -> Named Axiom -anaAxiom ax = findImplied ax $ makeNamed name ax +anaAxiom ax = findImplied ax $ makeNamed nm ax where names = getNames ax - name = concat $ intersperse "_" names + nm = concat $ intersperse "_" names findImplied :: Axiom -> Named Axiom -> Named Axiom findImplied ax sent = @@ -581,3 +586,524 @@ corr2theo _aname flag ssig tsig l1 l2 eMap1 eMap2 rref = do _ -> fail $ "non-unique symbol match:" ++ showDoc l1 " " ++ showDoc l2 " " _ -> fail "terms not yet supported in alignments" + +-- solving symbols of a pattern + +solveSymbols :: Set.Set Entity -> PatternVarMap -> OntologyDocument -> Result OntologyDocument +solveSymbols impSyms vMap (OntologyDocument pd (Ontology n is as fs)) = do + (declSyms, usedSyms, fs') <- + foldM (\(ds, us, flist) f -> do + (f', ds', us') <- solveFrame impSyms vMap f + return (Set.union ds ds', Set.union us us', flist++[f']) ) + (Set.empty, Set.empty, []) fs + let getKind str = case str of + "Class" -> Class + "ObjectProperty" -> ObjectProperty + "Individual" -> NamedIndividual + _ -> error $ "nyi:" ++ str + varSyms = foldl Set.union Set.empty $ map (\(x, (f, k)) -> if f then Set.empty else Set.singleton $ Entity Nothing (getKind k) x) $ Map.toList vMap + diffSyms = Set.difference usedSyms (Set.union declSyms $ Set.union impSyms varSyms) + -- each used symbol must be declared, imported or variable + -- TODO: this test should take into account imports. Commented out for now because of structuring! + --if Set.null diffSyms then + return $ OntologyDocument pd $ Ontology n is as fs' + --else error $ "undeclared symbols in the body of the pattern. impSyms:" ++ show impSyms ++ + -- " declSyms:" ++ show declSyms ++ " usedSyms:" ++ show usedSyms ++ + -- " varSyms:" ++ show varSyms ++ " diffSyms:" ++ show diffSyms + +-- solving symbols for each frame, also keep track of declared and used symbols + +solveFrame :: Set.Set Entity -> PatternVarMap -> Frame -> Result (Frame, Set.Set Entity, Set.Set Entity) +solveFrame impSyms vMap (Frame ext fBits) = do + let (ext', decl) = + case ext of + Misc _ -> (ext, Set.empty) + ClassEntity (UnsolvedClass i) -> + if i `elem` Map.keys vMap + then (ClassEntity $ VarExpression $ MVar False i, Set.empty) -- lists are not allowed in this position, so always simple class + else if (Entity Nothing Class i) `elem` impSyms + then (ClassEntity $ Expression i, Set.empty) -- add only if not member of impSyms + else (ClassEntity $ Expression i, Set.singleton $ Entity Nothing Class i) + ClassEntity _ -> error $ show ext -- no GCIs for now + ObjectEntity (UnsolvedObjProp i) -> + if i `elem` Map.keys vMap + then (ObjectEntity $ ObjectPropertyVar False i, Set.empty) -- lists are not allowed in this position, always object properties + else if (Entity Nothing ObjectProperty i) `elem` impSyms + then (ObjectEntity $ ObjectProp i, Set.empty) -- add only if not member of impSyms + else (ObjectEntity $ ObjectProp i, Set.singleton $ Entity Nothing ObjectProperty i) + ObjectEntity _ -> error $ show ext -- no GCIs for now + SimpleEntity (Entity l UnsolvedEntity i) -> + if i `elem` Map.keys vMap + then -- TODO: tests that it's an individual! + (IndividualVar i, Set.empty) + else (SimpleEntity $ Entity l NamedIndividual i, Set.singleton $ Entity l NamedIndividual i) + (fBits', used) <- foldM (\(fbs, us) fbit -> do + (fbit', us') <- solveFrameBit impSyms vMap fbit + return (fbs ++ [fbit'], Set.union us us')) ([], Set.empty) fBits + return (Frame ext' fBits', decl, used) + +-- solve symbols for each frame bit + +solveFrameBit :: Set.Set Entity -> PatternVarMap -> FrameBit -> Result (FrameBit, Set.Set Entity) +solveFrameBit impSyms vMap fbit = -- trace ("fbit:" ++ show fbit) $ + case fbit of + ListFrameBit mr lft -> + case lft of + AnnotationBit _ -> return (fbit, Set.empty) + ExpressionBit aces -> do + let (aces', used') = foldl (\(as, us) ace -> let (ace', us') = solveClassExpression impSyms vMap ace + in (as ++ [ace'], Set.union us us')) ([], Set.empty) aces + -- trace ("solved lft:" ++ show (ExpressionBit aces')) $ + return (ListFrameBit mr $ ExpressionBit aces', used') + ObjectBit aopes -> do + let (aopes', used') = foldl (\(as, us) aope -> + let (aope', us') = solveObjPropExpression impSyms vMap aope + in (as ++ [aope'], Set.union us us')) ([], Set.empty) aopes + -- trace ("solved lft:" ++ show (ObjectBit aopes')) $ + return (ListFrameBit mr $ ObjectBit aopes', used') + DataBit adpes -> error "nyi" + IndividualSameOrDifferent ainds -> return (fbit, Set.fromList $ map (\ai -> Entity Nothing NamedIndividual $ snd ai) ainds) + ObjectCharacteristics achars -> return (fbit, Set.empty) + IndividualFacts afacts -> do + let (afacts', used') = foldl (\(afs, usyms) (a, af) -> do + case af of + ObjectPropertyFact pn ope i -> let ((_, ope'), us') = solveObjPropExpression impSyms vMap ([], ope) + in (afs ++ [(a,ObjectPropertyFact pn ope' i)], Set.union usyms us') + DataPropertyFact _ _ _ -> error "data property nyi") + ([], Set.empty) afacts + return (ListFrameBit mr $ IndividualFacts afacts', used') + AnnFrameBit annos (AnnotationFrameBit _) -> return (fbit, Set.empty) + AnnFrameBit annos DataFunctional -> return (fbit, Set.empty) + AnnFrameBit annos (DatatypeBit drg) -> error "nyi" + AnnFrameBit annos (ClassDisjointUnion cexps) -> do + let (aces', used') = foldl (\(as, us) ce -> let (ace', us') = solveClassExpression impSyms vMap ([], ce) + in (as ++ [ace'], Set.union us us')) ([], Set.empty) cexps + return (AnnFrameBit annos $ ClassDisjointUnion $ map snd aces', used') + AnnFrameBit annos (ClassHasKey opexps dpexps) -> error "nyi" + AnnFrameBit annos (ObjectSubPropertyChain opexps) -> do + let (opexps', used') = foldl (\(as, us) ope -> + let (aope', us') = solveObjPropExpression impSyms vMap ([], ope) + in (as ++ [snd aope'], Set.union us us')) ([], Set.empty) opexps + -- trace ("solved lft:" ++ show (ObjectSubPropertyChain opexps')) $ + return (AnnFrameBit annos $ ObjectSubPropertyChain opexps', used') + +-- solve class expressions + +solveClassExpression :: Set.Set Entity -> PatternVarMap -> (Annotations, ClassExpression) -> ((Annotations, ClassExpression), Set.Set Entity) +solveClassExpression impSyms vMap (annos, cexp) = + let (cexp', used) = case cexp of + UnsolvedClass i -> if i `elem` Map.keys vMap then + let (b, _) = Map.findWithDefault (error "just checked") i vMap + in (VarExpression $ MVar b i, Set.empty) + else (Expression i, Set.singleton $ Entity Nothing Class i) + ObjectJunction j cexps -> let (cexps', used') = foldl (\(cs, u) c -> let ((_a, c'), u') = solveClassExpression impSyms vMap ([], c) + in (cs ++ [c'], Set.union u u')) ([], Set.empty) cexps + in (ObjectJunction j cexps', used') + Expression i -> error "nyi" + ObjectComplementOf cexp -> let ((_a, cexp'), u) = solveClassExpression impSyms vMap ([], cexp) + in (ObjectComplementOf cexp', u) + VarExpression _ -> error $ "should get a class expression but instead got " ++ show cexp + ObjectOneOf indivs -> (cexp, Set.fromList $ map (\i -> Entity Nothing NamedIndividual i) indivs) + ObjectValuesFrom q opexp cexp -> let ((_, cexp'), u1) = solveClassExpression impSyms vMap ([], cexp) + ((_, opexp'), u2) = solveObjPropExpression impSyms vMap ([], opexp) + in (ObjectValuesFrom q opexp' cexp', Set.union u1 u2) + ObjectHasValue opexp indiv -> error "nyi" + ObjectHasSelf opexp -> let ((_, opexp'), u) = solveObjPropExpression impSyms vMap ([], opexp) + in (ObjectHasSelf opexp', u) + ObjectCardinality (Cardinality cType aInt opexp mcexp) -> + let + (mcexp', u1) = + case mcexp of + Nothing -> (Nothing, Set.empty) + Just cexp -> let ((_a, cexp'), u) = solveClassExpression impSyms vMap ([], cexp) + in (Just cexp', u) + ((_, opexp'), u2) = solveObjPropExpression impSyms vMap ([], opexp) + in ( ObjectCardinality (Cardinality cType aInt opexp' mcexp'), Set.union u1 u2) + DataValuesFrom q dpexp drg -> error "nyi" + DataHasValue dpexp lit -> error "nyi" + DataCardinality (Cardinality cType aInt dpexp mdrg) -> error "nyi" + -- _ -> error $ "nyi:" ++ show cexp + in ((annos, cexp'), used) + +solveObjPropExpression :: Set.Set Entity -> PatternVarMap -> (Annotations, ObjectPropertyExpression) -> ((Annotations, ObjectPropertyExpression), Set.Set Entity) +solveObjPropExpression impSyms vMap (annos, opexp) = + let (opexp', used) = + case opexp of + ObjectProp r -> (opexp, Set.singleton $ Entity Nothing ObjectProperty r) + ObjectInverseOf opexp0 -> let ((_, opexp1), u) = solveObjPropExpression impSyms vMap ([], opexp0) + in (ObjectInverseOf opexp1, u) + ObjectPropertyVar _ _ -> error $ "expected object property expression but got " ++ show opexp + UnsolvedObjProp i -> if i `elem` Map.keys vMap then + let (b, _) = Map.findWithDefault (error "just checked") i vMap + in (ObjectPropertyVar b i, Set.empty) + else (ObjectProp i, Set.singleton $ Entity Nothing ObjectProperty i) + in ((annos, opexp'), used) + +-- solveIndividual :: Set.Set Entity -> PatternVarMap -> (Annotations, IndExpression) -> ((Annotations, IndExpression), Set.Set Entity) +-- solveIndividual _ _ _ = error "nyi" + +-- TODO: +-- write a method that solves a data property expression etc. +-- note: individuals are not stored as vars at any moment. + + +-- instantiate a macro with the values stored in a substitution + +instantiateMacro :: PatternVarMap -> GSubst -> OntologyDocument -> Result OntologyDocument +instantiateMacro vars subst (OntologyDocument pd (Ontology n is as fs)) = do + fs'<- instantiateFrames subst vars fs + return $ OntologyDocument pd $ Ontology n is as fs' + +-- instantiate frames + +instantiateFrames :: GSubst -> PatternVarMap -> [Frame] -> Result [Frame] +instantiateFrames subst vars = + mapM (instantiateFrame subst vars) + +-- instantiate a single frame + +instantiateFrame :: GSubst -> PatternVarMap -> Frame -> Result Frame +instantiateFrame subst var (Frame ext fBits) = do + ext' <- case ext of + ClassEntity (VarExpression (MVar b i)) -> -- TODO: handle lists! + if (i, "Class") `elem` Map.keys subst then do + let j = Map.findWithDefault (error "instantiateFrame") (i, "Class") subst + return $ ClassEntity $ Expression $ getIRIVal j + else fail $ "unknown class variable: " ++ show i + ClassEntity (Expression i) -> return $ ClassEntity $ Expression $ instParamName subst i + ClassEntity _ -> return ext + ObjectEntity (ObjectPropertyVar b i) -> -- TODO: handle lists! + if (i, "ObjectProperty") `elem` Map.keys subst then do + let j = Map.findWithDefault (error "instantiateFrame") (i, "ObjectProperty") subst + return $ ObjectEntity $ ObjectProp $ getIRIVal j + else fail $ "unknown object property variable: " ++ show i + ObjectEntity (ObjectProp i) -> + return $ ObjectEntity $ ObjectProp + $ instParamName subst i + ObjectEntity _ -> return ext + SimpleEntity ent -> return $ SimpleEntity $ ent{cutIRI = instParamName subst $ cutIRI ent} + -- TODO: we get this for individuals declared in the bodies! what about data props? + IndividualVar i -> + if (i, "Individual") `elem` Map.keys subst then do + let j = Map.findWithDefault (error "instantiateFrame") (i, "Individual") subst + return $ SimpleEntity $ Entity Nothing NamedIndividual $ getIRIVal j + else fail $ "unknown individual variable: " ++ show i + Misc _ -> return ext -- TODO: check if ok! error $ show ext + fBits' <- mapM (instantiateFrameBit subst var) fBits + return $ Frame ext' fBits' + +instantiateFrameBit :: GSubst -> PatternVarMap -> FrameBit -> Result FrameBit +instantiateFrameBit subst var fbit = + case fbit of + ListFrameBit mr lfb -> + case lfb of + AnnotationBit _ -> return fbit + ExpressionBit aces -> do + aces' <- mapM (instantiateClassExpression subst var) aces + return $ ListFrameBit mr $ ExpressionBit aces' + ObjectBit aopexps -> do + aopexps' <- mapM (instantiateObjectPropertyExpression subst var) aopexps + return $ ListFrameBit mr $ ObjectBit aopexps' + DataBit adpexps -> error $ show lfb + IndividualSameOrDifferent aindivs -> trace ("subst:" ++ show subst ++ " var:" ++ show var ++ " fbit:" ++ show fbit) $ + return $ ListFrameBit mr $ IndividualSameOrDifferent $ + concatMap (\(a,i) -> if (i,"Individual")`elem` Map.keys subst then + let j = Map.findWithDefault (error "instantiateFrameBit, individual") (i, "Individual") subst + in [(a, instParamName subst $ getIRIVal j)] + else if (i,"list") `elem` Map.keys subst then + let j = Map.findWithDefault (error "instantiateFrameBit, list") (i, "list") subst + in case j of + ListVal k inds -> + if (k == "Individual") || null inds then + map (\x -> (a,x)) inds + else error $ "expected a list of individuals but got a list of "++ show k ++"s instead" + _ -> error $ "expected a list of individuals but got " ++ show j + else [(a, instParamName subst $ i)]) aindivs --TODO: this is wrong and needs to be fixed, we get a list and this should be concatenated + ObjectCharacteristics _achars -> return fbit + DataPropRange _ -> return fbit + IndividualFacts afacts -> do + afacts' <- mapM (\(a, af) -> case af of + ObjectPropertyFact pn ope i -> do + (_, ope') <- instantiateObjectPropertyExpression subst var ([], ope) + let j = if (i,"Individual")`elem` Map.keys subst then + getIRIVal $ Map.findWithDefault (error "instantiateFrameBit") (i, "Individual") subst + else instParamName subst i + return (a, ObjectPropertyFact pn ope' j) + DataPropertyFact pn dpe lit -> error "data property fact nyi") afacts + return $ ListFrameBit mr $ IndividualFacts afacts' + AnnFrameBit annos afb -> do + annos' <- + case annos of + [] -> return annos + _ -> mapM (instantiateAnno subst var) annos + case afb of + AnnotationFrameBit at -> return $ AnnFrameBit annos' afb + DataFunctional -> return $ AnnFrameBit annos' afb + DatatypeBit drg -> error $ show fbit + ClassDisjointUnion cexps -> do + aexps' <- mapM (instantiateClassExpression subst var) $ map (\x -> ([], x)) cexps + return $ AnnFrameBit annos' $ ClassDisjointUnion $ map snd aexps' + ClassHasKey opexps dpexps -> error $ show fbit + ObjectSubPropertyChain opexps -> do + aopexps' <- mapM (instantiateObjectPropertyExpression subst var) $ map (\x -> ([], x)) opexps + return $ AnnFrameBit annos' $ ObjectSubPropertyChain $ map snd aopexps' + +instantiateAnno :: GSubst -> PatternVarMap -> Annotation -> Result Annotation +instantiateAnno subst var anno = + case anno of + Annotation annos aprop aval -> do + case aval of + AnnValue x -> + if (x, "String") `elem` Map.keys subst then do + let v = getIRIVal $ Map.findWithDefault (error "already checked") (x, "String") subst + return $ Annotation annos aprop $ AnnValue v -- should be AnnValLit but I don't know yet what to put in it! TODO + else return anno + _ -> return anno + + +instantiateClassExpression :: GSubst -> PatternVarMap -> (Annotations, ClassExpression) -> Result (Annotations, ClassExpression) +instantiateClassExpression subst var (annos, cexp) = + case cexp of + UnsolvedClass _ -> error $ "unsolved class at instantiation: " ++ show cexp + Expression i -> return (annos, Expression $ instParamName subst i) + VarExpression (MVar b x) -> + if b then error "list occuring in not allowed position" + else do + let v = getIRIVal $ Map.findWithDefault (error $ "unknown var:" ++ show x ++ " b:" ++ show b ++ " subst:" ++ show subst) (x, "Class") subst + return (annos, Expression v) + ObjectJunction q cexps -> do + acexps <- mapM (instClassExprAux subst var) $ + map (\x -> ([], x)) cexps + return (annos, ObjectJunction q $ map snd $ concat acexps) + ObjectComplementOf cexp0 -> do + (_, cexp') <- instantiateClassExpression subst var ([], cexp0) + return (annos, ObjectComplementOf cexp') + ObjectOneOf indivs -> do + indivs' <- mapM (instIndiv subst var) indivs + return (annos, ObjectOneOf $ concat indivs') -- TODO: instantiate individuals! + ObjectValuesFrom q opexp cexp0 -> do + (_, opexp') <- instantiateObjectPropertyExpression subst var ([], opexp) + (_, cexp') <- instantiateClassExpression subst var ([], cexp0) + return (annos, ObjectValuesFrom q opexp' cexp') + ObjectHasValue opexp indiv -> do + (_, opexp') <- instantiateObjectPropertyExpression subst var ([], opexp) + error "nyi" + ObjectHasSelf opexp -> do + (_, opexp') <- instantiateObjectPropertyExpression subst var ([], opexp) + return (annos, ObjectHasSelf opexp') + ObjectCardinality (Cardinality cType aInt opexp mcexp) -> do + mcexp' <- case mcexp of + Nothing -> return Nothing + Just cexp0 -> do + (_, cexp') <- instantiateClassExpression subst var ([], cexp0) + return $ Just cexp' + (_, opexp') <- instantiateObjectPropertyExpression subst var ([], opexp) + return (annos, ObjectCardinality (Cardinality cType aInt opexp' mcexp')) + _ -> return (annos, cexp) +{- Expression Class -- nothing to instantiate + | DataValuesFrom QuantifierType DataPropertyExpression DataRange --TODO: once we have data properties as well! + | DataHasValue DataPropertyExpression Literal + | DataCardinality (Cardinality DataPropertyExpression DataRange) +-} + +instClassExprAux :: GSubst -> PatternVarMap -> (Annotations, ClassExpression) -> Result [(Annotations, ClassExpression)] +instClassExprAux subst var (annos, cexp) = + case cexp of + UnsolvedClass _ -> error $ "unsolved class at instantiation: " ++ show cexp + Expression i -> return [(annos, Expression $ instParamName subst i)] + VarExpression (MVar b x) -> + if b then do + let v = Map.findWithDefault (error $ "unknown var:" ++ show x ++ " b:" ++ show b ++ " subst:" ++ show subst) (x, "list") subst + case v of + ListVal str iris -> + if str == "Class" then return $ map (\i -> ([], Expression i)) iris + else error $ "expected list of classes, kind mismatch" + _ -> error $ "list variable with non-list value" + else do + let v = getIRIVal $ Map.findWithDefault (error $ "unknown var:" ++ show x ++ " b:" ++ show b ++ " subst:" ++ show subst) (x, "Class") subst + return [(annos, Expression v)] + ObjectJunction q cexps -> do + acexps <- mapM (instClassExprAux subst var) $ + map (\x -> ([], x)) cexps + return [(annos, ObjectJunction q $ map snd $ concat acexps)] + ObjectComplementOf cexp0 -> do + (_, cexp') <- instantiateClassExpression subst var ([], cexp0) + return [(annos, ObjectComplementOf cexp')] + ObjectOneOf indivs -> do + indivs' <- mapM (instIndiv subst var) indivs + return [(annos, ObjectOneOf $ concat indivs')] + ObjectValuesFrom q opexp cexp0 -> do + (_, opexp') <- instantiateObjectPropertyExpression subst var ([], opexp) + (_, cexp') <- instantiateClassExpression subst var ([], cexp0) + return [(annos, ObjectValuesFrom q opexp' cexp')] + ObjectHasValue opexp indiv -> do + (_, opexp') <- instantiateObjectPropertyExpression subst var ([], opexp) + error "nyi" + ObjectHasSelf opexp -> do + (_, opexp') <- instantiateObjectPropertyExpression subst var ([], opexp) + return [(annos, ObjectHasSelf opexp')] + ObjectCardinality (Cardinality cType aInt opexp mcexp) -> do + mcexp' <- case mcexp of + Nothing -> return Nothing + Just cexp0 -> do + (_, cexp') <- instantiateClassExpression subst var ([], cexp0) -- TODO: test for this, are lists allowed here? + return $ Just cexp' + (_, opexp') <- instantiateObjectPropertyExpression subst var ([], opexp) + return [(annos, ObjectCardinality (Cardinality cType aInt opexp' mcexp'))] + _ -> return [(annos, cexp)] + +instantiateObjectPropertyExpression :: GSubst -> PatternVarMap -> (Annotations, ObjectPropertyExpression) -> Result (Annotations, ObjectPropertyExpression) +instantiateObjectPropertyExpression subst var (annos, obexp) = + case obexp of + ObjectProp i -> return (annos, ObjectProp $ instParamName subst i) -- nothing to instantiate + ObjectInverseOf opexp -> do + (_, opexp') <- instantiateObjectPropertyExpression subst var ([], opexp) + return (annos, ObjectInverseOf opexp') + ObjectPropertyVar b x -> do -- TODO: lists + let v = getIRIVal $ Map.findWithDefault (error $ "unknown var:" ++ show x ++ " subst:" ++ show subst) (x, "ObjectProperty") subst + return (annos, ObjectProp v) + UnsolvedObjProp _ -> error $ "unsolved object property at instantiation: " ++ show obexp + +instIndiv :: GSubst -> PatternVarMap -> IRI -> Result [IRI] +instIndiv subst var i = + if (i, "Individual") `elem` Map.keys subst then + let j = Map.findWithDefault (error "instIndiv") (i, "Individual") subst + in case j of + PlainVal v -> return [v] + _ -> error $ "expected plain value but got " ++ show j + else if (i, "list") `elem` Map.keys subst then + let j = Map.findWithDefault (error "instIndiv") (i, "list") subst + in case j of + ListVal k vs -> trace ("j:" ++ show j) $ if k == "Individual" then return vs else + if null vs then return vs else error $ "expected a list of individuals but got a list of "++ show k ++ "s instead" + _ -> error "plain value when expecting a list" + else return [instParamName subst i] + + +-- delete symbols from a solved macro, for optional parameters +deleteSymbolsMacro :: Set.Set Entity -> OntologyDocument -> Result OntologyDocument +deleteSymbolsMacro delSyms (OntologyDocument pd (Ontology n is as fs)) = do + fs' <- deleteSymbolsFrames delSyms fs + return $ OntologyDocument pd $ Ontology n is as fs' + +deleteSymbolsFrames :: Set.Set Entity -> [Frame] -> Result [Frame] +deleteSymbolsFrames delSyms fs = do + fs' <- mapM (deleteSymbolsFrame delSyms) fs + return $ concat fs' + +deleteSymbolsFrame :: Set.Set Entity -> Frame -> Result [Frame] +deleteSymbolsFrame delSyms f@(Frame ext fBits) = + case ext of + ClassEntity (VarExpression (MVar b i)) -> -- lists can't occur here + if Set.member i $ Set.map (\x -> idToIRI $ entityToId x) delSyms + then return [] + else do + fBits' <- mapM (deleteSymbolsFrameBit delSyms) fBits + return [Frame ext $ concat fBits'] + _ -> do + fBits' <- mapM (deleteSymbolsFrameBit delSyms) fBits + return [Frame ext $ concat fBits'] + +deleteSymbolsFrameBit :: Set.Set Entity -> FrameBit -> Result [FrameBit] +deleteSymbolsFrameBit delSyms fbit = + case fbit of + ListFrameBit mr lfb -> + case lfb of + ExpressionBit acexps -> do + let acexps' = filter (\ac -> classExpNoDeletedSymbol delSyms $ snd ac) acexps + case acexps' of + [] -> return [] + _ -> return [ListFrameBit mr $ ExpressionBit acexps'] + ObjectBit aopexps -> do + let aopexps' = filter (\ao -> objPropExpNoDeletedSymbol delSyms $ snd ao) aopexps + case aopexps' of + [] -> return [] + _ -> return [ListFrameBit mr $ ObjectBit aopexps'] + DataBit _adpexp -> return [] + IndividualSameOrDifferent ainds -> do + let ainds' = filter (\ai -> checkIRI delSyms NamedIndividual $ snd ai ) ainds + case ainds' of + [] -> return [] + _ -> return [ListFrameBit mr $ IndividualSameOrDifferent ainds'] + IndividualFacts afacts -> do + let afacts' = filter (\af -> factNoDelSym delSyms $ snd af) afacts + case afacts' of + [] -> return [] + _ -> return [ListFrameBit mr $ IndividualFacts afacts'] + _ -> return [fbit] + AnnFrameBit annos afb -> + case afb of + ClassDisjointUnion cexps -> do + let cexps' = filter (classExpNoDeletedSymbol delSyms) cexps + if length cexps' == length cexps then return [fbit] + else return [] + ClassHasKey opexps dpexps -> return [] -- TODO: no data properties yet + ObjectSubPropertyChain opexps -> do + let opexps' = filter (objPropExpNoDeletedSymbol delSyms) opexps + if length opexps' == length opexps then return [fbit] else return [] + _ -> return [fbit] + +factNoDelSym :: Set.Set Entity -> Fact -> Bool +factNoDelSym delSyms fact = + case fact of + ObjectPropertyFact _pn ope i -> + let + x = objPropExpNoDeletedSymbol delSyms ope + y = checkIRI delSyms NamedIndividual i + in x && y + _ -> False -- TODO: for now! + +checkIRI :: Set.Set Entity -> EntityType -> IRI -> Bool +checkIRI delSyms ck c = + case Set.toList $ Set.filter (\(Entity _ ik i) -> i == c && ik == ck) delSyms of + [] -> True + _ -> False + +classExpNoDeletedSymbol :: Set.Set Entity -> ClassExpression -> Bool +classExpNoDeletedSymbol delSyms cexp = trace ("checking:" ++ show cexp) $ + case cexp of + Expression c -> checkIRI delSyms Class c + UnsolvedClass c -> checkIRI delSyms Class c -- TODO: is this possible? + VarExpression (MVar b c) -> if b then True + else checkIRI delSyms Class c + ObjectJunction _jt cexps -> foldl (\a b -> a && b) True $ map (classExpNoDeletedSymbol delSyms) cexps + ObjectComplementOf cexp' -> classExpNoDeletedSymbol delSyms cexp' + ObjectOneOf inds -> foldl (\a b -> a && b) True $ map (checkIRI delSyms NamedIndividual) inds + ObjectValuesFrom _qt opexp cexp' -> + let + x = classExpNoDeletedSymbol delSyms cexp' + y = objPropExpNoDeletedSymbol delSyms opexp + in x && y + ObjectHasValue opexp ind -> + let + x = objPropExpNoDeletedSymbol delSyms opexp + y = checkIRI delSyms NamedIndividual ind + in x && y + ObjectHasSelf opexp -> + objPropExpNoDeletedSymbol delSyms opexp + ObjectCardinality (Cardinality _ _ opexp mcexp ) -> + let + x = case mcexp of + Nothing -> True + Just cexp' -> classExpNoDeletedSymbol delSyms cexp' + y = objPropExpNoDeletedSymbol delSyms opexp + in x && y + {- TODO: add these after handling dpexp! + | DataValuesFrom QuantifierType DataPropertyExpression DataRange + | DataHasValue DataPropertyExpression Literal + | DataCardinality (Cardinality DataPropertyExpression DataRange) -} + _ -> False + +objPropExpNoDeletedSymbol :: Set.Set Entity -> ObjectPropertyExpression -> Bool +objPropExpNoDeletedSymbol delSyms opexp = + case opexp of + ObjectProp op -> checkIRI delSyms ObjectProperty op + ObjectInverseOf opexp' -> objPropExpNoDeletedSymbol delSyms opexp' + ObjectPropertyVar b i -> if b then True else checkIRI delSyms ObjectProperty i + UnsolvedObjProp i -> checkIRI delSyms ObjectProperty i + +convertEntities :: Entity -> Entity -> SymbMapItems +convertEntities sym1 sym2 = + if entityKind sym1 == entityKind sym2 then + SymbMapItems (EntityType $ entityKind sym1) [(cutIRI sym1, Just $ cutIRI sym2)] + else error $ "kind mismatch:" ++ show sym1 ++ " " ++ show sym2 diff --git a/Static/AnalysisLibrary.hs b/Static/AnalysisLibrary.hs index 2564176bc8..eb4603653b 100644 --- a/Static/AnalysisLibrary.hs +++ b/Static/AnalysisLibrary.hs @@ -22,6 +22,8 @@ module Static.AnalysisLibrary , LNS ) where +--import Debug.Trace + import Logic.Logic import Logic.Grothendieck import Logic.Coerce @@ -159,7 +161,8 @@ 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 + missNames = -- trace ("spNs:" ++ show spNs ++ " declNs:" ++ show declNs) $ + Set.toList $ spNs Set.\\ declNs unDecls = map (addDownload True) $ filter (isNothing . (`lookupGlobalEnvDG` initDG)) missNames is = unDecls ++ is' @@ -205,7 +208,7 @@ anaStringAux mln lgraph opts topLns initDG mt file posFileName (_, libenv) -- lookup or read a library anaLibFile :: LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph -> LibName -> ResultT IO (LibName, LibEnv) -anaLibFile lgraph opts topLns libenv initDG ln = +anaLibFile lgraph opts topLns libenv initDG ln = -- trace ("known:" ++ show (Map.keys libenv)) $ let lnstr = show ln in case find (== ln) $ Map.keys libenv of Just ln' -> do analyzing opts $ "from " ++ lnstr @@ -369,6 +372,21 @@ anaGenericity lg libEnv ln dg opts eo name return (Genericity (Params ps') (Imported imps') pos, GenSig nsigI nsigPs $ JustNode ns, dg'') +anaImports :: LogicGraph -> LibEnv -> LibName -> DGraph -> HetcatsOpts + -> ExpOverrides -> NodeName -> IMPORTED + -> Result (IMPORTED, MaybeNode, DGraph) +anaImports lg libEnv ln dg opts eo name (Imported imps) = do + l <- lookupCurrentLogic "IMPORTS" lg + let baseNode = maybe (EmptyNode l) JustNode (currentBaseTheory dg) + (imps', nsigI, dg') <- case imps of + [] -> return ([], baseNode, dg) + _ -> do + (is', _, nsig', dgI) <- anaUnion False lg libEnv ln dg baseNode + (extName "Imports" name) opts eo imps $ getRange imps + return (is', JustNode nsig', dgI) + return (Imported imps', nsigI, dg') +-- TODO: this method should be called in anaGenericity + expCurieT :: GlobalAnnos -> ExpOverrides -> IRI -> ResultT IO IRI expCurieT ga eo = liftR . expCurieR ga eo @@ -376,7 +394,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 = -- trace ("itm:" ++ show itm) $ case itm of Spec_defn spn2 gen asp pos -> do let spn' = if null (iriToStringUnsecure spn2) then @@ -564,8 +582,241 @@ anaLibItem lg opts topLns currLn libenv dg eo itm = Newcomorphism_defn com _ -> ResultT $ do dg' <- anaComorphismDef com dg return $ Result [] $ Just (itm, dg', libenv, lg, eo) + Pattern_defn sname params imps body r -> do + let spn' = if null (iriToStringUnsecure sname) then + simpleIdToIRI $ mkSimpleId "Spec" else sname + spn <- expCurieT (globalAnnos dg) eo spn' + let spstr = iriToStringUnsecure spn + nName = makeName spn + analyzing opts $ "pattern " ++ spstr + -- spec names are parsed as unsolved. But here we solve them all to specs, no vars possible. + let imps'' = case imps of + Imported asps -> Imported $ + map (\asp -> + case item asp of + UnsolvedName x rg -> asp{item =Spec_inst x [] Nothing rg} + _ -> asp) + asps + (imps', nsigI, dg1) <- liftR $ anaImports lg libenv currLn dg opts eo nName imps'' + (params', pinfos, vMap, lastParam, dg2) <- liftR $ anaPatternParams lg libenv currLn dg1 opts eo nName nsigI params + (dg3, expBodySig) <- liftR $ anaPatternBody lg libenv currLn dg2 opts eo nName pinfos vMap nsigI lastParam body + -- pinfos are sent for locals, lastParam is needed to solve their parameters correctly + let entry = PatternEntry $ PatternSig False nsigI pinfos vMap expBodySig + itm' = Pattern_defn sname params' imps' (getBody expBodySig) r + genv = globalEnv dg3 + if Map.member spn genv + then + liftR $ plain_error (itm, dg, libenv, lg, eo) + (alreadyDefined spstr) r + else -- trace ("inserting:" ++ show entry) $ + return (itm', dg3{globalEnv = Map.insert spn entry genv}, + libenv, lg, eo) _ -> return (itm, dg, libenv, lg, eo) +anaPatternParams :: LogicGraph -> LibEnv -> LibName -> DGraph -> HetcatsOpts + -> ExpOverrides -> NodeName -> MaybeNode -> [PatternParam] + -> Result ([PatternParam], [PatternParamInfo], PatternVarMap, MaybeNode, DGraph) +anaPatternParams lg lenv ln dg opts eo name impN params = + foldM (\(plist, slist, vMap, aNode, aDG) param -> do + (p, s, vMap', bNode, bDG) <- anaPatternParam lg lenv ln aDG opts eo name vMap aNode param + return (plist ++ [p], slist ++ [s], vMap', bNode, bDG)) + ([], [], Map.empty, impN, dg) params + +anaPatternParam :: LogicGraph -> LibEnv -> LibName -> DGraph -> HetcatsOpts + -> ExpOverrides -> NodeName -> PatternVarMap -> MaybeNode -> PatternParam + -> Result (PatternParam, PatternParamInfo, PatternVarMap, MaybeNode, DGraph) +anaPatternParam lg lenv ln dg opts eo name vMap prevParamNode pParam = + case pParam of + StringParam i -> do + l <- lookupCurrentLogic "anaPatternParam" lg + return (pParam, StringParamInfo i, Map.insert i (False, "String") vMap, EmptyNode l, dg) + OntoParam isOpt aSpec -> do + (sp', psig, dg') <- anaSpecTop None False lg lenv ln dg prevParamNode name opts eo (item aSpec) nullRange + let aSpec' = aSpec{item = sp'} + aSig = getSig psig + iSig = case prevParamNode of + EmptyNode _ -> Nothing + JustNode x -> Just $ getSig x + (vMap', _) <- addSigSymsToVarMap vMap (mkIRI "") iSig aSig + return (OntoParam isOpt aSpec', + SingleParamInfo isOpt psig, + vMap', + JustNode psig, + dg') + ListParam oList -> + case oList of + EmptyParamList -> do + l <- lookupCurrentLogic "anaPatternParam" lg + return (ListParam oList, + ListParamInfo 0 True (EmptyNode l) Nothing, + vMap, + EmptyNode l, + dg) + OntoListCons aSpecs -> + case reverse aSpecs of + [] -> error "empty list, should never happen" + lastSpec : sps' -> do + let emptyListName = mkIRI "empty" + (lastSpecSolved, exactSize, listVar) = + case item lastSpec of + UnsolvedName x rg -> if x == emptyListName + then (lastSpec{item = EmptyList}, True, emptyListName) + else (lastSpec{item = ListVariable x}, False, x) + _ -> error "Last element of the list must be empty or a variable name" + (aSpecs', nsigs, dg') <- + foldM (\(slist, nlist, aDg) asp -> do + (sp', mnsig, bDg) <- anaListElem lg lenv ln aDg opts eo name vMap prevParamNode asp + return ( slist ++ [sp'] + , nlist ++ case mnsig of + EmptyNode _ -> [] + _ -> [mnsig] + , bDg) + ) + ([], [], dg) $ map item $ reverse $ lastSpecSolved : sps' + let oList' = map (\(x,y) -> x{item = y}) $ zip aSpecs aSpecs' + pParam' = ListParam $ OntoListCons oList' + size = length aSpecs - 1 -- TODO: check this! + firstNode = head nsigs + iSig = case prevParamNode of + EmptyNode _ -> Nothing + JustNode x -> Just $ getSig x + (vMap', newKinds) <- + foldM (\(f, k) nsig -> addSigSymsToVarMap f listVar iSig $ getSig nsig) (vMap, Set.empty) $ + map (\n -> case n of + JustNode x -> x + _ -> error "should never happen" + ) nsigs + let newK = case Set.toList newKinds of + [x] -> x + _ -> "ontology" + (vMap'', tailName) = if listVar == emptyListName then (vMap', Nothing) else (Map.insert listVar (True, "list") vMap', Just listVar) + return (pParam', ListParamInfo size exactSize firstNode tailName, vMap'', firstNode, dg') + +anaListElem :: LogicGraph -> LibEnv -> LibName -> DGraph -> HetcatsOpts + -> ExpOverrides -> NodeName -> PatternVarMap -> MaybeNode -> SPEC + -> Result (SPEC, MaybeNode, DGraph) +anaListElem lg lenv ln dg opts eo name vMap prevParamNode sp = do + l <- lookupCurrentLogic "anaListElem" lg + case sp of + EmptyList -> return (sp, EmptyNode l, dg) + ListVariable _ -> return (sp, EmptyNode l, dg) + _ -> do + (sp', nsig, bDg) <- anaSpecTop None False lg lenv ln dg + prevParamNode name opts eo + sp nullRange + return (sp', JustNode nsig, bDg) + +addSigSymsToVarMap :: PatternVarMap -> IRI -> Maybe G_sign -> G_sign -> Result (PatternVarMap, Set.Set String) +addSigSymsToVarMap vMap tailName exclSig aSig = + case aSig of + G_sign lid (ExtSign sig _) _ -> do + let syms = symset_of lid sig + symsExcl <- case exclSig of + Nothing -> return Set.empty + Just (G_sign lidE (ExtSign sigE _) _) -> do + sigE' <- coercePlainSign lidE lid "coerce in addSigSymsToVarMap" sigE + return $ symset_of lid sigE' + let insertOrFail f s k = + let sIRI = idToIRI $ sym_name lid s in + if sIRI `elem` Map.keys f then + error $ "variable named " ++ show s ++ "already used in " ++ show f + else (Map.insert sIRI (if sIRI == tailName then (True, "list") else (False, symKind lid s)) f, Set.insert (symKind lid s) k) + (vMap', newKinds) = foldl (\(f, k) s -> insertOrFail f s k) (vMap, Set.empty) $ Set.toList $ Set.difference syms symsExcl + return (vMap', newKinds) + +anaPatternBody :: LogicGraph -> LibEnv -> LibName -> DGraph -> HetcatsOpts + -> ExpOverrides -> NodeName -> [PatternParamInfo] -> PatternVarMap -> MaybeNode -> MaybeNode -> LocalOrSpec -> + Result (DGraph, LocalOrSpecSig) +anaPatternBody lg lenv ln dg opts eo name pinfos vMap impNode lastParam body = + case body of + Spec_pattern aspec -> do + sp'<- solveBody lg lenv ln dg opts eo name vMap impNode $ item aspec + -- trace ("sp':" ++ show sp') $ + -- trace ("solvedBody:" ++ show sp') $ + return (dg, SpecSig $ Spec_pattern aspec{item = sp'}) + Local_pattern locals aspec -> do + (dg', psigs, items) <- solveLocals lg lenv ln dg opts eo name pinfos vMap impNode lastParam locals + --let vMap' = foldl Map.union vMap $ map (\(PatternSig _ _ _ f _) -> f) $ Map.elems psigs + sp' <- solveBody lg lenv ln dg' opts eo name vMap impNode $ item aspec + return (dg', LocalSig psigs $ Local_pattern items $ aspec{item = sp'}) + +solveLocals :: LogicGraph -> LibEnv -> LibName -> DGraph -> HetcatsOpts + -> ExpOverrides -> NodeName -> [PatternParamInfo] -> PatternVarMap -> MaybeNode -> MaybeNode -> [LIB_ITEM] -> + Result (DGraph ,Map.Map IRI PatternSig, [LIB_ITEM]) +solveLocals lg lenv ln dg opts eo name pinfos vMap impNode lastParam locals = do + (dg', psigs, items) <- + foldM (\(dg0, psigs0, items0) l -> do + (dg1, psigs1, lItem) <- solveLocal lg lenv ln dg0 opts eo name pinfos vMap impNode lastParam l + return (dg1, Map.union psigs0 psigs1, items0 ++ [lItem])) + (dg, Map.empty, []) locals + return (dg', psigs, items) + +solveLocal :: LogicGraph -> LibEnv -> LibName -> DGraph -> HetcatsOpts + -> ExpOverrides -> NodeName -> [PatternParamInfo] -> PatternVarMap -> MaybeNode -> MaybeNode -> LIB_ITEM -> + Result (DGraph, Map.Map IRI PatternSig, LIB_ITEM) +solveLocal lg lenv ln dg opts eo name pinfos vMap impNode lastParam local = + case local of + Pattern_defn lname lparams limp (Spec_pattern asp) lRange -> do + (lparams', pinfos', vMap', _aNode, dg1) <- anaPatternParams lg lenv ln dg opts eo (makeName lname) lastParam lparams + let intVMap = Map.intersection vMap vMap' + if intVMap == Map.empty + then do + sp' <- solveBody lg lenv ln dg1 opts eo name (Map.union vMap vMap') impNode $ item asp + let asp' = asp {item = sp'} + lpsig = PatternSig True impNode (pinfos') vMap' $ SpecSig $ Spec_pattern asp' + -- here always add the parameters of the global pattern before those of the local one + -- should be pinfos ++ pinfos' + -- but: if we don't do this,then the lists of formal and actual params with match during instantiation + -- trace ("solved local:" ++ show lpsig) $ + return (dg1, Map.fromAscList [(lname, lpsig)], + Pattern_defn lname lparams' limp (Spec_pattern asp') lRange) + -- trace ("sp':" ++ show sp') $ error "solveLocal nyi" + else fail $ "redeclaring variables in local pattern:" ++ (show $ Map.keys intVMap) + _ -> fail $ "only pattern definitions allowed in local part of a pattern" + +solveBody :: LogicGraph -> LibEnv -> LibName -> DGraph -> HetcatsOpts + -> ExpOverrides -> NodeName -> PatternVarMap -> MaybeNode -> SPEC -> + Result SPEC +solveBody lg lenv ln dg opts eo name vMap impNode sp = + case sp of + UnsolvedName i rg -> if i `elem` Map.keys vMap then + let (_, j) = Map.findWithDefault (error "just checked") i vMap + in if j == "list" then return $ ListVariable i + else return $ NormalVariable i + else return sp -- can't solve now, will be solved later + Basic_spec (G_basic_spec lid bspec) r -> do + iSyms <- case impNode of + EmptyNode _ -> return Set.empty + JustNode n -> + case getSig n of + G_sign lidI (ExtSign sigI _) _ -> do + sigI' <- coercePlainSign lidI lid "solveBody" sigI -- TODO: heterogenity won't work + return $ symset_of lid sigI' + bspec' <- solve_symbols lid iSyms vMap bspec + return $ Basic_spec (G_basic_spec lid bspec') r + Extension aspecs r -> do + aspecs' <- mapM (solveBody lg lenv ln dg opts eo name vMap impNode) (map item aspecs) + return $ Extension (map (\(x,y) -> x{item = y}) $ zip aspecs aspecs') r + Union aspecs r -> do + aspecs' <- mapM (solveBody lg lenv ln dg opts eo name vMap impNode) (map item aspecs) + return $ Union (map (\(x,y) -> x{item = y}) $ zip aspecs aspecs') r + Group aspec r -> do + sp' <- solveBody lg lenv ln dg opts eo name vMap impNode $ item aspec + return $ Group (aspec{item = sp'}) r + Spec_inst n fitArgs miri r -> do + let solveFitArgs f = + case item f of + Fit_spec asp gm rg -> do + sp'<- solveBody lg lenv ln dg opts eo name vMap impNode $ item asp + return $ f{item = Fit_spec asp{item = sp'} gm rg} + _ -> return f + fitArgs' <- mapM solveFitArgs fitArgs + return $ Spec_inst n fitArgs' miri r -- maybe here unsolved arguments should be solved to variables! + OntoList aspecs -> do + aspecs' <- mapM (solveBody lg lenv ln dg opts eo name vMap impNode) $ map item aspecs + return $ OntoList $ map (\(x,y) -> x{item = y}) $ zip aspecs aspecs' + _ -> error $ show sp + symbolsOf :: LogicGraph -> G_sign -> G_sign -> [CORRESPONDENCE] -> Result (Set.Set (G_symbol, G_symbol)) symbolsOf lg gs1@(G_sign l1 (ExtSign sig1 sys1) _) @@ -666,7 +917,7 @@ anaViewDefn lg ln libenv dg opts eo vn gen vt gsis pos = do tmor <- gEmbedComorphism imor gsigmaS'' fmor <- comp mor tmor return (gsigmaS', fmor) - emor <- fmap gEmbed $ anaGmaps lg opts pos gsigmaS' gsigmaT hsis + emor <- fmap gEmbed $ anaGmaps lg opts pos gsigmaS' gsigmaT Nothing hsis -- TODO: Nothing for now! gmor <- comp tmor emor let vsig = ExtViewSig src gmor $ ExtGenSig gsig tar voidView = nodeS == nodeT && isInclusion gmor diff --git a/Static/AnalysisStructured.hs b/Static/AnalysisStructured.hs index b841b96448..da83d3fb64 100644 --- a/Static/AnalysisStructured.hs +++ b/Static/AnalysisStructured.hs @@ -53,6 +53,7 @@ import Static.GTheory import Syntax.AS_Structured import Syntax.Print_AS_Structured +import Syntax.AS_Library import Common.AS_Annotation hiding (isAxiom, isDef) import Common.Consistency @@ -65,6 +66,7 @@ import Common.LibName import Common.Result import Common.Utils (number) import Common.Lib.MapSet (imageSet, setInsert) +import qualified Common.OrderedMap as OMap import Data.Graph.Inductive.Graph import qualified Data.Set as Set @@ -79,6 +81,9 @@ import Proofs.ComputeColimit (insertColimitInGraph) import Common.Lib.Graph import Static.ComputeTheory +import Static.History + +import Debug.Trace -- overrides CUIRIE expansion for Download_items type ExpOverrides = Map.Map IRI FilePath @@ -320,7 +325,8 @@ anaSpecAux conser addSyms optNodes lg if isStructured opts then return (bspec, mkExtSign $ empty_signature lid, []) else - let res@(Result ds mb) = extBasicAnalysis lid (getName name) + let res@(Result ds mb) = -- trace ("sig in extBasicAnalysis:" ++ show sig ++ " bspec:" ++ show bspec) $ + extBasicAnalysis lid (getName name) ln bspec sig $ globalAnnos dg0 in case mb of Nothing | null ds -> @@ -339,7 +345,8 @@ anaSpecAux conser addSyms optNodes lg (if addSyms then Set.union sys sysd else sysd) $ symset_of lid sigma_complete) startSigId (toThSens ax) startThId - dg'' <- createConsLink DefLink conser lg dg' nsig' ns DGLinkExtension + dg'' <- -- trace ("gsysd:" ++ show gsysd) $ + createConsLink DefLink conser lg dg' nsig' ns DGLinkExtension return (Basic_spec (G_basic_spec lid bspec') pos, ns, dg'') EmptySpec pos -> case nsig of EmptyNode _ -> do @@ -523,10 +530,40 @@ 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 + Spec_inst spname' afitargs mImp pos0 -> trace ("\n\n**** ana spec inst *** " ++ show spname' ++ " afitargs:" ++ show afitargs) $ do spname <- expCurieR (globalAnnos dg) eo spname' let pos = if null afitargs then iriPos spname else pos0 adjustPos pos $ case lookupGlobalEnvDG spname dg of + Just (PatternEntry patSig@(PatternSig _local imp params vMap _body)) -> -- trace ("patSig:" ++ show patSig) $ + -- 1. solve afitargs using params and imp + case (length afitargs, length params) of + (la, lp) -> do + if (la == lp) && la > 0 then do + crtL@(Logic cl) <- lookupCurrentLogic "anaGmaps" lg + (afitargs', patSig'@(PatternSig _local _imp' _params' vMap' bodySig), dg', nsig', gm', subst) <- anaPatternInstArgs lg libEnv opts eo ln dg imp nsig name spname patSig Nothing (EmptyNode crtL) afitargs -- no previous morphism and sig, therefore nothing + -- let body' = getBody bodySig + (dg2, lastParamAndNewNodes, spB) <- --trace ("calling instMacro on " ++ show spname' ++ "[" ++ show afitargs ++ "] subst:" ++ show subst ++ " gm':" ++ show gm') $ + instantiateMacro lg libEnv opts eo ln dg' imp (JustNode nsig') name spname subst vMap' gm' bodySig + (dgI, allPrevDefs) <- unionNodes lg dg2 (makeName $ mkIRI "TESTNAME") $ nub lastParamAndNewNodes + --the body should extend the last argument + (sp', nsig'', dg3) <- -- trace ("spB:" ++ show spB) $ + anaSpecTop conser addSyms lg libEnv ln dgI (JustNode allPrevDefs) + name -- (makeName $ addSuffixToIRI "_source" $ getName name) + opts eo (item spB) nullRange + -- TODO: nsig' should be the node of instantiateMacro!!! + --incl <- ginclusion lg (getSig nsig') (getSig nsig'') + --let dg3 = insLink dg'' incl globalDef SeeTarget (getNode nsig') (getNode nsig'') + -- trace ("sp':" ++ show sp' ++ " nsig'':" ++ show nsig'' ++ "dg3:"++ show (labEdges $ dgBody dg3)) $ + trace ("dg3:"++ show (length $ nodes $ dgBody dg3) ++ " theorem links:" ++ show (length $ filter (\(_,_, dglab) -> isGlobalThm $ dgl_type dglab) $ labEdges $ dgBody dg3)) $ + trace ("afitargs':" ++ show afitargs') $ + return (Spec_inst spname' afitargs' mImp pos0, nsig'', dg3) -- was nsig'' + else if la == 0 then error "arguments missing in instantiation" + else if lp == 0 then error "pattern without arguments" + else error $ "mismatch in length of arguments:" ++ show la ++ " " ++ show lp + -- 2. generate fitting morphisms and theorem links from the params to the nodes of fitargs + -- 3. substitute vars in body using the fitting morphisms -> a structured DOL spec, Body + -- here is also where the missing arguments induce rejections in the body + -- 4. replace the P[A1; ... An] with (Imp then A1) and ... and (Imp then An) then Body Just (SpecEntry gs@(ExtGenSig (GenSig _ params _) body@(NodeSig nB gsigmaB))) -> case (length afitargs, length params) of @@ -542,11 +579,13 @@ anaSpecAux conser addSyms optNodes lg gsigma <- gsigUnionMaybe lg addSyms nsig gsigmaB let (fsig@(NodeSig node _), dg2) = insGSig dg name (DGInst spname) gsigma - incl <- ginclusion lg gsigmaB gsigma + incl <- -- trace ("gsigmaB:" ++ show gsigmaB ++ " gsigma:" ++ show gsigma) $ + ginclusion lg gsigmaB gsigma let dg3 = case nsig of JustNode (NodeSig nI _) | nI == nB -> dg2 _ -> insLink dg2 incl globalDef (DGLinkMorph spname) nB node - dg4 <- createConsLink DefLink conser lg dg3 nsig fsig SeeTarget + dg4 <- -- trace ("nsig:" ++ show nsig ++ " fsig:" ++ show fsig) $ + createConsLink DefLink conser lg dg3 nsig fsig SeeTarget return (sp, fsig, dg4) -- now the case with parameters (la, lp) | la == lp -> do @@ -615,7 +654,10 @@ anaSpecAux conser addSyms optNodes lg let (cNodes', cEdges') = networkDiagram dg cItems eItems (ns, dg') <- insertColimitInGraph libEnv ln dg cNodes' cEdges' name return (sp, ns, dg') - _ -> fail $ "AnalysisStructured: " ++ show (prettyLG lg sp) + UnsolvedName x pos -> -- this should not happen, but when it does, solve as spec_inst. + anaSpecAux conser addSyms optNodes lg + libEnv ln dg nsig name opts eo (Spec_inst x [] Nothing pos) rg + _ -> fail $ "in AnalysisStructured: " ++ show (prettyLG lg sp) -- | build the diagram of a network specified as a list of network elements to be added @@ -751,6 +793,21 @@ anaExtraction lg libEnv ln dg nsig name rg (ExtractOrRemove b iris _) = if not b let dg'' = insLink dg' incl globalThm SeeSource (getNode nsig') n return (nsig', dg'') +unionNodes :: LogicGraph -> DGraph -> NodeName -> [NodeSig] -> Result (DGraph, NodeSig) +unionNodes lg dg name nsigs = + case nsigs of + [ns] -> return (dg, ns) + _ -> do + let nsigs' = reverse nsigs + gbigSigma <- gsigManyUnion lg (map getSig nsigs') + let (ns@(NodeSig node _), dg2) = insGSig dg name + DGUnion gbigSigma + insE dgl (NodeSig n gsigma) = do + incl <- ginclusion lg gsigma gbigSigma + return $ insLink dgl incl globalDef SeeTarget n node + dg3 <- foldM insE dg2 nsigs' + return (dg3, ns) + anaUnion :: Bool -> LogicGraph -> LibEnv -> LibName -> DGraph -> MaybeNode -> NodeName -> HetcatsOpts -> ExpOverrides -> [Annoted SPEC] -> Range -> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph) @@ -991,16 +1048,25 @@ partitionGmaps l = let G_logic_translation _ -> False) $ reverse l in (reverse rs, reverse hs) -anaGmaps :: LogicGraph -> HetcatsOpts -> Range -> G_sign -> G_sign +anaGmaps :: LogicGraph -> HetcatsOpts -> Range -> G_sign -> G_sign -> Maybe G_morphism -> [G_mapping] -> Result G_morphism -anaGmaps lg opts pos psig@(G_sign lidP sigmaP _) asig@(G_sign lidA sigmaA _) +anaGmaps lg opts pos psig@(G_sign lidP sigmaP _) asig@(G_sign lidA sigmaA _) mgm gsis = adjustPos pos $ if isStructured opts then return $ mkG_morphism lidP $ ext_ide sigmaP - else if null gsis then do + else do + if null gsis then do -- trace ("gsis is null psig:" ++ show psig ++ " asig:" ++ show asig) $ do (G_sign lidP' sigmaP' _, _) <- gSigCoerce lg psig (Logic lidA) sigmaA' <- coerceSign lidA lidP' "anaGmaps" sigmaA + prevMap <- case mgm of + Nothing -> return Map.empty + Just prevGMor -> + case prevGMor of + G_morphism prevLid prevMor _ -> do + prevMor' <- coerceMorphism prevLid lidP' "anaGmaps:coerceMorphism" prevMor + let symMap = symmap_of lidP' prevMor' + return $ Map.mapKeys (symbol_to_raw lidP') $ Map.map (symbol_to_raw lidP') symMap fmap (mkG_morphism lidP') $ - ext_induced_from_to_morphism lidP' Map.empty sigmaP' sigmaA' + ext_induced_from_to_morphism lidP' prevMap sigmaP' sigmaA' else do cl <- lookupCurrentLogic "anaGmaps" lg G_symb_map_items_list lid sis <- homogenizeGM cl gsis @@ -1008,10 +1074,21 @@ anaGmaps lg opts pos psig@(G_sign lidP sigmaP _) asig@(G_sign lidA sigmaA _) sigmaP' <- coerceSign lidP' lid "anaGmaps1" sigmaP'' (G_sign lidA' sigmaA'' _, _) <- gSigCoerce lg asig (Logic lid) sigmaA' <- coerceSign lidA' lid "anaGmaps2" sigmaA'' - rmap <- stat_symb_map_items lid (plainSign sigmaP') + rMap <- stat_symb_map_items lid (plainSign sigmaP') (Just $ plainSign sigmaA') sis + prevMap <- case mgm of + Nothing -> return Map.empty + Just prevGMor -> + case prevGMor of + G_morphism prevLid prevMor _ -> do + prevMor' <- coerceMorphism prevLid lid "anaFitArg:coerceMorphism" prevMor + let symMap = symmap_of lid prevMor' + return $ Map.mapKeys (symbol_to_raw lid) $ Map.map (symbol_to_raw lid) symMap + let crtMap = if Map.intersection rMap prevMap == Map.empty + then Map.union rMap prevMap + else error $ "trying to map previously mapped symbol:" ++ (show $ Map.intersection rMap prevMap) -- TODO: don't fail if the symbols are mapped in the same way fmap (mkG_morphism lid) - $ ext_induced_from_to_morphism lid rmap sigmaP' sigmaA' + $ ext_induced_from_to_morphism lid crtMap sigmaP' sigmaA' {- let symI = sym_of lidP sigmaI' @@ -1024,28 +1101,184 @@ anaGmaps lg opts pos psig@(G_sign lidP sigmaP _) asig@(G_sign lidA sigmaA _) -- also output symbols that are affected -} +-- TODO: analysis of fit args must be different for non-local patterns +-- the signature morphism will not expand the previous definitions +-- different argument in the call in spec_inst!!!! + anaFitArg :: LogicGraph -> LibEnv -> LibName -> DGraph -> IRI -> MaybeNode - -> NodeSig -> HetcatsOpts -> NodeName -> ExpOverrides -> FIT_ARG + -> NodeSig -> HetcatsOpts -> NodeName -> ExpOverrides + -> MaybeNode -> MaybeNode -> Maybe G_morphism -> GSubst -> FIT_ARG -> Result (FIT_ARG, DGraph, (G_morphism, NodeSig)) -anaFitArg lg libEnv ln dg spname nsigI nsigP@(NodeSig nP gsigmaP) opts name eo fv = +anaFitArg lg libEnv ln dg spname nsigI nsigP@(NodeSig nP gsigmaP) opts name eo csig prevSig mgm prevSubst fv = let ga = globalAnnos dg in case fv of + Fit_string s _ -> error $ "nyi for " ++ (show s) Fit_spec asp gsis pos -> do - (sp', nsigA, dg') <- anaSpec False True lg libEnv ln + (sp', nsigA', dg0) <- -- trace ("calling ana spec:" ++ show asp ++ " nsigI:"++ show nsigI ++ "nsigP:" ++ show nsigP)$ + anaSpec False True lg libEnv ln dg nsigI name opts eo (item asp) pos - (_, Comorphism aid) <- + -- if the context and the previous argument are both not EmptyNodes + -- unite the argument, the context and the previous argument + (nsigA, dg') <- + case (prevSig, csig) of + (EmptyNode _, EmptyNode _) -> return (nsigA', dg0) + _ -> do + let pN = case prevSig of + EmptyNode _ -> [] + JustNode x -> [x] + cN = case csig of + EmptyNode _ -> [] + JustNode x -> [x] + gbigSigma <- gsigManyUnion lg $ map getSig $ + pN ++ cN ++ [nsigA'] + let (uSig@(NodeSig unode _), dg1) = insGSig dg0 (extName "Union" name) + DGUnion gbigSigma + insE dgl (NodeSig n gs) = do + incl <- ginclusion lg gs gbigSigma + -- trace ("inclusion for:" ++ show gs ++ " is " ++ show incl ) $ + return $ insLink dgl incl globalDef SeeTarget n unode + dg2 <- foldM insE dg1 $ pN ++ cN ++ [nsigA'] + return (uSig, dg2) + (_, Comorphism aid) <- -- trace ("nsigA:" ++ show nsigA) $ logicUnion lg (getNodeLogic nsigP) (getNodeLogic nsigA) let tl = Logic $ targetLogic aid - (nsigA'@(NodeSig nA' gsigA'), dg'') <- coerceNode lg dg' nsigA name tl + (nsigA''@(NodeSig nA' gsigA'), dg'') <- coerceNode lg dg' nsigA name tl (gsigmaP', pmor) <- gSigCoerce lg gsigmaP tl tmor <- gEmbedComorphism pmor gsigmaP - gmor <- anaGmaps lg opts pos gsigmaP' gsigA' gsis + gmor <- -- trace ("gsis:" ++ show gsis ++ " gsigmaP':" ++ show gsigmaP' ++ " gsigA':" ++ show gsigA' ++ " mgm:" ++ show mgm) $ + anaGmaps lg opts pos gsigmaP' gsigA' mgm gsis eGmor <- comp tmor $ gEmbed gmor return ( Fit_spec (replaceAnnoted sp' asp) gsis pos , if nP == nA' && isInclusion eGmor then dg'' else insLink dg'' eGmor globalThm (DGLinkInst spname $ Fitted gsis) nP nA' - , (gmor, nsigA')) + , (gmor, nsigA'')) + Fit_ctx (G_symbol slid ssym) (G_symbol tlid tsym) pos -> do + let tRSym = symbol_to_raw slid $ coerceSymbol tlid slid tsym + sRSym = symbol_to_raw slid ssym + case csig of + EmptyNode _ -> error "anaFitArg: empty context" -- should never happen + JustNode c -> do + (nsigA@(NodeSig na sigA), dg') <- + case (prevSig, nsigI) of + (EmptyNode _, EmptyNode _) -> return (c, dg) + (EmptyNode _, JustNode i) -> do -- first argument is an abbreviation, unite i and c + gUnionSig <- gsigManyUnion lg $ map getSig [c, i] + let (usig@(NodeSig unode _), dg0) = + insGSig dg (extName "Union" name) DGUnion gUnionSig + insE dgl (NodeSig n gs) = do + incl <- ginclusion lg gs gUnionSig + return $ insLink dgl incl globalDef SeeTarget n unode + dg1 <- foldM insE dg0 [c, i] + return (usig, dg1) + (JustNode x, _) -> do -- isig should be already in prevSig, don't add another link + gUnionSig <- gsigManyUnion lg $ map getSig [c, x] + let (usig@(NodeSig unode _), dg0) = + insGSig dg (extName "Union" name) DGUnion gUnionSig + insE dgl (NodeSig n gs) = do + incl <- ginclusion lg gs gUnionSig + return $ insLink dgl incl globalDef SeeTarget n unode + dg1 <- foldM insE dg0 [c, x] + return (usig, dg1) + ssig <- case gsigmaP of + G_sign plid psig _ -> coerceSign plid slid "anaFitArg:coercePlainSign" psig + tsig <- case sigA of + G_sign plid psig _ -> coerceSign plid slid "anaFitArg:coercePlainSign" psig + prevMap <- case mgm of + Nothing -> return Map.empty + Just prevGMor -> + case prevGMor of + G_morphism prevLid prevMor _ -> do + prevMor' <- coerceMorphism prevLid slid "anaFitArg:coerceMorphism" prevMor + let symMap = symmap_of slid prevMor' + isysms = case nsigI of + EmptyNode _ -> Set.empty + JustNode inode -> case getSig inode of + G_sign ilid (ExtSign isig _) _ -> Set.map (\x -> coerceSymbol ilid slid x) $ symset_of ilid isig + -- trace ("***isysms:" ++ show isysms) $ + return $ Map.mapKeys (symbol_to_raw slid) $ Map.map (symbol_to_raw slid) $ + Map.filterWithKey (\x _ -> not $ Set.member x isysms) symMap -- TODO: dont map the symbols in imports! + let crtMapAux = Map.fromList [(sRSym, tRSym)] + crtMap = if Map.intersection crtMapAux prevMap == Map.empty + then Map.union prevMap crtMapAux + else error $ "trying to map previously mapped symbol:" ++ (show $ Map.intersection crtMapAux prevMap) -- TODO: don't fail if the symbols are mapped in the same way + mor <- -- trace ("\n***********************\ninduced:" ++ show crtMap ++ " ssig:" ++ show ssig ++ " tsig:" ++ show tsig) $ + induced_from_to_morphism slid crtMap ssig tsig + let gmor = mkG_morphism slid mor + dg'' = insLink dg' (gEmbed gmor) globalThm (DGLinkInstArg spname) nP na + return (fv, dg'', (gmor, nsigA)) + Fit_new (G_symbol slid ssym) (G_symbol tlid tsym) pos -> do + -- trace ("_________________________mgm in fit_new:" ++ show mgm ++ "\n_________nsigP:" ++ show nsigP ++ "\n_____prevSig:" ++ show prevSig ++ "\n ssym:" ++ show ssym ++ "\ntsym:" ++ show tsym) $ do + let tRSym = symbol_to_raw slid $ coerceSymbol tlid slid tsym + sRSym = symbol_to_raw slid ssym + sigA <- add_symb_to_sign tlid (empty_signature tlid) tsym + let extSigA = ExtSign sigA (Set.singleton tsym) + (asig@(NodeSig a gA), dg0) = insGSig dg (extName "Actual" name) (DGInst spname) $ G_sign tlid extSigA startSigId + uNodes = (case csig of + EmptyNode _ -> [] + JustNode x -> [x]) ++ + (case prevSig of + EmptyNode _ -> case nsigI of + EmptyNode _ -> [] + JustNode x -> [x] + JustNode x -> [x]) + gUnionSig <- -- trace ("\nextSigA:" ++ show extSigA ++ " unodes:" ++ (show $ map getSig uNodes)) $ + gsigManyUnion lg $ [gA] ++ map getSig uNodes + let (usig@(NodeSig unode _), dg1) = + insGSig dg0 (extName "Union" name) DGUnion gUnionSig + insE dgl (NodeSig n gs) = do + incl <- -- trace ("\n=============\ninclusion from " ++ show gs ++ "\n\nto " ++ show gUnionSig) $ + ginclusion lg gs gUnionSig + return $ insLink dgl incl globalDef SeeTarget n unode + dg2 <- foldM insE dg1 $ asig:uNodes + ssig@(ExtSign pssig _) <- case gsigmaP of + G_sign plid psig _ -> coerceSign plid slid "anaFitArg:coercePlainSign" psig + tsig <- case gUnionSig of + G_sign plid psig _ -> coerceSign plid slid "anaFitArg:coercePlainSign" psig + prevMap <- -- trace ("\n=============\nmgm:"++ show mgm ++ "\nssig:"++show ssig ++ "\ntsig:"++ show tsig) $ + case mgm of + Nothing -> return Map.empty + Just prevGMor -> + case prevGMor of + G_morphism prevLid prevMor _ -> do + prevMor' <- coerceMorphism prevLid slid "anaFitArg:coerceMorphism" prevMor + let symMap = symmap_of slid prevMor' + isysms = case nsigI of + EmptyNode _ -> Set.empty + JustNode inode -> case getSig inode of + G_sign ilid (ExtSign isig _) _ -> Set.map (\x -> coerceSymbol ilid slid x) $ symset_of ilid isig + -- trace ("symMap:" ++ show symMap) $ + return $ Map.mapKeys (symbol_to_raw slid) $ Map.map (symbol_to_raw slid) $ + Map.filterWithKey (\x _ -> not $ Set.member x isysms) symMap + let crtMapAux = Map.fromList [(sRSym, tRSym)] + substMap = Map.fromList $ concatMap (\((xIRI, xKind),y)-> case y of + PlainVal yIRI -> let xSym = symbol_to_raw slid $ new_symbol slid xIRI xKind + ySym = symbol_to_raw slid $ new_symbol slid yIRI xKind + + in -- [(xSym, ySym)] + if Set.member xSym (Set.map (symbol_to_raw slid) $ symset_of slid pssig) + then [(xSym, ySym)] + else [] + _ -> []) $ Map.toList prevSubst + crtMap = if Map.intersection crtMapAux prevMap == Map.empty + then Map.union prevMap crtMapAux + else -- don't fail if the symbols are mapped in the same way + let intersMapKeys = Map.keys $ Map.intersection crtMapAux prevMap + allMappedSameWay = foldl (\b k -> let v1 = Map.findWithDefault (error "not in crt") k crtMapAux + v2 = Map.findWithDefault (error "not in prev") k prevMap + in (v1 == v2) && b + ) True intersMapKeys + in Map.union crtMapAux prevMap -- TODO: why does the check fail? + --if allMappedSameWay then Map.union prevMap crtMapAux + --else + -- error $ "trying to map previously mapped symbol:" ++ (show $ Map.intersection crtMapAux prevMap) + mor <- -- trace ("\n=============\nssig:"++ show ssig ++ "\n tsig:" ++ show tsig ++ "\n prevMap:" ++ show prevMap ++ "\n substMap:" ++ show substMap) $ + induced_from_to_morphism slid (Map.union crtMap substMap) ssig tsig + let gmor = mkG_morphism slid mor + dg'' = -- trace ("gmor after induced:" ++ show gmor) $ + insLink dg2 (gEmbed gmor) globalThm (DGLinkInstArg spname) nP unode + return (fv, dg'', (gmor, usig)) + -- trace ("sigA:" ++ show usig) $ error "fit_new nyi" Fit_view vn' afitargs pos -> do vn <- expCurieR ga eo vn' case lookupGlobalEnvDG vn dg of @@ -1106,7 +1339,7 @@ anaFitArgs :: LogicGraph -> LibEnv -> HetcatsOpts -> ExpOverrides -> LibName -> -> Result ([FIT_ARG], DGraph, [(G_morphism, NodeSig)], NodeName) anaFitArgs lg libEnv opts eo ln spname imps (fas', dg1, args, name') (nsig', fa) = do let n1 = inc name' - (fa', dg', arg) <- anaFitArg lg libEnv ln dg1 spname imps nsig' opts n1 eo fa + (fa', dg', arg) <- anaFitArg lg libEnv ln dg1 spname imps nsig' opts n1 eo imps imps Nothing Map.empty fa -- TODO: this is wrong! return (fa' : fas', dg', arg : args, n1) anaAllFitArgs :: LogicGraph -> LibEnv -> HetcatsOpts -> ExpOverrides -> LibName -> DGraph @@ -1128,6 +1361,596 @@ anaAllFitArgs lg libEnv opts eo ln dg nsig name spname return ( zipWith replaceAnnoted (reverse fitargs') afitargs, dg3 , (morDelta, gsigma', ns)) +anaPatternInstArgs :: LogicGraph -> LibEnv -> HetcatsOpts -> ExpOverrides -> LibName -> DGraph + -> MaybeNode -> MaybeNode + -> NodeName -> IRI -> PatternSig -> Maybe G_morphism -> MaybeNode -> [Annoted FIT_ARG] + -> Result ([Annoted FIT_ARG], PatternSig, DGraph, NodeSig, Maybe G_morphism, GSubst) +anaPatternInstArgs lg libEnv opts eo ln dg isig csig name spname + psig@(PatternSig local imps params vMap body) mgm crtNode afitargs = trace ("in anaPatternInstArgs name:" ++ show name) $ do + l@(Logic crtLid) <- lookupCurrentLogic "anaPatternInstArgs" lg + -- before the arguments are analysed, we have to go through their list + -- and check if any Missing_arg nullRange appears + -- if it does, check that it occurs on the position of an optional parameter + -- if it doesn't give an error + -- else construct a new PatternSig that keeps only the present parameters and has a new body + -- add it temporarily to globalEnv and proceed, then restore the old definition + let zipped = zip params afitargs + idImps <- case isig of + EmptyNode _ -> return Nothing + JustNode (NodeSig _ gisig) -> + case gisig of + G_sign ilid (ExtSign esig _) _ -> do + esig' <- coercePlainSign ilid crtLid "coerceSign in anaPatternInstArgs" esig + let emor = ide esig' + return $ Just $ G_morphism crtLid emor startMorId + let startMor = case mgm of + Nothing -> idImps + Just _ -> mgm + (missingNodes, zipped', _, dgP) <- + foldM (\(ns, ls, lastParam, dg0) ((p,a), i) -> + case item a of + Missing_arg _ -> -- trace ("p:" ++ show p) $ + case p of + SingleParamInfo True parSig -> return (ns ++ [parSig], ls, lastParam, dg0) + _ -> fail $ "unexpected missing argument for non-optional parameter:" ++ show p + _ -> do --TODO: remove missing symbols only! if there were missing arguments before! + (dg1, newParam, p') <- removeMissingSymbolsParam lg libEnv ln dg0 lastParam ns name i p + -- don't return p, add a new node in the DG extending the previous argument that removes all symbols and sentences from dgn_theory p + -- that include symbols from ns + return $ (ns, ls ++ [(p',a)], newParam, dg1) ) + ([], [], isig, dg) $ zip zipped [1..] + (afitargs', dg', nsig', subst, gm') <- --trace ("zipped':" ++ (show $ map (\x -> case x of + -- SingleParamInfo _ xs -> dgn_theory $ labDG dgP $ getNode xs + -- _ -> error "nyi") $ map fst zipped')) $ + foldM (\(args0, dg0, nsig0, subst0, gm0) ((par0, arg0), idx ) -> do + (arg1, dg1, nsig1, subst1, gm1) <- -- trace ("\nFOLD\nsubst0:" ++ show subst0 ++ "\ngm0:" ++ show gm0) $ + anaPatternInstArg lg libEnv opts eo ln dg0 isig csig nsig0 name spname idx + subst0 gm0 par0 arg0 + let nsig2 = case nsig1 of -- this is a trick to make lists work! + EmptyNode _ -> nsig0 + _ -> nsig1 + return (args0 ++ [arg1], dg1, nsig2, subst1, gm1)) + ([], dgP, crtNode, Map.empty, startMor) $ zip zipped' [1..] + let lastParamSig = case nsig' of + EmptyNode _ -> error "should not happen" + JustNode x -> x + case missingNodes of + [] -> return (afitargs', psig, dg', lastParamSig, gm', subst) + _ -> do + (vMap', body') <- removeMissingOptionalSymbolsBody lg libEnv ln missingNodes vMap body + return (afitargs', PatternSig local imps (map fst zipped') vMap' body', dg', lastParamSig, gm', subst) + +removeMissingSymbolsParam :: LogicGraph -> LibEnv -> LibName -> DGraph -> MaybeNode -> + [NodeSig] -> NodeName -> Int -> PatternParamInfo -> + Result (DGraph, MaybeNode, PatternParamInfo) +removeMissingSymbolsParam lg libEnv ln dg lastParam ns name idx p = do + -- shortcut: if ns is empty, return (dg, JustNode psig, p) + case p of + SingleParamInfo optFlag psig -> + if null ns then return (dg, JustNode psig, p) + else do + let gth = dgn_theory $ labDG dg $ getNode psig + case gth of + G_theory lid syn (ExtSign sig nIsyms) sid sens tid -> do + let delSyms = concatMap (\n -> let gs = getSig n in + case gs of + G_sign slid (ExtSign _ syms) _ -> + map (\x -> coerceSymbol slid lid x) $ Set.toList syms + ) ns + mor <- cogenerated_sign lid (Set.fromList delSyms) sig + let sens' = OMap.fromList $ + filter (\(_, y) -> Set.null $ Set.intersection + (Set.fromList delSyms) $ + Set.fromList $ symsOfSen lid sig $ sentence y) + $ OMap.toList sens + gth' = G_theory lid syn (ExtSign (dom mor) nIsyms) sid sens' tid + newNode = newInfoNodeLab (incBy idx $ extName "Formal" name) + (newNodeInfo DGFormalParams) gth' + newNodeNr = getNewNodeDG dg + dg' = changesDGH dg [InsertNode (newNodeNr, newNode)] + newParNode = NodeSig newNodeNr $ signOf gth' + dg'' <- case lastParam of + EmptyNode _ -> return dg' + JustNode prevSig -> do + incl <- ginclusion lg (getSig prevSig) $ signOf gth' + return $ insLink dg' incl + globalDef DGLinkImports (getNode prevSig) newNodeNr + -- trace ("newParNode:" ++ show newParNode) $ + return (dg'', JustNode newParNode, SingleParamInfo optFlag newParNode) + _ -> return (dg, lastParam, p) -- don't remove from lists yet + +removeMissingOptionalSymbolsBody :: LogicGraph -> LibEnv -> LibName -> [NodeSig] -> PatternVarMap -> LocalOrSpecSig + -> Result (PatternVarMap, LocalOrSpecSig) +removeMissingOptionalSymbolsBody lg libEnv ln missingNodes vMap bodySig = do + Logic lid <- lookupCurrentLogic "removeMissingOptionalSymbols" lg + let delSyms = concatMap (\n -> let gs = getSig n in + case gs of + G_sign slid (ExtSign _ syms) _ -> map (\x -> coerceSymbol slid lid x) $ Set.toList syms ) missingNodes + + delSymsName = map (\x -> idToIRI $ sym_name lid x) delSyms + removeSymbolsFromSpec sp = + case sp of + Basic_spec (G_basic_spec blid bsp) rg -> do + let delSyms' = map (coerceSymbol lid blid) delSyms + bsp' <- delete_symbols_macro blid (Set.fromList delSyms') bsp + -- trace ("\n\n\nspec after deleting symbols: " ++ show bsp') $ + return $ Basic_spec (G_basic_spec blid bsp') rg + Spec_inst _ fArgs _ _ -> trace ("delSyms:" ++ show delSyms ++ "\nsp:" ++ show sp) $ do + let missingArgs = filter (\fa -> case item fa of + Fit_spec fs _ _ -> + case item fs of + NormalVariable x -> x `elem` delSymsName + _ -> False -- TODO: should we cover other cases too? + _ -> False) fArgs + case missingArgs of + [] -> return sp + _ -> do + let esig = empty_signature lid + bsp = case convertTheory lid of + Nothing -> error "can't convert empty theory to basic spec" + Just f -> f (esig, []) + return $ Basic_spec (G_basic_spec lid bsp) nullRange + Extension asps rg -> do + asps' <- mapM (\asp -> do + sp' <- removeSymbolsFromSpec $ item asp + return $ asp{item = sp'}) asps + return $ Extension asps' rg + Union asps rg -> do + asps' <- mapM (\asp -> do + sp' <- removeSymbolsFromSpec $ item asp + return $ asp{item = sp'}) asps + return $ Union asps' rg + _ -> error $ "only some specs for now:" ++ show sp + vMap' = foldl (\f s -> Map.delete ( idToIRI $ sym_name lid s) f) vMap delSyms + bodySig' <- case getBody bodySig of + Spec_pattern asp -> do + sp' <- removeSymbolsFromSpec $ item asp + return $ SpecSig $ Spec_pattern $ asp{item = sp'} + Local_pattern locals asp -> trace ("body:" ++ show bodySig) $ error "2" + -- trace ("body:" ++ show bodySig ++" body':"++ show bodySig') $ + return (vMap', bodySig') + +anaPatternInstArg :: LogicGraph -> LibEnv -> HetcatsOpts -> ExpOverrides -> LibName -> DGraph + -> MaybeNode -> MaybeNode -> MaybeNode + -> NodeName -> IRI -> Int -> GSubst -> Maybe G_morphism -> PatternParamInfo -> Annoted FIT_ARG + -> Result (Annoted FIT_ARG, DGraph, MaybeNode, GSubst, Maybe G_morphism) +anaPatternInstArg lg libEnv opts eo ln dg0 isig csig prevSig name spname idx subst0 mgm0 par0 arg0 = --trace ("***** arg0 in argInst:" ++ show arg0 ++ " subst0:" ++ show subst0 ++ " par0 in argInst:" ++ show par0) $ + case item arg0 of + Fit_string s r -> + case par0 of + StringParamInfo i -> do + l <- lookupCurrentLogic "fit string" lg + return (arg0, dg0, EmptyNode l, Map.insert (i, "String") (PlainVal s) subst0, mgm0) + _ -> error $ "parameter mismatch, got a string when expecting a " ++ show par0 + Fit_spec asp gm r -> + case item asp of + NormalVariable i -> error "vars should be solved by now!" + UnsolvedName i rg -> -- trace ("solving an unsolved name in inst arg:" ++ "tks:" ++ show (getTokens $ iriPath i) ++ " cmps:" ++ show (getComps $ iriPath i)) $ + -- TODO: here we must also pass the parameter, so we can check its symbols + -- 1. if i is the name of a spec entry in globalEnv + -- solve to Spec_inst i [] Nothing nullRange + -- and the substitution should be inducedFromTo + if i `elem` Map.keys (globalEnv dg0) then + case (par0, Map.findWithDefault (error "anaPatternInstArg: already checked") i (globalEnv dg0)) of + (SingleParamInfo b pSig, SpecEntry eGSig) -> do + let arg1 = Fit_spec (emptyAnno $ Spec_inst i [] Nothing nullRange) [] nullRange + l <- lookupCurrentLogic "fit string" lg + -- empty node was isig in next line + (arg2, dg1, (gmor, nsigA)) <- anaFitArg lg libEnv ln dg0 spname isig pSig opts (incBy idx $ extName "Arg" name) + eo csig prevSig mgm0 subst0 arg1 + case gmor of + G_morphism lid mor _ -> do -- trace ("arg2:"++ show arg2 ++ " gmor:" ++ show gmor ++ " nsigA:"++ show nsigA) $ do + let smap = symmap_of lid mor + isyms = case isig of + EmptyNode _ -> Set.empty + JustNode inode -> case getSig inode of + G_sign ilid (ExtSign sigI _) _ -> Set.map (coerceSymbol ilid lid) $ symset_of ilid sigI + subst1 = foldl (\f (ssym, tsym) -> + let (sn, sk) = (idToIRI $ sym_name lid ssym, symKind lid ssym) + tn = idToIRI $ sym_name lid tsym + in Map.insert (sn, sk) (PlainVal tn) f) subst0 $ filter (\(x,_) -> not $ Set.member x isyms) $ Map.toList smap + -- TODO: any compatibility checks must be done here + return (arg0{item=arg2}, dg1, JustNode nsigA, subst1, Just gmor) + _ -> error $ "argument mismatch in instantiation. parameter: " ++ show par0 ++ "\n argument: " ++ show arg0 + else do + case par0 of + SingleParamInfo b pNSig -> + case getSig pNSig of + G_sign lid (ExtSign _ newDecls) _ -> + case Set.toList newDecls of + [sym] -> do + let noCtxOrNoMatch = do + let arg1 = Fit_new (G_symbol lid sym) (G_symbol lid (rename_symbol lid sym (iriPath $ instParamName subst0 i))) nullRange + (arg2, dg1, (gmor, nsigA)) <- -- trace ("================ calling anaFitArg. pNSig:" ++ show pNSig ++ " arg1:" ++ show arg1 ++ " mgm0:" ++ show mgm0) $ + anaFitArg lg libEnv ln dg0 spname isig pNSig opts (incBy idx $ extName "Arg" name) + eo csig prevSig mgm0 subst0 arg1 + -- try: only extend previous morphism if the pattern is local! + case gmor of + G_morphism glid mor _ -> do -- trace ("gmor:" ++ show gmor) $ do + let smap = symmap_of glid mor + isyms = case isig of + EmptyNode _ -> Set.empty + JustNode inode -> case getSig inode of + G_sign ilid (ExtSign sigI _) _ -> Set.map (coerceSymbol ilid glid) $ symset_of ilid sigI + subst1 = foldl (\f (ssym, tsym) -> + let (sn, sk) = (idToIRI $ sym_name glid ssym, symKind glid ssym) + tn = idToIRI $ sym_name glid tsym + in Map.insert (sn, sk) (PlainVal tn) f) + subst0 $ filter (\(x,_) -> not $ Set.member x isyms) $ Map.toList smap + -- TODO: any compatibility checks must be done here + return (arg0{item=arg2}, dg1, JustNode nsigA, subst1, Just gmor) + case csig of + EmptyNode _ -> noCtxOrNoMatch + JustNode c -> + case getSig c of + G_sign lid1 (ExtSign ctx _) _ -> do + let ctxSyms = filter (\csym -> ((idToIRI $ sym_name lid1 csym) == i) && (symKind lid1 csym == symKind lid sym)) $ Set.toList $ symset_of lid1 ctx + case ctxSyms of + [] -> -- trace ("err2:"++ show i) $ + noCtxOrNoMatch + [ctxSym] -> do-- trace "symbol in ctx" $ do + let arg1 = Fit_ctx (G_symbol lid sym) (G_symbol lid1 ctxSym) nullRange + (arg2, dg1, (gmor, nsigA)) <- anaFitArg lg libEnv ln dg0 spname isig pNSig + opts (extName "Arg" name) eo csig + prevSig mgm0 subst0 arg1 + case gmor of + G_morphism glid mor _ -> do + let smap = symmap_of glid mor + isyms = case isig of + EmptyNode _ -> Set.empty + JustNode inode -> case getSig inode of + G_sign ilid (ExtSign sigI _) _ -> + Set.map (coerceSymbol ilid glid) $ symset_of ilid sigI + subst1 = foldl (\f (ssym, tsym) -> + let (sn, sk) = (idToIRI $ sym_name glid ssym, symKind glid ssym) + tn = idToIRI $ sym_name glid tsym + in Map.insert (sn, sk) (PlainVal tn) f) + subst0 $ filter (\(x,_) -> not $ Set.member x isyms) $ Map.toList smap + -- TODO: any compatibility checks must be done here + -- trace ("++++++ computed subst1:"++ show subst1) $ + return (arg0{item=arg2}, dg1, JustNode nsigA, subst1, Just gmor) + _ -> fail $ "multiple occurences of abbreviated name in the context:" ++ show ctxSyms + _ -> fail $ "ambiguity in use of abbreviation notation, parameter has more than one symbol:" ++ show par0 + _ -> fail $ "abbreviation notation can be used only for single ontology arguments, not for lists: " ++ show i ++ " par0:" ++ show par0 + -- 2. if i is a symbol from the context (nsig) + -- solve to context fit x |-> i + -- and the substitution maps x to i + -- where x is the unique symbol declared in the param + -- 3. otherwise, i is a new symbol of same kind as x + -- and the substitution maps x to i + OntoList aspecs -> trace ("asp:" ++ show asp) $ do + -- 1. generate a temporary param for the template node of the param list + -- SingleParamInfo False n where the signature of the head of the param list is JustNode n + let (par1, tailName) = case par0 of + SingleParamInfo _ _ -> error $ "\nexpecting single argument: " ++ show par0 ++ "\nbut got a list: " ++ show aspecs + ListParamInfo _ _ (JustNode n) tn -> let x = case tn of + Nothing -> nullIRI + Just y -> y + in (SingleParamInfo False n, x) -- TODO: not safe for empty, do it right!!!! + _ -> error $ "instantiating empty list pattern:" ++ show par0 ++ " with non-empty argument:" ++ show aspecs + -- 2. analyze each elem of aspecs as a single argument for this param + -- use anaPatternInstArg lg libEnv opts eo ln dg0 isig csig prevSig name spname subst0 mgm0 par0 arg0 + -- it returns the analysed arg, the dgraph, justnode node of argument, substitution, generated morphism + -- but update prevSig name spname subst0 mgm0 par0 arg0; fold the dgs; store the nodes of args + let emptyOntoName = mkIRI "empty" + (aspecs', aNodes, subst1, dg1) <- + foldM (\(anaSpecs, specNodes, substI, aDg) (crtSp, idx) -> trace ("crtSp:" ++ show crtSp) $ + case item crtSp of + UnsolvedName x _ | x == emptyOntoName -> return (anaSpecs, specNodes, substI, aDg) + _ -> do + (crtSp', aDg', argNode, aSubst, aMor) <- + anaPatternInstArg lg libEnv opts eo ln + aDg isig csig prevSig -- TODO: check that prevSig is fine here + name spname idx -- TODO: give proper names + subst0 + mgm0 -- TODO: check that this is ok + par1 $ + emptyAnno $ Fit_spec crtSp [] nullRange + -- trace ("\naMor:" ++ show aMor) $ + return (anaSpecs ++ [crtSp'], + specNodes ++ [argNode], + if substI == Map.empty then aSubst else substI, -- only interested in the first substitution. TODO: add it to mgm0? + aDg') + ) ([], [], Map.empty, dg0) $ zip aspecs [1..] + -- 3. unite the resulting nodes + (dg2, argUnion) <- unionNodes lg dg1 (makeName $ mkIRI "UnionNode") $ concatMap (\aN -> case aN of + JustNode x -> [x] + _ -> []) aNodes + -- 4. generate a substitution: subst of the first argument plus list variable to tail of analyzed args + let subst2 = case aspecs' of + _:asps -> + let (k, iriList) = foldl (\(_k0, iris0) as0 -> case item as0 of + Fit_new gsym1 gsym2 _ -> + case gsym1 of + G_symbol lid1 sym1 -> + case gsym2 of + G_symbol lid2 sym2 -> + let -- name1 = idToIRI $ sym_name lid1 sym1 + kind1 = symKind lid1 sym1 + name2 = idToIRI $ sym_name lid2 sym2 + in (kind1, iris0 ++ [name2]) + Fit_ctx gsym1 gsym2 _ -> + case gsym1 of + G_symbol lid1 sym1 -> + case gsym2 of + G_symbol lid2 sym2 -> + let -- name1 = idToIRI $ sym_name lid1 sym1 + kind1 = symKind lid1 sym1 + name2 = idToIRI $ sym_name lid2 sym2 + in (kind1, iris0 ++ [name2]) + _ -> error "only fit new/ctx for now!" + ) + + ("", []) asps + in Map.insert (tailName, "list") (ListVal k iriList) subst1 + + _ -> subst1 + l <- lookupCurrentLogic "fit string" lg + mgm1 <- extendWithSubst l mgm0 $ concatMap (\((x,k), y) -> case y of + PlainVal z -> [((x,k), (z,k))] + _ -> []) $ Map.toList subst2 + trace ("subst1:" ++ show subst1 ++ "subst2:" ++ show subst2 ++ "\nmgm0:" ++ show mgm1 ++ "\narg0:" ++ show arg0 ++ "\naspecs':" ++ show aspecs') $ + return (arg0, dg2, JustNode argUnion, subst2, mgm0) + -- 5. instantiate the body with the substitution and add a link from the united arguments to the body + -- this should happen elsewhere! + Spec_inst spn afitargs miri rg -> do + -- 0. instantiate arguments using the subst + let afitargs' = map (\a -> case item a of + Fit_spec annosp gmaps aRg -> + case item annosp of + UnsolvedName n _ -> a {item = Fit_spec (emptyAnno $ UnsolvedName (instParamName subst0 n) nullRange) gmaps aRg} + NormalVariable x -> + let xKeys = filter (\(k, _) -> k == x) $ Map.keys subst0 + in case xKeys of + [] -> error $ "variable not found:" ++ show x + (y,k):_ -> let val = Map.findWithDefault (error "not possible") (y,k) subst0 + in case val of + PlainVal v -> a{item = Fit_spec (emptyAnno $ UnsolvedName v nullRange) gmaps aRg} + _ -> error "only plainval for now" + _ -> a + _ -> a) afitargs + -- 1. analyze the spec + (newSp, newNode, dg1) <- anaSpecAux None False False lg -- TODO: check if False False is right + libEnv ln dg0 isig name opts eo (Spec_inst spn afitargs' miri rg) nullRange --TODO: check if isig is right + -- 2. generate morphism from sig of par0 to the sig of the instantiated spec + (Logic crtLid) <- lookupCurrentLogic "spec_inst" lg + (parsig, pnode) <- case par0 of + SingleParamInfo _ ns -> return (getSig ns, ns) + _ -> error "expected single param info" + let tarsig = getSig newNode + ssig <- case parsig of + G_sign plid psig _ -> coerceSign plid crtLid "coercesign 1" psig + tsig <- case tarsig of + G_sign tlid tsig _ -> coerceSign tlid crtLid "coercesign 2" tsig + mor <- induced_from_to_morphism crtLid Map.empty ssig tsig + -- 3. add the morphism to the dgraph as a theorem link + let dg2 = insLink dg1 (gEmbed $ mkG_morphism crtLid mor) globalThm DGImpliesLink (getNode pnode) $ getNode newNode + -- 4. the subst should be extended with the symbol map of the morphism + morAsMap = symmap_of crtLid mor + isyms = case isig of + EmptyNode _ -> Set.empty + JustNode inode -> case getSig inode of + G_sign ilid (ExtSign sigI _) _ -> + Set.map (coerceSymbol ilid crtLid) $ symset_of ilid sigI + subst1 = foldl (\f (ssym, tsym) -> + let (sn, sk) = (idToIRI $ sym_name crtLid ssym, symKind crtLid ssym) + tn = idToIRI $ sym_name crtLid tsym + in Map.insert (sn, sk) (PlainVal tn) f) + subst0 $ filter (\(x,_) -> not $ Set.member x isyms) $ Map.toList morAsMap + -- 5. return (the argument, the last dgraph, JustNode the node of the spec, the subst, ?the morphism?) + return (arg0, dg2, JustNode newNode, subst1, Just $ mkG_morphism crtLid mor) + -- error $ "subst0:" ++ show subst0 ++ " after:" ++ show subst1 + _ -> trace ("itm:" ++ (show $ item arg0) ++ "\npar0:" ++ show par0) $ + error "only unsolved names for now" + _ -> trace ("itm:" ++ (show $ item arg0)) $ + error "only fit_spec for now" + +instantiateMacro :: LogicGraph -> LibEnv ->HetcatsOpts -> ExpOverrides -> LibName -> + DGraph -> MaybeNode -> MaybeNode + -> NodeName -> IRI -> GSubst -> PatternVarMap -> Maybe G_morphism -> LocalOrSpecSig -> Result (DGraph, [NodeSig], Annoted SPEC) +instantiateMacro lg libEnv opts eo ln dg imp nsig name spname subst vars mgmPrev macro = + --trace ("~~~~~~~~~~~~~~~~instantiateMacro:" ++ show macro ++ "\nsubst:" ++ show subst ++ + -- "\nnsig:" ++ show nsig ++ "\nimp:"++ show imp ++ "\nmgmPrev:"++ show mgmPrev ++ "\nvars:" ++ show vars) $ + {- (Logic lid) <- lookupCurrentLogic "macro" lg + let th = (empty_signature lid, []) + bsp = case convertTheory lid of + Just f -> f th + _ -> error "cannot convert theory" + return (dg, emptyAnno $ Basic_spec (G_basic_spec lid bsp) nullRange) -} + case macro of + LocalSig localVarMaps (Local_pattern _ localBody) -> do + let gEnv' = foldl (\g (n, s) -> Map.insert n (PatternEntry s) g) (globalEnv dg) $ Map.toList localVarMaps + dg' = dg {globalEnv = gEnv'} + instantiateMacro lg libEnv opts eo ln dg' imp nsig name spname subst vars mgmPrev (SpecSig $ Spec_pattern localBody) -- TODO: will this be enough? + -- trace ("known:" ++ show (Map.keys gEnv')) $ error "local patterns nyi" + SpecSig (Spec_pattern asp) -> + instMacroAux lg libEnv opts eo ln dg imp nsig name spname subst vars mgmPrev asp + _ -> fail $ "illegal pattern signature:" ++ show macro + + +instMacroAux :: LogicGraph -> LibEnv ->HetcatsOpts -> ExpOverrides -> LibName -> + DGraph -> MaybeNode -> MaybeNode + -> NodeName -> IRI -> GSubst -> PatternVarMap -> Maybe G_morphism + -> Annoted SPEC -> Result (DGraph, [NodeSig], Annoted SPEC) +instMacroAux lg libEnv opts eo ln crtDG imp crtNSig name spname crtSubst vars crtGM asp0 = -- trace ("+++++ instMacroAux for " ++ show asp0) $ + case item asp0 of + Basic_spec gbsp rg -> + case gbsp of + G_basic_spec lid bsp -> do + bsp'<- instantiate_macro lid vars crtSubst bsp + let lastNode = case crtNSig of + JustNode x -> x + _ -> error "no last param of a pattern, should not happend" + --trace ("bsp':" ++ show bsp') $ + return (crtDG, [lastNode], asp0{item = Basic_spec (G_basic_spec lid bsp') rg}) + Group asp1 rg -> do + (dg2, ns2, asp2) <- instMacroAux lg libEnv opts eo ln crtDG imp crtNSig name spname crtSubst vars crtGM asp1 + return (dg2, ns2, asp0{item = Group asp2 rg}) + Extension asps rg -> do + (dg1, ns1, asps1) <- foldM (\(aDg, ns, as) a -> do + (dg', ns', a') <- instMacroAux lg libEnv opts eo ln aDg imp crtNSig name spname crtSubst vars crtGM a + return (dg', ns ++ ns', as ++ [a']) ) (crtDG, [], []) asps + return (dg1, ns1, asp0{item = Extension asps1 rg}) + Union asps rg -> do + (dg1, ns1, asps1)<- foldM (\(aDg, ns, as) a -> do + (dg',ns',a') <- instMacroAux lg libEnv opts eo ln aDg imp crtNSig name spname crtSubst vars crtGM a + return (dg', ns ++ ns', as ++ [a']) ) (crtDG, [], []) asps + -- trace ("ns1:" ++ show ns1) $ + return (dg1, ns1, asp0{item = Union asps1 rg}) + Spec_inst sn afitargs _ _ -> trace ("\n\nin instmacro spec_inst:" ++ show (item asp0) ++ " crtSubst:" ++ show crtSubst) $ + do -- here afitargs must be instantiated if they are variables!!! + let snEntry = Map.findWithDefault (error $ "unknown pattern:" ++ show sn) sn $ globalEnv crtDG + case snEntry of + PatternEntry patSig@(PatternSig isLocal _ pParams pMap pBody) -> do + l@(Logic crtLid) <- lookupCurrentLogic "anaPatternInstArgs" lg + idImps <- case imp of + EmptyNode _ -> return Nothing + JustNode (NodeSig _ gisig) -> + case gisig of + G_sign ilid (ExtSign esig _) _ -> do + esig' <- coercePlainSign ilid crtLid "coerceSign in anaPatternInstArgs" esig + let emor = ide esig' + return $ Just $ G_morphism crtLid emor startMorId + let solveVars aFitArg = --trace ("solving:" ++ show aFitArg) $ + case item aFitArg of + Fit_spec asp1 gm rg -> + case item asp1 of + OntoList asps -> + let + args0 = map (\a-> emptyAnno $ Fit_spec a [] nullRange) asps + res = map solveVars args0 + listToOntoList aList = + let + allNames = concatMap (\a -> case item a of + Fit_spec x _ _ -> + case item x of + UnsolvedName _ _ -> [item x] + OntoList xs -> map item xs) aList + in emptyAnno $ OntoList $ map emptyAnno allNames + in -- trace ("vars: " ++ show (concatMap fst res)) $ + (concatMap fst res, aFitArg{item= Fit_spec (listToOntoList $ map snd res) gm rg}) + UnsolvedName i _ -> + if i == mkIRI "empty" then error "empty list as argument in instantiation of pattern nyi" + else ([], aFitArg) + NormalVariable i -> -- trace ("normal variable: " ++ show i ++ " crtSubst:" ++ show crtSubst ++ " vars:" ++ show vars ++ " pMap:" ++ show pMap) $ + if i `elem` Map.keys vars then + let (b, k) = Map.findWithDefault (error "notPossible") i vars + val = Map.findWithDefault (error "variable not mapped") (i,k) crtSubst + valIRI = case val of + PlainVal valiri -> valiri + _ -> error "normal variable mapped to list" + in ([((i,k), (valIRI,k))], aFitArg{item = Fit_spec asp1{item= UnsolvedName valIRI nullRange} gm rg}) + else + case filter (\(x,_y) -> x == i) $ Map.keys crtSubst of + [(a, k)] -> + let + val = Map.findWithDefault (error "variable not mapped") (i,k) crtSubst + valIRI = case val of + PlainVal valiri -> valiri + _ -> error "normal variable mapped to list" + in ([((i,k), (valIRI,k))], aFitArg{item = Fit_spec asp1{item= UnsolvedName valIRI nullRange} gm rg}) + _ -> error $ "unknown variable:" ++ show i ++ " in " ++ show vars + ListVariable i -> + if i `elem` Map.keys vars then + let (b, k) = Map.findWithDefault (error "not possible") i vars + in if k == "list" then + let val = Map.findWithDefault (error "variable not mapped") (i, k) crtSubst + in case val of + ListVal k' vals -> + let genItem = Fit_spec asp1{item= OntoList $ map (\v -> emptyAnno $ UnsolvedName v nullRange) vals} gm rg + in if not $ null vals then ([], aFitArg{item = genItem}) -- error $ "genItem:" ++ show genItem. TODO: dont map i to values? + else ([], aFitArg{item = Fit_spec asp1{item = UnsolvedName (mkIRI "empty") nullRange} gm rg}) + -- TODO: this does not suffice, we need to generate empty ontology here already! + _ -> error $ "expected list argument but got single element" + else error $ "expected list but got " ++ k + else + case filter (\(x,_y) -> x == i) $ Map.keys crtSubst of + [(a, k)] -> + let + val = Map.findWithDefault (error "variable not mapped") (i,k) crtSubst + in case val of + PlainVal valiri -> error "list mapped to normal value" + ListVal valKind valVals -> case valVals of + [] -> ([], aFitArg{item = Fit_spec asp1{item = UnsolvedName (mkIRI "empty") nullRange} gm rg}) + _ -> ([], aFitArg{item = Fit_spec asp1{item = OntoList $ map (\x -> emptyAnno $ UnsolvedName x nullRange) valVals} gm rg}) + _ -> error $ "unknown list variable: " ++ show i ++ " vars: " ++ show vars + _ -> ([], aFitArg) + _ -> ([], aFitArg) + solved = map solveVars afitargs + afitargs0 = map snd solved + aitems = filter (\x -> case item x of + Fit_spec y _ _ -> case item y of + UnsolvedName anIRI _ -> trace ("anIRI:" ++ show anIRI ) $ anIRI == mkIRI "empty" + _ -> False + _ -> False) afitargs0 + newVars = concatMap fst solved + zipped = --trace ("~~~~~~~~~~~~~newVars:"++ show newVars) $ + zip pParams afitargs0 -- TODO: allow optionals in locals!!!! + -- TODO: if isLocal start with subst1 else start with empty subst? + (Logic lid) <- lookupCurrentLogic "macro" lg + let th = (empty_signature lid, []) + bsp = case convertTheory lid of + Just f -> f th + _ -> error "cannot convert theory" + if not $ null aitems then + instMacroAux lg libEnv opts eo ln crtDG imp crtNSig name spname crtSubst vars crtGM $ asp0{item = Basic_spec (G_basic_spec lid bsp) nullRange} -- error "empty list as argument, not yet done" + else do + gmor' <- -- trace ("~~~~~~~~~~~~~zipped:"++ show zipped) $ + if isLocal then + case crtGM of + Nothing -> extendWithSubst l idImps newVars + Just agm -> return $ Just agm + else return idImps -- TODO: old variant: extendWithSubst l idImps newVars + -- TODO: by using anaPatternInstArg instead of anaPatternInstArgs we lose missing arguments! + -- can we replace it? + -- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + {-(afitargs', dg', nsig', subst', gm') <- -- trace ("~~~~~~~~~~~~~crtSubst:"++ show crtSubst ++ " gmor':" ++ show gmor') $ + foldM (\(args0, dg0, nsig0, subst0, gm0) ((par0, arg0), idx) -> do + (arg1, dg1, nsig1, subst1, gm1) <- -- trace ("subst0 in spec_inst:" ++ show subst0 ++ " nsig0:" ++ show nsig0) $ + anaPatternInstArg lg libEnv opts eo ln dg0 + imp (EmptyNode l) nsig0 -- TODO: context is always empty now + name spname idx subst0 gm0 par0 arg0 + --trace ("$$$after analysis nsig':" ++ show nsig1 ++ " gm1:" ++ show gm1) $ + return (args0 ++ [arg1], dg1, nsig1, subst1, gm1)) + ([], crtDG, crtNSig, crtSubst, gmor') -- the last argument node should not be EmptyNode, but the target of gmor'. Try with nsig? + $ zip zipped [1..]-} + (afitargs', patSig'@(PatternSig _local _imp' _params' vMap' bodySig), dg', nsig', gm', subst') <- + anaPatternInstArgs lg libEnv opts eo ln crtDG imp (EmptyNode l) name spname patSig gmor' crtNSig afitargs0 + -- (afitargs', patSig'@(PatternSig _local _imp' _params' vMap' bodySig), dg', nsig', subst') <- anaPatternInstArgs lg libEnv opts eo ln dg imp nsig name spname patSig afitargs + --trace ("\n\n\n recursive call:" ++ show subst' ++ " nsig':" ++ show nsig') $ + -- TODO: revert below if above + -- instantiateMacro lg libEnv opts eo ln dg' imp nsig' name spname (Map.union subst' crtSubst) vars gm' pBody + instantiateMacro lg libEnv opts eo ln dg' imp (JustNode nsig') name spname + (Map.union subst' crtSubst) (Map.union vMap' vars) -- TODO: is this fine or add vars? + gm' bodySig + -- instantiateMacro lg libEnv opts eo ln dg' imp nsig' name spname (Map.union subst' subst) vars gm' pBody + -- error $ "spec_inst:" ++ show sn ++ " args:" ++ show afitargs ++ " vars:" ++ show vars ++ " subst:" ++ show subst + -- 1. afitargs should give raise to signature morphisms from the nodes of the params to the nodes of the args + -- 2. and to a subst' + -- 3. the body of sn should be instantiated in the new dgraph, with the union of subst and subst', with the varmap taken from the signature of sn in the globalEnv + _ -> fail $ "expected a pattern entry but found:" ++ show snEntry + _ -> fail $ "only non-structured bodies for now:" ++ show (globalEnv crtDG) + -- instMacroAux dg nsig subst mgmPrev asp + -- _ -> fail $ "illegal pattern signature:" ++ show macro + +extendWithSubst :: AnyLogic -> Maybe G_morphism -> [((IRI, String),(IRI, String))] -> Result (Maybe G_morphism) +extendWithSubst (Logic l) mgm newVars = do + case mgm of + Nothing -> return Nothing -- TODO: wrong, should still generate a morphism! + Just gm -> + case gm of + G_morphism crtLid emor _ -> do + let + ssyms = map (\(x,y) -> new_symbol crtLid x y) $ map fst newVars + tsyms = map (\(x,y) -> new_symbol crtLid x y) $ map snd newVars + crtMap = Map.fromList $ map (\(x, y) -> (symbol_to_raw crtLid x, symbol_to_raw crtLid y)) $ zip ssyms tsyms + ssig <- foldM (add_symb_to_sign crtLid) (empty_signature crtLid) ssyms + tsig <- foldM (add_symb_to_sign crtLid) (empty_signature crtLid) tsyms + mor <- induced_from_to_morphism crtLid crtMap (ExtSign ssig Set.empty) (ExtSign tsig Set.empty) + rmor <- morphism_union crtLid emor mor + -- trace ("ssig:" ++ show ssig ++ "tsig:" ++ show tsig ++ "rmor:" ++ show rmor) $ + return $ Just $ G_morphism crtLid rmor startMorId + 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/Static/DevGraph.hs b/Static/DevGraph.hs index 4e23d93221..a21e6a9bb1 100644 --- a/Static/DevGraph.hs +++ b/Static/DevGraph.hs @@ -685,6 +685,7 @@ data GlobalEntry = | AlignEntry AlignSig | UnitEntry UnitSig | NetworkEntry GDiagram + | PatternEntry PatternSig deriving (Show, Typeable) getGlobEntryNodes :: GlobalEntry -> Set.Set Node @@ -706,6 +707,27 @@ data AlignSig = AlignMor NodeSig GMorphism NodeSig NodeSig -- b deriving (Show, Eq, Typeable) +-- true for local patterns, imports, list of nodes for those parameters that are ontologies, kinded vars, body +data PatternSig = PatternSig Bool MaybeNode [PatternParamInfo] PatternVarMap LocalOrSpecSig + deriving (Show, Typeable) + +data LocalOrSpecSig = SpecSig LocalOrSpec + | LocalSig (Map.Map IRI PatternSig) LocalOrSpec + -- store the varmaps of local subpatterns so they dont get recomputed every time + deriving (Show, Typeable) + +getBody :: LocalOrSpecSig -> LocalOrSpec +getBody (SpecSig x) = x +getBody (LocalSig _ x) = x + +data PatternParamInfo = SingleParamInfo Bool NodeSig -- optional or not, node in graph + | ListParamInfo Int Bool MaybeNode (Maybe IRI) + -- length (currrently saves the number of elements before last), + -- exact or minimal, node of list template, name of tail if not empty list + | StringParamInfo IRI + deriving (Show, Eq, Typeable) +-- TODO: extend for data parameters + type GlobalEnv = Map.Map IRI GlobalEntry getGlobNodes :: GlobalEnv -> Set.Set Node diff --git a/Syntax/AS_Library.der.hs b/Syntax/AS_Library.der.hs index 5a8d050886..2dddcdb0ba 100644 --- a/Syntax/AS_Library.der.hs +++ b/Syntax/AS_Library.der.hs @@ -36,6 +36,8 @@ import Syntax.AS_Structured import Framework.AS import Framework.ATC_Framework () +-- import Debug.Trace + data LIB_DEFN = Lib_defn LibName [Annoted LIB_ITEM] Range [Annotation] {- pos: "library" list of annotations is parsed preceding the first LIB_ITEM @@ -82,8 +84,13 @@ data LIB_ITEM = Spec_defn SPEC_NAME GENERICITY (Annoted SPEC) Range -- pos: "newlogic", Logic_name, "=", opt "end" | Newcomorphism_defn ComorphismDef Range -- pos: "newcomorphism", Comorphism_name, "=", opt "end" + | Pattern_defn SPEC_NAME [PatternParam] IMPORTED LocalOrSpec Range deriving (Show, Typeable) +data LocalOrSpec = Local_pattern [LIB_ITEM] (Annoted SPEC) | + Spec_pattern (Annoted SPEC) + deriving (Show, Typeable) + data AlignSem = SingleDomain | GlobalDomain | ContextualizedDomain deriving (Show, Typeable, Bounded, Enum) @@ -110,6 +117,12 @@ addDownloadAux unique j = (if unique then UniqueItem i else ItemMaps [ItemNameMap i Nothing]) $ iriPos i +data PatternParam = StringParam IRI | OntoParam Bool (Annoted SPEC) | ListParam OntoList + deriving (Show, Typeable) + -- the bool flag is true for optional parameters + +data OntoList = EmptyParamList | OntoListCons [Annoted SPEC] deriving (Show, Typeable) + data GENERICITY = Genericity PARAMS IMPORTED Range deriving (Show, Typeable) -- pos: many of "[","]" opt ("given", commas) @@ -175,6 +188,12 @@ getDeclSpecNames :: LIB_ITEM -> [IRI] getDeclSpecNames li = case li of Spec_defn sn _ _ _ -> [sn] Download_items _ di _ -> getImportNames di + Pattern_defn sn _ _ (Spec_pattern _) _ -> [sn] + Pattern_defn sn _ _ (Local_pattern lis _) _ -> + [sn] ++ concatMap getDeclSpecNames lis + -- here we add as declared the local subpatterns + -- should this have local visibility? + -- things get complicated _ -> [] getImportNames :: DownloadItems -> [IRI] @@ -188,7 +207,8 @@ getOms o = case o of MkNetwork _ -> [] getSpecDef :: LIB_ITEM -> [SPEC] -getSpecDef li = case li of +getSpecDef li = -- trace ("li:" ++ show li) $ + case li of Spec_defn _ _ as _ -> [item as] View_defn _ _ (View_type s1 s2 _) _ _ -> [item s1, item s2] Entail_defn _ (Entail_type s1 s2 _) _ -> getOms s1 ++ getOms s2 @@ -196,4 +216,6 @@ getSpecDef li = case li of getOms s1 ++ getOms s2 ++ getOms as Align_defn _ _ (View_type s1 s2 _) _ _ _ -> [item s1, item s2] Module_defn _ (Module_type s1 s2 _) _ _ -> [item s1, item s2] + Pattern_defn _ _ _ (Spec_pattern s) _ -> [item s] + Pattern_defn _ _ _ (Local_pattern lis s) _ -> concatMap getSpecDef lis ++ [item s] _ -> [] diff --git a/Syntax/AS_Structured.der.hs b/Syntax/AS_Structured.der.hs index f8b2cc376f..d4cd573982 100644 --- a/Syntax/AS_Structured.der.hs +++ b/Syntax/AS_Structured.der.hs @@ -31,10 +31,13 @@ import Logic.Grothendieck ( G_basic_spec , G_symb_items_list , G_symb_map_items_list + , G_symbol , LogicGraph , setCurLogic , setSyntax ) +-- import Debug.Trace + -- for spec-defn and view-defn see AS_Library data SPEC = Basic_spec G_basic_spec Range @@ -75,6 +78,12 @@ 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 + | UnsolvedName IRI Range + | NormalVariable IRI + | ListVariable IRI + | ListValue [IRI] + | OntoList [Annoted SPEC] + | EmptyList deriving (Show, Typeable) data Network = Network [LABELED_ONTO_OR_INTPR_REF] [IRI] Range @@ -120,6 +129,11 @@ data FIT_ARG = Fit_spec (Annoted SPEC) [G_mapping] Range -- pos: opt "fit" | Fit_view IRI [Annoted FIT_ARG] Range -- annotations before the view keyword are stored in Spec_inst + | Fit_string IRI Range + | Fit_ctx G_symbol G_symbol Range + | Fit_new G_symbol G_symbol Range + | Fit_list [Annoted SPEC] Range + | Missing_arg Range deriving (Show, Typeable) type SPEC_NAME = IRI @@ -237,3 +251,5 @@ getSpecs :: FIT_ARG -> [Annoted SPEC] getSpecs fa = case fa of Fit_spec as _ _ -> [as] Fit_view _ fas _ -> concatMap (getSpecs . item) fas + _ -> [] -- trace (show fa) [] + diff --git a/Syntax/Parse_AS_Architecture.hs b/Syntax/Parse_AS_Architecture.hs index 0308e0018a..668902c613 100644 --- a/Syntax/Parse_AS_Architecture.hs +++ b/Syntax/Parse_AS_Architecture.hs @@ -119,7 +119,7 @@ unitSpec l = NOTE: this can also be a spec name. If this is the case, this unit spec will be converted on the static analysis stage. See Static.AnalysisArchitecture.ana_UNIT_SPEC. -} - do gps@(gs : gss, _) <- annoParser (caslGroupSpec l) `separatedBy` crossT + do gps@(gs : gss, _) <- annoParser (caslGroupSpec l True) `separatedBy` crossT let rest = unitRestType l gps if null gss then option ( {- case item gs of @@ -130,7 +130,7 @@ unitSpec l = unitRestType :: LogicGraph -> ([Annoted SPEC], [Token]) -> AParser st UNIT_SPEC unitRestType l (gs, ps) = do a <- asKey funS -- see Note - g <- annoParser $ caslGroupSpec l + g <- annoParser $ caslGroupSpec l True -- TODO: if wrong here and line 122, set True to False return (Unit_type gs g $ catRange (ps ++ [a])) {- Note: the minus from funS (and crossT) would be misinterpreted as diff --git a/Syntax/Parse_AS_Library.hs b/Syntax/Parse_AS_Library.hs index 3a950aec3a..f665fce345 100644 --- a/Syntax/Parse_AS_Library.hs +++ b/Syntax/Parse_AS_Library.hs @@ -41,6 +41,8 @@ import Control.Monad import Framework.AS +import Debug.Trace + lGAnnos :: LogicGraph -> AParser st (LogicGraph, [Annotation]) lGAnnos lG = do as <- annos @@ -119,10 +121,11 @@ specDefn l = do n <- hetIRI l g <- generics l e <- equalT - a <- aSpec l + a <- aSpec l True -- OMS, not macros q <- optEnd + --trace ("spec:" ++ show (Spec_defn n g a nullRange)) $ return . Spec_defn n g a - . catRange $ [s, e] ++ maybeToList q + . catRange $ [s, e] ++ maybeToList q -- CASL view-defn or DOL IntprDefn viewDefn :: LogicGraph -> AParser st LIB_ITEM @@ -166,9 +169,9 @@ queryDefn l = do lg <- lookupCurrentLogic "query-defn" l (vs, cs) <- parseItemsList lg w <- asKey whereS - Basic_spec bs _ <- lookupCurrentSyntax "query-defn" l >>= basicSpec l + Basic_spec bs _ <- lookupCurrentSyntax "query-defn" l >>= basicSpec l True i <- asKey inS - oms <- aSpec l + oms <- aSpec l True mt <- optionMaybe $ asKey "along" >> hetIRI l o <- optEnd return . Query_defn n vs bs oms mt . catRange @@ -214,7 +217,7 @@ libItem l = specDefn l s2 <- colonT et <- equivType l s3 <- equalT - sp <- fmap MkOms $ aSpec l + sp <- fmap MkOms $ aSpec l True ep <- optEnd return . Equiv_defn en et sp . catRange $ s1 : s2 : s3 : maybeToList ep @@ -305,11 +308,39 @@ libItem l = specDefn l (catRange ([s1, s2, s3, s4, s5, s6, s7, s8] ++ maybeToList q))) <|> -- just a spec (turned into "spec spec = sp") do p1 <- getPos - a <- aSpec l + a <- aSpec l True p2 <- getPos if p1 == p2 then fail "cannot parse spec" else return (Spec_defn nullIRI (Genericity (Params []) (Imported []) nullRange) a nullRange) + <|> -- pattern defn + patternParser l + +patternParser :: LogicGraph -> AParser st LIB_ITEM +patternParser l = do + s1 <- asKey "pattern" + n <- hetIRI l + (pars, ps1) <- macroParams l + (imp, ps2) <- option ([], nullRange) (imports l) + s2 <- equalT + a <- --trace ("parsed equal:" ++ show pars) $ + localOrSpec l + q <- optEnd + let pattern = Pattern_defn n pars (Imported imp) a nullRange + trace ("pattern:" ++ show pattern) $ + return . Pattern_defn n pars (Imported imp) a + . catRange $ [s1, s2] ++ maybeToList q + +localOrSpec :: LogicGraph -> AParser st LocalOrSpec +localOrSpec l = do + _s1 <- asKey "let" + locals <- many1 (patternParser l) -- separatedBy (patternParser l) skip -- this might have problems + _s2 <- asKey "in" + a <- aSpec l False + return $ Local_pattern locals a + <|> do + a <- aSpec l False -- TODO: this makes sure that the bodies are parsed as macros and not as ontologies + return $ Spec_pattern a downloadItems :: LogicGraph -> AParser st (DownloadItems, [Token]) downloadItems l = do @@ -332,12 +363,12 @@ entailType l = do i <- asKey inS nw <- parseNetwork l r <- asKey entailsS - g <- groupSpec l + g <- groupSpec l True return . OMSInNetwork n nw g $ catRange [i, r] _ -> fail "OMSName expected" omsOrNetwork :: LogicGraph -> AParser st OmsOrNetwork -omsOrNetwork l = fmap (MkOms . emptyAnno) $ groupSpec l +omsOrNetwork l = fmap (MkOms . emptyAnno) $ groupSpec l True -- no macros in networks equivType :: LogicGraph -> AParser st EQUIV_TYPE equivType l = do @@ -361,16 +392,16 @@ alignArity = choice $ map (\ a -> asKey (showAlignArity a) >> return a) -- | Parse view type also used in alignments viewType :: LogicGraph -> AParser st VIEW_TYPE viewType l = do - sp1 <- annoParser (groupSpec l) + sp1 <- annoParser (groupSpec l True) s <- asKey toS - sp2 <- annoParser (groupSpec l) + sp2 <- annoParser (groupSpec l True) return $ View_type sp1 sp2 $ tokPos s moduleType :: LogicGraph -> AParser st MODULE_TYPE moduleType l = do - sp1 <- aSpec l + sp1 <- aSpec l True s <- asKey ofS - sp2 <- aSpec l + sp2 <- aSpec l True return $ Module_type sp1 sp2 (tokPos s) restrictionSignature :: LogicGraph -> AParser st G_symb_items_list @@ -415,14 +446,42 @@ params l = do param :: LogicGraph -> AParser st (Annoted SPEC, Range) param l = do b <- oBracketT - pa <- aSpec l + pa <- aSpec l True + -- macros not allowed in params of CASL generic specs c <- cBracketT return (pa, toRange b [] c) +macroParams :: LogicGraph -> AParser st ([PatternParam], Range) +macroParams l = do + _o <- oBracketT + (pars, _ps) <- separatedBy (macroParam l) semiT + _c <- cBracketT + return (pars, nullRange) --TODO: get the range right + + +macroParam :: LogicGraph -> AParser st PatternParam +macroParam l = do + (elems, _ps) <- separatedBy (elemParser l) doubleColonT + case elems of + [(x, isOpt)] -> return $ OntoParam isOpt x + _ -> return $ ListParam $ OntoListCons $ map fst elems + <|> do + _ <- asKey "xsd:string" + i <- hetIRI l + return $ StringParam i + +elemParser :: LogicGraph -> AParser st (Annoted SPEC, Bool) +elemParser lg = do + optParam <- option nullTok $ asKey "?" + a <- aSpec lg True + return (a, (optParam /= nullTok)) + -- TODO: always True, macros not allowed as parameters + -- TODO: for now, but we need to handle the empty list + imports :: LogicGraph -> AParser st ([Annoted SPEC], Range) imports l = do s <- asKey givenS - (sps, ps) <- separatedBy (annoParser $ groupSpec l) anComma + (sps, ps) <- separatedBy (annoParser $ groupSpec l True) anComma -- macro not allowed in imports, always True return (sps, catRange (s : ps)) newlogicP :: AParser st (IRI, Token) diff --git a/Syntax/Parse_AS_Structured.hs b/Syntax/Parse_AS_Structured.hs index b83441f8e4..d7e5bbbcd0 100644 --- a/Syntax/Parse_AS_Structured.hs +++ b/Syntax/Parse_AS_Structured.hs @@ -55,6 +55,8 @@ import Data.Char import Data.Maybe import Control.Monad +import Debug.Trace + expandCurieM :: LogicGraph -> IRI -> GenParser Char st IRI expandCurieM lG i = case expandCurie (prefixes lG) i of @@ -271,51 +273,51 @@ flatExts = concatMap $ \ as -> case item as of sps -> sps _ -> [as] -spec :: LogicGraph -> AParser st (Annoted SPEC) -spec l = do - sp1 <- annoParser2 (specThen l) +spec :: LogicGraph -> Bool -> AParser st (Annoted SPEC) +spec l flag = do + sp1 <- annoParser2 (specThen l flag) option sp1 $ do k <- asKey "bridge" rs <- many (renaming l) - sp2 <- annoParser2 (specThen l) + sp2 <- annoParser2 (specThen l flag) return . emptyAnno . Bridge sp1 rs sp2 $ tokPos k -specThen :: LogicGraph -> AParser st (Annoted SPEC) -specThen l = do - (sps, ps) <- annoParser2 (specA l) `separatedBy` asKey thenS +specThen :: LogicGraph -> Bool -> AParser st (Annoted SPEC) +specThen l flag = do + (sps, ps) <- annoParser2 (specA l flag) `separatedBy` asKey thenS return $ case sps of [sp] -> sp _ -> emptyAnno (Extension (flatExts sps) $ catRange ps) -specA :: LogicGraph -> AParser st (Annoted SPEC) -specA l = do - sp <- annoParser2 $ specB l +specA :: LogicGraph -> Bool -> AParser st (Annoted SPEC) +specA l flag = do + sp <- annoParser2 $ specB l flag option sp $ do t <- asKey andS <|> asKey intersectS - (sps, ts) <- annoParser2 (specB l) `separatedBy` asKey (tokStr t) + (sps, ts) <- annoParser2 (specB l flag) `separatedBy` asKey (tokStr t) let cons = case tokStr t of "and" -> Union _ -> Intersection return $ emptyAnno (cons (sp : sps) $ catRange (t : ts)) -specB :: LogicGraph -> AParser st (Annoted SPEC) -specB l = do +specB :: LogicGraph -> Bool -> AParser st (Annoted SPEC) +specB l flag = do p1 <- asKey localS - sp1 <- aSpec l + sp1 <- aSpec l flag p2 <- asKey withinS - sp2 <- annoParser2 $ specB l + sp2 <- annoParser2 $ specB l flag return (emptyAnno $ Local_spec sp1 sp2 $ tokPos p1 `appRange` tokPos p2) - <|> specC l + <|> specC l flag -specC :: LogicGraph -> AParser st (Annoted SPEC) -specC lG = do - let spD = annoParser $ specD lG +specC :: LogicGraph -> Bool -> AParser st (Annoted SPEC) +specC lG flag = do + let spD = annoParser $ specD lG flag rest = spD >>= translationList [ (`fmap` extraction lG) . Extraction , (`fmap` renaming lG) . Translation , (`fmap` restriction lG) . Reduction , (`fmap` approximation lG) . Approximation - , (`fmap` filtering lG) . Filtering + , (`fmap` filtering lG flag) . Filtering , (`fmap` minimization lG) . Minimization] l@(Logic lid) <- lookupCurrentLogic "specC" lG {- if the current logic has an associated data_logic, @@ -326,8 +328,8 @@ specC lG = do Nothing -> rest Just lD@(Logic dl) -> do p1 <- asKey dataS -- not a keyword - sp1 <- annoParser $ basicSpec lG (lD, Nothing) - <|> caslGroupSpec (setCurLogic (language_name dl) lG) + sp1 <- annoParser $ basicSpec lG flag (lD, Nothing) + <|> caslGroupSpec (setCurLogic (language_name dl) lG) flag sp2 <- spD return (emptyAnno $ Data lD l sp1 sp2 $ tokPos p1) <|> rest @@ -393,16 +395,16 @@ extraction lg = do (is,commas) <- separatedBy (hetIRI lg) commaT return . ExtractOrRemove (tokStr p == extractS) is $ catRange (p:commas) -filtering :: LogicGraph -> AParser st FILTERING -filtering lg = do +filtering :: LogicGraph -> Bool -> AParser st FILTERING +filtering lg flag = do p <- asKey selectS <|> asKey rejectS - filtering_aux p lg + filtering_aux p lg flag -filtering_aux :: Token -> LogicGraph -> AParser st FILTERING -filtering_aux p lg = +filtering_aux :: Token -> LogicGraph -> Bool -> AParser st FILTERING +filtering_aux p lg flag = do s <- lookupCurrentSyntax "filtering" lg - Basic_spec bs _ <- basicSpec lg s + Basic_spec bs _ <- basicSpec lg flag s return . FilterBasicSpec (tokStr p == selectS) bs $ tokPos p <|> do @@ -422,52 +424,53 @@ groupSpecLookhead lG = minimizeKey :: AParser st Token minimizeKey = choice $ map asKey [minimizeS, closedworldS, "maximize"] -specD :: LogicGraph -> AParser st SPEC +specD :: LogicGraph -> Bool -> AParser st SPEC -- do some lookahead for free spec, to avoid clash with free type -specD l = do +specD l flag = do p <- asKey freeS `followedWith` groupSpecLookhead l - sp <- annoParser $ groupSpec l + sp <- annoParser $ groupSpec l flag return (Free_spec sp $ tokPos p) <|> do p <- asKey cofreeS `followedWith` groupSpecLookhead l - sp <- annoParser $ groupSpec l + sp <- annoParser $ groupSpec l flag return (Cofree_spec sp $ tokPos p) <|> do p <- minimizeKey `followedWith` groupSpecLookhead l - sp <- annoParser $ groupSpec l + sp <- annoParser $ groupSpec l flag return (Minimize_spec sp $ tokPos p) <|> do p <- asKey closedS `followedWith` groupSpecLookhead l - sp <- annoParser $ groupSpec l + sp <- annoParser $ groupSpec l flag return (Closed_spec sp $ tokPos p) - <|> specE l + <|> specE l flag -specE :: LogicGraph -> AParser st SPEC -specE l = logicSpec l +specE :: LogicGraph -> Bool -> AParser st SPEC +specE l flag = logicSpec l flag <|> combineSpec l - <|> (lookAhead (groupSpecLookhead l) >> groupSpec l) - <|> (lookupCurrentSyntax "basic spec" l >>= basicSpec l) + <|> (lookAhead (groupSpecLookhead l) >> groupSpec l flag) + <|> (lookupCurrentSyntax "basic spec" l >>= basicSpec l flag) -- | call a logic specific parser if it exists callParser :: Maybe (AParser st a) -> String -> String -> AParser st a callParser p name itemType = fromMaybe (unexpected $ "no " ++ itemType ++ " parser for " ++ name) p -basicSpec :: LogicGraph -> (AnyLogic, Maybe IRI) -> AParser st SPEC -basicSpec lG (Logic lid, sm) = do +basicSpec :: LogicGraph -> Bool -> (AnyLogic, Maybe IRI) -> AParser st SPEC +basicSpec lG flag (Logic lid, sm) = do p <- getPos + let whichParser = if flag then basicSpecParser sm lid else macroParser sm lid bspec <- callParser - (liftM (\ ps -> ps (prefixes lG)) (basicSpecParser sm lid)) + (liftM (\ ps -> ps (prefixes lG)) whichParser) (showSyntax lid sm) "basic specification" q <- getPos return $ Basic_spec (G_basic_spec lid bspec) $ Range [p, q] -logicSpec :: LogicGraph -> AParser st SPEC -logicSpec lG = do +logicSpec :: LogicGraph -> Bool -> AParser st SPEC +logicSpec lG flag = do (s1, ln) <- qualification lG many $ qualification lG -- ignore multiple qualifications for now s2 <- colonT - sp <- annoParser $ specD $ setLogicName ln lG + sp <- annoParser $ specD (setLogicName ln lG) flag return $ Qualified_spec ln sp $ toRange s1 [] s2 combineSpec :: LogicGraph -> AParser st SPEC @@ -499,55 +502,131 @@ lookupAndSetComorphismName c lg = do Comorphism cid <- lookupComorphism c lg return $ setCurLogic (language_name $ targetLogic cid) lg -aSpec :: LogicGraph -> AParser st (Annoted SPEC) -aSpec = annoParser2 . spec +aSpec :: LogicGraph -> Bool -> AParser st (Annoted SPEC) +aSpec lg flag = annoParser2 $ spec lg flag -- | grouped spec or spec-inst without optional DOL import -caslGroupSpec :: LogicGraph -> AParser st SPEC +caslGroupSpec :: LogicGraph -> Bool -> AParser st SPEC caslGroupSpec = groupSpecAux False -- | grouped spec or spec-inst with optional import -groupSpec :: LogicGraph -> AParser st SPEC -groupSpec = groupSpecAux True +groupSpec :: LogicGraph -> Bool -> AParser st SPEC +groupSpec = groupSpecAux True -groupSpecAux :: Bool -> LogicGraph -> AParser st SPEC -groupSpecAux withImport l = do +groupSpecAux :: Bool -> LogicGraph -> Bool -> AParser st SPEC +groupSpecAux withImport l flag = do b <- oBraceT do c <- cBraceT return $ EmptySpec $ catRange [b, c] <|> do - a <- aSpec l + a <- aSpec l flag addAnnos c <- cBraceT return $ Group a $ catRange [b, c] <|> do - n <- hetIRI l - (f, ps) <- fitArgs l + n <- hetIRI l -- TODO: here we should try to parse a compoundIRI and if that fails, try to parse a spec inst! + {- (f, ps) <- fitArgs l flag mi <- if withImport then optionMaybe (hetIRI l) else return Nothing - return (Spec_inst n f mi ps) + case f of + [] -> return $ UnsolvedName n nullRange + _ -> return (Spec_inst n f mi ps) + -} + mf <- optionMaybe (fitArgsPattern l flag withImport) + case mf of + Nothing -> return $ UnsolvedName n nullRange + Just ((f, mi), ps) -> let inst = Spec_inst n f mi ps + in -- trace ("inst:" ++ show inst) $ + return inst + +fitArgsPattern :: LogicGraph -> Bool -> Bool -> AParser st (([Annoted FIT_ARG], Maybe IRI), Range) +fitArgsPattern l flag withImport = do + o <- oBracketT + (fas, _) <- separatedBy (fitArg l flag) semiT + let (fas1, _ps) = unzip fas + c <- cBracketT + return ((fas1, Nothing), toRange o [] c) -fitArgs :: LogicGraph -> AParser st ([Annoted FIT_ARG], Range) -fitArgs l = do - fas <- many (fitArg l) +fitArgs :: LogicGraph -> Bool -> AParser st ([Annoted FIT_ARG], Range) +fitArgs l flag = do + fas <- many (fitArg l flag) let (fas1, ps) = unzip fas return (fas1, concatMapRange id ps) -fitArg :: LogicGraph -> AParser st (Annoted FIT_ARG, Range) -fitArg l = do - b <- oBracketT - fa <- annoParser (fittingArg l) - c <- cBracketT - return (fa, toRange b [] c) - -fittingArg :: LogicGraph -> AParser st FIT_ARG -fittingArg l = do +fitArg :: LogicGraph -> Bool -> AParser st (Annoted FIT_ARG, Range) +fitArg l flag = do + let emptyParam = do + _ <- lookAhead $ try semiT <|> try cBracketT + return $ Missing_arg nullRange + fa <- annoParser emptyParam + -- trace ("**** just scanned 1: " ++ show fa) $ + return (fa, nullRange) + <|> do + -- b <- oBracketT + fa <- annoParser $ fitString l flag + -- c <- cBracketT + -- trace ("**** just scanned 2: " ++ show fa) $ + return (fa, nullRange) + <|> do + fa <- annoParser $ fittingArg l flag + -- trace ("**** just scanned 3: " ++ show fa) $ + return (fa, nullRange) + <|> do + s <- scanString + -- trace ("**** just scanned 4: " ++ s) $ + return (Annoted (Fit_string (mkIRI s) nullRange) nullRange [][], nullRange) + <|> do + _b <- oBracketT + (aspecs, _) <- separatedBy (iParser l flag) commaT + _c <- cBracketT + return (Annoted (Fit_spec (Annoted (OntoList aspecs) nullRange [] []) [] nullRange) nullRange [] [], nullRange) + +iParser :: LogicGraph -> Bool -> AParser st (Annoted SPEC) +iParser l flag = do + i <- hetIRI l --compoundIriCurie + asp <- option (Annoted (UnsolvedName i nullRange) nullRange [][]) $ + do + b <- oBracketT -- after a bracket, check if there's a separator. If there's a comma, it's a compound id. If theres a ;, it's a spec_inst. + fstI <- compoundIriCurie --hetIRI l + asp' <- + do + _ <- commaT + (ts, ps) <- mixId ([],[]) ([],[]) `separatedBy` commaT + c <- cBracketT + _ <- option () skip + return $ Annoted (UnsolvedName (i {iriPath = addComponents (iriPath i) ((iriPath fstI):ts, toRange b ps c)}) nullRange) nullRange [] [] + <|> do + _ <- semiT + (fas, _) <- (fitArg l flag) `separatedBy` semiT + let (f, _ps) = unzip fas + _c <- cBracketT + _ <- option () skip + let fstArg = Annoted (Fit_spec (Annoted (UnsolvedName fstI nullRange) nullRange [][]) [] nullRange) nullRange [][] + inst = Spec_inst i (fstArg:f) Nothing nullRange + return $ Annoted inst nullRange [] [] + <|> do + _ <- cBracketT + return $ Annoted (UnsolvedName i{iriPath = addComponents (iriPath i) ([iriPath fstI], nullRange)} nullRange) nullRange [][] + return asp' + return asp + <|> aSpec l flag + +fitString :: LogicGraph -> Bool -> AParser st FIT_ARG +fitString l flag = do + (s, _) <- separatedBy (iParser l flag) doubleColonT + case s of + [] -> error "should be caught by the other case" + [x] -> return $ Fit_spec x [] nullRange + _ -> return $ Fit_spec (Annoted (OntoList s) nullRange [][]) [] nullRange -- Fit_list s nullRange + +fittingArg :: LogicGraph -> Bool -> AParser st FIT_ARG +fittingArg l flag = do s <- asKey viewS vn <- hetIRI l - (fa, ps) <- fitArgs l + (fa, ps) <- fitArgs l flag return (Fit_view vn fa (tokPos s `appRange` ps)) <|> do - sp <- aSpec l + sp <- aSpec l flag (symbit, ps) <- option ([], nullRange) $ do s <- asKey fitS (m, qs) <- parseMapping l diff --git a/Syntax/Print_AS_Structured.hs b/Syntax/Print_AS_Structured.hs index f85f7ec772..c311e8c823 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] + _ -> text $ show spec instance Pretty Network where pretty (Network cs es _) = fsep $ ppWithCommas cs