a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach{- |

8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy GimblettModule : $Header$

e071fb22ea9923a2a4ff41184d80ca46b55ee932Till MossakowskiDescription : static analysis of DOL documents and CASL specification libraries

e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederCopyright : (c) Till Mossakowski, Uni Magdeburg 2002-2016

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : GPLv2 or higher, see LICENSE.txt

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachMaintainer : till@informatik.uni-bremen.de

b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiStability : provisional

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability : non-portable(Logic)

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachStatic analysis of DOL documents and CASL specification libraries

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett Follows the verification semantics sketched in Chap. IV:6

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach of the CASL Reference Manual.

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach Follows the semantics of DOL documents, DOL OMG standard, clause 10.2.1

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-}

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblettmodule Static.AnalysisLibrary

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett ( anaLibFileOrGetEnv

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach , anaLibDefn

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach , anaSourceFile

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach , anaLibItem

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach , anaViewDefn

90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett , LNS

eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett ) where

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblettimport Logic.Logic

eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettimport Logic.Grothendieck

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblettimport Logic.Comorphism

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Logic.Coerce

1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblettimport Logic.ExtSign

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Logic.Prover

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettimport Syntax.AS_Structured

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Syntax.Print_AS_Structured

792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maederimport Syntax.Print_AS_Library ()

0ea916d1e6aea10fd7b84f802fb5148a79d8c20aAndy Gimblettimport Syntax.AS_Library

04ceed96d1528b939f2e592d0656290d81d1c045Andy Gimblett

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblettimport Static.GTheory

eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettimport Static.DevGraph

1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblettimport Static.DgUtils

c4b2418421546a337f83332fe0db04742dcd735dAndy Gimblettimport Static.ComputeTheory

41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimblettimport Static.AnalysisStructured

41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimblettimport Static.AnalysisArchitecture

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettimport Static.ArchDiagram (emptyExtStUnitCtx)

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettimport Common.AS_Annotation hiding (isAxiom, isDef)

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettimport Common.Consistency

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettimport Common.GlobalAnnotations

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettimport Common.ConvertGlobalAnnos

41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimblettimport Common.AnalyseAnnos

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettimport Common.ExtSign

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettimport Common.Result

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblettimport Common.ResultT

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblettimport Common.LibName

90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblettimport Common.Id

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettimport Common.IRI

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettimport qualified Common.Unlit as Unlit

41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimblett

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettimport Driver.Options

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettimport Driver.ReadFn

eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettimport Driver.ReadLibDefn

eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettimport Driver.WriteLibDefn

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett

61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblettimport qualified Data.Map as Map

eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettimport qualified Data.Set as Set

eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettimport Data.Either (lefts, rights)

eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettimport Data.List

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblettimport Data.Maybe

eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblettimport Control.Monad

eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettimport Control.Monad.Trans

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblettimport System.Directory

61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblettimport System.FilePath

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblettimport LF.Twelf2DG

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblettimport Framework.Analysis

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettimport MMT.Hets2mmt (mmtRes)

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett-- a set of library names to check for cyclic imports

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimbletttype LNS = Set.Set LibName

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett

820947bd01ca952c3909eaa0366c6914c87cc1cbTill Mossakowski{- | parsing and static analysis for files

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettParameters: logic graph, default logic, file name -}

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettanaSourceFile :: LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett -> FilePath -> ResultT IO (LibName, LibEnv)

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettanaSourceFile = anaSource Nothing

90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy GimblettanaSource :: Maybe LibName -- ^ suggested library name

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett -> LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett -> FilePath -> ResultT IO (LibName, LibEnv)

90047eafd2de482c67bcd13103c6064e9b0cb254Andy GimblettanaSource mln lg opts topLns libenv initDG origName = ResultT $ do

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett let mName = useCatalogURL opts origName

90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett fname = fromMaybe mName $ stripPrefix "file://" mName

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett syn = case defSyntax opts of

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett "" -> Nothing

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett s -> Just $ simpleIdToIRI $ mkSimpleId s

90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett lgraph = setSyntax syn $ setCurLogic (defLogic opts) lg

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach fname' <- getContentAndFileType opts fname

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett case fname' of

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett Left err -> return $ fail err

af745a4a6cb26002e55b69f90d837fe9c6176d4bAndy Gimblett Right (mr, _, file, inputLit) ->

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett if any (`isSuffixOf` file) [envSuffix, prfSuffix] then

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett return . fail $ "no matching source file for '" ++ fname ++ "' found."

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett else let

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett input = (if unlit opts then Unlit.unlit else id) inputLit

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett libStr = if isAbsolute fname

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett then convertFileToLibStr fname

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett else dropExtensions fname

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett nLn = case mln of

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett Nothing | useLibPos opts && not (checkUri fname) ->

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett Just $ emptyLibName libStr

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett _ -> mln

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett fn2 = keepOrigClifName opts origName file

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett in

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett if runMMT opts then mmtRes fname else

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett if takeExtension file /= ('.' : show TwelfIn)

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett then runResultT $

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett anaString nLn lgraph opts topLns libenv initDG input fn2 mr

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett else do

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett res <- anaTwelfFile opts file

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett return $ case res of

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett Nothing -> fail $ "failed to analyse file: " ++ file

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett Just (lname, lenv) -> return (lname, Map.union lenv libenv)

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett-- | parsing of input string (content of file)

e95030058b77cb83593c85aa4c506caf154f63b7Andy GimblettanaString :: Maybe LibName -- ^ suggested library name

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett -> LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph -> String

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett -> FilePath -> Maybe String -- ^ mime-type of file

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett -> ResultT IO (LibName, LibEnv)

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy GimblettanaString mln lgraph opts topLns libenv initDG input file mr = do

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett curDir <- lift getCurrentDirectory -- get full path for parser positions

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett let realFileName = curDir </> file

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett posFileName = case mln of

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett Just gLn | useLibPos opts -> libToFileName gLn

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett _ -> if checkUri file then file else realFileName

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett lift $ putIfVerbose opts 2 $ "Reading file " ++ file

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett libdefns <- readLibDefn lgraph opts mr file posFileName input

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett when (null libdefns) . fail $ "failed to read contents of file: " ++ file

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett foldM (anaStringAux mln lgraph opts topLns initDG mr file posFileName)

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett (error "Static.AnalysisLibrary.anaString", libenv)

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett $ case analysis opts of

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett Skip -> [last libdefns]

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett _ -> libdefns

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett-- | calling static analysis for parsed library-defn

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettanaStringAux :: Maybe LibName -- ^ suggested library name

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett -> LogicGraph -> HetcatsOpts -> LNS -> DGraph -> Maybe String -> FilePath

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett -> FilePath -> (LibName, LibEnv) -> LIB_DEFN -> ResultT IO (LibName, LibEnv)

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettanaStringAux mln lgraph opts topLns initDG mt file posFileName (_, libenv)

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett (Lib_defn pln is' ps ans) = do

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett let pm = fst $ partPrefixes ans

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett expnd i = fromMaybe i $ expandCurie pm i

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett spNs = Set.unions . map (Set.map expnd . getSpecNames)

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett $ concatMap (getSpecDef . item) is'

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett declNs = Set.fromList . map expnd

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett $ concatMap (getDeclSpecNames . item) is'

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett missNames = Set.toList $ spNs Set.\\ declNs

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett unDecls = map (addDownload True) $ filter

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett (isNothing . (`lookupGlobalEnvDG` initDG)) missNames

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett is = unDecls ++ is'

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett spN = convertFileToLibStr file

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett noLibName = getLibId pln == nullIRI

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett nIs = case is of

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett [Annoted (Spec_defn spn gn as qs) rs [] []]

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett | noLibName && null (iriToStringUnsecure spn)

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett -> [Annoted (Spec_defn (simpleIdToIRI $ mkSimpleId spN)

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett gn as qs) rs [] []]

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett _ -> is

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett emptyFilePath = null $ getFilePath pln

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett ln = setMimeType mt $ if emptyFilePath then setFilePath posFileName

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett $ if noLibName then fromMaybe (emptyLibName spN) mln else pln

e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett else pln

e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett ast = Lib_defn ln nIs ps ans

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett case analysis opts of

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett Skip -> do

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett lift $ putIfVerbose opts 1 $

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett "Skipping static analysis of library " ++ show ln

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett ga <- liftR $ addGlobalAnnos emptyGlobalAnnos ans

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett lift $ writeLibDefn lgraph ga file opts ast

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett liftR mzero

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett _ -> do

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett let libstring = libToFileName ln

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett unless (isSuffixOf libstring (dropExtension file)

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett || not emptyFilePath) . lift . putIfVerbose opts 1

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett $ "### file name '" ++ file ++ "' does not match library name '"

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett ++ libstring ++ "'"

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett lift $ putIfVerbose opts 1 $ "Analyzing "

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett ++ (if noLibName then "file " ++ file ++ " as " else "")

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett ++ "library " ++ show ln

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett (lnFinal, ld, ga, lenv) <-

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett anaLibDefn lgraph opts topLns libenv initDG ast file

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett case Map.lookup lnFinal lenv of

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett Nothing -> error $ "anaString: missing library: " ++ show lnFinal

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett Just dg -> lift $ do

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett writeLibDefn lgraph ga file opts ld

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett when (hasEnvOut opts)

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett (writeFileInfo opts lnFinal file ld dg)

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett return (lnFinal, lenv)

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett-- lookup or read a library

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy GimblettanaLibFile :: LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph -> LibName

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett -> ResultT IO (LibName, LibEnv)

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy GimblettanaLibFile lgraph opts topLns libenv initDG ln =

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett let lnstr = show ln in case find (== ln) $ Map.keys libenv of

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett Just ln' -> do

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett analyzing opts $ "from " ++ lnstr

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett return (ln', libenv)

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett Nothing ->

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett do

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett putMessageIORes opts 1 $ "Downloading " ++ lnstr ++ " ..."

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett res <- anaLibFileOrGetEnv lgraph

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett (if recurse opts then opts else opts

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett { outtypes = []

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett , unlit = False })

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett (Set.insert ln topLns) libenv initDG (Just ln) $ libNameToFile ln

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett putMessageIORes opts 1 $ "... loaded " ++ lnstr

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett return res

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett-- | lookup or read a library

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy GimblettanaLibFileOrGetEnv :: LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett -> Maybe LibName -> FilePath -> ResultT IO (LibName, LibEnv)

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy GimblettanaLibFileOrGetEnv lgraph opts topLns libenv initDG mln file = do

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett let envFile = rmSuffix file ++ envSuffix

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett recent_envFile <- lift $ checkRecentEnv opts envFile file

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett if recent_envFile

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett then do

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett mgc <- lift $ readVerbose lgraph opts mln envFile

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett case mgc of

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett Nothing -> do

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett lift $ putIfVerbose opts 1 $ "Deleting " ++ envFile

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett lift $ removeFile envFile

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett anaSource mln lgraph opts topLns libenv initDG file

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett Just (ld@(Lib_defn ln _ _ _), gc) -> do

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett lift $ writeLibDefn lgraph (globalAnnos gc) file opts ld

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett -- get all DGRefs from DGraph

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett mEnv <- foldl

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett ( \ ioLibEnv labOfDG -> let node = snd labOfDG in

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett if isDGRef node then do

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett let ln2 = dgn_libname node

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett p_libEnv <- ioLibEnv

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett if Map.member ln2 p_libEnv then

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett return p_libEnv

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett else fmap snd $ anaLibFile lgraph

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett opts topLns p_libEnv initDG ln2

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett else ioLibEnv)

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett (return $ Map.insert ln gc libenv)

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett $ labNodesDG gc

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett return (ln, mEnv)

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett else anaSource mln lgraph opts topLns libenv initDG file

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett

{- | analyze a LIB_DEFN.

Parameters: logic graph, default logic, opts, library env, LIB_DEFN.

Call this function as follows:

> do Result diags res <- runResultT (anaLibDefn ...)

> mapM_ (putStrLn . show) diags

-}

anaLibDefn :: LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph -> LIB_DEFN

-> FilePath -> ResultT IO (LibName, LIB_DEFN, GlobalAnnos, LibEnv)

anaLibDefn lgraph opts topLns libenv dg (Lib_defn ln alibItems pos ans) file

= do

let libStr = libToFileName ln

isDOLlib = elem ':' libStr

gannos <- showDiags1 opts $ liftR $ addGlobalAnnos

(defPrefixGlobalAnnos $ if isDOLlib then file else libStr) ans

allAnnos <- liftR $ mergeGlobalAnnos (globalAnnos dg) gannos

(libItems', dg', libenv', _, _) <- foldM (anaLibItemAux opts topLns ln)

([], dg { globalAnnos = allAnnos }, libenv

, lgraph, Map.empty) (map item alibItems)

let dg1 = computeDGraphTheories libenv' $ markFree libenv'

$ markHiding libenv' $ fromMaybe dg' $ maybeResult

$ shortcutUnions dg'

newLD = Lib_defn ln

(zipWith replaceAnnoted (reverse libItems') alibItems) pos ans

dg2 = dg1 { optLibDefn = Just newLD }

return (ln, newLD, globalAnnos dg2, Map.insert ln dg2 libenv')

shortcutUnions :: DGraph -> Result DGraph

shortcutUnions dgraph = let spNs = getGlobNodes $ globalEnv dgraph in

foldM (\ dg (n, nl) -> let

locTh = dgn_theory nl

innNs = innDG dg n

in case outDG dg n of

[(_, t, et@DGLink {dgl_type = lt})]

| Set.notMember n spNs && null (getThSens locTh) && isGlobalDef lt

&& length innNs > 1

&& all (\ (_, _, el) -> case dgl_type el of

ScopedLink Global DefLink (ConsStatus cs None LeftOpen)

| cs == getCons lt -> True

_ -> False) innNs

&& case nodeInfo nl of

DGNode DGUnion _ -> True

_ -> False

-> foldM (\ dg' (s, _, el) -> do

newMor <- composeMorphisms (dgl_morphism el) $ dgl_morphism et

return $ insLink dg' newMor

(dgl_type el) (dgl_origin el) s t) (delNodeDG n dg) innNs

_ -> return dg) dgraph $ topsortedNodes dgraph

defPrefixGlobalAnnos :: FilePath -> GlobalAnnos

defPrefixGlobalAnnos file = emptyGlobalAnnos

{ prefix_map = Map.singleton ""

$ fromMaybe nullIRI $ parseIRIReference $ file ++ "?" }

anaLibItemAux :: HetcatsOpts -> LNS -> LibName

-> ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides) -> LIB_ITEM

-> ResultT IO ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)

anaLibItemAux opts topLns ln q@(libItems', dg1, libenv1, lg, eo) libItem = let

currLog = currentLogic lg

newOpts = if elem currLog ["DMU", "Framework"] then

opts { defLogic = currLog } else opts

in ResultT $ do

res2@(Result diags2 res) <- runResultT

$ anaLibItem lg newOpts topLns ln libenv1 dg1 eo libItem

runResultT $ showDiags1 opts (liftR res2)

let mRes = case res of

Just (libItem', dg1', libenv1', newLG, eo') ->

Just (libItem' : libItems', dg1', libenv1', newLG, eo')

Nothing -> Just q

if outputToStdout opts then

if hasErrors diags2 then

fail "Stopped due to errors"

else runResultT $ liftR $ Result [] mRes

else runResultT $ liftR $ Result diags2 mRes

putMessageIORes :: HetcatsOpts -> Int -> String -> ResultT IO ()

putMessageIORes opts i msg =

if outputToStdout opts

then lift $ putIfVerbose opts i msg

else liftR $ message () msg

analyzing :: HetcatsOpts -> String -> ResultT IO ()

analyzing opts = putMessageIORes opts 1 . ("Analyzing " ++)

alreadyDefined :: String -> String

alreadyDefined str = "Name " ++ str ++ " already defined"

-- | analyze a GENERICITY

anaGenericity :: LogicGraph -> LibEnv -> LibName -> DGraph -> HetcatsOpts

-> ExpOverrides -> NodeName -> GENERICITY

-> Result (GENERICITY, GenSig, DGraph)

anaGenericity lg libEnv ln dg opts eo name

gen@(Genericity (Params psps) (Imported isps) pos) =

let ms = currentBaseTheory dg in

adjustPos pos $ case psps of

[] -> do -- no parameter ...

unless (null isps) $ plain_error ()

"Parameterless specifications must not have imports" pos

l <- lookupCurrentLogic "GENERICITY" lg

return (gen, GenSig (EmptyNode l) []

$ maybe (EmptyNode l) JustNode ms, dg)

_ -> do

l <- lookupCurrentLogic "IMPORTS" lg

let baseNode = maybe (EmptyNode l) JustNode ms

(imps', nsigI, dg') <- case isps of

[] -> return ([], baseNode, dg)

_ -> do

(is', _, nsig', dgI) <- anaUnion False lg libEnv ln dg baseNode

(extName "Imports" name) opts eo isps $ getRange isps

return (is', JustNode nsig', dgI)

(ps', nsigPs, ns, dg'') <- anaUnion False lg libEnv ln dg' nsigI

(extName "Parameters" name) opts eo psps $ getRange psps

return (Genericity (Params ps') (Imported imps') pos,

GenSig nsigI nsigPs $ JustNode ns, dg'')

expCurieT :: GlobalAnnos -> ExpOverrides -> IRI -> ResultT IO IRI

expCurieT ga eo = liftR . expCurieR ga eo

-- | analyse a LIB_ITEM

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 =

case itm of

Spec_defn spn2 gen asp pos -> do

let spn' = if null (iriToStringUnsecure spn2) then

simpleIdToIRI $ mkSimpleId "Spec" else spn2

spn <- expCurieT (globalAnnos dg) eo spn'

let spstr = iriToStringUnsecure spn

nName = makeName spn

analyzing opts $ "spec " ++ spstr

(gen', gsig@(GenSig _ _args allparams), dg') <-

liftR $ anaGenericity lg libenv currLn dg opts eo nName gen

(sanno1, impliesA) <- liftR $ getSpecAnnos pos asp

when impliesA $ liftR $ plain_error ()

"unexpected initial %implies in spec-defn" pos

(sp', body, dg'') <-

liftR (anaSpecTop sanno1 True lg libenv currLn dg'

allparams nName opts eo (item asp) pos)

let libItem' = Spec_defn spn gen' (replaceAnnoted sp' asp) pos

genv = globalEnv dg

if Map.member spn genv

then liftR $ plain_error (libItem', dg'', libenv, lg, eo)

(alreadyDefined spstr) pos

else

-- let (_n, dg''') = addSpecNodeRT dg'' (UnitSig args body) $ show spn

return

( libItem'

, dg'' { globalEnv = Map.insert spn (SpecEntry

$ ExtGenSig gsig body) genv }

, libenv, lg, eo)

Entail_defn en' etype pos -> do

en <- expCurieT (globalAnnos dg) eo en'

analyzing opts $ "entailment " ++ iriToStringUnsecure en

liftR $ anaEntailmentDefn lg currLn libenv dg opts eo en etype pos

View_defn vn' gen vt gsis pos -> do

vn <- expCurieT (globalAnnos dg) eo vn'

analyzing opts $ "view " ++ iriToStringUnsecure vn

liftR $ anaViewDefn lg currLn libenv dg opts eo vn gen vt gsis pos

Align_defn an' arities atype acorresps _ pos -> do

an <- expCurieT (globalAnnos dg) eo an'

analyzing opts $ "alignment " ++ iriToStringUnsecure an

anaAlignDefn lg currLn libenv dg opts eo an arities atype acorresps pos

Arch_spec_defn asn' asp pos -> do

asn <- expCurieT (globalAnnos dg) eo asn'

let asstr = iriToStringUnsecure asn

analyzing opts $ "arch spec " ++ asstr

(_, _, diag, archSig, dg', asp') <- liftR $ anaArchSpec lg libenv currLn dg

opts eo emptyExtStUnitCtx Nothing $ item asp

let asd' = Arch_spec_defn asn (replaceAnnoted asp' asp) pos

genv = globalEnv dg'

if Map.member asn genv

then liftR $ plain_error (asd', dg', libenv, lg, eo)

(alreadyDefined asstr) pos

else do

let aName = show asn

dg'' = updateNodeNameRT dg'

(refSource $ getPointerFromRef archSig)

True aName

dg3 = dg'' { archSpecDiags =

Map.insert aName diag

$ archSpecDiags dg''}

return (asd', dg3

{ globalEnv = Map.insert asn

(ArchOrRefEntry True archSig) genv }

, libenv, lg, eo)

Unit_spec_defn usn' usp pos -> do

usn <- expCurieT (globalAnnos dg) eo usn'

let usstr = iriToStringUnsecure usn

analyzing opts $ "unit spec " ++ usstr

l <- lookupCurrentLogic "Unit_spec_defn" lg

(rSig, dg', usp') <-

liftR $ anaUnitSpec lg libenv currLn dg opts eo (EmptyNode l) Nothing usp

unitSig <- liftR $ getUnitSigFromRef rSig

let usd' = Unit_spec_defn usn usp' pos

genv = globalEnv dg'

if Map.member usn genv

then liftR $ plain_error (itm, dg', libenv, lg, eo)

(alreadyDefined usstr) pos

else return (usd', dg'

{ globalEnv = Map.insert usn (UnitEntry unitSig) genv },

libenv, lg, eo)

Ref_spec_defn rn' rsp pos -> do

rn <- expCurieT (globalAnnos dg) eo rn'

let rnstr = iriToStringUnsecure rn

l <- lookupCurrentLogic "Ref_spec_defn" lg

(_, _, _, rsig, dg', rsp') <- liftR $ anaRefSpec lg libenv currLn dg opts eo

(EmptyNode l) rn emptyExtStUnitCtx Nothing rsp

analyzing opts $ "ref spec " ++ rnstr

let rsd' = Ref_spec_defn rn rsp' pos

genv = globalEnv dg'

if Map.member rn genv

then liftR $ plain_error (itm, dg', libenv, lg, eo)

(alreadyDefined rnstr) pos

else return ( rsd', dg'

{ globalEnv = Map.insert rn (ArchOrRefEntry False rsig) genv }

, libenv, lg, eo)

Logic_decl logN pos -> do

putMessageIORes opts 1 . show $ prettyLG lg itm

(mth, newLg) <- liftR

$ adjustPos pos $ anaSublogic opts logN currLn dg libenv lg

case mth of

Nothing ->

return (itm, dg { currentBaseTheory = Nothing }, libenv, newLg, eo)

Just (s, (libName, refDG, (_, lbl))) -> do

-- store th-lbl in newDG

let dg2 = if libName /= currLn then

let (s2, (genv, newDG)) = refExtsigAndInsert libenv libName refDG

(globalEnv dg, dg) (getName $ dgn_name lbl) s

in newDG { globalEnv = genv

, currentBaseTheory = Just $ extGenBody s2 }

else dg { currentBaseTheory = Just $ extGenBody s }

return (itm, dg2, libenv, newLg, eo)

Download_items ln items pos ->

if Set.member ln topLns then

liftR $ mkError "illegal cyclic library import"

$ Set.map getLibId topLns

else do

let newOpts = opts { intype = GuessIn }

(ln', libenv') <- anaLibFile lg newOpts topLns libenv

(cpIndexMaps dg emptyDG { globalAnnos =

emptyGlobalAnnos { prefix_map = prefix_map $ globalAnnos dg }}) ln

unless (ln == ln')

$ liftR $ warning ()

(shows ln " does not match internal name " ++ shows ln' "")

pos

case Map.lookup ln' libenv' of

Nothing -> error $ "Internal error: did not find library "

++ show ln' ++ " available: " ++ show (Map.keys libenv')

Just dg' -> do

let dg0 = cpIndexMaps dg' dg

fn = libToFileName ln'

currFn = libToFileName currLn

(realItems, errs, origItems) = case items of

ItemMaps rawIms ->

let (ims, warns) = foldr (\ im@(ItemNameMap i mi)

(is, ws) -> if Just i == mi then

(ItemNameMap i Nothing : is

, warning () (show i ++ " item no renamed")

(getRange mi) : ws)

else (im : is, ws)) ([], []) rawIms

expIms = map (expandCurieItemNameMap fn currFn) ims

leftExpIms = lefts expIms

in if not $ null leftExpIms

then ([], leftExpIms, itemNameMapsToIRIs ims)

else (rights expIms, warns, itemNameMapsToIRIs ims)

UniqueItem i ->

let is = Map.keys $ globalEnv dg'

ks = case is of

[_] -> is

_ -> filter (== getLibId ln') is

in case ks of

[j] -> case expCurie (globalAnnos dg) eo i of

Nothing -> ([], [prefixErrorIRI i], [i])

Just expI -> case expCurie (globalAnnos dg) eo j of

Nothing -> ([], [prefixErrorIRI j], [i, j])

Just expJ ->

([ItemNameMap expJ (Just expI)], [], [i, j])

_ ->

( []

, [ mkError ("non-unique name within imported library: "

++ intercalate ", " (map show is))

ln'], [])

additionalEo = Map.fromList $ map (\ o -> (o, fn)) origItems

eo' = Map.unionWith (\ _ p2 -> p2) eo additionalEo

mapM_ liftR errs

dg1 <- liftR $ anaItemNamesOrMaps libenv' ln' dg' dg0 realItems

return (itm, dg1, libenv', lg, eo')

Newlogic_defn ld _ -> ResultT $ do

dg' <- anaLogicDef ld dg

return $ Result [] $ Just (itm, dg', libenv, lg, eo)

Newcomorphism_defn com _ -> ResultT $ do

dg' <- anaComorphismDef com dg

return $ Result [] $ Just (itm, dg', libenv, lg, eo)

_ -> return (itm, dg, libenv, lg, eo)

symbolsOf :: LogicGraph -> G_sign -> G_sign -> [CORRESPONDENCE]

-> Result (Set.Set (G_symbol, G_symbol))

symbolsOf lg gs1@(G_sign l1 (ExtSign sig1 sys1) _)

gs2@(G_sign l2 (ExtSign sig2 sys2) _) corresps =

case corresps of

[] -> return Set.empty

c : corresps' -> case c of

Default_correspondence -> symbolsOf lg gs1 gs2 corresps' -- TO DO

Correspondence_block _ _ cs -> do

sPs1 <- symbolsOf lg gs1 gs2 cs

sPs2 <- symbolsOf lg gs1 gs2 corresps'

return $ Set.union sPs1 sPs2

Single_correspondence _ (G_symb_items_list lid1 sis1)

(G_symb_items_list lid2 sis2) _ _ -> do

ss1 <- coerceSymbItemsList lid1 l1 "symbolsOf1" sis1

rs1 <- stat_symb_items l1 sig1 ss1

ss2 <- coerceSymbItemsList lid2 l2 "symbolsOf1" sis2

rs2 <- stat_symb_items l2 sig2 ss2

p <- case (rs1, rs2) of

([r1], [r2]) -> -- trace (show r1 ++ " " ++ show (Set.toList sys1)) $

case

( filter (\ sy -> matches l1 sy r1) $ Set.toList sys1

, filter (\ sy -> matches l2 sy r2) $ Set.toList sys2) of

([s1], [s2]) ->

return (G_symbol l1 s1, G_symbol l2 s2)

(ll1, ll2) -> {- trace

("sys1:" ++ (show $

Set.toList sys1

)) $ -}

error

$ "non-unique symbol match: " ++ show ll1 ++ "\n" ++ show ll2

_ -> mkError "non-unique raw symbols" c

ps <- symbolsOf lg gs1 gs2 corresps'

return $ Set.insert p ps

-- | analyse an entailment type

-- | analyse genericity and view type and construct gmorphism

anaEntailmentDefn :: LogicGraph -> LibName -> LibEnv -> DGraph -> HetcatsOpts

-> ExpOverrides -> IRI -> ENTAIL_TYPE -> Range

-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)

anaEntailmentDefn lg ln libEnv dg opts eo en et pos = do

case et of

Entail_type on1 on2 range -> do

case (on1, on2) of

(MkOms asp1, MkOms asp2) -> do

let spS = item asp1

spT = item asp2

name = makeName en

l <- lookupCurrentLogic "ENTAIL_DEFN" lg

(spSrc', srcNsig, dg') <- anaSpec False lg libEnv ln dg (EmptyNode l)

(extName "Source" name) opts eo spS $ getRange spS

(spTgt', tgtNsig, dg'') <- anaSpec True lg libEnv ln dg' (EmptyNode l)

(extName "Target" name) opts eo spT $ getRange spT

incl <- ginclusion lg (getSig tgtNsig) (getSig srcNsig)

let dg3 = insLink dg'' incl globalThm SeeSource (getNode tgtNsig) (getNode srcNsig)

gsig = GenSig (EmptyNode l) [] (EmptyNode l)

let vsig = ExtViewSig srcNsig incl $ ExtGenSig gsig tgtNsig

return (Entail_defn en et pos, dg3{

globalEnv = Map.insert en (ViewOrStructEntry True vsig) $ globalEnv dg3},

libEnv, lg, eo)

_ -> fail "entailment between networks not supported yet"

_ -> fail "omsinnetwork entailment not supported yet"

-- | analyse genericity and view type and construct gmorphism

anaViewDefn :: LogicGraph -> LibName -> LibEnv -> DGraph -> HetcatsOpts

-> ExpOverrides -> IRI -> GENERICITY -> VIEW_TYPE

-> [G_mapping] -> Range

-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)

anaViewDefn lg ln libenv dg opts eo vn gen vt gsis pos = do

let vName = makeName vn

(gen', gsig@(GenSig _ _ allparams), dg') <-

anaGenericity lg libenv ln dg opts eo vName gen

(vt', (src@(NodeSig nodeS gsigmaS)

, tar@(NodeSig nodeT gsigmaT@(G_sign lidT _ _))), dg'') <-

anaViewType lg libenv ln dg' allparams opts eo vName vt

let genv = globalEnv dg''

if Map.member vn genv

then plain_error (View_defn vn gen' vt' gsis pos, dg'', libenv, lg, eo)

(alreadyDefined $ iriToStringUnsecure vn) pos

else do

let (tsis, hsis) = partitionGmaps gsis

(gsigmaS', tmor) <- if null tsis then do

(gsigmaS', imor) <- gSigCoerce lg gsigmaS (Logic lidT)

tmor <- gEmbedComorphism imor gsigmaS

return (gsigmaS', tmor)

else do

mor <- anaRenaming lg allparams gsigmaS opts (Renaming tsis pos)

let gsigmaS'' = cod mor

(gsigmaS', imor) <- gSigCoerce lg gsigmaS'' (Logic lidT)

tmor <- gEmbedComorphism imor gsigmaS''

fmor <- comp mor tmor

return (gsigmaS', fmor)

emor <- fmap gEmbed $ anaGmaps lg opts pos gsigmaS' gsigmaT hsis

gmor <- comp tmor emor

let vsig = ExtViewSig src gmor $ ExtGenSig gsig tar

voidView = nodeS == nodeT && isInclusion gmor

when voidView $ warning ()

("identity mapping of source to same target for view: " ++

iriToStringUnsecure vn) pos

return (View_defn vn gen' vt' gsis pos,

(if voidView then dg'' else insLink dg'' gmor globalThm

(DGLinkView vn $ Fitted gsis) nodeS nodeT)

-- 'LeftOpen' for conserv correct?

{ globalEnv = Map.insert vn (ViewOrStructEntry True vsig) genv }

, libenv, lg, eo)

{- | analyze a VIEW_TYPE

The first four arguments give the global context

The AnyLogic is the current logic

The NodeSig is the signature of the parameter of the view

flag, whether just the structure shall be analysed -}

anaViewType :: LogicGraph -> LibEnv -> LibName -> DGraph -> MaybeNode -> HetcatsOpts

-> ExpOverrides

-> NodeName -> VIEW_TYPE -> Result (VIEW_TYPE, (NodeSig, NodeSig), DGraph)

anaViewType lg libEnv ln dg parSig opts eo name (View_type aspSrc aspTar pos) = do

-- trace "called anaViewType" $ do

l <- lookupCurrentLogic "VIEW_TYPE" lg

let spS = item aspSrc

spT = item aspTar

(spSrc', srcNsig, dg') <- anaSpec False lg libEnv ln dg (EmptyNode l)

(extName "Source" name) opts eo spS $ getRange spS

(spTar', tarNsig, dg'') <- anaSpec True lg libEnv ln dg' parSig

(extName "Target" name) opts eo spT $ getRange spT

return (View_type (replaceAnnoted spSrc' aspSrc)

(replaceAnnoted spTar' aspTar)

pos,

(srcNsig, tarNsig), dg'')

anaAlignDefn :: LogicGraph -> LibName -> LibEnv -> DGraph -> HetcatsOpts

-> ExpOverrides -> IRI -> Maybe ALIGN_ARITIES -> VIEW_TYPE

-> [CORRESPONDENCE] -> Range

-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)

anaAlignDefn lg ln libenv dg opts eo an arities atype acorresps pos = do

l <- lookupCurrentLogic "Align_defn" lg

(atype', (src, tar), dg') <- liftR

$ anaViewType lg libenv ln dg (EmptyNode l) opts eo (makeName an) atype

let gsig1 = getSig src

gsig2 = getSig tar

case (gsig1, gsig2) of

(G_sign lid1 gsign1 ind1, G_sign lid2 gsign2 _) ->

if Logic lid1 == Logic lid2 then do

-- arities TO DO

pairsSet <- liftR $ symbolsOf lg gsig1 gsig2 acorresps

let leftList = map fst $ Set.toList pairsSet

rightList = map snd $ Set.toList pairsSet

isTotal gsig sList = Set.fromList sList == symsOfGsign gsig

isInjective sList = length sList == length (nub sList)

checkArity sList1 sList2 gsig arity = case arity of

AA_InjectiveAndTotal -> isTotal gsig sList1 &&

isInjective sList2

AA_Injective -> isInjective sList2

AA_Total -> isTotal gsig sList1

_ -> True

aCheck = case arities of

Nothing -> True

Just (Align_arities aleft aright) ->

checkArity leftList rightList gsig1 aleft &&

checkArity rightList leftList gsig2 aright

if not aCheck then

liftR $ mkError "Arities do not check" arities

else do

newDg <- do

-- (A_source, A_target, A_bridge,

-- A_source -> O1, A_target -> O2)

(gt1, gt2, gt, gmor1, gmor2) <- liftR $

generateWAlign an gsig1 gsig2 acorresps

-- A_source

let n1 = getNewNodeDG dg'

labN1 = newInfoNodeLab

(makeName an

{abbrevFragment = abbrevFragment an ++ "_source"})

(newNodeInfo DGAlignment)

gt1

dg1 = insLNodeDG (n1, labN1) dg'

-- A_target

n2 = getNewNodeDG dg1

labN2 = newInfoNodeLab

(makeName an

{abbrevFragment = abbrevFragment an ++ "_target"})

(newNodeInfo DGAlignment)

gt2

dg2 = insLNodeDG (n2, labN2) dg1

-- A_bridge

n = getNewNodeDG dg2

labN = newInfoNodeLab

(makeName an

{abbrevFragment = abbrevFragment an ++ "_bridge"})

(newNodeInfo DGAlignment)

gt

dg3 = insLNodeDG (n, labN) dg2

-- A_target-> O2

(_, dg4) = insLEdgeDG

(n2, getNode tar, globDefLink gmor2 $ DGLinkAlign an)

dg3

-- A_source -> O1

(_, dg5) = insLEdgeDG

(n1, getNode src, globDefLink gmor1 $ DGLinkAlign an)

dg4

-- inclusion of A_source in A_bridge

incl1 <- liftR $ ginclusion lg (signOf gt1) $ signOf gt

-- inclusion of A_target in A_bridge

incl2 <- liftR $ ginclusion lg (signOf gt2) $ signOf gt

-- add the inclusions to the dg

let (_, dg6) = insLEdgeDG

(n1, n,

globDefLink incl1 $ DGLinkAlign an) dg5

(_, dg7) = insLEdgeDG

(n2, n,

globDefLink incl2 $ DGLinkAlign an) dg6

-- store the alignment in the global env

asign = WAlign (NodeSig n1 $ signOf gt1) incl1 gmor1

(NodeSig n2 $ signOf gt2) incl2 gmor2

src tar (NodeSig n $ signOf gt)

return dg7 {globalEnv = Map.insert an (AlignEntry asign)

$ globalEnv dg7}

let itm = Align_defn an arities atype' acorresps SingleDomain pos

anstr = iriToStringUnsecure an

if Map.member an $ globalEnv dg

then liftR $ plain_error (itm, dg, libenv, lg, eo)

(alreadyDefined anstr) pos

else return (itm, newDg, libenv, lg, eo)

else liftR $ fatal_error

("Alignments only work between ontologies in the same logic\n"

++ show (prettyLG lg atype)) pos

generateWAlign :: IRI -> G_sign -> G_sign -> [CORRESPONDENCE]

-> Result (G_theory, G_theory, G_theory, GMorphism, GMorphism)

generateWAlign an

(G_sign lid1 (ExtSign ssig _) _)

(G_sign lid2 (ExtSign tsig _) _)

corrs = do

tsig' <- coercePlainSign lid2 lid1 "coercePlainSign" tsig

-- 1. initialize

let

sig1 = empty_signature lid1

sig2 = empty_signature lid1

sig = empty_signature lid1

phi1 = Map.empty

phi2 = Map.empty

-- 2. for each correspondence (e1,e2,r),

-- build the bridge ontology (s', sens')

-- the signatures s1'' and s2'' of the involved symbols

-- together with the maps (aname:e1 -> e1) and (aname:e2 -> e2)

-- This is done by corresp2th, in a logic dependent way.

let addCorresp (s1, s2, s, sens, p1, p2) (G_symb_items_list lids1 l1,

G_symb_items_list lids2 l2, rrel) = do

l1' <- coerceSymbItemsList lids1 lid1 "coerceSymbItemsList" l1

l2' <- coerceSymbItemsList lids2 lid1 "coerceSymbItemsList" l2

(sigb, senb, s1', s2', eMap1, eMap2) <-

corresp2th lid1 (iriToStringUnsecure an)

ssig tsig'

l1' l2' p1 p2 rrel

s1'' <- signature_union lid1 s1 s1'

s2'' <- signature_union lid1 s2 s2'

s' <- signature_union lid1 s sigb

let p1' = Map.union eMap1 p1

p2' = Map.union eMap2 p2

sens' = sens ++ senb

return (s1'', s2'', s', sens', p1', p2')

(sig1'', sig2'', sig'', sens'', sMap1, sMap2) <- foldM addCorresp

(sig1, sig2, sig, [], phi1, phi2) $

map (\c -> case c of

Single_correspondence _ s1 s2 (Just rref) _ ->

(s1, s2, refToRel rref)

_ -> error "only single correspondences for now")

corrs

-- 3. make G_ results

-- gth1 is A_source

let gth1 = noSensGTheory lid1 (mkExtSign sig1'') startSigId

-- gth2 is A_target

gth2 = noSensGTheory lid1 (mkExtSign sig2'') startSigId

-- gth is A_bridge

gth = G_theory lid1 Nothing (mkExtSign sig'') startSigId

(toThSens sens'') startThId

-- prepare the maps for morphism generation

rsMap1 = Map.mapKeys (symbol_to_raw lid1) $

Map.map (symbol_to_raw lid1) sMap1

rsMap2 = Map.mapKeys (symbol_to_raw lid1) $

Map.map (symbol_to_raw lid1) sMap2

-- mor1 should go from A_source to O1: sig1'' to ssig

mor1 <- induced_from_to_morphism

lid1 rsMap1 (mkExtSign sig1'') (mkExtSign ssig)

let gmor1 = gEmbed2 (signOf gth1) $ mkG_morphism lid1 mor1

-- mor2 should go from A_target to O2: sig2'' to tsig'

mor2 <- {- trace "mor2:" $

trace ("source: " ++ (show sig2'')) $

trace ("target: " ++ (show tsig')) $ -}

induced_from_to_morphism

lid1 rsMap2 (mkExtSign sig2'') (mkExtSign tsig')

let gmor2 = gEmbed2 (signOf gth2) $ mkG_morphism lid1 mor2

return (gth1, gth2, gth, gmor1, gmor2)

-- the first DGraph dg' is that of the imported library

anaItemNamesOrMaps :: LibEnv -> LibName -> DGraph -> DGraph

-> [ItemNameMap] -> Result DGraph

anaItemNamesOrMaps libenv' ln refDG dg items = do

(genv1, dg1) <- foldM

(anaItemNameOrMap libenv' ln refDG) (globalEnv dg, dg) items

gannos'' <- mergeGlobalAnnos (globalAnnos refDG) $ globalAnnos dg

return dg1

{ globalAnnos = gannos''

, globalEnv = genv1 }

anaItemNameOrMap :: LibEnv -> LibName -> DGraph -> (GlobalEnv, DGraph)

-> ItemNameMap -> Result (GlobalEnv, DGraph)

anaItemNameOrMap libenv ln refDG res (ItemNameMap old m) =

anaItemNameOrMap1 libenv ln refDG res (old, fromMaybe old m)

-- | Auxiliary function for not yet implemented features

anaErr :: String -> a

anaErr f = error $ "*** Analysis of " ++ f ++ " is not yet implemented!"

anaItemNameOrMap1 :: LibEnv -> LibName -> DGraph -> (GlobalEnv, DGraph)

-> (IRI, IRI) -> Result (GlobalEnv, DGraph)

anaItemNameOrMap1 libenv ln refDG (genv, dg) (old, new) = do

entry <- maybe (notFoundError "item" old) return

$ lookupGlobalEnvDG old refDG

maybeToResult (iriPos new) (iriToStringUnsecure new ++ " already used")

$ case Map.lookup new genv of

Nothing -> Just ()

Just _ -> Nothing

case entry of

SpecEntry extsig ->

return $ snd $ refExtsigAndInsert libenv ln refDG (genv, dg) new extsig

ViewOrStructEntry b vsig ->

let (dg1, vsig1) = refViewsig libenv ln refDG dg (makeName new) vsig

genv1 = Map.insert new (ViewOrStructEntry b vsig1) genv

in return (genv1, dg1)

UnitEntry _usig -> anaErr "unit spec download"

AlignEntry _asig -> anaErr "alignment download"

ArchOrRefEntry b _rsig -> anaErr $ (if b then "arch" else "ref")

++ " spec download"

refNodesig :: LibEnv -> LibName -> DGraph -> DGraph -> (NodeName, NodeSig)

-> (DGraph, NodeSig)

refNodesig libenv refln refDG dg

(name, NodeSig refn sigma@(G_sign lid sig ind)) =

let (ln, _, (n, lbl)) =

lookupRefNode libenv refln refDG refn

refInfo = newRefInfo ln n

new = newInfoNodeLab name refInfo

$ noSensGTheory lid sig ind

nodeCont = new { globalTheory = globalTheory lbl }

node = getNewNodeDG dg

in case lookupInAllRefNodesDG refInfo dg of

Just existNode -> (dg, NodeSig existNode sigma)

Nothing ->

( insNodeDG (node, nodeCont) dg

, NodeSig node sigma)

refNodesigs :: LibEnv -> LibName -> DGraph -> DGraph -> [(NodeName, NodeSig)]

-> (DGraph, [NodeSig])

refNodesigs libenv ln = mapAccumR . refNodesig libenv ln

refExtsigAndInsert :: LibEnv -> LibName -> DGraph -> (GlobalEnv, DGraph)

-> IRI -> ExtGenSig -> (ExtGenSig, (GlobalEnv, DGraph))

refExtsigAndInsert libenv ln refDG (genv, dg) new extsig =

let (dg1, extsig1) = refExtsig libenv ln refDG dg (makeName new) extsig

genv1 = Map.insert new (SpecEntry extsig1) genv

in (extsig1, (genv1, dg1))

refExtsig :: LibEnv -> LibName -> DGraph -> DGraph -> NodeName -> ExtGenSig

-> (DGraph, ExtGenSig)

refExtsig libenv ln refDG dg name

(ExtGenSig (GenSig imps params gsigmaP) body) = let

pName = extName "Parameters" name

(dg1, imps1) = case imps of

EmptyNode _ -> (dg, imps)

JustNode ns -> let

(dg0, nns) = refNodesig libenv ln refDG dg (extName "Imports" name, ns)

in (dg0, JustNode nns)

(dg2, params1) = refNodesigs libenv ln refDG dg1

$ snd $ foldr (\ p (n, l) -> let nn = inc n in

(nn, (nn, p) : l)) (pName, []) params

(dg3, gsigmaP1) = case gsigmaP of

EmptyNode _ -> (dg, gsigmaP)

JustNode ns -> let

(dg0, nns) = refNodesig libenv ln refDG dg2 (pName, ns)

in (dg0, JustNode nns)

(dg4, body1) = refNodesig libenv ln refDG dg3 (name, body)

in (dg4, ExtGenSig (GenSig imps1 params1 gsigmaP1) body1)

refViewsig :: LibEnv -> LibName -> DGraph -> DGraph -> NodeName -> ExtViewSig

-> (DGraph, ExtViewSig)

refViewsig libenv ln refDG dg name (ExtViewSig src mor extsig) = let

(dg1, src1) = refNodesig libenv ln refDG dg (extName "Source" name, src)

(dg2, extsig1) = refExtsig libenv ln refDG dg1 (extName "Target" name) extsig

in (dg2, ExtViewSig src1 mor extsig1)

-- BEGIN CURIE expansion

expandCurieItemNameMap :: FilePath -> FilePath -> ItemNameMap

-> Either (Result ()) ItemNameMap

expandCurieItemNameMap fn newFn (ItemNameMap i1 mi2) =

case expandCurieByPath fn i1 of

Just i -> case mi2 of

Nothing -> Right $ ItemNameMap i mi2

Just j -> case expandCurieByPath newFn j of

Nothing -> Left $ prefixErrorIRI j

mj -> Right $ ItemNameMap i mj

Nothing -> Left $ prefixErrorIRI i1

itemNameMapsToIRIs :: [ItemNameMap] -> [IRI]

itemNameMapsToIRIs = concatMap (\ (ItemNameMap i mi) -> [i | isNothing mi])

-- END CURIE expansion