{- |
Module      :  ./Static/AnalysisLibrary.hs
Description :  static analysis of DOL documents and CASL specification libraries
Copyright   :  (c) Till Mossakowski, Uni Magdeburg 2002-2016
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable(Logic)

Static analysis of DOL documents and CASL specification libraries
   Follows the verification semantics sketched in Chap. IV:6
   of the CASL Reference Manual.
   Follows the semantics of DOL documents, DOL OMG standard, clause 10.2.1
-}

module Static.AnalysisLibrary
    ( anaLibFileOrGetEnv
    , anaLibDefn
    , anaSourceFile
    , anaLibItem
    , anaViewDefn
    , LNS
    ) where

import Logic.Logic
import Logic.Grothendieck
import Logic.Coerce
import Logic.Prover

import Syntax.AS_Structured
import Syntax.Print_AS_Structured
import Syntax.Print_AS_Library ()
import Syntax.AS_Library

import Static.GTheory
import Static.DevGraph
import Static.DgUtils
import Static.ComputeTheory
import Static.AnalysisStructured
import Static.AnalysisArchitecture
import Static.ArchDiagram (emptyExtStUnitCtx)

import Common.AS_Annotation hiding (isAxiom, isDef)
import Common.Consistency
import Common.GlobalAnnotations
import Common.ConvertGlobalAnnos
import Common.AnalyseAnnos
import Common.ExtSign
import Common.Result
import Common.ResultT
import Common.LibName
import Common.Id
import Common.IRI
import Common.DocUtils
import qualified Common.Unlit as Unlit
import Common.Utils
import qualified Control.Monad.Fail as Fail

import Driver.Options
import Driver.ReadFn
import Driver.ReadLibDefn
import Driver.WriteLibDefn

import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Either (lefts, rights)
import Data.List
import Data.Maybe

import Control.Monad
import Control.Monad.Trans

import System.Directory
import System.FilePath

import LF.Twelf2DG
import Framework.Analysis

import MMT.Hets2mmt (mmtRes)
import Proofs.ComputeColimit

-- a set of library names to check for cyclic imports
type LNS = Set.Set LibName

{- | parsing and static analysis for files
Parameters: logic graph, default logic, file name -}
anaSourceFile :: LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph
  -> FilePath -> ResultT IO (LibName, LibEnv)
anaSourceFile :: LogicGraph
-> HetcatsOpts
-> LNS
-> LibEnv
-> DGraph
-> FilePath
-> ResultT IO (LibName, LibEnv)
anaSourceFile = Maybe LibName
-> LogicGraph
-> HetcatsOpts
-> LNS
-> LibEnv
-> DGraph
-> FilePath
-> ResultT IO (LibName, LibEnv)
anaSource Maybe LibName
forall a. Maybe a
Nothing

anaSource :: Maybe LibName -- ^ suggested library name
  -> LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph
  -> FilePath -> ResultT IO (LibName, LibEnv)
anaSource :: Maybe LibName
-> LogicGraph
-> HetcatsOpts
-> LNS
-> LibEnv
-> DGraph
-> FilePath
-> ResultT IO (LibName, LibEnv)
anaSource mln :: Maybe LibName
mln lg :: LogicGraph
lg opts :: HetcatsOpts
opts topLns :: LNS
topLns libenv :: LibEnv
libenv initDG :: DGraph
initDG origName :: FilePath
origName = IO (Result (LibName, LibEnv)) -> ResultT IO (LibName, LibEnv)
forall (m :: * -> *) a. m (Result a) -> ResultT m a
ResultT (IO (Result (LibName, LibEnv)) -> ResultT IO (LibName, LibEnv))
-> IO (Result (LibName, LibEnv)) -> ResultT IO (LibName, LibEnv)
forall a b. (a -> b) -> a -> b
$ do
  let mName :: FilePath
mName = HetcatsOpts -> FilePath -> FilePath
useCatalogURL HetcatsOpts
opts FilePath
origName
      fname :: FilePath
fname = FilePath -> FilePath -> FilePath
tryToStripPrefix "file://" FilePath
mName
      syn :: Maybe IRI
syn = case HetcatsOpts -> FilePath
defSyntax HetcatsOpts
opts of
        "" -> Maybe IRI
forall a. Maybe a
Nothing
        s :: FilePath
s -> IRI -> Maybe IRI
forall a. a -> Maybe a
Just (IRI -> Maybe IRI) -> IRI -> Maybe IRI
forall a b. (a -> b) -> a -> b
$ SIMPLE_ID -> IRI
simpleIdToIRI (SIMPLE_ID -> IRI) -> SIMPLE_ID -> IRI
forall a b. (a -> b) -> a -> b
$ FilePath -> SIMPLE_ID
mkSimpleId FilePath
s
      lgraph :: LogicGraph
lgraph = Maybe IRI -> LogicGraph -> LogicGraph
setSyntax Maybe IRI
syn (LogicGraph -> LogicGraph) -> LogicGraph -> LogicGraph
forall a b. (a -> b) -> a -> b
$ FilePath -> LogicGraph -> LogicGraph
setCurLogic (HetcatsOpts -> FilePath
defLogic HetcatsOpts
opts) LogicGraph
lg
  Either
  FilePath (Maybe FilePath, Maybe FilePath, FileInfo, FilePath)
fname' <- HetcatsOpts
-> FilePath
-> IO
     (Either
        FilePath (Maybe FilePath, Maybe FilePath, FileInfo, FilePath))
getContentAndFileType HetcatsOpts
opts FilePath
fname
  FilePath
dir <- IO FilePath
getCurrentDirectory
  case Either
  FilePath (Maybe FilePath, Maybe FilePath, FileInfo, FilePath)
fname' of
    Left err :: FilePath
err -> Result (LibName, LibEnv) -> IO (Result (LibName, LibEnv))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (LibName, LibEnv) -> IO (Result (LibName, LibEnv)))
-> Result (LibName, LibEnv) -> IO (Result (LibName, LibEnv))
forall a b. (a -> b) -> a -> b
$ FilePath -> Result (LibName, LibEnv)
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
Fail.fail FilePath
err
    Right (mr :: Maybe FilePath
mr, _, file :: FileInfo
file, inputLit :: FilePath
inputLit) ->
        if (FilePath -> Bool) -> [FilePath] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isSuffixOf` (FileInfo -> FilePath
filePath FileInfo
file)) [FilePath
envSuffix, FilePath
prfSuffix] then
          Result (LibName, LibEnv) -> IO (Result (LibName, LibEnv))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (LibName, LibEnv) -> IO (Result (LibName, LibEnv)))
-> (FilePath -> Result (LibName, LibEnv))
-> FilePath
-> IO (Result (LibName, LibEnv))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Result (LibName, LibEnv)
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
Fail.fail (FilePath -> IO (Result (LibName, LibEnv)))
-> FilePath -> IO (Result (LibName, LibEnv))
forall a b. (a -> b) -> a -> b
$ "no matching source file for '" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
fname FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "' found."
        else let
        input :: FilePath
input = (if HetcatsOpts -> Bool
unlit HetcatsOpts
opts then FilePath -> FilePath
Unlit.unlit else FilePath -> FilePath
forall a. a -> a
id) FilePath
inputLit
        libStr :: FilePath
libStr = if FilePath -> Bool
isAbsolute FilePath
fname
              then FilePath -> FilePath
convertFileToLibStr FilePath
fname
              else FilePath -> FilePath
dropExtensions FilePath
fname
        nLn :: Maybe LibName
nLn = case Maybe LibName
mln of
              Nothing | HetcatsOpts -> Bool
useLibPos HetcatsOpts
opts Bool -> Bool -> Bool
&& Bool -> Bool
not (FilePath -> Bool
checkUri FilePath
fname) ->
                LibName -> Maybe LibName
forall a. a -> Maybe a
Just (LibName -> Maybe LibName) -> LibName -> Maybe LibName
forall a b. (a -> b) -> a -> b
$ FilePath -> LibName
emptyLibName FilePath
libStr
              _ -> Maybe LibName
mln
        fn2 :: FilePath
fn2 = HetcatsOpts -> FilePath -> FilePath -> FilePath
keepOrigClifName HetcatsOpts
opts FilePath
origName (FileInfo -> FilePath
filePath FileInfo
file)
        fnAbs :: FilePath
fnAbs = if FilePath -> Bool
isAbsolute FilePath
fn2 then FilePath
fn2 else FilePath
dir FilePath -> FilePath -> FilePath
</> FilePath
fn2
        url :: FilePath
url = if FilePath -> Bool
checkUri FilePath
fn2 then FilePath
fn2 else "file://" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
fnAbs
        in
        if HetcatsOpts -> Bool
runMMT HetcatsOpts
opts then FilePath -> IO (Result (LibName, LibEnv))
mmtRes FilePath
fname else
            if FilePath -> FilePath
takeExtension (FileInfo -> FilePath
filePath FileInfo
file) FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
/= ('.' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: InType -> FilePath
forall a. Show a => a -> FilePath
show InType
TwelfIn)
            then ResultT IO (LibName, LibEnv) -> IO (Result (LibName, LibEnv))
forall (m :: * -> *) a. ResultT m a -> m (Result a)
runResultT (ResultT IO (LibName, LibEnv) -> IO (Result (LibName, LibEnv)))
-> ResultT IO (LibName, LibEnv) -> IO (Result (LibName, LibEnv))
forall a b. (a -> b) -> a -> b
$
                 Maybe LibName
-> LogicGraph
-> HetcatsOpts
-> LNS
-> LibEnv
-> DGraph
-> FilePath
-> FilePath
-> Maybe FilePath
-> ResultT IO (LibName, LibEnv)
anaString Maybe LibName
nLn LogicGraph
lgraph HetcatsOpts
opts LNS
topLns LibEnv
libenv DGraph
initDG FilePath
input FilePath
url Maybe FilePath
mr
            else do
              Maybe (LibName, LibEnv)
res <- HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
anaTwelfFile HetcatsOpts
opts (FileInfo -> FilePath
filePath FileInfo
file)
              Result (LibName, LibEnv) -> IO (Result (LibName, LibEnv))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (LibName, LibEnv) -> IO (Result (LibName, LibEnv)))
-> Result (LibName, LibEnv) -> IO (Result (LibName, LibEnv))
forall a b. (a -> b) -> a -> b
$ case Maybe (LibName, LibEnv)
res of
                Nothing -> FilePath -> Result (LibName, LibEnv)
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
Fail.fail (FilePath -> Result (LibName, LibEnv))
-> FilePath -> Result (LibName, LibEnv)
forall a b. (a -> b) -> a -> b
$ "failed to analyse file: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (FileInfo -> FilePath
filePath FileInfo
file)
                Just (lname :: LibName
lname, lenv :: LibEnv
lenv) -> (LibName, LibEnv) -> Result (LibName, LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (LibName
lname, LibEnv -> LibEnv -> LibEnv
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union LibEnv
lenv LibEnv
libenv)

-- | parsing of input string (content of file)
anaString :: Maybe LibName -- ^ suggested library name
  -> LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph -> String
  -> FilePath -> Maybe String -- ^ mime-type of file
  -> ResultT IO (LibName, LibEnv)
anaString :: Maybe LibName
-> LogicGraph
-> HetcatsOpts
-> LNS
-> LibEnv
-> DGraph
-> FilePath
-> FilePath
-> Maybe FilePath
-> ResultT IO (LibName, LibEnv)
anaString mln :: Maybe LibName
mln lgraph :: LogicGraph
lgraph opts :: HetcatsOpts
opts topLns :: LNS
topLns libenv :: LibEnv
libenv initDG :: DGraph
initDG input :: FilePath
input file :: FilePath
file mr :: Maybe FilePath
mr = do
  FilePath
curDir <- IO FilePath -> ResultT IO FilePath
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift IO FilePath
getCurrentDirectory -- get full path for parser positions
  let realFileName :: FilePath
realFileName = FilePath
curDir FilePath -> FilePath -> FilePath
</> FilePath
file
      posFileName :: FilePath
posFileName = case Maybe LibName
mln of
          Just gLn :: LibName
gLn | HetcatsOpts -> Bool
useLibPos HetcatsOpts
opts -> LibName -> FilePath
libToFileName LibName
gLn
          _ -> if FilePath -> Bool
checkUri FilePath
file then FilePath
file else FilePath
realFileName
  IO () -> ResultT IO ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> ResultT IO ()) -> IO () -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 2 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "Reading file " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
file
  [LIB_DEFN]
libdefns <- LogicGraph
-> HetcatsOpts
-> Maybe FilePath
-> FilePath
-> FilePath
-> FilePath
-> ResultT IO [LIB_DEFN]
readLibDefn LogicGraph
lgraph HetcatsOpts
opts Maybe FilePath
mr FilePath
file FilePath
posFileName FilePath
input
  Bool -> ResultT IO () -> ResultT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([LIB_DEFN] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [LIB_DEFN]
libdefns) (ResultT IO () -> ResultT IO ())
-> (FilePath -> ResultT IO ()) -> FilePath -> ResultT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> ResultT IO ()
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
Fail.fail (FilePath -> ResultT IO ()) -> FilePath -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ "failed to read contents of file: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
file
  ((LibName, LibEnv) -> LIB_DEFN -> ResultT IO (LibName, LibEnv))
-> (LibName, LibEnv) -> [LIB_DEFN] -> ResultT IO (LibName, LibEnv)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Maybe LibName
-> LogicGraph
-> HetcatsOpts
-> LNS
-> DGraph
-> Maybe FilePath
-> FilePath
-> FilePath
-> (LibName, LibEnv)
-> LIB_DEFN
-> ResultT IO (LibName, LibEnv)
anaStringAux Maybe LibName
mln LogicGraph
lgraph HetcatsOpts
opts LNS
topLns DGraph
initDG Maybe FilePath
mr FilePath
file FilePath
posFileName)
        (FilePath -> LibName
forall a. HasCallStack => FilePath -> a
error "Static.AnalysisLibrary.anaString", LibEnv
libenv)
    ([LIB_DEFN] -> ResultT IO (LibName, LibEnv))
-> [LIB_DEFN] -> ResultT IO (LibName, LibEnv)
forall a b. (a -> b) -> a -> b
$ case HetcatsOpts -> AnaType
analysis HetcatsOpts
opts of
      Skip -> [[LIB_DEFN] -> LIB_DEFN
forall a. [a] -> a
last [LIB_DEFN]
libdefns]
      _ -> [LIB_DEFN]
libdefns

-- | calling static analysis for parsed library-defn
anaStringAux :: Maybe LibName -- ^ suggested library name
  -> LogicGraph -> HetcatsOpts -> LNS -> DGraph -> Maybe String -> FilePath
  -> FilePath -> (LibName, LibEnv) -> LIB_DEFN -> ResultT IO (LibName, LibEnv)
anaStringAux :: Maybe LibName
-> LogicGraph
-> HetcatsOpts
-> LNS
-> DGraph
-> Maybe FilePath
-> FilePath
-> FilePath
-> (LibName, LibEnv)
-> LIB_DEFN
-> ResultT IO (LibName, LibEnv)
anaStringAux mln :: Maybe LibName
mln lgraph :: LogicGraph
lgraph opts :: HetcatsOpts
opts topLns :: LNS
topLns initDG :: DGraph
initDG mt :: Maybe FilePath
mt file :: FilePath
file posFileName :: FilePath
posFileName (_, libenv :: LibEnv
libenv)
             (Lib_defn pln :: LibName
pln is' :: [Annoted LIB_ITEM]
is' ps :: Range
ps ans :: [Annotation]
ans) = do
  let pm :: Map FilePath IRI
pm = Map FilePath IRI -> Map FilePath IRI -> Map FilePath IRI
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union ((Map FilePath IRI, [Annotation]) -> Map FilePath IRI
forall a b. (a, b) -> a
fst ((Map FilePath IRI, [Annotation]) -> Map FilePath IRI)
-> (Map FilePath IRI, [Annotation]) -> Map FilePath IRI
forall a b. (a -> b) -> a -> b
$ [Annotation] -> (Map FilePath IRI, [Annotation])
partPrefixes [Annotation]
ans) (LogicGraph -> Map FilePath IRI
prefixes LogicGraph
lgraph)
      expnd :: IRI -> IRI
expnd i :: IRI
i = IRI -> Maybe IRI -> IRI
forall a. a -> Maybe a -> a
fromMaybe IRI
i (Maybe IRI -> IRI) -> Maybe IRI -> IRI
forall a b. (a -> b) -> a -> b
$ Map FilePath IRI -> IRI -> Maybe IRI
expandCurie Map FilePath IRI
pm IRI
i
      spNs :: Set IRI
spNs = [Set IRI] -> Set IRI
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set IRI] -> Set IRI)
-> ([SPEC] -> [Set IRI]) -> [SPEC] -> Set IRI
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SPEC -> Set IRI) -> [SPEC] -> [Set IRI]
forall a b. (a -> b) -> [a] -> [b]
map ((IRI -> IRI) -> Set IRI -> Set IRI
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map IRI -> IRI
expnd (Set IRI -> Set IRI) -> (SPEC -> Set IRI) -> SPEC -> Set IRI
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SPEC -> Set IRI
getSpecNames)
        ([SPEC] -> Set IRI) -> [SPEC] -> Set IRI
forall a b. (a -> b) -> a -> b
$ (Annoted LIB_ITEM -> [SPEC]) -> [Annoted LIB_ITEM] -> [SPEC]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (LIB_ITEM -> [SPEC]
getSpecDef (LIB_ITEM -> [SPEC])
-> (Annoted LIB_ITEM -> LIB_ITEM) -> Annoted LIB_ITEM -> [SPEC]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted LIB_ITEM -> LIB_ITEM
forall a. Annoted a -> a
item) [Annoted LIB_ITEM]
is'
      declNs :: Set IRI
declNs = [IRI] -> Set IRI
forall a. Ord a => [a] -> Set a
Set.fromList ([IRI] -> Set IRI) -> ([IRI] -> [IRI]) -> [IRI] -> Set IRI
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IRI -> IRI) -> [IRI] -> [IRI]
forall a b. (a -> b) -> [a] -> [b]
map IRI -> IRI
expnd
        ([IRI] -> Set IRI) -> [IRI] -> Set IRI
forall a b. (a -> b) -> a -> b
$ (Annoted LIB_ITEM -> [IRI]) -> [Annoted LIB_ITEM] -> [IRI]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (LIB_ITEM -> [IRI]
getDeclSpecNames (LIB_ITEM -> [IRI])
-> (Annoted LIB_ITEM -> LIB_ITEM) -> Annoted LIB_ITEM -> [IRI]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted LIB_ITEM -> LIB_ITEM
forall a. Annoted a -> a
item) [Annoted LIB_ITEM]
is'
      missNames :: [IRI]
missNames = Set IRI -> [IRI]
forall a. Set a -> [a]
Set.toList (Set IRI -> [IRI]) -> Set IRI -> [IRI]
forall a b. (a -> b) -> a -> b
$ Set IRI
spNs Set IRI -> Set IRI -> Set IRI
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set IRI
declNs
      unDecls :: [Annoted LIB_ITEM]
unDecls = (IRI -> Annoted LIB_ITEM) -> [IRI] -> [Annoted LIB_ITEM]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> IRI -> Annoted LIB_ITEM
addDownload Bool
True) ([IRI] -> [Annoted LIB_ITEM]) -> [IRI] -> [Annoted LIB_ITEM]
forall a b. (a -> b) -> a -> b
$ (IRI -> Bool) -> [IRI] -> [IRI]
forall a. (a -> Bool) -> [a] -> [a]
filter
          (Maybe GlobalEntry -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe GlobalEntry -> Bool)
-> (IRI -> Maybe GlobalEntry) -> IRI -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IRI -> DGraph -> Maybe GlobalEntry
`lookupGlobalEnvDG` DGraph
initDG)) [IRI]
missNames
      is :: [Annoted LIB_ITEM]
is = [Annoted LIB_ITEM]
unDecls [Annoted LIB_ITEM] -> [Annoted LIB_ITEM] -> [Annoted LIB_ITEM]
forall a. [a] -> [a] -> [a]
++ [Annoted LIB_ITEM]
is'
      spN :: FilePath
spN = FilePath -> FilePath
convertFileToLibStr FilePath
file
      noLibName :: Bool
noLibName = LibName -> IRI
getLibId LibName
pln IRI -> IRI -> Bool
forall a. Eq a => a -> a -> Bool
== IRI
nullIRI
      nIs :: [Annoted LIB_ITEM]
nIs = case [Annoted LIB_ITEM]
is of
        [Annoted (Spec_defn spn :: IRI
spn gn :: GENERICITY
gn as :: Annoted SPEC
as qs :: Range
qs) rs :: Range
rs [] []]
            | Bool
noLibName Bool -> Bool -> Bool
&& FilePath -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (IRI -> FilePath
iriToStringUnsecure IRI
spn)
                -> [LIB_ITEM
-> Range -> [Annotation] -> [Annotation] -> Annoted LIB_ITEM
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
Annoted (IRI -> GENERICITY -> Annoted SPEC -> Range -> LIB_ITEM
Spec_defn (SIMPLE_ID -> IRI
simpleIdToIRI (SIMPLE_ID -> IRI) -> SIMPLE_ID -> IRI
forall a b. (a -> b) -> a -> b
$ FilePath -> SIMPLE_ID
mkSimpleId FilePath
spN)
                             GENERICITY
gn Annoted SPEC
as Range
qs) Range
rs [] []]
        _ -> [Annoted LIB_ITEM]
is
      emptyFilePath :: Bool
emptyFilePath = FilePath -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (FilePath -> Bool) -> FilePath -> Bool
forall a b. (a -> b) -> a -> b
$ LibName -> FilePath
getFilePath LibName
pln
      ln :: LibName
ln = Maybe FilePath -> LibName -> LibName
setMimeType Maybe FilePath
mt (LibName -> LibName) -> LibName -> LibName
forall a b. (a -> b) -> a -> b
$ if Bool
emptyFilePath then FilePath -> LibName -> LibName
setFilePath FilePath
posFileName
            (LibName -> LibName) -> LibName -> LibName
forall a b. (a -> b) -> a -> b
$ if Bool
noLibName then LibName -> Maybe LibName -> LibName
forall a. a -> Maybe a -> a
fromMaybe (FilePath -> LibName
emptyLibName FilePath
spN) Maybe LibName
mln else LibName
pln
           else LibName
pln
      ast :: LIB_DEFN
ast = LibName -> [Annoted LIB_ITEM] -> Range -> [Annotation] -> LIB_DEFN
Lib_defn LibName
ln [Annoted LIB_ITEM]
nIs Range
ps [Annotation]
ans
  case HetcatsOpts -> AnaType
analysis HetcatsOpts
opts of
      Skip -> do
          IO () -> ResultT IO ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> ResultT IO ()) -> IO () -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 1 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$
                  "Skipping static analysis of library " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ LibName -> FilePath
forall a. Show a => a -> FilePath
show LibName
ln
          GlobalAnnos
ga <- Result GlobalAnnos -> ResultT IO GlobalAnnos
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result GlobalAnnos -> ResultT IO GlobalAnnos)
-> Result GlobalAnnos -> ResultT IO GlobalAnnos
forall a b. (a -> b) -> a -> b
$ GlobalAnnos -> [Annotation] -> Result GlobalAnnos
addGlobalAnnos GlobalAnnos
emptyGlobalAnnos [Annotation]
ans
          IO () -> ResultT IO ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> ResultT IO ()) -> IO () -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ LogicGraph
-> GlobalAnnos -> FilePath -> HetcatsOpts -> LIB_DEFN -> IO ()
writeLibDefn LogicGraph
lgraph GlobalAnnos
ga FilePath
file HetcatsOpts
opts LIB_DEFN
ast
          Result (LibName, LibEnv) -> ResultT IO (LibName, LibEnv)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR Result (LibName, LibEnv)
forall (m :: * -> *) a. MonadPlus m => m a
mzero
      _ -> do
          let libstring :: FilePath
libstring = LibName -> FilePath
libToString LibName
ln
          Bool -> ResultT IO () -> ResultT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isSuffixOf FilePath
libstring (FilePath -> FilePath
dropExtension FilePath
file)
              Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
emptyFilePath) (ResultT IO () -> ResultT IO ())
-> (FilePath -> ResultT IO ()) -> FilePath -> ResultT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO () -> ResultT IO ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> ResultT IO ())
-> (FilePath -> IO ()) -> FilePath -> ResultT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 1
              (FilePath -> ResultT IO ()) -> FilePath -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ "### file name '" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
file FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "' does not match library name '"
              FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
libstring FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "'"
          IO () -> ResultT IO ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> ResultT IO ()) -> IO () -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 1 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "Analyzing "
              FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (if Bool
noLibName then "file " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
file FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " as " else "")
              FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "library " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ LibName -> FilePath
forall a. Show a => a -> FilePath
show LibName
ln
          (lnFinal :: LibName
lnFinal, ld :: LIB_DEFN
ld, ga :: GlobalAnnos
ga, lenv :: LibEnv
lenv) <-
              LogicGraph
-> HetcatsOpts
-> LNS
-> LibEnv
-> DGraph
-> LIB_DEFN
-> FilePath
-> ResultT IO (LibName, LIB_DEFN, GlobalAnnos, LibEnv)
anaLibDefn LogicGraph
lgraph HetcatsOpts
opts LNS
topLns LibEnv
libenv DGraph
initDG LIB_DEFN
ast FilePath
file
          case LibName -> LibEnv -> Maybe DGraph
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup LibName
lnFinal LibEnv
lenv of
              Nothing -> FilePath -> ResultT IO (LibName, LibEnv)
forall a. HasCallStack => FilePath -> a
error (FilePath -> ResultT IO (LibName, LibEnv))
-> FilePath -> ResultT IO (LibName, LibEnv)
forall a b. (a -> b) -> a -> b
$ "anaString: missing library: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ LibName -> FilePath
forall a. Show a => a -> FilePath
show LibName
lnFinal
              Just dg :: DGraph
dg -> IO (LibName, LibEnv) -> ResultT IO (LibName, LibEnv)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (LibName, LibEnv) -> ResultT IO (LibName, LibEnv))
-> IO (LibName, LibEnv) -> ResultT IO (LibName, LibEnv)
forall a b. (a -> b) -> a -> b
$ do
                  LogicGraph
-> GlobalAnnos -> FilePath -> HetcatsOpts -> LIB_DEFN -> IO ()
writeLibDefn LogicGraph
lgraph GlobalAnnos
ga FilePath
file HetcatsOpts
opts LIB_DEFN
ld
                  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (HetcatsOpts -> Bool
hasEnvOut HetcatsOpts
opts)
                        (HetcatsOpts -> LibName -> FilePath -> LIB_DEFN -> DGraph -> IO ()
forall a.
ShATermLG a =>
HetcatsOpts -> LibName -> FilePath -> LIB_DEFN -> a -> IO ()
writeFileInfo HetcatsOpts
opts LibName
lnFinal FilePath
file LIB_DEFN
ld DGraph
dg)
                  (LibName, LibEnv) -> IO (LibName, LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (LibName
lnFinal, LibEnv
lenv)

-- lookup or read a library
anaLibFile :: LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph -> LibName
           -> ResultT IO (LibName, LibEnv)
anaLibFile :: LogicGraph
-> HetcatsOpts
-> LNS
-> LibEnv
-> DGraph
-> LibName
-> ResultT IO (LibName, LibEnv)
anaLibFile lgraph :: LogicGraph
lgraph opts :: HetcatsOpts
opts topLns :: LNS
topLns libenv :: LibEnv
libenv initDG :: DGraph
initDG ln :: LibName
ln =
    let lnstr :: FilePath
lnstr = LibName -> FilePath
forall a. Show a => a -> FilePath
show LibName
ln in case (LibName -> Bool) -> [LibName] -> Maybe LibName
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (LibName -> LibName -> Bool
forall a. Eq a => a -> a -> Bool
== LibName
ln) ([LibName] -> Maybe LibName) -> [LibName] -> Maybe LibName
forall a b. (a -> b) -> a -> b
$ LibEnv -> [LibName]
forall k a. Map k a -> [k]
Map.keys LibEnv
libenv of
    Just ln' :: LibName
ln' -> do
        HetcatsOpts -> FilePath -> ResultT IO ()
analyzing HetcatsOpts
opts (FilePath -> ResultT IO ()) -> FilePath -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ "from " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
lnstr
        (LibName, LibEnv) -> ResultT IO (LibName, LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (LibName
ln', LibEnv
libenv)
    Nothing ->
            do
            HetcatsOpts -> Int -> FilePath -> ResultT IO ()
putMessageIORes HetcatsOpts
opts 1 (FilePath -> ResultT IO ()) -> FilePath -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ "Downloading " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
lnstr FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " ..."
            (LibName, LibEnv)
res <- LogicGraph
-> HetcatsOpts
-> LNS
-> LibEnv
-> DGraph
-> Maybe LibName
-> FilePath
-> ResultT IO (LibName, LibEnv)
anaLibFileOrGetEnv LogicGraph
lgraph
              (if HetcatsOpts -> Bool
recurse HetcatsOpts
opts then HetcatsOpts
opts else HetcatsOpts
opts
                      { outtypes :: [OutType]
outtypes = []
                      , unlit :: Bool
unlit = Bool
False })
              (LibName -> LNS -> LNS
forall a. Ord a => a -> Set a -> Set a
Set.insert LibName
ln LNS
topLns) LibEnv
libenv DGraph
initDG (LibName -> Maybe LibName
forall a. a -> Maybe a
Just LibName
ln) (FilePath -> ResultT IO (LibName, LibEnv))
-> FilePath -> ResultT IO (LibName, LibEnv)
forall a b. (a -> b) -> a -> b
$ LibName -> FilePath
libNameToFile LibName
ln
            HetcatsOpts -> Int -> FilePath -> ResultT IO ()
putMessageIORes HetcatsOpts
opts 1 (FilePath -> ResultT IO ()) -> FilePath -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ "... loaded " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
lnstr
            (LibName, LibEnv) -> ResultT IO (LibName, LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (LibName, LibEnv)
res

-- | lookup or read a library
anaLibFileOrGetEnv :: LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph
                   -> Maybe LibName -> FilePath -> ResultT IO (LibName, LibEnv)
anaLibFileOrGetEnv :: LogicGraph
-> HetcatsOpts
-> LNS
-> LibEnv
-> DGraph
-> Maybe LibName
-> FilePath
-> ResultT IO (LibName, LibEnv)
anaLibFileOrGetEnv lgraph :: LogicGraph
lgraph opts :: HetcatsOpts
opts topLns :: LNS
topLns libenv :: LibEnv
libenv initDG :: DGraph
initDG mln :: Maybe LibName
mln file :: FilePath
file = do
     let envFile :: FilePath
envFile = FilePath -> FilePath
rmSuffix FilePath
file FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
envSuffix
     Bool
recent_envFile <- IO Bool -> ResultT IO Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO Bool -> ResultT IO Bool) -> IO Bool -> ResultT IO Bool
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> FilePath -> FilePath -> IO Bool
checkRecentEnv HetcatsOpts
opts FilePath
envFile FilePath
file
     if Bool
recent_envFile
        then do
             Maybe (LIB_DEFN, DGraph)
mgc <- IO (Maybe (LIB_DEFN, DGraph))
-> ResultT IO (Maybe (LIB_DEFN, DGraph))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (Maybe (LIB_DEFN, DGraph))
 -> ResultT IO (Maybe (LIB_DEFN, DGraph)))
-> IO (Maybe (LIB_DEFN, DGraph))
-> ResultT IO (Maybe (LIB_DEFN, DGraph))
forall a b. (a -> b) -> a -> b
$ LogicGraph
-> HetcatsOpts
-> Maybe LibName
-> FilePath
-> IO (Maybe (LIB_DEFN, DGraph))
forall a.
ShATermLG a =>
LogicGraph
-> HetcatsOpts -> Maybe LibName -> FilePath -> IO (Maybe a)
readVerbose LogicGraph
lgraph HetcatsOpts
opts Maybe LibName
mln FilePath
envFile
             case Maybe (LIB_DEFN, DGraph)
mgc of
                 Nothing -> do
                     IO () -> ResultT IO ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> ResultT IO ()) -> IO () -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 1 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "Deleting " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
envFile
                     IO () -> ResultT IO ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> ResultT IO ()) -> IO () -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> IO ()
removeFile FilePath
envFile
                     Maybe LibName
-> LogicGraph
-> HetcatsOpts
-> LNS
-> LibEnv
-> DGraph
-> FilePath
-> ResultT IO (LibName, LibEnv)
anaSource Maybe LibName
mln LogicGraph
lgraph HetcatsOpts
opts LNS
topLns LibEnv
libenv DGraph
initDG FilePath
file
                 Just (ld :: LIB_DEFN
ld@(Lib_defn ln :: LibName
ln _ _ _), gc :: DGraph
gc) -> do
                     IO () -> ResultT IO ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> ResultT IO ()) -> IO () -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ LogicGraph
-> GlobalAnnos -> FilePath -> HetcatsOpts -> LIB_DEFN -> IO ()
writeLibDefn LogicGraph
lgraph (DGraph -> GlobalAnnos
globalAnnos DGraph
gc) FilePath
file HetcatsOpts
opts LIB_DEFN
ld
                          -- get all DGRefs from DGraph
                     LibEnv
mEnv <- (ResultT IO LibEnv -> LNode DGNodeLab -> ResultT IO LibEnv)
-> ResultT IO LibEnv -> [LNode DGNodeLab] -> ResultT IO LibEnv
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl
                         ( \ ioLibEnv :: ResultT IO LibEnv
ioLibEnv labOfDG :: LNode DGNodeLab
labOfDG -> let node :: DGNodeLab
node = LNode DGNodeLab -> DGNodeLab
forall a b. (a, b) -> b
snd LNode DGNodeLab
labOfDG in
                               if DGNodeLab -> Bool
isDGRef DGNodeLab
node then do
                                 let ln2 :: LibName
ln2 = DGNodeLab -> LibName
dgn_libname DGNodeLab
node
                                 LibEnv
p_libEnv <- ResultT IO LibEnv
ioLibEnv
                                 if LibName -> LibEnv -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member LibName
ln2 LibEnv
p_libEnv then
                                    LibEnv -> ResultT IO LibEnv
forall (m :: * -> *) a. Monad m => a -> m a
return LibEnv
p_libEnv
                                    else ((LibName, LibEnv) -> LibEnv)
-> ResultT IO (LibName, LibEnv) -> ResultT IO LibEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (LibName, LibEnv) -> LibEnv
forall a b. (a, b) -> b
snd (ResultT IO (LibName, LibEnv) -> ResultT IO LibEnv)
-> ResultT IO (LibName, LibEnv) -> ResultT IO LibEnv
forall a b. (a -> b) -> a -> b
$ LogicGraph
-> HetcatsOpts
-> LNS
-> LibEnv
-> DGraph
-> LibName
-> ResultT IO (LibName, LibEnv)
anaLibFile LogicGraph
lgraph
                                         HetcatsOpts
opts LNS
topLns LibEnv
p_libEnv DGraph
initDG LibName
ln2
                               else ResultT IO LibEnv
ioLibEnv)
                         (LibEnv -> ResultT IO LibEnv
forall (m :: * -> *) a. Monad m => a -> m a
return (LibEnv -> ResultT IO LibEnv) -> LibEnv -> ResultT IO LibEnv
forall a b. (a -> b) -> a -> b
$ LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln DGraph
gc LibEnv
libenv)
                         ([LNode DGNodeLab] -> ResultT IO LibEnv)
-> [LNode DGNodeLab] -> ResultT IO LibEnv
forall a b. (a -> b) -> a -> b
$ DGraph -> [LNode DGNodeLab]
labNodesDG DGraph
gc
                     (LibName, LibEnv) -> ResultT IO (LibName, LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (LibName
ln, LibEnv
mEnv)
        else Maybe LibName
-> LogicGraph
-> HetcatsOpts
-> LNS
-> LibEnv
-> DGraph
-> FilePath
-> ResultT IO (LibName, LibEnv)
anaSource Maybe LibName
mln LogicGraph
lgraph HetcatsOpts
opts LNS
topLns LibEnv
libenv DGraph
initDG FilePath
file

{- | 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 :: LogicGraph
-> HetcatsOpts
-> LNS
-> LibEnv
-> DGraph
-> LIB_DEFN
-> FilePath
-> ResultT IO (LibName, LIB_DEFN, GlobalAnnos, LibEnv)
anaLibDefn lgraph :: LogicGraph
lgraph opts :: HetcatsOpts
opts topLns :: LNS
topLns libenv :: LibEnv
libenv dg :: DGraph
dg (Lib_defn ln :: LibName
ln alibItems :: [Annoted LIB_ITEM]
alibItems pos :: Range
pos ans :: [Annotation]
ans) file :: FilePath
file = do
  let libStr :: FilePath
libStr = LibName -> FilePath
libToFileName LibName
ln
      isDOLlib :: Bool
isDOLlib = Char -> FilePath -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem ':' FilePath
libStr
  GlobalAnnos
gannos <- HetcatsOpts -> ResultT IO GlobalAnnos -> ResultT IO GlobalAnnos
forall a. HetcatsOpts -> ResultT IO a -> ResultT IO a
showDiags1 HetcatsOpts
opts (ResultT IO GlobalAnnos -> ResultT IO GlobalAnnos)
-> ResultT IO GlobalAnnos -> ResultT IO GlobalAnnos
forall a b. (a -> b) -> a -> b
$ Result GlobalAnnos -> ResultT IO GlobalAnnos
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result GlobalAnnos -> ResultT IO GlobalAnnos)
-> Result GlobalAnnos -> ResultT IO GlobalAnnos
forall a b. (a -> b) -> a -> b
$ GlobalAnnos -> [Annotation] -> Result GlobalAnnos
addGlobalAnnos
    (FilePath -> GlobalAnnos
defPrefixGlobalAnnos (FilePath -> GlobalAnnos) -> FilePath -> GlobalAnnos
forall a b. (a -> b) -> a -> b
$ if Bool
isDOLlib then FilePath
file else FilePath
libStr) [Annotation]
ans
  GlobalAnnos
allAnnos <- Result GlobalAnnos -> ResultT IO GlobalAnnos
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result GlobalAnnos -> ResultT IO GlobalAnnos)
-> Result GlobalAnnos -> ResultT IO GlobalAnnos
forall a b. (a -> b) -> a -> b
$ GlobalAnnos -> GlobalAnnos -> Result GlobalAnnos
mergeGlobalAnnos (DGraph -> GlobalAnnos
globalAnnos DGraph
dg) GlobalAnnos
gannos
  (libItems' :: [LIB_ITEM]
libItems', dg' :: DGraph
dg', libenv' :: LibEnv
libenv', _, _) <- (([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
 -> LIB_ITEM
 -> ResultT
      IO ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides))
-> ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
-> [LIB_ITEM]
-> ResultT
     IO ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (HetcatsOpts
-> LNS
-> LibName
-> ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
-> LIB_ITEM
-> ResultT
     IO ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
anaLibItemAux HetcatsOpts
opts LNS
topLns LibName
ln)
      ([], DGraph
dg { globalAnnos :: GlobalAnnos
globalAnnos = GlobalAnnos
allAnnos }, LibEnv
libenv
      , LogicGraph
lgraph, ExpOverrides
forall k a. Map k a
Map.empty) ((Annoted LIB_ITEM -> LIB_ITEM) -> [Annoted LIB_ITEM] -> [LIB_ITEM]
forall a b. (a -> b) -> [a] -> [b]
map Annoted LIB_ITEM -> LIB_ITEM
forall a. Annoted a -> a
item [Annoted LIB_ITEM]
alibItems)
  let dg1 :: DGraph
dg1 = LibEnv -> LibName -> DGraph -> DGraph
computeDGraphTheories LibEnv
libenv' LibName
ln (DGraph -> DGraph) -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$ LibEnv -> DGraph -> DGraph
markFree LibEnv
libenv'
        (DGraph -> DGraph) -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$ LibEnv -> DGraph -> DGraph
markHiding LibEnv
libenv' (DGraph -> DGraph) -> DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$ DGraph -> Maybe DGraph -> DGraph
forall a. a -> Maybe a -> a
fromMaybe DGraph
dg' (Maybe DGraph -> DGraph) -> Maybe DGraph -> DGraph
forall a b. (a -> b) -> a -> b
$ Result DGraph -> Maybe DGraph
forall a. Result a -> Maybe a
maybeResult
        (Result DGraph -> Maybe DGraph) -> Result DGraph -> Maybe DGraph
forall a b. (a -> b) -> a -> b
$ DGraph -> Result DGraph
shortcutUnions DGraph
dg'
      newLD :: LIB_DEFN
newLD = LibName -> [Annoted LIB_ITEM] -> Range -> [Annotation] -> LIB_DEFN
Lib_defn LibName
ln
        ((LIB_ITEM -> Annoted LIB_ITEM -> Annoted LIB_ITEM)
-> [LIB_ITEM] -> [Annoted LIB_ITEM] -> [Annoted LIB_ITEM]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith LIB_ITEM -> Annoted LIB_ITEM -> Annoted LIB_ITEM
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted ([LIB_ITEM] -> [LIB_ITEM]
forall a. [a] -> [a]
reverse [LIB_ITEM]
libItems') [Annoted LIB_ITEM]
alibItems) Range
pos [Annotation]
ans
      dg2 :: DGraph
dg2 = DGraph
dg1 { optLibDefn :: Maybe LIB_DEFN
optLibDefn = LIB_DEFN -> Maybe LIB_DEFN
forall a. a -> Maybe a
Just LIB_DEFN
newLD }
  (LibName, LIB_DEFN, GlobalAnnos, LibEnv)
-> ResultT IO (LibName, LIB_DEFN, GlobalAnnos, LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (LibName
ln, LIB_DEFN
newLD, DGraph -> GlobalAnnos
globalAnnos DGraph
dg2, LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert LibName
ln DGraph
dg2 LibEnv
libenv')

shortcutUnions :: DGraph -> Result DGraph
shortcutUnions :: DGraph -> Result DGraph
shortcutUnions dgraph :: DGraph
dgraph = let spNs :: Set Int
spNs = GlobalEnv -> Set Int
getGlobNodes (GlobalEnv -> Set Int) -> GlobalEnv -> Set Int
forall a b. (a -> b) -> a -> b
$ DGraph -> GlobalEnv
globalEnv DGraph
dgraph in
  (DGraph -> LNode DGNodeLab -> Result DGraph)
-> DGraph -> [LNode DGNodeLab] -> Result DGraph
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ dg :: DGraph
dg (n :: Int
n, nl :: DGNodeLab
nl) -> let
  locTh :: G_theory
locTh = DGNodeLab -> G_theory
dgn_theory DGNodeLab
nl
  innNs :: [LEdge DGLinkLab]
innNs = DGraph -> Int -> [LEdge DGLinkLab]
innDG DGraph
dg Int
n
  in case DGraph -> Int -> [LEdge DGLinkLab]
outDG DGraph
dg Int
n of
       [(_, t :: Int
t, et :: DGLinkLab
et@DGLink {dgl_type :: DGLinkLab -> DGLinkType
dgl_type = DGLinkType
lt})]
         | Int -> Set Int -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember Int
n Set Int
spNs Bool -> Bool -> Bool
&& [FilePath] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (G_theory -> [FilePath]
getThSens G_theory
locTh) Bool -> Bool -> Bool
&& DGLinkType -> Bool
isGlobalDef DGLinkType
lt
           Bool -> Bool -> Bool
&& Bool -> Bool
not (DGraph -> Int -> Bool
hasOutgoingFreeEdge DGraph
dg Int
t)
           Bool -> Bool -> Bool
&& [LEdge DGLinkLab] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [LEdge DGLinkLab]
innNs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1
           Bool -> Bool -> Bool
&& (LEdge DGLinkLab -> Bool) -> [LEdge DGLinkLab] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\ (_, _, el :: DGLinkLab
el) -> case DGLinkLab -> DGLinkType
dgl_type DGLinkLab
el of
                ScopedLink Global DefLink (ConsStatus cs :: Conservativity
cs None LeftOpen)
                  | Conservativity
cs Conservativity -> Conservativity -> Bool
forall a. Eq a => a -> a -> Bool
== DGLinkType -> Conservativity
getCons DGLinkType
lt -> Bool
True
                _ -> Bool
False) [LEdge DGLinkLab]
innNs
           Bool -> Bool -> Bool
&& case DGNodeLab -> DGNodeInfo
nodeInfo DGNodeLab
nl of
                DGNode DGUnion _ -> Bool
True
                _ -> Bool
False
         -> (DGraph -> LEdge DGLinkLab -> Result DGraph)
-> DGraph -> [LEdge DGLinkLab] -> Result DGraph
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ dg' :: DGraph
dg' (s :: Int
s, _, el :: DGLinkLab
el) -> do
             GMorphism
newMor <- GMorphism -> GMorphism -> Result GMorphism
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
composeMorphisms (DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
el) (GMorphism -> Result GMorphism) -> GMorphism -> Result GMorphism
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
et
             DGraph -> Result DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return (DGraph -> Result DGraph) -> DGraph -> Result DGraph
forall a b. (a -> b) -> a -> b
$ DGraph
-> GMorphism -> DGLinkType -> DGLinkOrigin -> Int -> Int -> DGraph
insLink DGraph
dg' GMorphism
newMor
              (DGLinkLab -> DGLinkType
dgl_type DGLinkLab
el) (DGLinkLab -> DGLinkOrigin
dgl_origin DGLinkLab
el) Int
s Int
t) (Int -> DGraph -> DGraph
delNodeDG Int
n DGraph
dg) [LEdge DGLinkLab]
innNs
       _ -> DGraph -> Result DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return DGraph
dg) DGraph
dgraph ([LNode DGNodeLab] -> Result DGraph)
-> [LNode DGNodeLab] -> Result DGraph
forall a b. (a -> b) -> a -> b
$ DGraph -> [LNode DGNodeLab]
topsortedNodes DGraph
dgraph

defPrefixGlobalAnnos :: FilePath -> GlobalAnnos
defPrefixGlobalAnnos :: FilePath -> GlobalAnnos
defPrefixGlobalAnnos file :: FilePath
file = GlobalAnnos
emptyGlobalAnnos
  { prefix_map :: Map FilePath IRI
prefix_map = FilePath -> IRI -> Map FilePath IRI
forall k a. k -> a -> Map k a
Map.singleton ""
    (IRI -> Map FilePath IRI) -> IRI -> Map FilePath IRI
forall a b. (a -> b) -> a -> b
$ IRI -> Maybe IRI -> IRI
forall a. a -> Maybe a -> a
fromMaybe IRI
nullIRI (Maybe IRI -> IRI) -> Maybe IRI -> IRI
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe IRI
parseIRIReference (FilePath -> Maybe IRI) -> FilePath -> Maybe IRI
forall a b. (a -> b) -> a -> b
$ FilePath
file FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "?" }

anaLibItemAux :: HetcatsOpts -> LNS -> LibName
  -> ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides) -> LIB_ITEM
  -> ResultT IO ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
anaLibItemAux :: HetcatsOpts
-> LNS
-> LibName
-> ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
-> LIB_ITEM
-> ResultT
     IO ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
anaLibItemAux opts :: HetcatsOpts
opts topLns :: LNS
topLns ln :: LibName
ln q :: ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
q@(libItems' :: [LIB_ITEM]
libItems', dg1 :: DGraph
dg1, libenv1 :: LibEnv
libenv1, lg :: LogicGraph
lg, eo :: ExpOverrides
eo) libItem :: LIB_ITEM
libItem = let
  currLog :: FilePath
currLog = LogicGraph -> FilePath
currentLogic LogicGraph
lg
  newOpts :: HetcatsOpts
newOpts = if FilePath -> [FilePath] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem FilePath
currLog ["DMU", "Framework"] then
              HetcatsOpts
opts { defLogic :: FilePath
defLogic = FilePath
currLog } else HetcatsOpts
opts
  in IO (Result ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides))
-> ResultT
     IO ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. m (Result a) -> ResultT m a
ResultT (IO (Result ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides))
 -> ResultT
      IO ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides))
-> IO
     (Result ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides))
-> ResultT
     IO ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a b. (a -> b) -> a -> b
$ do
      res2 :: Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
res2@(Result diags2 :: [Diagnosis]
diags2 res :: Maybe (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
res) <- ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> IO (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
forall (m :: * -> *) a. ResultT m a -> m (Result a)
runResultT
        (ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
 -> IO
      (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)))
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> IO (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
forall a b. (a -> b) -> a -> b
$ LogicGraph
-> HetcatsOpts
-> LNS
-> LibName
-> LibEnv
-> DGraph
-> ExpOverrides
-> LIB_ITEM
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
anaLibItem LogicGraph
lg HetcatsOpts
newOpts LNS
topLns LibName
ln LibEnv
libenv1 DGraph
dg1 ExpOverrides
eo LIB_ITEM
libItem
      ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> IO (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
forall (m :: * -> *) a. ResultT m a -> m (Result a)
runResultT (ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
 -> IO
      (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)))
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> IO (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
forall a b. (a -> b) -> a -> b
$ HetcatsOpts
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a. HetcatsOpts -> ResultT IO a -> ResultT IO a
showDiags1 HetcatsOpts
opts (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
res2)
      let mRes :: Maybe ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
mRes = case Maybe (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
res of
             Just (libItem' :: LIB_ITEM
libItem', dg1' :: DGraph
dg1', libenv1' :: LibEnv
libenv1', newLG :: LogicGraph
newLG, eo' :: ExpOverrides
eo') ->
                 ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
-> Maybe ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a. a -> Maybe a
Just (LIB_ITEM
libItem' LIB_ITEM -> [LIB_ITEM] -> [LIB_ITEM]
forall a. a -> [a] -> [a]
: [LIB_ITEM]
libItems', DGraph
dg1', LibEnv
libenv1', LogicGraph
newLG, ExpOverrides
eo')
             Nothing -> ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
-> Maybe ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a. a -> Maybe a
Just ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
q
      if HetcatsOpts -> Bool
outputToStdout HetcatsOpts
opts then
         if [Diagnosis] -> Bool
hasErrors [Diagnosis]
diags2 then
            FilePath
-> IO
     (Result ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides))
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
Fail.fail "Stopped due to errors"
            else ResultT IO ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
-> IO
     (Result ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides))
forall (m :: * -> *) a. ResultT m a -> m (Result a)
runResultT (ResultT IO ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
 -> IO
      (Result ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)))
-> ResultT
     IO ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
-> IO
     (Result ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides))
forall a b. (a -> b) -> a -> b
$ Result ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT
     IO ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
 -> ResultT
      IO ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides))
-> Result ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT
     IO ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a b. (a -> b) -> a -> b
$ [Diagnosis]
-> Maybe ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
-> Result ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a. [Diagnosis] -> Maybe a -> Result a
Result [] Maybe ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
mRes
         else ResultT IO ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
-> IO
     (Result ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides))
forall (m :: * -> *) a. ResultT m a -> m (Result a)
runResultT (ResultT IO ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
 -> IO
      (Result ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)))
-> ResultT
     IO ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
-> IO
     (Result ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides))
forall a b. (a -> b) -> a -> b
$ Result ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT
     IO ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
 -> ResultT
      IO ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides))
-> Result ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT
     IO ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a b. (a -> b) -> a -> b
$ [Diagnosis]
-> Maybe ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
-> Result ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
diags2 Maybe ([LIB_ITEM], DGraph, LibEnv, LogicGraph, ExpOverrides)
mRes

putMessageIORes :: HetcatsOpts -> Int -> String -> ResultT IO ()
putMessageIORes :: HetcatsOpts -> Int -> FilePath -> ResultT IO ()
putMessageIORes opts :: HetcatsOpts
opts i :: Int
i msg :: FilePath
msg =
   if HetcatsOpts -> Bool
outputToStdout HetcatsOpts
opts
   then IO () -> ResultT IO ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> ResultT IO ()) -> IO () -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts Int
i FilePath
msg
   else Result () -> ResultT IO ()
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result () -> ResultT IO ()) -> Result () -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ () -> FilePath -> Result ()
forall a. a -> FilePath -> Result a
message () FilePath
msg

analyzing :: HetcatsOpts -> String -> ResultT IO ()
analyzing :: HetcatsOpts -> FilePath -> ResultT IO ()
analyzing opts :: HetcatsOpts
opts = HetcatsOpts -> Int -> FilePath -> ResultT IO ()
putMessageIORes HetcatsOpts
opts 1 (FilePath -> ResultT IO ())
-> (FilePath -> FilePath) -> FilePath -> ResultT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ("Analyzing " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++)

alreadyDefined :: String -> String
alreadyDefined :: FilePath -> FilePath
alreadyDefined str :: FilePath
str = "Name " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
str FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " already defined"

-- | analyze a GENERICITY
anaGenericity :: LogicGraph -> LibEnv -> LibName -> DGraph -> HetcatsOpts
  -> ExpOverrides -> NodeName -> GENERICITY
  -> Result (GENERICITY, GenSig, DGraph)
anaGenericity :: LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> NodeName
-> GENERICITY
-> Result (GENERICITY, GenSig, DGraph)
anaGenericity lg :: LogicGraph
lg libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg opts :: HetcatsOpts
opts eo :: ExpOverrides
eo name :: NodeName
name
    gen :: GENERICITY
gen@(Genericity (Params psps :: [Annoted SPEC]
psps) (Imported isps :: [Annoted SPEC]
isps) pos :: Range
pos) =
  let ms :: Maybe NodeSig
ms = DGraph -> Maybe NodeSig
currentBaseTheory DGraph
dg in
  Range
-> Result (GENERICITY, GenSig, DGraph)
-> Result (GENERICITY, GenSig, DGraph)
forall a. Range -> Result a -> Result a
adjustPos Range
pos (Result (GENERICITY, GenSig, DGraph)
 -> Result (GENERICITY, GenSig, DGraph))
-> Result (GENERICITY, GenSig, DGraph)
-> Result (GENERICITY, GenSig, DGraph)
forall a b. (a -> b) -> a -> b
$ case [Annoted SPEC]
psps of
  [] -> do -- no parameter ...
    Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Annoted SPEC] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Annoted SPEC]
isps) (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ () -> FilePath -> Range -> Result ()
forall a. a -> FilePath -> Range -> Result a
plain_error ()
      "Parameterless specifications must not have imports" Range
pos
    AnyLogic
l <- FilePath -> LogicGraph -> Result AnyLogic
forall (m :: * -> *).
MonadFail m =>
FilePath -> LogicGraph -> m AnyLogic
lookupCurrentLogic "GENERICITY" LogicGraph
lg
    (GENERICITY, GenSig, DGraph) -> Result (GENERICITY, GenSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (GENERICITY
gen, MaybeNode -> [NodeSig] -> MaybeNode -> GenSig
GenSig (AnyLogic -> MaybeNode
EmptyNode AnyLogic
l) []
      (MaybeNode -> GenSig) -> MaybeNode -> GenSig
forall a b. (a -> b) -> a -> b
$ MaybeNode -> (NodeSig -> MaybeNode) -> Maybe NodeSig -> MaybeNode
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (AnyLogic -> MaybeNode
EmptyNode AnyLogic
l) NodeSig -> MaybeNode
JustNode Maybe NodeSig
ms, DGraph
dg)
  _ -> do
   AnyLogic
l <- FilePath -> LogicGraph -> Result AnyLogic
forall (m :: * -> *).
MonadFail m =>
FilePath -> LogicGraph -> m AnyLogic
lookupCurrentLogic "IMPORTS" LogicGraph
lg
   let baseNode :: MaybeNode
baseNode = MaybeNode -> (NodeSig -> MaybeNode) -> Maybe NodeSig -> MaybeNode
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (AnyLogic -> MaybeNode
EmptyNode AnyLogic
l) NodeSig -> MaybeNode
JustNode Maybe NodeSig
ms
   (imps' :: [Annoted SPEC]
imps', nsigI :: MaybeNode
nsigI, dg' :: DGraph
dg') <- case [Annoted SPEC]
isps of
     [] -> ([Annoted SPEC], MaybeNode, DGraph)
-> Result ([Annoted SPEC], MaybeNode, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], MaybeNode
baseNode, DGraph
dg)
     _ -> do
      (is' :: [Annoted SPEC]
is', _, nsig' :: NodeSig
nsig', dgI :: DGraph
dgI) <- Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> [Annoted SPEC]
-> Range
-> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
anaUnion Bool
False LogicGraph
lg LibEnv
libEnv LibName
ln DGraph
dg MaybeNode
baseNode
          (FilePath -> NodeName -> NodeName
extName "Imports" NodeName
name) HetcatsOpts
opts ExpOverrides
eo [Annoted SPEC]
isps (Range -> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph))
-> Range -> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
forall a b. (a -> b) -> a -> b
$ [Annoted SPEC] -> Range
forall a. GetRange a => a -> Range
getRange [Annoted SPEC]
isps
      ([Annoted SPEC], MaybeNode, DGraph)
-> Result ([Annoted SPEC], MaybeNode, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Annoted SPEC]
is', NodeSig -> MaybeNode
JustNode NodeSig
nsig', DGraph
dgI)
   (ps' :: [Annoted SPEC]
ps', nsigPs :: [NodeSig]
nsigPs, ns :: NodeSig
ns, dg'' :: DGraph
dg'') <- Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> [Annoted SPEC]
-> Range
-> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
anaUnion Bool
False LogicGraph
lg LibEnv
libEnv LibName
ln DGraph
dg' MaybeNode
nsigI
          (FilePath -> NodeName -> NodeName
extName "Parameters" NodeName
name) HetcatsOpts
opts ExpOverrides
eo [Annoted SPEC]
psps (Range -> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph))
-> Range -> Result ([Annoted SPEC], [NodeSig], NodeSig, DGraph)
forall a b. (a -> b) -> a -> b
$ [Annoted SPEC] -> Range
forall a. GetRange a => a -> Range
getRange [Annoted SPEC]
psps
   (GENERICITY, GenSig, DGraph) -> Result (GENERICITY, GenSig, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (PARAMS -> IMPORTED -> Range -> GENERICITY
Genericity ([Annoted SPEC] -> PARAMS
Params [Annoted SPEC]
ps') ([Annoted SPEC] -> IMPORTED
Imported [Annoted SPEC]
imps') Range
pos,
     MaybeNode -> [NodeSig] -> MaybeNode -> GenSig
GenSig MaybeNode
nsigI [NodeSig]
nsigPs (MaybeNode -> GenSig) -> MaybeNode -> GenSig
forall a b. (a -> b) -> a -> b
$ NodeSig -> MaybeNode
JustNode NodeSig
ns, DGraph
dg'')

expCurieT :: GlobalAnnos -> ExpOverrides -> IRI -> ResultT IO IRI
expCurieT :: GlobalAnnos -> ExpOverrides -> IRI -> ResultT IO IRI
expCurieT ga :: GlobalAnnos
ga eo :: ExpOverrides
eo = Result IRI -> ResultT IO IRI
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result IRI -> ResultT IO IRI)
-> (IRI -> Result IRI) -> IRI -> ResultT IO IRI
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GlobalAnnos -> ExpOverrides -> IRI -> Result IRI
expCurieR GlobalAnnos
ga ExpOverrides
eo

-- | analyse a LIB_ITEM
anaLibItem :: LogicGraph -> HetcatsOpts -> LNS -> LibName -> LibEnv -> DGraph
  -> ExpOverrides -> LIB_ITEM
  -> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
anaLibItem :: LogicGraph
-> HetcatsOpts
-> LNS
-> LibName
-> LibEnv
-> DGraph
-> ExpOverrides
-> LIB_ITEM
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
anaLibItem lg :: LogicGraph
lg opts :: HetcatsOpts
opts topLns :: LNS
topLns currLn :: LibName
currLn libenv :: LibEnv
libenv dg :: DGraph
dg eo :: ExpOverrides
eo itm :: LIB_ITEM
itm =
 case LIB_ITEM
itm of
  Spec_defn spn2 :: IRI
spn2 gen :: GENERICITY
gen asp :: Annoted SPEC
asp pos :: Range
pos -> do
    let spn' :: IRI
spn' = if FilePath -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (IRI -> FilePath
iriToStringUnsecure IRI
spn2) then
         SIMPLE_ID -> IRI
simpleIdToIRI (SIMPLE_ID -> IRI) -> SIMPLE_ID -> IRI
forall a b. (a -> b) -> a -> b
$ FilePath -> SIMPLE_ID
mkSimpleId "Spec" else IRI
spn2
    IRI
spn <- GlobalAnnos -> ExpOverrides -> IRI -> ResultT IO IRI
expCurieT (DGraph -> GlobalAnnos
globalAnnos DGraph
dg) ExpOverrides
eo IRI
spn'
    let spstr :: FilePath
spstr = IRI -> FilePath
iriToStringUnsecure IRI
spn
        nName :: NodeName
nName = IRI -> NodeName
makeName IRI
spn
    HetcatsOpts -> FilePath -> ResultT IO ()
analyzing HetcatsOpts
opts (FilePath -> ResultT IO ()) -> FilePath -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ "spec " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
spstr
    (gen' :: GENERICITY
gen', gsig :: GenSig
gsig@(GenSig _ _args :: [NodeSig]
_args allparams :: MaybeNode
allparams), dg' :: DGraph
dg') <-
      Result (GENERICITY, GenSig, DGraph)
-> ResultT IO (GENERICITY, GenSig, DGraph)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result (GENERICITY, GenSig, DGraph)
 -> ResultT IO (GENERICITY, GenSig, DGraph))
-> Result (GENERICITY, GenSig, DGraph)
-> ResultT IO (GENERICITY, GenSig, DGraph)
forall a b. (a -> b) -> a -> b
$ LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> NodeName
-> GENERICITY
-> Result (GENERICITY, GenSig, DGraph)
anaGenericity LogicGraph
lg LibEnv
libenv LibName
currLn DGraph
dg HetcatsOpts
opts ExpOverrides
eo NodeName
nName GENERICITY
gen
    (sanno1 :: Conservativity
sanno1, impliesA :: Bool
impliesA) <- Result (Conservativity, Bool) -> ResultT IO (Conservativity, Bool)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result (Conservativity, Bool)
 -> ResultT IO (Conservativity, Bool))
-> Result (Conservativity, Bool)
-> ResultT IO (Conservativity, Bool)
forall a b. (a -> b) -> a -> b
$ Range -> Annoted SPEC -> Result (Conservativity, Bool)
forall a. Range -> Annoted a -> Result (Conservativity, Bool)
getSpecAnnos Range
pos Annoted SPEC
asp
    Bool -> ResultT IO () -> ResultT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
impliesA (ResultT IO () -> ResultT IO ()) -> ResultT IO () -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ Result () -> ResultT IO ()
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result () -> ResultT IO ()) -> Result () -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ () -> FilePath -> Range -> Result ()
forall a. a -> FilePath -> Range -> Result a
plain_error ()
      "unexpected initial %implies in spec-defn" Range
pos
    (sp' :: SPEC
sp', body :: NodeSig
body, dg'' :: DGraph
dg'') <-
      Result (SPEC, NodeSig, DGraph)
-> ResultT IO (SPEC, NodeSig, DGraph)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Conservativity
-> Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> SPEC
-> Range
-> Result (SPEC, NodeSig, DGraph)
anaSpecTop Conservativity
sanno1 Bool
True LogicGraph
lg LibEnv
libenv LibName
currLn DGraph
dg'
            MaybeNode
allparams NodeName
nName HetcatsOpts
opts ExpOverrides
eo (Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
asp) Range
pos)
    let libItem' :: LIB_ITEM
libItem' = IRI -> GENERICITY -> Annoted SPEC -> Range -> LIB_ITEM
Spec_defn IRI
spn GENERICITY
gen' (SPEC -> Annoted SPEC -> Annoted SPEC
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted SPEC
sp' Annoted SPEC
asp) Range
pos
        genv :: GlobalEnv
genv = DGraph -> GlobalEnv
globalEnv DGraph
dg
    if IRI -> GlobalEnv -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member IRI
spn GlobalEnv
genv
      then Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
 -> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a b. (a -> b) -> a -> b
$ (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> FilePath
-> Range
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a. a -> FilePath -> Range -> Result a
plain_error (LIB_ITEM
libItem', DGraph
dg'', LibEnv
libenv, LogicGraph
lg, ExpOverrides
eo)
              (FilePath -> FilePath
alreadyDefined FilePath
spstr) Range
pos
      else
        -- let (_n, dg''') = addSpecNodeRT dg'' (UnitSig args body) $ show spn
        (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. Monad m => a -> m a
return
        ( LIB_ITEM
libItem'
        , DGraph
dg'' { globalEnv :: GlobalEnv
globalEnv = IRI -> GlobalEntry -> GlobalEnv -> GlobalEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert IRI
spn (ExtGenSig -> GlobalEntry
SpecEntry
                  (ExtGenSig -> GlobalEntry) -> ExtGenSig -> GlobalEntry
forall a b. (a -> b) -> a -> b
$ GenSig -> NodeSig -> ExtGenSig
ExtGenSig GenSig
gsig NodeSig
body) GlobalEnv
genv }
        , LibEnv
libenv, LogicGraph
lg, ExpOverrides
eo)
  Entail_defn en' :: IRI
en' etype :: ENTAIL_TYPE
etype pos :: Range
pos -> do
    IRI
en <- GlobalAnnos -> ExpOverrides -> IRI -> ResultT IO IRI
expCurieT (DGraph -> GlobalAnnos
globalAnnos DGraph
dg) ExpOverrides
eo IRI
en'
    HetcatsOpts -> FilePath -> ResultT IO ()
analyzing HetcatsOpts
opts (FilePath -> ResultT IO ()) -> FilePath -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ "entailment " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ IRI -> FilePath
iriToStringUnsecure IRI
en
    Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
 -> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a b. (a -> b) -> a -> b
$ LogicGraph
-> LibName
-> LibEnv
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> IRI
-> ENTAIL_TYPE
-> Range
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
anaEntailmentDefn LogicGraph
lg LibName
currLn LibEnv
libenv DGraph
dg HetcatsOpts
opts ExpOverrides
eo IRI
en ENTAIL_TYPE
etype Range
pos
  View_defn vn' :: IRI
vn' gen :: GENERICITY
gen vt :: VIEW_TYPE
vt gsis :: [G_mapping]
gsis pos :: Range
pos -> do
    IRI
vn <- GlobalAnnos -> ExpOverrides -> IRI -> ResultT IO IRI
expCurieT (DGraph -> GlobalAnnos
globalAnnos DGraph
dg) ExpOverrides
eo IRI
vn'
    HetcatsOpts -> FilePath -> ResultT IO ()
analyzing HetcatsOpts
opts (FilePath -> ResultT IO ()) -> FilePath -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ "view " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ IRI -> FilePath
iriToStringUnsecure IRI
vn
    Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
 -> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a b. (a -> b) -> a -> b
$ LogicGraph
-> LibName
-> LibEnv
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> IRI
-> GENERICITY
-> VIEW_TYPE
-> [G_mapping]
-> Range
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
anaViewDefn LogicGraph
lg LibName
currLn LibEnv
libenv DGraph
dg HetcatsOpts
opts ExpOverrides
eo IRI
vn GENERICITY
gen VIEW_TYPE
vt [G_mapping]
gsis Range
pos
  Align_defn an' :: IRI
an' arities :: Maybe ALIGN_ARITIES
arities atype :: VIEW_TYPE
atype acorresps :: [CORRESPONDENCE]
acorresps _ pos :: Range
pos -> do
    IRI
an <- GlobalAnnos -> ExpOverrides -> IRI -> ResultT IO IRI
expCurieT (DGraph -> GlobalAnnos
globalAnnos DGraph
dg) ExpOverrides
eo IRI
an'
    HetcatsOpts -> FilePath -> ResultT IO ()
analyzing HetcatsOpts
opts (FilePath -> ResultT IO ()) -> FilePath -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ "alignment " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ IRI -> FilePath
iriToStringUnsecure IRI
an
    LogicGraph
-> LibName
-> LibEnv
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> IRI
-> Maybe ALIGN_ARITIES
-> VIEW_TYPE
-> [CORRESPONDENCE]
-> Range
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
anaAlignDefn LogicGraph
lg LibName
currLn LibEnv
libenv DGraph
dg HetcatsOpts
opts ExpOverrides
eo IRI
an Maybe ALIGN_ARITIES
arities VIEW_TYPE
atype [CORRESPONDENCE]
acorresps Range
pos
  Arch_spec_defn asn' :: IRI
asn' asp :: Annoted ARCH_SPEC
asp pos :: Range
pos -> do
    IRI
asn <- GlobalAnnos -> ExpOverrides -> IRI -> ResultT IO IRI
expCurieT (DGraph -> GlobalAnnos
globalAnnos DGraph
dg) ExpOverrides
eo IRI
asn'
    let asstr :: FilePath
asstr = IRI -> FilePath
iriToStringUnsecure IRI
asn
    HetcatsOpts -> FilePath -> ResultT IO ()
analyzing HetcatsOpts
opts (FilePath -> ResultT IO ()) -> FilePath -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ "arch spec " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
asstr
    (_, _, diag :: Diag
diag, archSig :: RefSig
archSig, dg' :: DGraph
dg', asp' :: ARCH_SPEC
asp') <- Result
  ([DiagNodeSig], Maybe DiagNodeSig, Diag, RefSig, DGraph, ARCH_SPEC)
-> ResultT
     IO
     ([DiagNodeSig], Maybe DiagNodeSig, Diag, RefSig, DGraph, ARCH_SPEC)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result
   ([DiagNodeSig], Maybe DiagNodeSig, Diag, RefSig, DGraph, ARCH_SPEC)
 -> ResultT
      IO
      ([DiagNodeSig], Maybe DiagNodeSig, Diag, RefSig, DGraph,
       ARCH_SPEC))
-> Result
     ([DiagNodeSig], Maybe DiagNodeSig, Diag, RefSig, DGraph, ARCH_SPEC)
-> ResultT
     IO
     ([DiagNodeSig], Maybe DiagNodeSig, Diag, RefSig, DGraph, ARCH_SPEC)
forall a b. (a -> b) -> a -> b
$ LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> ExtStUnitCtx
-> Maybe Int
-> ARCH_SPEC
-> Result
     ([DiagNodeSig], Maybe DiagNodeSig, Diag, RefSig, DGraph, ARCH_SPEC)
anaArchSpec LogicGraph
lg LibEnv
libenv LibName
currLn DGraph
dg
      HetcatsOpts
opts ExpOverrides
eo ExtStUnitCtx
emptyExtStUnitCtx Maybe Int
forall a. Maybe a
Nothing (ARCH_SPEC
 -> Result
      ([DiagNodeSig], Maybe DiagNodeSig, Diag, RefSig, DGraph,
       ARCH_SPEC))
-> ARCH_SPEC
-> Result
     ([DiagNodeSig], Maybe DiagNodeSig, Diag, RefSig, DGraph, ARCH_SPEC)
forall a b. (a -> b) -> a -> b
$ Annoted ARCH_SPEC -> ARCH_SPEC
forall a. Annoted a -> a
item Annoted ARCH_SPEC
asp
    let asd' :: LIB_ITEM
asd' = IRI -> Annoted ARCH_SPEC -> Range -> LIB_ITEM
Arch_spec_defn IRI
asn (ARCH_SPEC -> Annoted ARCH_SPEC -> Annoted ARCH_SPEC
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted ARCH_SPEC
asp' Annoted ARCH_SPEC
asp) Range
pos
        genv :: GlobalEnv
genv = DGraph -> GlobalEnv
globalEnv DGraph
dg'
    if IRI -> GlobalEnv -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member IRI
asn GlobalEnv
genv
      then Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
 -> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a b. (a -> b) -> a -> b
$ (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> FilePath
-> Range
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a. a -> FilePath -> Range -> Result a
plain_error (LIB_ITEM
asd', DGraph
dg', LibEnv
libenv, LogicGraph
lg, ExpOverrides
eo)
               (FilePath -> FilePath
alreadyDefined FilePath
asstr) Range
pos
      else do
            let aName :: FilePath
aName = IRI -> FilePath
forall a. Show a => a -> FilePath
show IRI
asn
                rSource :: Int
rSource = RTPointer -> Int
refSource (RTPointer -> Int) -> RTPointer -> Int
forall a b. (a -> b) -> a -> b
$ RefSig -> RTPointer
getPointerFromRef RefSig
archSig
                dg'' :: DGraph
dg'' = DGraph -> Int -> Bool -> FilePath -> DGraph
updateNodeNameRT DGraph
dg' Int
rSource
                       Bool
True FilePath
aName
                dg3 :: DGraph
dg3 = DGraph
dg'' { 
                        archSpecDiags :: Map FilePath Diag
archSpecDiags = FilePath -> Diag -> Map FilePath Diag -> Map FilePath Diag
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert FilePath
aName Diag
diag (Map FilePath Diag -> Map FilePath Diag)
-> Map FilePath Diag -> Map FilePath Diag
forall a b. (a -> b) -> a -> b
$ DGraph -> Map FilePath Diag
archSpecDiags DGraph
dg''
                       , specRoots :: Map FilePath [Int]
specRoots = FilePath -> [Int] -> Map FilePath [Int] -> Map FilePath [Int]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert FilePath
aName [Int
rSource] (Map FilePath [Int] -> Map FilePath [Int])
-> Map FilePath [Int] -> Map FilePath [Int]
forall a b. (a -> b) -> a -> b
$ DGraph -> Map FilePath [Int]
specRoots DGraph
dg''
                      }
            (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. Monad m => a -> m a
return (LIB_ITEM
asd', DGraph
dg3
              { globalEnv :: GlobalEnv
globalEnv = IRI -> GlobalEntry -> GlobalEnv -> GlobalEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert IRI
asn
                            (Bool -> RefSig -> GlobalEntry
ArchOrRefEntry Bool
True RefSig
archSig) GlobalEnv
genv }
              , LibEnv
libenv, LogicGraph
lg, ExpOverrides
eo)
  Unit_spec_defn usn' :: IRI
usn' usp :: UNIT_SPEC
usp pos :: Range
pos -> do
    IRI
usn <- GlobalAnnos -> ExpOverrides -> IRI -> ResultT IO IRI
expCurieT (DGraph -> GlobalAnnos
globalAnnos DGraph
dg) ExpOverrides
eo IRI
usn'
    let usstr :: FilePath
usstr = IRI -> FilePath
iriToStringUnsecure IRI
usn
    HetcatsOpts -> FilePath -> ResultT IO ()
analyzing HetcatsOpts
opts (FilePath -> ResultT IO ()) -> FilePath -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ "unit spec " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
usstr
    AnyLogic
l <- FilePath -> LogicGraph -> ResultT IO AnyLogic
forall (m :: * -> *).
MonadFail m =>
FilePath -> LogicGraph -> m AnyLogic
lookupCurrentLogic "Unit_spec_defn" LogicGraph
lg
    (rSig :: RefSig
rSig, dg' :: DGraph
dg', usp' :: UNIT_SPEC
usp') <-
      Result (RefSig, DGraph, UNIT_SPEC)
-> ResultT IO (RefSig, DGraph, UNIT_SPEC)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result (RefSig, DGraph, UNIT_SPEC)
 -> ResultT IO (RefSig, DGraph, UNIT_SPEC))
-> Result (RefSig, DGraph, UNIT_SPEC)
-> ResultT IO (RefSig, DGraph, UNIT_SPEC)
forall a b. (a -> b) -> a -> b
$ LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> IRI
-> MaybeNode
-> Maybe RTPointer
-> UNIT_SPEC
-> Result (RefSig, DGraph, UNIT_SPEC)
anaUnitSpec LogicGraph
lg LibEnv
libenv LibName
currLn DGraph
dg HetcatsOpts
opts ExpOverrides
eo 
                          IRI
usn' (AnyLogic -> MaybeNode
EmptyNode AnyLogic
l) Maybe RTPointer
forall a. Maybe a
Nothing UNIT_SPEC
usp
    UnitSig
unitSig <- Result UnitSig -> ResultT IO UnitSig
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result UnitSig -> ResultT IO UnitSig)
-> Result UnitSig -> ResultT IO UnitSig
forall a b. (a -> b) -> a -> b
$ RefSig -> Result UnitSig
getUnitSigFromRef RefSig
rSig
    let usd' :: LIB_ITEM
usd' = IRI -> UNIT_SPEC -> Range -> LIB_ITEM
Unit_spec_defn IRI
usn UNIT_SPEC
usp' Range
pos
        genv :: GlobalEnv
genv = DGraph -> GlobalEnv
globalEnv DGraph
dg'
    if IRI -> GlobalEnv -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member IRI
usn GlobalEnv
genv
      then Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
 -> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a b. (a -> b) -> a -> b
$ (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> FilePath
-> Range
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a. a -> FilePath -> Range -> Result a
plain_error (LIB_ITEM
itm, DGraph
dg', LibEnv
libenv, LogicGraph
lg, ExpOverrides
eo)
               (FilePath -> FilePath
alreadyDefined FilePath
usstr) Range
pos
      else (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. Monad m => a -> m a
return (LIB_ITEM
usd', DGraph
dg'
             { globalEnv :: GlobalEnv
globalEnv = IRI -> GlobalEntry -> GlobalEnv -> GlobalEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert IRI
usn (UnitSig -> GlobalEntry
UnitEntry UnitSig
unitSig) GlobalEnv
genv },
             LibEnv
libenv, LogicGraph
lg, ExpOverrides
eo)
  Ref_spec_defn rn' :: IRI
rn' rsp :: REF_SPEC
rsp pos :: Range
pos -> do
    IRI
rn <- GlobalAnnos -> ExpOverrides -> IRI -> ResultT IO IRI
expCurieT (DGraph -> GlobalAnnos
globalAnnos DGraph
dg) ExpOverrides
eo IRI
rn'
    let rnstr :: FilePath
rnstr = IRI -> FilePath
iriToStringUnsecure IRI
rn
    AnyLogic
l <- FilePath -> LogicGraph -> ResultT IO AnyLogic
forall (m :: * -> *).
MonadFail m =>
FilePath -> LogicGraph -> m AnyLogic
lookupCurrentLogic "Ref_spec_defn" LogicGraph
lg
    (_, _, _, rsig :: RefSig
rsig, dg' :: DGraph
dg', rsp' :: REF_SPEC
rsp') <- Result
  ([DiagNodeSig], Maybe DiagNodeSig, Maybe Diag, RefSig, DGraph,
   REF_SPEC)
-> ResultT
     IO
     ([DiagNodeSig], Maybe DiagNodeSig, Maybe Diag, RefSig, DGraph,
      REF_SPEC)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result
   ([DiagNodeSig], Maybe DiagNodeSig, Maybe Diag, RefSig, DGraph,
    REF_SPEC)
 -> ResultT
      IO
      ([DiagNodeSig], Maybe DiagNodeSig, Maybe Diag, RefSig, DGraph,
       REF_SPEC))
-> Result
     ([DiagNodeSig], Maybe DiagNodeSig, Maybe Diag, RefSig, DGraph,
      REF_SPEC)
-> ResultT
     IO
     ([DiagNodeSig], Maybe DiagNodeSig, Maybe Diag, RefSig, DGraph,
      REF_SPEC)
forall a b. (a -> b) -> a -> b
$ 
        Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> MaybeNode
-> IRI
-> ExtStUnitCtx
-> Maybe RTPointer
-> REF_SPEC
-> Result
     ([DiagNodeSig], Maybe DiagNodeSig, Maybe Diag, RefSig, DGraph,
      REF_SPEC)
anaRefSpec Bool
True LogicGraph
lg LibEnv
libenv LibName
currLn DGraph
dg HetcatsOpts
opts ExpOverrides
eo
      (AnyLogic -> MaybeNode
EmptyNode AnyLogic
l) IRI
rn ExtStUnitCtx
emptyExtStUnitCtx Maybe RTPointer
forall a. Maybe a
Nothing REF_SPEC
rsp
    HetcatsOpts -> FilePath -> ResultT IO ()
analyzing HetcatsOpts
opts (FilePath -> ResultT IO ()) -> FilePath -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ "ref spec " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
rnstr
    let rsd' :: LIB_ITEM
rsd' = IRI -> REF_SPEC -> Range -> LIB_ITEM
Ref_spec_defn IRI
rn REF_SPEC
rsp' Range
pos
        genv :: GlobalEnv
genv = DGraph -> GlobalEnv
globalEnv DGraph
dg'
        getSources :: RTPointer -> [Int]
getSources p :: RTPointer
p = 
          case RTPointer
p of
           NPComp f :: Map IRI RTPointer
f -> (RTPointer -> [Int]) -> [RTPointer] -> [Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap RTPointer -> [Int]
getSources ([RTPointer] -> [Int]) -> [RTPointer] -> [Int]
forall a b. (a -> b) -> a -> b
$ Map IRI RTPointer -> [RTPointer]
forall k a. Map k a -> [a]
Map.elems Map IRI RTPointer
f
           _ -> [RTPointer -> Int
refSource RTPointer
p]
        sources :: [Int]
sources = RTPointer -> [Int]
getSources (RTPointer -> [Int]) -> RTPointer -> [Int]
forall a b. (a -> b) -> a -> b
$ RefSig -> RTPointer
getPointerFromRef RefSig
rsig
    if IRI -> GlobalEnv -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member IRI
rn GlobalEnv
genv
      then Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
 -> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a b. (a -> b) -> a -> b
$ (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> FilePath
-> Range
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a. a -> FilePath -> Range -> Result a
plain_error (LIB_ITEM
itm, DGraph
dg', LibEnv
libenv, LogicGraph
lg, ExpOverrides
eo)
               (FilePath -> FilePath
alreadyDefined FilePath
rnstr) Range
pos
      else (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. Monad m => a -> m a
return ( LIB_ITEM
rsd', DGraph
dg'
        { globalEnv :: GlobalEnv
globalEnv = IRI -> GlobalEntry -> GlobalEnv -> GlobalEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert IRI
rn (Bool -> RefSig -> GlobalEntry
ArchOrRefEntry Bool
False RefSig
rsig) GlobalEnv
genv
        , specRoots :: Map FilePath [Int]
specRoots = FilePath -> [Int] -> Map FilePath [Int] -> Map FilePath [Int]
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert FilePath
rnstr [Int]
sources (Map FilePath [Int] -> Map FilePath [Int])
-> Map FilePath [Int] -> Map FilePath [Int]
forall a b. (a -> b) -> a -> b
$ DGraph -> Map FilePath [Int]
specRoots DGraph
dg' }
        , LibEnv
libenv, LogicGraph
lg, ExpOverrides
eo)
  Logic_decl logN :: LogicDescr
logN pos :: Range
pos -> do
    HetcatsOpts -> Int -> FilePath -> ResultT IO ()
putMessageIORes HetcatsOpts
opts 1 (FilePath -> ResultT IO ())
-> (Doc -> FilePath) -> Doc -> ResultT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> FilePath
forall a. Show a => a -> FilePath
show (Doc -> ResultT IO ()) -> Doc -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ LogicGraph -> LIB_ITEM -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg LIB_ITEM
itm
    (mth :: Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab))
mth, newLg :: LogicGraph
newLg) <- Result
  (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab)), LogicGraph)
-> ResultT
     IO
     (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab)), LogicGraph)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR
      (Result
   (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab)), LogicGraph)
 -> ResultT
      IO
      (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab)),
       LogicGraph))
-> Result
     (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab)), LogicGraph)
-> ResultT
     IO
     (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab)), LogicGraph)
forall a b. (a -> b) -> a -> b
$ Range
-> Result
     (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab)), LogicGraph)
-> Result
     (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab)), LogicGraph)
forall a. Range -> Result a -> Result a
adjustPos Range
pos (Result
   (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab)), LogicGraph)
 -> Result
      (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab)),
       LogicGraph))
-> Result
     (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab)), LogicGraph)
-> Result
     (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab)), LogicGraph)
forall a b. (a -> b) -> a -> b
$ HetcatsOpts
-> LogicDescr
-> LibName
-> DGraph
-> LibEnv
-> LogicGraph
-> Result
     (Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab)), LogicGraph)
anaSublogic HetcatsOpts
opts LogicDescr
logN LibName
currLn DGraph
dg LibEnv
libenv LogicGraph
lg
    case Maybe (ExtGenSig, (LibName, DGraph, LNode DGNodeLab))
mth of
      Nothing ->
        (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. Monad m => a -> m a
return (LIB_ITEM
itm, DGraph
dg { currentBaseTheory :: Maybe NodeSig
currentBaseTheory = Maybe NodeSig
forall a. Maybe a
Nothing }, LibEnv
libenv, LogicGraph
newLg, ExpOverrides
eo)
      Just (s :: ExtGenSig
s, (libName :: LibName
libName, refDG :: DGraph
refDG, (_, lbl :: DGNodeLab
lbl))) -> do
            -- store th-lbl in newDG
        let dg2 :: DGraph
dg2 = if LibName
libName LibName -> LibName -> Bool
forall a. Eq a => a -> a -> Bool
/= LibName
currLn then
              let (s2 :: ExtGenSig
s2, (genv :: GlobalEnv
genv, newDG :: DGraph
newDG)) = LibEnv
-> LibName
-> DGraph
-> (GlobalEnv, DGraph)
-> IRI
-> ExtGenSig
-> (ExtGenSig, (GlobalEnv, DGraph))
refExtsigAndInsert LibEnv
libenv LibName
libName DGraph
refDG
                    (DGraph -> GlobalEnv
globalEnv DGraph
dg, DGraph
dg) (NodeName -> IRI
getName (NodeName -> IRI) -> NodeName -> IRI
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> NodeName
dgn_name DGNodeLab
lbl) ExtGenSig
s
              in DGraph
newDG { globalEnv :: GlobalEnv
globalEnv = GlobalEnv
genv
                       , currentBaseTheory :: Maybe NodeSig
currentBaseTheory = NodeSig -> Maybe NodeSig
forall a. a -> Maybe a
Just (NodeSig -> Maybe NodeSig) -> NodeSig -> Maybe NodeSig
forall a b. (a -> b) -> a -> b
$ ExtGenSig -> NodeSig
extGenBody ExtGenSig
s2 }
              else DGraph
dg { currentBaseTheory :: Maybe NodeSig
currentBaseTheory = NodeSig -> Maybe NodeSig
forall a. a -> Maybe a
Just (NodeSig -> Maybe NodeSig) -> NodeSig -> Maybe NodeSig
forall a b. (a -> b) -> a -> b
$ ExtGenSig -> NodeSig
extGenBody ExtGenSig
s }
        (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. Monad m => a -> m a
return (LIB_ITEM
itm, DGraph
dg2, LibEnv
libenv, LogicGraph
newLg, ExpOverrides
eo)
  Network_defn anIri :: IRI
anIri (Network cItems :: [LABELED_ONTO_OR_INTPR_REF]
cItems eItems :: [IRI]
eItems _) pos :: Range
pos -> do
    IRI
nn <- GlobalAnnos -> ExpOverrides -> IRI -> ResultT IO IRI
expCurieT (DGraph -> GlobalAnnos
globalAnnos DGraph
dg) ExpOverrides
eo IRI
anIri
    let nnstr :: FilePath
nnstr = IRI -> FilePath
iriToStringUnsecure IRI
nn
    HetcatsOpts -> FilePath -> ResultT IO ()
analyzing HetcatsOpts
opts (FilePath -> ResultT IO ()) -> FilePath -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ "network " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
nnstr
    let (cNodes :: [Int]
cNodes, cEdges :: [LEdge DGLinkLab]
cEdges) = DGraph
-> [LABELED_ONTO_OR_INTPR_REF]
-> [IRI]
-> ([Int], [LEdge DGLinkLab])
networkDiagram DGraph
dg [LABELED_ONTO_OR_INTPR_REF]
cItems [IRI]
eItems
        diag :: GDiagram
diag = DGraph -> [Int] -> [LEdge DGLinkLab] -> GDiagram
makeDiagram DGraph
dg [Int]
cNodes [LEdge DGLinkLab]
cEdges
        genv :: GlobalEnv
genv = DGraph -> GlobalEnv
globalEnv DGraph
dg
    if IRI -> GlobalEnv -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member IRI
nn GlobalEnv
genv 
       then
        Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
 -> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a b. (a -> b) -> a -> b
$ (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> FilePath
-> Range
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a. a -> FilePath -> Range -> Result a
plain_error (LIB_ITEM
itm, DGraph
dg, LibEnv
libenv, LogicGraph
lg, ExpOverrides
eo)
               (FilePath -> FilePath
alreadyDefined FilePath
nnstr) Range
pos
       else
        (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. Monad m => a -> m a
return (LIB_ITEM
itm, DGraph
dg{globalEnv :: GlobalEnv
globalEnv = IRI -> GlobalEntry -> GlobalEnv -> GlobalEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert IRI
nn (GDiagram -> GlobalEntry
NetworkEntry GDiagram
diag) GlobalEnv
genv},
                LibEnv
libenv, LogicGraph
lg, ExpOverrides
eo)
  Download_items ln :: LibName
ln items :: DownloadItems
items pos :: Range
pos ->
    if LibName -> LNS -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member LibName
ln LNS
topLns then
     Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
 -> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a b. (a -> b) -> a -> b
$ FilePath
-> Set IRI
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a b. (GetRange a, Pretty a) => FilePath -> a -> Result b
mkError "illegal cyclic library import"
       (Set IRI
 -> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
-> Set IRI
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a b. (a -> b) -> a -> b
$ (LibName -> IRI) -> LNS -> Set IRI
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map LibName -> IRI
getLibId LNS
topLns
    else do
        let newOpts :: HetcatsOpts
newOpts = HetcatsOpts
opts { intype :: InType
intype = InType
GuessIn }
        (ln' :: LibName
ln', libenv' :: LibEnv
libenv') <- LogicGraph
-> HetcatsOpts
-> LNS
-> LibEnv
-> DGraph
-> LibName
-> ResultT IO (LibName, LibEnv)
anaLibFile LogicGraph
lg HetcatsOpts
newOpts LNS
topLns LibEnv
libenv
          (DGraph -> DGraph -> DGraph
cpIndexMaps DGraph
dg DGraph
emptyDG { globalAnnos :: GlobalAnnos
globalAnnos =
            GlobalAnnos
emptyGlobalAnnos { prefix_map :: Map FilePath IRI
prefix_map = GlobalAnnos -> Map FilePath IRI
prefix_map (GlobalAnnos -> Map FilePath IRI)
-> GlobalAnnos -> Map FilePath IRI
forall a b. (a -> b) -> a -> b
$ DGraph -> GlobalAnnos
globalAnnos DGraph
dg }}) LibName
ln
        Bool -> ResultT IO () -> ResultT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (LibName
ln LibName -> LibName -> Bool
forall a. Eq a => a -> a -> Bool
== LibName
ln')
          (ResultT IO () -> ResultT IO ()) -> ResultT IO () -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ Result () -> ResultT IO ()
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result () -> ResultT IO ()) -> Result () -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ () -> FilePath -> Range -> Result ()
forall a. a -> FilePath -> Range -> Result a
warning ()
              (LibName -> FilePath -> FilePath
forall a. Show a => a -> FilePath -> FilePath
shows LibName
ln " does not match internal name " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ LibName -> FilePath -> FilePath
forall a. Show a => a -> FilePath -> FilePath
shows LibName
ln' "")
              Range
pos
        case LibName -> LibEnv -> Maybe DGraph
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup LibName
ln' LibEnv
libenv' of
          Nothing -> FilePath
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a. HasCallStack => FilePath -> a
error (FilePath
 -> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
-> FilePath
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a b. (a -> b) -> a -> b
$ "Internal error: did not find library "
            FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ LibName -> FilePath
forall a. Show a => a -> FilePath
show LibName
ln' FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " available: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [LibName] -> FilePath
forall a. Show a => a -> FilePath
show (LibEnv -> [LibName]
forall k a. Map k a -> [k]
Map.keys LibEnv
libenv')
          Just dg' :: DGraph
dg' -> do
            let dg0 :: DGraph
dg0 = DGraph -> DGraph -> DGraph
cpIndexMaps DGraph
dg' DGraph
dg
                fn :: FilePath
fn = LibName -> FilePath
libToFileName LibName
ln'
                currFn :: FilePath
currFn = LibName -> FilePath
libToFileName LibName
currLn
                (realItems :: [ItemNameMap]
realItems, errs :: [Result ()]
errs, origItems :: [IRI]
origItems) = case DownloadItems
items of
                  ItemMaps rawIms :: [ItemNameMap]
rawIms ->
                    let (ims :: [ItemNameMap]
ims, warns :: [Result ()]
warns) = (ItemNameMap
 -> ([ItemNameMap], [Result ()]) -> ([ItemNameMap], [Result ()]))
-> ([ItemNameMap], [Result ()])
-> [ItemNameMap]
-> ([ItemNameMap], [Result ()])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ im :: ItemNameMap
im@(ItemNameMap i :: IRI
i mi :: Maybe IRI
mi)
                          (is :: [ItemNameMap]
is, ws :: [Result ()]
ws) -> if IRI -> Maybe IRI
forall a. a -> Maybe a
Just IRI
i Maybe IRI -> Maybe IRI -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe IRI
mi then
                            (IRI -> Maybe IRI -> ItemNameMap
ItemNameMap IRI
i Maybe IRI
forall a. Maybe a
Nothing ItemNameMap -> [ItemNameMap] -> [ItemNameMap]
forall a. a -> [a] -> [a]
: [ItemNameMap]
is
                            , () -> FilePath -> Range -> Result ()
forall a. a -> FilePath -> Range -> Result a
warning () (IRI -> FilePath
forall a. Show a => a -> FilePath
show IRI
i FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " item no renamed")
                              (Maybe IRI -> Range
forall a. GetRange a => a -> Range
getRange Maybe IRI
mi) Result () -> [Result ()] -> [Result ()]
forall a. a -> [a] -> [a]
: [Result ()]
ws)
                            else (ItemNameMap
im ItemNameMap -> [ItemNameMap] -> [ItemNameMap]
forall a. a -> [a] -> [a]
: [ItemNameMap]
is, [Result ()]
ws)) ([], []) [ItemNameMap]
rawIms
                        expIms :: [Either (Result ()) ItemNameMap]
expIms = (ItemNameMap -> Either (Result ()) ItemNameMap)
-> [ItemNameMap] -> [Either (Result ()) ItemNameMap]
forall a b. (a -> b) -> [a] -> [b]
map (FilePath
-> FilePath -> ItemNameMap -> Either (Result ()) ItemNameMap
expandCurieItemNameMap FilePath
fn FilePath
currFn) [ItemNameMap]
ims
                        leftExpIms :: [Result ()]
leftExpIms = [Either (Result ()) ItemNameMap] -> [Result ()]
forall a b. [Either a b] -> [a]
lefts [Either (Result ()) ItemNameMap]
expIms
                    in if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Result ()] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Result ()]
leftExpIms
                        then ([], [Result ()]
leftExpIms, [ItemNameMap] -> [IRI]
itemNameMapsToIRIs [ItemNameMap]
ims)
                        else ([Either (Result ()) ItemNameMap] -> [ItemNameMap]
forall a b. [Either a b] -> [b]
rights [Either (Result ()) ItemNameMap]
expIms, [Result ()]
warns, [ItemNameMap] -> [IRI]
itemNameMapsToIRIs [ItemNameMap]
ims)
                  UniqueItem i :: IRI
i ->
                    let is :: [IRI]
is = GlobalEnv -> [IRI]
forall k a. Map k a -> [k]
Map.keys (GlobalEnv -> [IRI]) -> GlobalEnv -> [IRI]
forall a b. (a -> b) -> a -> b
$ DGraph -> GlobalEnv
globalEnv DGraph
dg'
                        ks :: [IRI]
ks = case [IRI]
is of
                               [_] -> [IRI]
is
                               _ -> (IRI -> Bool) -> [IRI] -> [IRI]
forall a. (a -> Bool) -> [a] -> [a]
filter (IRI -> IRI -> Bool
forall a. Eq a => a -> a -> Bool
== LibName -> IRI
getLibId LibName
ln') [IRI]
is
                    in case [IRI]
ks of
                    [j :: IRI
j] -> case GlobalAnnos -> ExpOverrides -> IRI -> Maybe IRI
expCurie (DGraph -> GlobalAnnos
globalAnnos DGraph
dg) ExpOverrides
eo IRI
i of
                      Nothing -> ([], [IRI -> Result ()
forall a. IRI -> Result a
prefixErrorIRI IRI
i], [IRI
i])
                      Just expI :: IRI
expI -> case GlobalAnnos -> ExpOverrides -> IRI -> Maybe IRI
expCurie (DGraph -> GlobalAnnos
globalAnnos DGraph
dg) ExpOverrides
eo IRI
j of
                        Nothing -> ([], [IRI -> Result ()
forall a. IRI -> Result a
prefixErrorIRI IRI
j], [IRI
i, IRI
j])
                        Just expJ :: IRI
expJ ->
                            ([IRI -> Maybe IRI -> ItemNameMap
ItemNameMap IRI
expJ (IRI -> Maybe IRI
forall a. a -> Maybe a
Just IRI
expI)], [], [IRI
i, IRI
j])
                    _ ->
                     ( []
                     , [ FilePath -> LibName -> Result ()
forall a b. (GetRange a, Pretty a) => FilePath -> a -> Result b
mkError ("non-unique name within imported library: "
                                  FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate ", " ((IRI -> FilePath) -> [IRI] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map IRI -> FilePath
forall a. Show a => a -> FilePath
show [IRI]
is))
                         LibName
ln'], [])
                additionalEo :: ExpOverrides
additionalEo = [(IRI, FilePath)] -> ExpOverrides
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(IRI, FilePath)] -> ExpOverrides)
-> [(IRI, FilePath)] -> ExpOverrides
forall a b. (a -> b) -> a -> b
$ (IRI -> (IRI, FilePath)) -> [IRI] -> [(IRI, FilePath)]
forall a b. (a -> b) -> [a] -> [b]
map (\ o :: IRI
o -> (IRI
o, FilePath
fn)) [IRI]
origItems
                eo' :: ExpOverrides
eo' = (FilePath -> FilePath -> FilePath)
-> ExpOverrides -> ExpOverrides -> ExpOverrides
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith (\ _ p2 :: FilePath
p2 -> FilePath
p2) ExpOverrides
eo ExpOverrides
additionalEo
            (Result () -> ResultT IO ()) -> [Result ()] -> ResultT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Result () -> ResultT IO ()
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR [Result ()]
errs
            DGraph
dg1 <- Result DGraph -> ResultT IO DGraph
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result DGraph -> ResultT IO DGraph)
-> Result DGraph -> ResultT IO DGraph
forall a b. (a -> b) -> a -> b
$ LibEnv
-> LibName -> DGraph -> DGraph -> [ItemNameMap] -> Result DGraph
anaItemNamesOrMaps LibEnv
libenv' LibName
ln' DGraph
dg' DGraph
dg0 [ItemNameMap]
realItems
            (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. Monad m => a -> m a
return (LIB_ITEM
itm, DGraph
dg1, LibEnv
libenv', LogicGraph
lg, ExpOverrides
eo')
  Newlogic_defn ld :: LogicDef
ld _ -> IO (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. m (Result a) -> ResultT m a
ResultT (IO (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
 -> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
-> IO (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a b. (a -> b) -> a -> b
$ do
    DGraph
dg' <- LogicDef -> DGraph -> IO DGraph
anaLogicDef LogicDef
ld DGraph
dg
    Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> IO (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
 -> IO
      (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)))
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> IO (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
forall a b. (a -> b) -> a -> b
$ [Diagnosis]
-> Maybe (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a. [Diagnosis] -> Maybe a -> Result a
Result [] (Maybe (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
 -> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
-> Maybe (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a b. (a -> b) -> a -> b
$ (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> Maybe (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a. a -> Maybe a
Just (LIB_ITEM
itm, DGraph
dg', LibEnv
libenv, LogicGraph
lg, ExpOverrides
eo)
  Newcomorphism_defn com :: ComorphismDef
com _ -> IO (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. m (Result a) -> ResultT m a
ResultT (IO (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
 -> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
-> IO (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a b. (a -> b) -> a -> b
$ do
    DGraph
dg' <- ComorphismDef -> DGraph -> IO DGraph
anaComorphismDef ComorphismDef
com DGraph
dg
    Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> IO (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
 -> IO
      (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)))
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> IO (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
forall a b. (a -> b) -> a -> b
$ [Diagnosis]
-> Maybe (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a. [Diagnosis] -> Maybe a -> Result a
Result [] (Maybe (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
 -> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
-> Maybe (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a b. (a -> b) -> a -> b
$ (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> Maybe (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a. a -> Maybe a
Just (LIB_ITEM
itm, DGraph
dg', LibEnv
libenv, LogicGraph
lg, ExpOverrides
eo)
  _ -> (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. Monad m => a -> m a
return (LIB_ITEM
itm, DGraph
dg, LibEnv
libenv, LogicGraph
lg, ExpOverrides
eo)

symbolsOf :: LogicGraph -> G_sign -> G_sign -> [CORRESPONDENCE]
  -> Result (Set.Set (G_symbol, G_symbol))
symbolsOf :: LogicGraph
-> G_sign
-> G_sign
-> [CORRESPONDENCE]
-> Result (Set (G_symbol, G_symbol))
symbolsOf lg :: LogicGraph
lg gs1 :: G_sign
gs1@(G_sign l1 :: lid
l1 (ExtSign sig1 :: sign
sig1 sys1 :: Set symbol
sys1) _)
 gs2 :: G_sign
gs2@(G_sign l2 :: lid
l2 (ExtSign sig2 :: sign
sig2 sys2 :: Set symbol
sys2) _) corresps :: [CORRESPONDENCE]
corresps =
 case [CORRESPONDENCE]
corresps of
  [] -> Set (G_symbol, G_symbol) -> Result (Set (G_symbol, G_symbol))
forall (m :: * -> *) a. Monad m => a -> m a
return Set (G_symbol, G_symbol)
forall a. Set a
Set.empty
  c :: CORRESPONDENCE
c : corresps' :: [CORRESPONDENCE]
corresps' -> case CORRESPONDENCE
c of
    Default_correspondence -> LogicGraph
-> G_sign
-> G_sign
-> [CORRESPONDENCE]
-> Result (Set (G_symbol, G_symbol))
symbolsOf LogicGraph
lg G_sign
gs1 G_sign
gs2 [CORRESPONDENCE]
corresps' -- TO DO
    Correspondence_block _ _ cs :: [CORRESPONDENCE]
cs -> do
      Set (G_symbol, G_symbol)
sPs1 <- LogicGraph
-> G_sign
-> G_sign
-> [CORRESPONDENCE]
-> Result (Set (G_symbol, G_symbol))
symbolsOf LogicGraph
lg G_sign
gs1 G_sign
gs2 [CORRESPONDENCE]
cs
      Set (G_symbol, G_symbol)
sPs2 <- LogicGraph
-> G_sign
-> G_sign
-> [CORRESPONDENCE]
-> Result (Set (G_symbol, G_symbol))
symbolsOf LogicGraph
lg G_sign
gs1 G_sign
gs2 [CORRESPONDENCE]
corresps'
      Set (G_symbol, G_symbol) -> Result (Set (G_symbol, G_symbol))
forall (m :: * -> *) a. Monad m => a -> m a
return (Set (G_symbol, G_symbol) -> Result (Set (G_symbol, G_symbol)))
-> Set (G_symbol, G_symbol) -> Result (Set (G_symbol, G_symbol))
forall a b. (a -> b) -> a -> b
$ Set (G_symbol, G_symbol)
-> Set (G_symbol, G_symbol) -> Set (G_symbol, G_symbol)
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (G_symbol, G_symbol)
sPs1 Set (G_symbol, G_symbol)
sPs2
    Single_correspondence _ (G_symb_items_list lid1 :: lid
lid1 sis1 :: [symb_items]
sis1)
        (G_symb_items_list lid2 :: lid
lid2 sis2 :: [symb_items]
sis2) _ _ -> do
      [symb_items]
ss1 <- lid -> lid -> FilePath -> [symb_items] -> Result [symb_items]
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> FilePath -> [symb_items1] -> m [symb_items2]
coerceSymbItemsList lid
lid1 lid
l1 "symbolsOf1" [symb_items]
sis1
      [raw_symbol]
rs1 <- lid -> sign -> [symb_items] -> Result [raw_symbol]
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> [symb_items] -> Result [raw_symbol]
stat_symb_items lid
l1 sign
sig1 [symb_items]
ss1
      [symb_items]
ss2 <- lid -> lid -> FilePath -> [symb_items] -> Result [symb_items]
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> FilePath -> [symb_items1] -> m [symb_items2]
coerceSymbItemsList lid
lid2 lid
l2 "symbolsOf2" [symb_items]
sis2
      [raw_symbol]
rs2 <- lid -> sign -> [symb_items] -> Result [raw_symbol]
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> [symb_items] -> Result [raw_symbol]
stat_symb_items lid
l2 sign
sig2 [symb_items]
ss2
      (G_symbol, G_symbol)
p <- case ([raw_symbol]
rs1, [raw_symbol]
rs2) of
        ([r1 :: raw_symbol
r1], [r2 :: raw_symbol
r2]) ->
         case
            ( (symbol -> Bool) -> [symbol] -> [symbol]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ sy :: symbol
sy -> lid -> symbol -> raw_symbol -> Bool
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> symbol -> raw_symbol -> Bool
matches lid
l1 symbol
sy raw_symbol
r1) ([symbol] -> [symbol]) -> [symbol] -> [symbol]
forall a b. (a -> b) -> a -> b
$ Set symbol -> [symbol]
forall a. Set a -> [a]
Set.toList Set symbol
sys1
            , (symbol -> Bool) -> [symbol] -> [symbol]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ sy :: symbol
sy -> lid -> symbol -> raw_symbol -> Bool
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> symbol -> raw_symbol -> Bool
matches lid
l2 symbol
sy raw_symbol
r2) ([symbol] -> [symbol]) -> [symbol] -> [symbol]
forall a b. (a -> b) -> a -> b
$ Set symbol -> [symbol]
forall a. Set a -> [a]
Set.toList Set symbol
sys2) of
          ([s1 :: symbol
s1], [s2 :: symbol
s2]) ->
            (G_symbol, G_symbol) -> Result (G_symbol, G_symbol)
forall (m :: * -> *) a. Monad m => a -> m a
return (lid -> symbol -> G_symbol
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> symbol -> G_symbol
G_symbol lid
l1 symbol
s1, lid -> symbol -> G_symbol
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> symbol -> G_symbol
G_symbol lid
l2 symbol
s2)
          (ll1 :: [symbol]
ll1, ll2 :: [symbol]
ll2) -> 
                 (G_symbol, G_symbol)
-> FilePath -> Range -> Result (G_symbol, G_symbol)
forall a. a -> FilePath -> Range -> Result a
plain_error (lid -> symbol -> G_symbol
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> symbol -> G_symbol
G_symbol lid
l1 (symbol -> G_symbol) -> symbol -> G_symbol
forall a b. (a -> b) -> a -> b
$ [symbol] -> symbol
forall a. [a] -> a
head [symbol]
ll1, lid -> symbol -> G_symbol
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> symbol -> G_symbol
G_symbol lid
l2 (symbol -> G_symbol) -> symbol -> G_symbol
forall a b. (a -> b) -> a -> b
$ [symbol] -> symbol
forall a. [a] -> a
head [symbol]
ll2) -- this is a hack!
                  ("Missing or non-unique symbol match " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ 
                   "for correspondence\nMatches for first symbol: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ 
                   [raw_symbol] -> FilePath -> FilePath
forall a. Pretty a => a -> FilePath -> FilePath
showDoc [raw_symbol]
rs1 "\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                   [symbol] -> FilePath -> FilePath
forall a. Pretty a => a -> FilePath -> FilePath
showDoc [symbol]
ll1 "\nMatches for second symbol: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ 
                   [raw_symbol] -> FilePath -> FilePath
forall a. Pretty a => a -> FilePath -> FilePath
showDoc [raw_symbol]
rs2 "\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                   [symbol] -> FilePath -> FilePath
forall a. Pretty a => a -> FilePath -> FilePath
showDoc [symbol]
ll2 "\n") 
                  Range
nullRange
        _ -> FilePath -> Result (G_symbol, G_symbol)
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
Fail.fail (FilePath -> Result (G_symbol, G_symbol))
-> FilePath -> Result (G_symbol, G_symbol)
forall a b. (a -> b) -> a -> b
$ "non-unique raw symbols"
      Set (G_symbol, G_symbol)
ps <- LogicGraph
-> G_sign
-> G_sign
-> [CORRESPONDENCE]
-> Result (Set (G_symbol, G_symbol))
symbolsOf LogicGraph
lg G_sign
gs1 G_sign
gs2 [CORRESPONDENCE]
corresps'
      Set (G_symbol, G_symbol) -> Result (Set (G_symbol, G_symbol))
forall (m :: * -> *) a. Monad m => a -> m a
return (Set (G_symbol, G_symbol) -> Result (Set (G_symbol, G_symbol)))
-> Set (G_symbol, G_symbol) -> Result (Set (G_symbol, G_symbol))
forall a b. (a -> b) -> a -> b
$ (G_symbol, G_symbol)
-> Set (G_symbol, G_symbol) -> Set (G_symbol, G_symbol)
forall a. Ord a => a -> Set a -> Set a
Set.insert (G_symbol, G_symbol)
p Set (G_symbol, G_symbol)
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 :: LogicGraph
-> LibName
-> LibEnv
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> IRI
-> ENTAIL_TYPE
-> Range
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
anaEntailmentDefn lg :: LogicGraph
lg ln :: LibName
ln libEnv :: LibEnv
libEnv dg :: DGraph
dg opts :: HetcatsOpts
opts eo :: ExpOverrides
eo en :: IRI
en et :: ENTAIL_TYPE
et pos :: Range
pos = do
  case ENTAIL_TYPE
et of
   Entail_type on1 :: OmsOrNetwork
on1 on2 :: OmsOrNetwork
on2 _ -> do
     case (OmsOrNetwork
on1, OmsOrNetwork
on2) of
      (MkOms asp1 :: Annoted SPEC
asp1, MkOms asp2 :: Annoted SPEC
asp2) -> do
        let spS :: SPEC
spS = Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
asp1
            spT :: SPEC
spT = Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
asp2
            name :: NodeName
name = IRI -> NodeName
makeName IRI
en
        AnyLogic
l <- FilePath -> LogicGraph -> Result AnyLogic
forall (m :: * -> *).
MonadFail m =>
FilePath -> LogicGraph -> m AnyLogic
lookupCurrentLogic "ENTAIL_DEFN" LogicGraph
lg
        (_spSrc' :: SPEC
_spSrc', srcNsig :: NodeSig
srcNsig, dg' :: DGraph
dg') <- Bool
-> Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> SPEC
-> Range
-> Result (SPEC, NodeSig, DGraph)
anaSpec Bool
False Bool
True LogicGraph
lg LibEnv
libEnv LibName
ln 
                          DGraph
dg (AnyLogic -> MaybeNode
EmptyNode AnyLogic
l) (FilePath -> NodeName -> NodeName
extName "Source" NodeName
name)
                          HetcatsOpts
opts ExpOverrides
eo SPEC
spS (Range -> Result (SPEC, NodeSig, DGraph))
-> Range -> Result (SPEC, NodeSig, DGraph)
forall a b. (a -> b) -> a -> b
$ SPEC -> Range
forall a. GetRange a => a -> Range
getRange SPEC
spS
        (_spTgt' :: SPEC
_spTgt', tgtNsig :: NodeSig
tgtNsig, dg'' :: DGraph
dg'') <- Bool
-> Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> SPEC
-> Range
-> Result (SPEC, NodeSig, DGraph)
anaSpec Bool
True Bool
True LogicGraph
lg LibEnv
libEnv LibName
ln 
                          DGraph
dg' (AnyLogic -> MaybeNode
EmptyNode AnyLogic
l)
                          (FilePath -> NodeName -> NodeName
extName "Target" NodeName
name) HetcatsOpts
opts ExpOverrides
eo SPEC
spT (Range -> Result (SPEC, NodeSig, DGraph))
-> Range -> Result (SPEC, NodeSig, DGraph)
forall a b. (a -> b) -> a -> b
$ SPEC -> Range
forall a. GetRange a => a -> Range
getRange SPEC
spT
        GMorphism
incl <- LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion LogicGraph
lg (NodeSig -> G_sign
getSig NodeSig
tgtNsig) (NodeSig -> G_sign
getSig NodeSig
srcNsig)
        let  dg3 :: DGraph
dg3 = DGraph
-> GMorphism -> DGLinkType -> DGLinkOrigin -> Int -> Int -> DGraph
insLink DGraph
dg'' GMorphism
incl DGLinkType
globalThm DGLinkOrigin
SeeSource
                   (NodeSig -> Int
getNode NodeSig
tgtNsig) (NodeSig -> Int
getNode NodeSig
srcNsig)
             gsig :: GenSig
gsig = MaybeNode -> [NodeSig] -> MaybeNode -> GenSig
GenSig (AnyLogic -> MaybeNode
EmptyNode AnyLogic
l) [] (AnyLogic -> MaybeNode
EmptyNode AnyLogic
l)
        let vsig :: ExtViewSig
vsig = NodeSig -> GMorphism -> ExtGenSig -> ExtViewSig
ExtViewSig NodeSig
srcNsig GMorphism
incl (ExtGenSig -> ExtViewSig) -> ExtGenSig -> ExtViewSig
forall a b. (a -> b) -> a -> b
$ GenSig -> NodeSig -> ExtGenSig
ExtGenSig GenSig
gsig NodeSig
tgtNsig
        (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. Monad m => a -> m a
return (IRI -> ENTAIL_TYPE -> Range -> LIB_ITEM
Entail_defn IRI
en ENTAIL_TYPE
et Range
pos, DGraph
dg3{
                  globalEnv :: GlobalEnv
globalEnv = IRI -> GlobalEntry -> GlobalEnv -> GlobalEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert IRI
en (Bool -> ExtViewSig -> GlobalEntry
ViewOrStructEntry Bool
True ExtViewSig
vsig)
                              (GlobalEnv -> GlobalEnv) -> GlobalEnv -> GlobalEnv
forall a b. (a -> b) -> a -> b
$ DGraph -> GlobalEnv
globalEnv DGraph
dg3},
                LibEnv
libEnv, LogicGraph
lg, ExpOverrides
eo)
      _ -> FilePath
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
Fail.fail "entailment between networks not supported yet"
   _ -> FilePath
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. MonadFail m => FilePath -> m a
Fail.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 :: LogicGraph
-> LibName
-> LibEnv
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> IRI
-> GENERICITY
-> VIEW_TYPE
-> [G_mapping]
-> Range
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
anaViewDefn lg :: LogicGraph
lg ln :: LibName
ln libenv :: LibEnv
libenv dg :: DGraph
dg opts :: HetcatsOpts
opts eo :: ExpOverrides
eo vn :: IRI
vn gen :: GENERICITY
gen vt :: VIEW_TYPE
vt gsis :: [G_mapping]
gsis pos :: Range
pos = do
  let vName :: NodeName
vName = IRI -> NodeName
makeName IRI
vn
  (gen' :: GENERICITY
gen', gsig :: GenSig
gsig@(GenSig _ _ allparams :: MaybeNode
allparams), dg' :: DGraph
dg') <-
       LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> NodeName
-> GENERICITY
-> Result (GENERICITY, GenSig, DGraph)
anaGenericity LogicGraph
lg LibEnv
libenv LibName
ln DGraph
dg HetcatsOpts
opts ExpOverrides
eo NodeName
vName GENERICITY
gen
  (vt' :: VIEW_TYPE
vt', (src :: NodeSig
src@(NodeSig nodeS :: Int
nodeS gsigmaS :: G_sign
gsigmaS)
        , tar :: NodeSig
tar@(NodeSig nodeT :: Int
nodeT gsigmaT :: G_sign
gsigmaT@(G_sign lidT :: lid
lidT _ _))), dg'' :: DGraph
dg'') <-
       LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> HetcatsOpts
-> ExpOverrides
-> NodeName
-> VIEW_TYPE
-> Result (VIEW_TYPE, (NodeSig, NodeSig), DGraph)
anaViewType LogicGraph
lg LibEnv
libenv LibName
ln DGraph
dg' MaybeNode
allparams HetcatsOpts
opts ExpOverrides
eo NodeName
vName VIEW_TYPE
vt
  let genv :: GlobalEnv
genv = DGraph -> GlobalEnv
globalEnv DGraph
dg''
  if IRI -> GlobalEnv -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member IRI
vn GlobalEnv
genv
    then (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> FilePath
-> Range
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a. a -> FilePath -> Range -> Result a
plain_error (IRI -> GENERICITY -> VIEW_TYPE -> [G_mapping] -> Range -> LIB_ITEM
View_defn IRI
vn GENERICITY
gen' VIEW_TYPE
vt' [G_mapping]
gsis Range
pos, DGraph
dg'', LibEnv
libenv, LogicGraph
lg, ExpOverrides
eo)
                    (FilePath -> FilePath
alreadyDefined (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ IRI -> FilePath
iriToStringUnsecure IRI
vn) Range
pos
    else do
      let (tsis :: [G_mapping]
tsis, hsis :: [G_mapping]
hsis) = [G_mapping] -> ([G_mapping], [G_mapping])
partitionGmaps [G_mapping]
gsis
      (gsigmaS' :: G_sign
gsigmaS', tmor :: GMorphism
tmor) <- if [G_mapping] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [G_mapping]
tsis then do
          (gsigmaS' :: G_sign
gsigmaS', imor :: AnyComorphism
imor) <- LogicGraph -> G_sign -> AnyLogic -> Result (G_sign, AnyComorphism)
gSigCoerce LogicGraph
lg G_sign
gsigmaS (lid -> AnyLogic
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> AnyLogic
Logic lid
lidT)
          GMorphism
tmor <- AnyComorphism -> G_sign -> Result GMorphism
gEmbedComorphism AnyComorphism
imor G_sign
gsigmaS
          (G_sign, GMorphism) -> Result (G_sign, GMorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (G_sign
gsigmaS', GMorphism
tmor)
        else do
          GMorphism
mor <- LogicGraph
-> MaybeNode
-> G_sign
-> HetcatsOpts
-> RENAMING
-> Result GMorphism
anaRenaming LogicGraph
lg MaybeNode
allparams G_sign
gsigmaS HetcatsOpts
opts ([G_mapping] -> Range -> RENAMING
Renaming [G_mapping]
tsis Range
pos)
          let gsigmaS'' :: G_sign
gsigmaS'' = GMorphism -> G_sign
forall object morphism.
Category object morphism =>
morphism -> object
cod GMorphism
mor
          (gsigmaS' :: G_sign
gsigmaS', imor :: AnyComorphism
imor) <- LogicGraph -> G_sign -> AnyLogic -> Result (G_sign, AnyComorphism)
gSigCoerce LogicGraph
lg G_sign
gsigmaS'' (lid -> AnyLogic
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> AnyLogic
Logic lid
lidT)
          GMorphism
tmor <- AnyComorphism -> G_sign -> Result GMorphism
gEmbedComorphism AnyComorphism
imor G_sign
gsigmaS''
          GMorphism
fmor <- GMorphism -> GMorphism -> Result GMorphism
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
comp GMorphism
mor GMorphism
tmor
          (G_sign, GMorphism) -> Result (G_sign, GMorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (G_sign
gsigmaS', GMorphism
fmor)
      GMorphism
emor <- (G_morphism -> GMorphism) -> Result G_morphism -> Result GMorphism
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap G_morphism -> GMorphism
gEmbed (Result G_morphism -> Result GMorphism)
-> Result G_morphism -> Result GMorphism
forall a b. (a -> b) -> a -> b
$ LogicGraph
-> HetcatsOpts
-> Range
-> G_sign
-> G_sign
-> [G_mapping]
-> Result G_morphism
anaGmaps LogicGraph
lg HetcatsOpts
opts Range
pos G_sign
gsigmaS' G_sign
gsigmaT [G_mapping]
hsis
      GMorphism
gmor <- GMorphism -> GMorphism -> Result GMorphism
forall object morphism.
Category object morphism =>
morphism -> morphism -> Result morphism
comp GMorphism
tmor GMorphism
emor
      let vsig :: ExtViewSig
vsig = NodeSig -> GMorphism -> ExtGenSig -> ExtViewSig
ExtViewSig NodeSig
src GMorphism
gmor (ExtGenSig -> ExtViewSig) -> ExtGenSig -> ExtViewSig
forall a b. (a -> b) -> a -> b
$ GenSig -> NodeSig -> ExtGenSig
ExtGenSig GenSig
gsig NodeSig
tar
          voidView :: Bool
voidView = Int
nodeS Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
nodeT Bool -> Bool -> Bool
&& GMorphism -> Bool
forall object morphism.
Category object morphism =>
morphism -> Bool
isInclusion GMorphism
gmor
      Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
voidView (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ () -> FilePath -> Range -> Result ()
forall a. a -> FilePath -> Range -> Result a
warning ()
        ("identity mapping of source to same target for view: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
            IRI -> FilePath
iriToStringUnsecure IRI
vn) Range
pos
      (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. Monad m => a -> m a
return (IRI -> GENERICITY -> VIEW_TYPE -> [G_mapping] -> Range -> LIB_ITEM
View_defn IRI
vn GENERICITY
gen' VIEW_TYPE
vt' [G_mapping]
gsis Range
pos,
                (if Bool
voidView then DGraph
dg'' else DGraph
-> GMorphism -> DGLinkType -> DGLinkOrigin -> Int -> Int -> DGraph
insLink DGraph
dg'' GMorphism
gmor DGLinkType
globalThm
                 (IRI -> Fitted -> DGLinkOrigin
DGLinkView IRI
vn (Fitted -> DGLinkOrigin) -> Fitted -> DGLinkOrigin
forall a b. (a -> b) -> a -> b
$ [G_mapping] -> Fitted
Fitted [G_mapping]
gsis) Int
nodeS Int
nodeT)
                -- 'LeftOpen' for conserv correct?
                { globalEnv :: GlobalEnv
globalEnv = IRI -> GlobalEntry -> GlobalEnv -> GlobalEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert IRI
vn (Bool -> ExtViewSig -> GlobalEntry
ViewOrStructEntry Bool
True ExtViewSig
vsig) GlobalEnv
genv }
               , LibEnv
libenv, LogicGraph
lg, ExpOverrides
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 :: LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> HetcatsOpts
-> ExpOverrides
-> NodeName
-> VIEW_TYPE
-> Result (VIEW_TYPE, (NodeSig, NodeSig), DGraph)
anaViewType lg :: LogicGraph
lg libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg parSig :: MaybeNode
parSig opts :: HetcatsOpts
opts eo :: ExpOverrides
eo name :: NodeName
name (View_type aspSrc :: Annoted SPEC
aspSrc aspTar :: Annoted SPEC
aspTar pos :: Range
pos) = do
  -- trace "called anaViewType" $ do
  AnyLogic
l <- FilePath -> LogicGraph -> Result AnyLogic
forall (m :: * -> *).
MonadFail m =>
FilePath -> LogicGraph -> m AnyLogic
lookupCurrentLogic "VIEW_TYPE" LogicGraph
lg
  let spS :: SPEC
spS = Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
aspSrc
      spT :: SPEC
spT = Annoted SPEC -> SPEC
forall a. Annoted a -> a
item Annoted SPEC
aspTar
  (spSrc' :: SPEC
spSrc', srcNsig :: NodeSig
srcNsig, dg' :: DGraph
dg') <- Bool
-> Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> SPEC
-> Range
-> Result (SPEC, NodeSig, DGraph)
anaSpec Bool
False Bool
True LogicGraph
lg LibEnv
libEnv LibName
ln DGraph
dg (AnyLogic -> MaybeNode
EmptyNode AnyLogic
l)
    (FilePath -> NodeName -> NodeName
extName "Source" NodeName
name) HetcatsOpts
opts ExpOverrides
eo SPEC
spS (Range -> Result (SPEC, NodeSig, DGraph))
-> Range -> Result (SPEC, NodeSig, DGraph)
forall a b. (a -> b) -> a -> b
$ SPEC -> Range
forall a. GetRange a => a -> Range
getRange SPEC
spS
  (spTar' :: SPEC
spTar', tarNsig :: NodeSig
tarNsig, dg'' :: DGraph
dg'') <- Bool
-> Bool
-> LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> NodeName
-> HetcatsOpts
-> ExpOverrides
-> SPEC
-> Range
-> Result (SPEC, NodeSig, DGraph)
anaSpec Bool
True Bool
True LogicGraph
lg LibEnv
libEnv LibName
ln DGraph
dg' MaybeNode
parSig
    (FilePath -> NodeName -> NodeName
extName "Target" NodeName
name) HetcatsOpts
opts ExpOverrides
eo SPEC
spT (Range -> Result (SPEC, NodeSig, DGraph))
-> Range -> Result (SPEC, NodeSig, DGraph)
forall a b. (a -> b) -> a -> b
$ SPEC -> Range
forall a. GetRange a => a -> Range
getRange SPEC
spT
  (VIEW_TYPE, (NodeSig, NodeSig), DGraph)
-> Result (VIEW_TYPE, (NodeSig, NodeSig), DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (Annoted SPEC -> Annoted SPEC -> Range -> VIEW_TYPE
View_type (SPEC -> Annoted SPEC -> Annoted SPEC
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted SPEC
spSrc' Annoted SPEC
aspSrc)
                    (SPEC -> Annoted SPEC -> Annoted SPEC
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted SPEC
spTar' Annoted SPEC
aspTar)
                    Range
pos,
          (NodeSig
srcNsig, NodeSig
tarNsig), DGraph
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 :: LogicGraph
-> LibName
-> LibEnv
-> DGraph
-> HetcatsOpts
-> ExpOverrides
-> IRI
-> Maybe ALIGN_ARITIES
-> VIEW_TYPE
-> [CORRESPONDENCE]
-> Range
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
anaAlignDefn lg :: LogicGraph
lg ln :: LibName
ln libenv :: LibEnv
libenv dg :: DGraph
dg opts :: HetcatsOpts
opts eo :: ExpOverrides
eo an :: IRI
an arities :: Maybe ALIGN_ARITIES
arities atype :: VIEW_TYPE
atype acorresps :: [CORRESPONDENCE]
acorresps pos :: Range
pos = do
     AnyLogic
l <- FilePath -> LogicGraph -> ResultT IO AnyLogic
forall (m :: * -> *).
MonadFail m =>
FilePath -> LogicGraph -> m AnyLogic
lookupCurrentLogic "Align_defn" LogicGraph
lg
     (atype' :: VIEW_TYPE
atype', (src :: NodeSig
src, tar :: NodeSig
tar), dg' :: DGraph
dg') <- Result (VIEW_TYPE, (NodeSig, NodeSig), DGraph)
-> ResultT IO (VIEW_TYPE, (NodeSig, NodeSig), DGraph)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR
       (Result (VIEW_TYPE, (NodeSig, NodeSig), DGraph)
 -> ResultT IO (VIEW_TYPE, (NodeSig, NodeSig), DGraph))
-> Result (VIEW_TYPE, (NodeSig, NodeSig), DGraph)
-> ResultT IO (VIEW_TYPE, (NodeSig, NodeSig), DGraph)
forall a b. (a -> b) -> a -> b
$ LogicGraph
-> LibEnv
-> LibName
-> DGraph
-> MaybeNode
-> HetcatsOpts
-> ExpOverrides
-> NodeName
-> VIEW_TYPE
-> Result (VIEW_TYPE, (NodeSig, NodeSig), DGraph)
anaViewType LogicGraph
lg LibEnv
libenv LibName
ln DGraph
dg (AnyLogic -> MaybeNode
EmptyNode AnyLogic
l) HetcatsOpts
opts ExpOverrides
eo (IRI -> NodeName
makeName IRI
an) VIEW_TYPE
atype
     let gsig1 :: G_sign
gsig1 = NodeSig -> G_sign
getSig NodeSig
src
         gsig2 :: G_sign
gsig2 = NodeSig -> G_sign
getSig NodeSig
tar
     case (G_sign
gsig1, G_sign
gsig2) of
      (G_sign lid1 :: lid
lid1 _ _, G_sign lid2 :: lid
lid2 _ _) ->
       if lid -> AnyLogic
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> AnyLogic
Logic lid
lid1 AnyLogic -> AnyLogic -> Bool
forall a. Eq a => a -> a -> Bool
== lid -> AnyLogic
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> AnyLogic
Logic lid
lid2 then do
        -- arities TO DO
        Set (G_symbol, G_symbol)
pairsSet <- Result (Set (G_symbol, G_symbol))
-> ResultT IO (Set (G_symbol, G_symbol))
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result (Set (G_symbol, G_symbol))
 -> ResultT IO (Set (G_symbol, G_symbol)))
-> Result (Set (G_symbol, G_symbol))
-> ResultT IO (Set (G_symbol, G_symbol))
forall a b. (a -> b) -> a -> b
$ LogicGraph
-> G_sign
-> G_sign
-> [CORRESPONDENCE]
-> Result (Set (G_symbol, G_symbol))
symbolsOf LogicGraph
lg G_sign
gsig1 G_sign
gsig2 [CORRESPONDENCE]
acorresps
        let leftList :: [G_symbol]
leftList = ((G_symbol, G_symbol) -> G_symbol)
-> [(G_symbol, G_symbol)] -> [G_symbol]
forall a b. (a -> b) -> [a] -> [b]
map (G_symbol, G_symbol) -> G_symbol
forall a b. (a, b) -> a
fst ([(G_symbol, G_symbol)] -> [G_symbol])
-> [(G_symbol, G_symbol)] -> [G_symbol]
forall a b. (a -> b) -> a -> b
$ Set (G_symbol, G_symbol) -> [(G_symbol, G_symbol)]
forall a. Set a -> [a]
Set.toList Set (G_symbol, G_symbol)
pairsSet
            rightList :: [G_symbol]
rightList = ((G_symbol, G_symbol) -> G_symbol)
-> [(G_symbol, G_symbol)] -> [G_symbol]
forall a b. (a -> b) -> [a] -> [b]
map (G_symbol, G_symbol) -> G_symbol
forall a b. (a, b) -> b
snd ([(G_symbol, G_symbol)] -> [G_symbol])
-> [(G_symbol, G_symbol)] -> [G_symbol]
forall a b. (a -> b) -> a -> b
$ Set (G_symbol, G_symbol) -> [(G_symbol, G_symbol)]
forall a. Set a -> [a]
Set.toList Set (G_symbol, G_symbol)
pairsSet
            isTotal :: G_sign -> [G_symbol] -> Bool
isTotal gsig :: G_sign
gsig sList :: [G_symbol]
sList = [G_symbol] -> Set G_symbol
forall a. Ord a => [a] -> Set a
Set.fromList [G_symbol]
sList Set G_symbol -> Set G_symbol -> Bool
forall a. Eq a => a -> a -> Bool
== G_sign -> Set G_symbol
symsOfGsign G_sign
gsig
            isInjective :: [a] -> Bool
isInjective sList :: [a]
sList = [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
sList Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([a] -> [a]
forall a. Eq a => [a] -> [a]
nub [a]
sList)
            checkArity :: [G_symbol] -> [a] -> G_sign -> ALIGN_ARITY -> Bool
checkArity sList1 :: [G_symbol]
sList1 sList2 :: [a]
sList2 gsig :: G_sign
gsig arity :: ALIGN_ARITY
arity = case ALIGN_ARITY
arity of
              AA_InjectiveAndTotal -> G_sign -> [G_symbol] -> Bool
isTotal G_sign
gsig [G_symbol]
sList1 Bool -> Bool -> Bool
&&
                                      [a] -> Bool
forall a. Eq a => [a] -> Bool
isInjective [a]
sList2
              AA_Injective -> [a] -> Bool
forall a. Eq a => [a] -> Bool
isInjective [a]
sList2
              AA_Total -> G_sign -> [G_symbol] -> Bool
isTotal G_sign
gsig [G_symbol]
sList1
              _ -> Bool
True
            aCheck :: Bool
aCheck = case Maybe ALIGN_ARITIES
arities of
                      Nothing -> Bool
True
                      Just (Align_arities aleft :: ALIGN_ARITY
aleft aright :: ALIGN_ARITY
aright) ->
                       [G_symbol] -> [G_symbol] -> G_sign -> ALIGN_ARITY -> Bool
forall a.
Eq a =>
[G_symbol] -> [a] -> G_sign -> ALIGN_ARITY -> Bool
checkArity [G_symbol]
leftList [G_symbol]
rightList G_sign
gsig1 ALIGN_ARITY
aleft Bool -> Bool -> Bool
&&
                       [G_symbol] -> [G_symbol] -> G_sign -> ALIGN_ARITY -> Bool
forall a.
Eq a =>
[G_symbol] -> [a] -> G_sign -> ALIGN_ARITY -> Bool
checkArity [G_symbol]
rightList [G_symbol]
leftList G_sign
gsig2 ALIGN_ARITY
aright
        if Bool -> Bool
not Bool
aCheck then
          Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
 -> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a b. (a -> b) -> a -> b
$ FilePath
-> Maybe ALIGN_ARITIES
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a b. (GetRange a, Pretty a) => FilePath -> a -> Result b
mkError "Arities do not check" Maybe ALIGN_ARITIES
arities
         else do
         DGraph
newDg <- do
            -- (A_source, A_target, A_bridge,
            --  A_source -> O1, A_target -> O2)
            (gt1 :: G_theory
gt1, gt2 :: G_theory
gt2, gt :: G_theory
gt, gmor1 :: GMorphism
gmor1, gmor2 :: GMorphism
gmor2) <- Result (G_theory, G_theory, G_theory, GMorphism, GMorphism)
-> ResultT IO (G_theory, G_theory, G_theory, GMorphism, GMorphism)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result (G_theory, G_theory, G_theory, GMorphism, GMorphism)
 -> ResultT IO (G_theory, G_theory, G_theory, GMorphism, GMorphism))
-> Result (G_theory, G_theory, G_theory, GMorphism, GMorphism)
-> ResultT IO (G_theory, G_theory, G_theory, GMorphism, GMorphism)
forall a b. (a -> b) -> a -> b
$
                IRI
-> G_sign
-> G_sign
-> [CORRESPONDENCE]
-> Result (G_theory, G_theory, G_theory, GMorphism, GMorphism)
generateWAlign IRI
an G_sign
gsig1 G_sign
gsig2 [CORRESPONDENCE]
acorresps
            -- A_source
            let n1 :: Int
n1 = DGraph -> Int
getNewNodeDG DGraph
dg'
                labN1 :: DGNodeLab
labN1 = NodeName -> DGNodeInfo -> G_theory -> DGNodeLab
newInfoNodeLab
                         (IRI -> NodeName
makeName (IRI -> NodeName) -> IRI -> NodeName
forall a b. (a -> b) -> a -> b
$ FilePath -> IRI -> IRI
addSuffixToIRI "_source" IRI
an)
                         (DGOrigin -> DGNodeInfo
newNodeInfo DGOrigin
DGAlignment)
                         G_theory
gt1
                dg1 :: DGraph
dg1 = LNode DGNodeLab -> DGraph -> DGraph
insLNodeDG (Int
n1, DGNodeLab
labN1) DGraph
dg'
            -- A_target
                n2 :: Int
n2 = DGraph -> Int
getNewNodeDG DGraph
dg1
                labN2 :: DGNodeLab
labN2 = NodeName -> DGNodeInfo -> G_theory -> DGNodeLab
newInfoNodeLab
                         (IRI -> NodeName
makeName (IRI -> NodeName) -> IRI -> NodeName
forall a b. (a -> b) -> a -> b
$ FilePath -> IRI -> IRI
addSuffixToIRI "_target" IRI
an)
                         (DGOrigin -> DGNodeInfo
newNodeInfo DGOrigin
DGAlignment)
                         G_theory
gt2
                dg2 :: DGraph
dg2 = LNode DGNodeLab -> DGraph -> DGraph
insLNodeDG (Int
n2, DGNodeLab
labN2) DGraph
dg1
             -- A_bridge
                n :: Int
n = DGraph -> Int
getNewNodeDG DGraph
dg2
                labN :: DGNodeLab
labN = NodeName -> DGNodeInfo -> G_theory -> DGNodeLab
newInfoNodeLab
                         (IRI -> NodeName
makeName (IRI -> NodeName) -> IRI -> NodeName
forall a b. (a -> b) -> a -> b
$ FilePath -> IRI -> IRI
addSuffixToIRI "_bridge" IRI
an)
                         (DGOrigin -> DGNodeInfo
newNodeInfo DGOrigin
DGAlignment)
                         G_theory
gt
                dg3 :: DGraph
dg3 = LNode DGNodeLab -> DGraph -> DGraph
insLNodeDG (Int
n, DGNodeLab
labN) DGraph
dg2
             -- A_target-> O2
                (_, dg4 :: DGraph
dg4) = LEdge DGLinkLab -> DGraph -> (LEdge DGLinkLab, DGraph)
insLEdgeDG
                         (Int
n2, NodeSig -> Int
getNode NodeSig
tar, GMorphism -> DGLinkOrigin -> DGLinkLab
globDefLink GMorphism
gmor2 (DGLinkOrigin -> DGLinkLab) -> DGLinkOrigin -> DGLinkLab
forall a b. (a -> b) -> a -> b
$ IRI -> DGLinkOrigin
DGLinkAlign IRI
an)
                         DGraph
dg3
             -- A_source -> O1
                (_, dg5 :: DGraph
dg5) = LEdge DGLinkLab -> DGraph -> (LEdge DGLinkLab, DGraph)
insLEdgeDG
                        (Int
n1, NodeSig -> Int
getNode NodeSig
src, GMorphism -> DGLinkOrigin -> DGLinkLab
globDefLink GMorphism
gmor1 (DGLinkOrigin -> DGLinkLab) -> DGLinkOrigin -> DGLinkLab
forall a b. (a -> b) -> a -> b
$ IRI -> DGLinkOrigin
DGLinkAlign IRI
an)
                        DGraph
dg4
             -- inclusion of A_source in A_bridge
            GMorphism
incl1 <- Result GMorphism -> ResultT IO GMorphism
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result GMorphism -> ResultT IO GMorphism)
-> Result GMorphism -> ResultT IO GMorphism
forall a b. (a -> b) -> a -> b
$ LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion LogicGraph
lg (G_theory -> G_sign
signOf G_theory
gt1) (G_sign -> Result GMorphism) -> G_sign -> Result GMorphism
forall a b. (a -> b) -> a -> b
$ G_theory -> G_sign
signOf G_theory
gt
             -- inclusion of A_target in A_bridge
            GMorphism
incl2 <- Result GMorphism -> ResultT IO GMorphism
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result GMorphism -> ResultT IO GMorphism)
-> Result GMorphism -> ResultT IO GMorphism
forall a b. (a -> b) -> a -> b
$ LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion LogicGraph
lg (G_theory -> G_sign
signOf G_theory
gt2) (G_sign -> Result GMorphism) -> G_sign -> Result GMorphism
forall a b. (a -> b) -> a -> b
$ G_theory -> G_sign
signOf G_theory
gt
             -- add the inclusions to the dg
            let (_, dg6 :: DGraph
dg6) = LEdge DGLinkLab -> DGraph -> (LEdge DGLinkLab, DGraph)
insLEdgeDG
                             (Int
n1, Int
n,
                               GMorphism -> DGLinkOrigin -> DGLinkLab
globDefLink GMorphism
incl1 (DGLinkOrigin -> DGLinkLab) -> DGLinkOrigin -> DGLinkLab
forall a b. (a -> b) -> a -> b
$ IRI -> DGLinkOrigin
DGLinkAlign IRI
an) DGraph
dg5
                (_, dg7 :: DGraph
dg7) = LEdge DGLinkLab -> DGraph -> (LEdge DGLinkLab, DGraph)
insLEdgeDG
                             (Int
n2, Int
n,
                               GMorphism -> DGLinkOrigin -> DGLinkLab
globDefLink GMorphism
incl2 (DGLinkOrigin -> DGLinkLab) -> DGLinkOrigin -> DGLinkLab
forall a b. (a -> b) -> a -> b
$ IRI -> DGLinkOrigin
DGLinkAlign IRI
an) DGraph
dg6
                -- store the alignment in the global env
                asign :: AlignSig
asign = NodeSig
-> GMorphism
-> GMorphism
-> NodeSig
-> GMorphism
-> GMorphism
-> NodeSig
-> NodeSig
-> NodeSig
-> AlignSig
WAlign (Int -> G_sign -> NodeSig
NodeSig Int
n1 (G_sign -> NodeSig) -> G_sign -> NodeSig
forall a b. (a -> b) -> a -> b
$ G_theory -> G_sign
signOf G_theory
gt1) GMorphism
incl1 GMorphism
gmor1
                              (Int -> G_sign -> NodeSig
NodeSig Int
n2 (G_sign -> NodeSig) -> G_sign -> NodeSig
forall a b. (a -> b) -> a -> b
$ G_theory -> G_sign
signOf G_theory
gt2) GMorphism
incl2 GMorphism
gmor2
                              NodeSig
src NodeSig
tar (Int -> G_sign -> NodeSig
NodeSig Int
n (G_sign -> NodeSig) -> G_sign -> NodeSig
forall a b. (a -> b) -> a -> b
$ G_theory -> G_sign
signOf G_theory
gt)
            DGraph -> ResultT IO DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return DGraph
dg7 {globalEnv :: GlobalEnv
globalEnv = IRI -> GlobalEntry -> GlobalEnv -> GlobalEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert IRI
an (AlignSig -> GlobalEntry
AlignEntry AlignSig
asign)
                            (GlobalEnv -> GlobalEnv) -> GlobalEnv -> GlobalEnv
forall a b. (a -> b) -> a -> b
$ DGraph -> GlobalEnv
globalEnv DGraph
dg7}
         let itm :: LIB_ITEM
itm = IRI
-> Maybe ALIGN_ARITIES
-> VIEW_TYPE
-> [CORRESPONDENCE]
-> AlignSem
-> Range
-> LIB_ITEM
Align_defn IRI
an Maybe ALIGN_ARITIES
arities VIEW_TYPE
atype' [CORRESPONDENCE]
acorresps AlignSem
SingleDomain Range
pos
             anstr :: FilePath
anstr = IRI -> FilePath
iriToStringUnsecure IRI
an
         if IRI -> GlobalEnv -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member IRI
an (GlobalEnv -> Bool) -> GlobalEnv -> Bool
forall a b. (a -> b) -> a -> b
$ DGraph -> GlobalEnv
globalEnv DGraph
dg
          then Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
 -> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a b. (a -> b) -> a -> b
$ (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> FilePath
-> Range
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a. a -> FilePath -> Range -> Result a
plain_error (LIB_ITEM
itm, DGraph
dg, LibEnv
libenv, LogicGraph
lg, ExpOverrides
eo)
                (FilePath -> FilePath
alreadyDefined FilePath
anstr) Range
pos
          else (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. Monad m => a -> m a
return (LIB_ITEM
itm, DGraph
newDg, LibEnv
libenv, LogicGraph
lg, ExpOverrides
eo)
       else Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
 -> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides))
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
-> ResultT IO (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a b. (a -> b) -> a -> b
$ FilePath
-> Range
-> Result (LIB_ITEM, DGraph, LibEnv, LogicGraph, ExpOverrides)
forall a. FilePath -> Range -> Result a
fatal_error
         ("Alignments only work between ontologies in the same logic\n"
         FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Doc -> FilePath
forall a. Show a => a -> FilePath
show (LogicGraph -> VIEW_TYPE -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg VIEW_TYPE
atype)) Range
pos

generateWAlign :: IRI -> G_sign -> G_sign -> [CORRESPONDENCE]
               -> Result (G_theory, G_theory, G_theory, GMorphism, GMorphism)
generateWAlign :: IRI
-> G_sign
-> G_sign
-> [CORRESPONDENCE]
-> Result (G_theory, G_theory, G_theory, GMorphism, GMorphism)
generateWAlign an :: IRI
an
               (G_sign lid1 :: lid
lid1 (ExtSign ssig :: sign
ssig _) _)
               (G_sign lid2 :: lid
lid2 (ExtSign tsig :: sign
tsig _) _)
               corrs :: [CORRESPONDENCE]
corrs = do
 sign
tsig' <- lid -> lid -> FilePath -> sign -> Result sign
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> FilePath -> sign1 -> m sign2
coercePlainSign lid
lid2 lid
lid1 "coercePlainSign" sign
tsig
 -- 1. initialize
 let
     sig1 :: sign
sig1 = lid -> sign
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign
empty_signature lid
lid1
     sig2 :: sign
sig2 = lid -> sign
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign
empty_signature lid
lid1
     sig :: sign
sig = lid -> sign
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign
empty_signature lid
lid1
     phi1 :: Map k a
phi1 = Map k a
forall k a. Map k a
Map.empty
     phi2 :: Map k a
phi2 = Map k a
forall k a. Map k a
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.
 -- first we check if we must disambiguate names in the bridge ontology
 let flag :: Bool
flag = let insNames :: Set [FilePath] -> lid -> [symb_items] -> Set [FilePath]
insNames aSet :: Set [FilePath]
aSet aLid :: lid
aLid aSItems :: [symb_items]
aSItems = (Set [FilePath] -> [FilePath] -> Set [FilePath])
-> Set [FilePath] -> [[FilePath]] -> Set [FilePath]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\s :: Set [FilePath]
s n :: [FilePath]
n -> [FilePath] -> Set [FilePath] -> Set [FilePath]
forall a. Ord a => a -> Set a -> Set a
Set.insert [FilePath]
n Set [FilePath]
s) Set [FilePath]
aSet ([[FilePath]] -> Set [FilePath]) -> [[FilePath]] -> Set [FilePath]
forall a b. (a -> b) -> a -> b
$
                                              (symb_items -> [FilePath]) -> [symb_items] -> [[FilePath]]
forall a b. (a -> b) -> [a] -> [b]
map (lid -> symb_items -> [FilePath]
forall lid basic_spec symbol symb_items symb_map_items.
Syntax lid basic_spec symbol symb_items symb_map_items =>
lid -> symb_items -> [FilePath]
symb_items_name lid
aLid) [symb_items]
aSItems
                (syms1 :: Set [FilePath]
syms1, syms2 :: Set [FilePath]
syms2) =
                 ((Set [FilePath], Set [FilePath])
 -> CORRESPONDENCE -> (Set [FilePath], Set [FilePath]))
-> (Set [FilePath], Set [FilePath])
-> [CORRESPONDENCE]
-> (Set [FilePath], Set [FilePath])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ (set1 :: Set [FilePath]
set1, set2 :: Set [FilePath]
set2) c :: CORRESPONDENCE
c -> case CORRESPONDENCE
c of
                               Single_correspondence _ (G_symb_items_list lidS1 :: lid
lidS1 sitems1 :: [symb_items]
sitems1)
                                                       (G_symb_items_list lidS2 :: lid
lidS2 sitems2 :: [symb_items]
sitems2) _ _ ->
                                   (Set [FilePath] -> lid -> [symb_items] -> Set [FilePath]
forall lid basic_spec symbol symb_items symb_map_items.
Syntax lid basic_spec symbol symb_items symb_map_items =>
Set [FilePath] -> lid -> [symb_items] -> Set [FilePath]
insNames Set [FilePath]
set1 lid
lidS1 [symb_items]
sitems1,
                                    Set [FilePath] -> lid -> [symb_items] -> Set [FilePath]
forall lid basic_spec symbol symb_items symb_map_items.
Syntax lid basic_spec symbol symb_items symb_map_items =>
Set [FilePath] -> lid -> [symb_items] -> Set [FilePath]
insNames Set [FilePath]
set2 lid
lidS2 [symb_items]
sitems2)
                               _ -> FilePath -> (Set [FilePath], Set [FilePath])
forall a. HasCallStack => FilePath -> a
error "only single corrs")
                       (Set [FilePath]
forall a. Set a
Set.empty, Set [FilePath]
forall a. Set a
Set.empty) [CORRESPONDENCE]
corrs
             in Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set [FilePath] -> Bool
forall a. Set a -> Bool
Set.null (Set [FilePath] -> Bool) -> Set [FilePath] -> Bool
forall a b. (a -> b) -> a -> b
$ Set [FilePath] -> Set [FilePath] -> Set [FilePath]
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set [FilePath]
syms1 Set [FilePath]
syms2
 -- then we set a flag in addCorresp to True if disambiguation is needed
 let addCorresp :: (sign, sign, sign, [Named sentence2], Map symbol2 symbol2,
 Map symbol2 symbol2)
-> (G_symb_items_list, G_symb_items_list, REL_REF)
-> Result
     (sign, sign, sign, [Named sentence2], Map symbol2 symbol2,
      Map symbol2 symbol2)
addCorresp (s1 :: sign
s1, s2 :: sign
s2, s :: sign
s, sens :: [Named sentence2]
sens, p1 :: Map symbol2 symbol2
p1, p2 :: Map symbol2 symbol2
p2) (G_symb_items_list lids1 :: lid
lids1 l1 :: [symb_items]
l1,
                            G_symb_items_list lids2 l2, rrel :: REL_REF
rrel) = do
       [symb_items]
l1' <- lid -> lid -> FilePath -> [symb_items] -> Result [symb_items]
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> FilePath -> [symb_items1] -> m [symb_items2]
coerceSymbItemsList lid
lids1 lid
lid1 "coerceSymbItemsList" [symb_items]
l1
       [symb_items]
l2' <- lid -> lid -> FilePath -> [symb_items] -> Result [symb_items]
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> FilePath -> [symb_items1] -> m [symb_items2]
coerceSymbItemsList lid
lids2 lid
lid1 "coerceSymbItemsList" [symb_items]
l2
       (sigb :: sign
sigb, senb :: [Named sentence2]
senb, s1' :: sign
s1', s2' :: sign
s2', eMap1 :: Map symbol2 symbol2
eMap1, eMap2 :: Map symbol2 symbol2
eMap2) <-
           lid
-> FilePath
-> Bool
-> sign
-> sign
-> [symb_items]
-> [symb_items]
-> Map symbol2 symbol2
-> Map symbol2 symbol2
-> REL_REF
-> Result
     (sign, [Named sentence2], sign, sign, Map symbol2 symbol2,
      Map symbol2 symbol2)
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid
-> FilePath
-> Bool
-> sign
-> sign
-> [symb_items]
-> [symb_items]
-> EndoMap symbol
-> EndoMap symbol
-> REL_REF
-> Result
     (sign, [Named sentence], sign, sign, EndoMap symbol,
      EndoMap symbol)
corresp2th lid
lid1 (IRI -> FilePath
iriToStringUnsecure IRI
an) Bool
flag
                           sign
ssig sign
tsig'
                           [symb_items]
l1' [symb_items]
l2' Map symbol2 symbol2
p1 Map symbol2 symbol2
p2 REL_REF
rrel
       sign
s1'' <- lid -> sign -> sign -> Result sign
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> sign -> Result sign
signature_union lid
lid1 sign
s1 sign
s1'
       sign
s2'' <- lid -> sign -> sign -> Result sign
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> sign -> Result sign
signature_union lid
lid1 sign
s2 sign
s2'
       sign
s' <- lid -> sign -> sign -> Result sign
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> sign -> Result sign
signature_union lid
lid1 sign
s sign
sigb
       let p1' :: Map symbol2 symbol2
p1' = Map symbol2 symbol2 -> Map symbol2 symbol2 -> Map symbol2 symbol2
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map symbol2 symbol2
eMap1 Map symbol2 symbol2
p1
           p2' :: Map symbol2 symbol2
p2' = Map symbol2 symbol2 -> Map symbol2 symbol2 -> Map symbol2 symbol2
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map symbol2 symbol2
eMap2 Map symbol2 symbol2
p2
           sens' :: [Named sentence2]
sens' = [Named sentence2]
sens [Named sentence2] -> [Named sentence2] -> [Named sentence2]
forall a. [a] -> [a] -> [a]
++ [Named sentence2]
senb
       (sign, sign, sign, [Named sentence2], Map symbol2 symbol2,
 Map symbol2 symbol2)
-> Result
     (sign, sign, sign, [Named sentence2], Map symbol2 symbol2,
      Map symbol2 symbol2)
forall (m :: * -> *) a. Monad m => a -> m a
return (sign
s1'', sign
s2'', sign
s', [Named sentence2]
sens', Map symbol2 symbol2
p1', Map symbol2 symbol2
p2')
 (sig1'' :: sign
sig1'', sig2'' :: sign
sig2'', sig'' :: sign
sig'', sens'' :: [Named sentence]
sens'', sMap1 :: Map symbol symbol
sMap1, sMap2 :: Map symbol symbol
sMap2) <- ((sign, sign, sign, [Named sentence], Map symbol symbol,
  Map symbol symbol)
 -> (G_symb_items_list, G_symb_items_list, REL_REF)
 -> Result
      (sign, sign, sign, [Named sentence], Map symbol symbol,
       Map symbol symbol))
-> (sign, sign, sign, [Named sentence], Map symbol symbol,
    Map symbol symbol)
-> [(G_symb_items_list, G_symb_items_list, REL_REF)]
-> Result
     (sign, sign, sign, [Named sentence], Map symbol symbol,
      Map symbol symbol)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (sign, sign, sign, [Named sentence], Map symbol symbol,
 Map symbol symbol)
-> (G_symb_items_list, G_symb_items_list, REL_REF)
-> Result
     (sign, sign, sign, [Named sentence], Map symbol symbol,
      Map symbol symbol)
forall sublogics2 basic_spec2 sentence2 symb_items symb_map_items2
       morphism2 symbol2 raw_symbol2 proof_tree2.
Logic
  lid
  sublogics2
  basic_spec2
  sentence2
  symb_items
  symb_map_items2
  sign
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
(sign, sign, sign, [Named sentence2], Map symbol2 symbol2,
 Map symbol2 symbol2)
-> (G_symb_items_list, G_symb_items_list, REL_REF)
-> Result
     (sign, sign, sign, [Named sentence2], Map symbol2 symbol2,
      Map symbol2 symbol2)
addCorresp
       (sign
sig1, sign
sig2, sign
sig, [], Map symbol symbol
forall k a. Map k a
phi1, Map symbol symbol
forall k a. Map k a
phi2) ([(G_symb_items_list, G_symb_items_list, REL_REF)]
 -> Result
      (sign, sign, sign, [Named sentence], Map symbol symbol,
       Map symbol symbol))
-> [(G_symb_items_list, G_symb_items_list, REL_REF)]
-> Result
     (sign, sign, sign, [Named sentence], Map symbol symbol,
      Map symbol symbol)
forall a b. (a -> b) -> a -> b
$
       (CORRESPONDENCE -> (G_symb_items_list, G_symb_items_list, REL_REF))
-> [CORRESPONDENCE]
-> [(G_symb_items_list, G_symb_items_list, REL_REF)]
forall a b. (a -> b) -> [a] -> [b]
map (\c :: CORRESPONDENCE
c -> case CORRESPONDENCE
c of
                   Single_correspondence _ s1 :: G_symb_items_list
s1 s2 :: G_symb_items_list
s2 (Just rref :: RELATION_REF
rref) _ ->
                     (G_symb_items_list
s1, G_symb_items_list
s2, RELATION_REF -> REL_REF
refToRel RELATION_REF
rref)
                   _ -> FilePath -> (G_symb_items_list, G_symb_items_list, REL_REF)
forall a. HasCallStack => FilePath -> a
error "only single correspondences for now")
       [CORRESPONDENCE]
corrs
 -- 3. make G_ results
 -- gth1 is A_source
 let gth1 :: G_theory
gth1 = lid -> ExtSign sign symbol -> SigId -> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_theory
noSensGTheory lid
lid1 (sign -> ExtSign sign symbol
forall sign symbol. sign -> ExtSign sign symbol
mkExtSign sign
sig1'') SigId
startSigId
 -- gth2 is A_target
     gth2 :: G_theory
gth2 = lid -> ExtSign sign symbol -> SigId -> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_theory
noSensGTheory lid
lid1 (sign -> ExtSign sign symbol
forall sign symbol. sign -> ExtSign sign symbol
mkExtSign sign
sig2'') SigId
startSigId
 -- gth is A_bridge
     gth :: G_theory
gth = lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory lid
lid1 Maybe IRI
forall a. Maybe a
Nothing (sign -> ExtSign sign symbol
forall sign symbol. sign -> ExtSign sign symbol
mkExtSign sign
sig'') SigId
startSigId
                                 ([Named sentence] -> ThSens sentence (AnyComorphism, BasicProof)
forall a b. Ord a => [Named a] -> ThSens a b
toThSens [Named sentence]
sens'') ThId
startThId
 -- prepare the maps for morphism generation
     rsMap1 :: Map raw_symbol raw_symbol
rsMap1 = (symbol -> raw_symbol)
-> Map symbol raw_symbol -> Map raw_symbol raw_symbol
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys (lid -> symbol -> raw_symbol
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> symbol -> raw_symbol
symbol_to_raw lid
lid1) (Map symbol raw_symbol -> Map raw_symbol raw_symbol)
-> Map symbol raw_symbol -> Map raw_symbol raw_symbol
forall a b. (a -> b) -> a -> b
$
              (symbol -> raw_symbol)
-> Map symbol symbol -> Map symbol raw_symbol
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (lid -> symbol -> raw_symbol
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> symbol -> raw_symbol
symbol_to_raw lid
lid1) Map symbol symbol
sMap1
     rsMap2 :: Map raw_symbol raw_symbol
rsMap2 = (symbol -> raw_symbol)
-> Map symbol raw_symbol -> Map raw_symbol raw_symbol
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys (lid -> symbol -> raw_symbol
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> symbol -> raw_symbol
symbol_to_raw lid
lid1) (Map symbol raw_symbol -> Map raw_symbol raw_symbol)
-> Map symbol raw_symbol -> Map raw_symbol raw_symbol
forall a b. (a -> b) -> a -> b
$
              (symbol -> raw_symbol)
-> Map symbol symbol -> Map symbol raw_symbol
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (lid -> symbol -> raw_symbol
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> symbol -> raw_symbol
symbol_to_raw lid
lid1) Map symbol symbol
sMap2
 -- mor1 should go from A_source to O1: sig1'' to ssig
 morphism
mor1 <- lid
-> Map raw_symbol raw_symbol
-> ExtSign sign symbol
-> ExtSign sign symbol
-> Result morphism
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid
-> EndoMap raw_symbol
-> ExtSign sign symbol
-> ExtSign sign symbol
-> Result morphism
induced_from_to_morphism
            lid
lid1 Map raw_symbol raw_symbol
rsMap1 (sign -> ExtSign sign symbol
forall sign symbol. sign -> ExtSign sign symbol
mkExtSign sign
sig1'') (sign -> ExtSign sign symbol
forall sign symbol. sign -> ExtSign sign symbol
mkExtSign sign
ssig)
 let gmor1 :: GMorphism
gmor1 = G_sign -> G_morphism -> GMorphism
gEmbed2 (G_theory -> G_sign
signOf G_theory
gth1) (G_morphism -> GMorphism) -> G_morphism -> GMorphism
forall a b. (a -> b) -> a -> b
$ lid -> morphism -> G_morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> morphism -> G_morphism
mkG_morphism lid
lid1 morphism
mor1
 -- mor2 should go from A_target to O2: sig2'' to tsig'
 morphism
mor2 <- {- trace "mor2:" $
         trace ("source: " ++ (show sig2'')) $
         trace ("target: " ++ (show tsig'))  $ -}
         lid
-> Map raw_symbol raw_symbol
-> ExtSign sign symbol
-> ExtSign sign symbol
-> Result morphism
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid
-> EndoMap raw_symbol
-> ExtSign sign symbol
-> ExtSign sign symbol
-> Result morphism
induced_from_to_morphism
            lid
lid1 Map raw_symbol raw_symbol
rsMap2 (sign -> ExtSign sign symbol
forall sign symbol. sign -> ExtSign sign symbol
mkExtSign sign
sig2'') (sign -> ExtSign sign symbol
forall sign symbol. sign -> ExtSign sign symbol
mkExtSign sign
tsig')
 let gmor2 :: GMorphism
gmor2 = G_sign -> G_morphism -> GMorphism
gEmbed2 (G_theory -> G_sign
signOf G_theory
gth2) (G_morphism -> GMorphism) -> G_morphism -> GMorphism
forall a b. (a -> b) -> a -> b
$ lid -> morphism -> G_morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> morphism -> G_morphism
mkG_morphism lid
lid1 morphism
mor2
 (G_theory, G_theory, G_theory, GMorphism, GMorphism)
-> Result (G_theory, G_theory, G_theory, GMorphism, GMorphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (G_theory
gth1, G_theory
gth2, G_theory
gth, GMorphism
gmor1, GMorphism
gmor2)

-- the first DGraph dg' is that of the imported library
anaItemNamesOrMaps :: LibEnv -> LibName -> DGraph -> DGraph
  -> [ItemNameMap] -> Result DGraph
anaItemNamesOrMaps :: LibEnv
-> LibName -> DGraph -> DGraph -> [ItemNameMap] -> Result DGraph
anaItemNamesOrMaps libenv' :: LibEnv
libenv' ln :: LibName
ln refDG :: DGraph
refDG dg :: DGraph
dg items :: [ItemNameMap]
items = do
  (genv1 :: GlobalEnv
genv1, dg1 :: DGraph
dg1) <- ((GlobalEnv, DGraph) -> ItemNameMap -> Result (GlobalEnv, DGraph))
-> (GlobalEnv, DGraph)
-> [ItemNameMap]
-> Result (GlobalEnv, DGraph)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM
    (LibEnv
-> LibName
-> DGraph
-> (GlobalEnv, DGraph)
-> ItemNameMap
-> Result (GlobalEnv, DGraph)
anaItemNameOrMap LibEnv
libenv' LibName
ln DGraph
refDG) (DGraph -> GlobalEnv
globalEnv DGraph
dg, DGraph
dg) [ItemNameMap]
items
  GlobalAnnos
gannos'' <- GlobalAnnos -> GlobalAnnos -> Result GlobalAnnos
mergeGlobalAnnos (DGraph -> GlobalAnnos
globalAnnos DGraph
refDG) (GlobalAnnos -> Result GlobalAnnos)
-> GlobalAnnos -> Result GlobalAnnos
forall a b. (a -> b) -> a -> b
$ DGraph -> GlobalAnnos
globalAnnos DGraph
dg
  DGraph -> Result DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return DGraph
dg1
    { globalAnnos :: GlobalAnnos
globalAnnos = GlobalAnnos
gannos''
    , globalEnv :: GlobalEnv
globalEnv = GlobalEnv
genv1 }

anaItemNameOrMap :: LibEnv -> LibName -> DGraph -> (GlobalEnv, DGraph)
  -> ItemNameMap -> Result (GlobalEnv, DGraph)
anaItemNameOrMap :: LibEnv
-> LibName
-> DGraph
-> (GlobalEnv, DGraph)
-> ItemNameMap
-> Result (GlobalEnv, DGraph)
anaItemNameOrMap libenv :: LibEnv
libenv ln :: LibName
ln refDG :: DGraph
refDG res :: (GlobalEnv, DGraph)
res (ItemNameMap old :: IRI
old m :: Maybe IRI
m) =
   LibEnv
-> LibName
-> DGraph
-> (GlobalEnv, DGraph)
-> (IRI, IRI)
-> Result (GlobalEnv, DGraph)
anaItemNameOrMap1 LibEnv
libenv LibName
ln DGraph
refDG (GlobalEnv, DGraph)
res (IRI
old, IRI -> Maybe IRI -> IRI
forall a. a -> Maybe a -> a
fromMaybe IRI
old Maybe IRI
m)

-- | Auxiliary function for not yet implemented features
anaErr :: String -> a
anaErr :: FilePath -> a
anaErr f :: FilePath
f = FilePath -> a
forall a. HasCallStack => FilePath -> a
error (FilePath -> a) -> FilePath -> a
forall a b. (a -> b) -> a -> b
$ "*** Analysis of " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
f FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " is not yet implemented!"

anaItemNameOrMap1 :: LibEnv -> LibName -> DGraph -> (GlobalEnv, DGraph)
  -> (IRI, IRI) -> Result (GlobalEnv, DGraph)
anaItemNameOrMap1 :: LibEnv
-> LibName
-> DGraph
-> (GlobalEnv, DGraph)
-> (IRI, IRI)
-> Result (GlobalEnv, DGraph)
anaItemNameOrMap1 libenv :: LibEnv
libenv ln :: LibName
ln refDG :: DGraph
refDG (genv :: GlobalEnv
genv, dg :: DGraph
dg) (old :: IRI
old, new :: IRI
new) = do
  GlobalEntry
entry <- Result GlobalEntry
-> (GlobalEntry -> Result GlobalEntry)
-> Maybe GlobalEntry
-> Result GlobalEntry
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (FilePath -> IRI -> Result GlobalEntry
forall a. FilePath -> IRI -> Result a
notFoundError "item" IRI
old) GlobalEntry -> Result GlobalEntry
forall (m :: * -> *) a. Monad m => a -> m a
return
            (Maybe GlobalEntry -> Result GlobalEntry)
-> Maybe GlobalEntry -> Result GlobalEntry
forall a b. (a -> b) -> a -> b
$ IRI -> DGraph -> Maybe GlobalEntry
lookupGlobalEnvDG IRI
old DGraph
refDG
  Range -> FilePath -> Maybe () -> Result ()
forall a. Range -> FilePath -> Maybe a -> Result a
maybeToResult (IRI -> Range
iriPos IRI
new) (IRI -> FilePath
iriToStringUnsecure IRI
new FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " already used")
    (Maybe () -> Result ()) -> Maybe () -> Result ()
forall a b. (a -> b) -> a -> b
$ case IRI -> GlobalEnv -> Maybe GlobalEntry
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup IRI
new GlobalEnv
genv of
    Nothing -> () -> Maybe ()
forall a. a -> Maybe a
Just ()
    Just _ -> Maybe ()
forall a. Maybe a
Nothing
  case GlobalEntry
entry of
    SpecEntry extsig :: ExtGenSig
extsig ->
      (GlobalEnv, DGraph) -> Result (GlobalEnv, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return ((GlobalEnv, DGraph) -> Result (GlobalEnv, DGraph))
-> (GlobalEnv, DGraph) -> Result (GlobalEnv, DGraph)
forall a b. (a -> b) -> a -> b
$ (ExtGenSig, (GlobalEnv, DGraph)) -> (GlobalEnv, DGraph)
forall a b. (a, b) -> b
snd ((ExtGenSig, (GlobalEnv, DGraph)) -> (GlobalEnv, DGraph))
-> (ExtGenSig, (GlobalEnv, DGraph)) -> (GlobalEnv, DGraph)
forall a b. (a -> b) -> a -> b
$ LibEnv
-> LibName
-> DGraph
-> (GlobalEnv, DGraph)
-> IRI
-> ExtGenSig
-> (ExtGenSig, (GlobalEnv, DGraph))
refExtsigAndInsert LibEnv
libenv LibName
ln DGraph
refDG (GlobalEnv
genv, DGraph
dg) IRI
new ExtGenSig
extsig
    ViewOrStructEntry b :: Bool
b vsig :: ExtViewSig
vsig ->
      let (dg1 :: DGraph
dg1, vsig1 :: ExtViewSig
vsig1) = LibEnv
-> LibName
-> DGraph
-> DGraph
-> NodeName
-> ExtViewSig
-> (DGraph, ExtViewSig)
refViewsig LibEnv
libenv LibName
ln DGraph
refDG DGraph
dg (IRI -> NodeName
makeName IRI
new) ExtViewSig
vsig
          genv1 :: GlobalEnv
genv1 = IRI -> GlobalEntry -> GlobalEnv -> GlobalEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert IRI
new (Bool -> ExtViewSig -> GlobalEntry
ViewOrStructEntry Bool
b ExtViewSig
vsig1) GlobalEnv
genv
      in (GlobalEnv, DGraph) -> Result (GlobalEnv, DGraph)
forall (m :: * -> *) a. Monad m => a -> m a
return (GlobalEnv
genv1, DGraph
dg1)
    UnitEntry _usig :: UnitSig
_usig -> FilePath -> Result (GlobalEnv, DGraph)
forall a. FilePath -> a
anaErr "unit spec download"
    AlignEntry _asig :: AlignSig
_asig -> FilePath -> Result (GlobalEnv, DGraph)
forall a. FilePath -> a
anaErr "alignment download"
    ArchOrRefEntry b :: Bool
b _rsig :: RefSig
_rsig -> FilePath -> Result (GlobalEnv, DGraph)
forall a. FilePath -> a
anaErr (FilePath -> Result (GlobalEnv, DGraph))
-> FilePath -> Result (GlobalEnv, DGraph)
forall a b. (a -> b) -> a -> b
$ (if Bool
b then "arch" else "ref")
      FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " spec download"
    NetworkEntry _gdiag :: GDiagram
_gdiag -> FilePath -> Result (GlobalEnv, DGraph)
forall a. FilePath -> a
anaErr "network download"

refNodesig :: LibEnv -> LibName -> DGraph -> DGraph -> (NodeName, NodeSig)
           -> (DGraph, NodeSig)
refNodesig :: LibEnv
-> LibName
-> DGraph
-> DGraph
-> (NodeName, NodeSig)
-> (DGraph, NodeSig)
refNodesig libenv :: LibEnv
libenv refln :: LibName
refln refDG :: DGraph
refDG dg :: DGraph
dg
  (name :: NodeName
name, NodeSig refn :: Int
refn sigma :: G_sign
sigma@(G_sign lid :: lid
lid sig :: ExtSign sign symbol
sig ind :: SigId
ind)) =
  let (ln :: LibName
ln, _, (n :: Int
n, lbl :: DGNodeLab
lbl)) =
         LibEnv
-> LibName -> DGraph -> Int -> (LibName, DGraph, LNode DGNodeLab)
lookupRefNode LibEnv
libenv LibName
refln DGraph
refDG Int
refn
      refInfo :: DGNodeInfo
refInfo = LibName -> Int -> DGNodeInfo
newRefInfo LibName
ln Int
n
      new :: DGNodeLab
new = NodeName -> DGNodeInfo -> G_theory -> DGNodeLab
newInfoNodeLab NodeName
name DGNodeInfo
refInfo
        (G_theory -> DGNodeLab) -> G_theory -> DGNodeLab
forall a b. (a -> b) -> a -> b
$ lid -> ExtSign sign symbol -> SigId -> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_theory
noSensGTheory lid
lid ExtSign sign symbol
sig SigId
ind
      nodeCont :: DGNodeLab
nodeCont = DGNodeLab
new { globalTheory :: Maybe G_theory
globalTheory = DGNodeLab -> Maybe G_theory
globalTheory DGNodeLab
lbl }
      node :: Int
node = DGraph -> Int
getNewNodeDG DGraph
dg
   in case DGNodeInfo -> DGraph -> Maybe Int
lookupInAllRefNodesDG DGNodeInfo
refInfo DGraph
dg of
        Just existNode :: Int
existNode -> (DGraph
dg, Int -> G_sign -> NodeSig
NodeSig Int
existNode G_sign
sigma)
        Nothing ->
          ( LNode DGNodeLab -> DGraph -> DGraph
insNodeDG (Int
node, DGNodeLab
nodeCont) DGraph
dg
          , Int -> G_sign -> NodeSig
NodeSig Int
node G_sign
sigma)

refNodesigs :: LibEnv -> LibName -> DGraph -> DGraph -> [(NodeName, NodeSig)]
            -> (DGraph, [NodeSig])
refNodesigs :: LibEnv
-> LibName
-> DGraph
-> DGraph
-> [(NodeName, NodeSig)]
-> (DGraph, [NodeSig])
refNodesigs libenv :: LibEnv
libenv ln :: LibName
ln = (DGraph -> (NodeName, NodeSig) -> (DGraph, NodeSig))
-> DGraph -> [(NodeName, NodeSig)] -> (DGraph, [NodeSig])
forall (t :: * -> *) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumR ((DGraph -> (NodeName, NodeSig) -> (DGraph, NodeSig))
 -> DGraph -> [(NodeName, NodeSig)] -> (DGraph, [NodeSig]))
-> (DGraph -> DGraph -> (NodeName, NodeSig) -> (DGraph, NodeSig))
-> DGraph
-> DGraph
-> [(NodeName, NodeSig)]
-> (DGraph, [NodeSig])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LibEnv
-> LibName
-> DGraph
-> DGraph
-> (NodeName, NodeSig)
-> (DGraph, NodeSig)
refNodesig LibEnv
libenv LibName
ln

refExtsigAndInsert :: LibEnv -> LibName -> DGraph -> (GlobalEnv, DGraph)
  -> IRI -> ExtGenSig -> (ExtGenSig, (GlobalEnv, DGraph))
refExtsigAndInsert :: LibEnv
-> LibName
-> DGraph
-> (GlobalEnv, DGraph)
-> IRI
-> ExtGenSig
-> (ExtGenSig, (GlobalEnv, DGraph))
refExtsigAndInsert libenv :: LibEnv
libenv ln :: LibName
ln refDG :: DGraph
refDG (genv :: GlobalEnv
genv, dg :: DGraph
dg) new :: IRI
new extsig :: ExtGenSig
extsig =
  let (dg1 :: DGraph
dg1, extsig1 :: ExtGenSig
extsig1) = LibEnv
-> LibName
-> DGraph
-> DGraph
-> NodeName
-> ExtGenSig
-> (DGraph, ExtGenSig)
refExtsig LibEnv
libenv LibName
ln DGraph
refDG DGraph
dg (IRI -> NodeName
makeName IRI
new) ExtGenSig
extsig
      genv1 :: GlobalEnv
genv1 = IRI -> GlobalEntry -> GlobalEnv -> GlobalEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert IRI
new (ExtGenSig -> GlobalEntry
SpecEntry ExtGenSig
extsig1) GlobalEnv
genv
  in (ExtGenSig
extsig1, (GlobalEnv
genv1, DGraph
dg1))

refExtsig :: LibEnv -> LibName -> DGraph -> DGraph -> NodeName -> ExtGenSig
          -> (DGraph, ExtGenSig)
refExtsig :: LibEnv
-> LibName
-> DGraph
-> DGraph
-> NodeName
-> ExtGenSig
-> (DGraph, ExtGenSig)
refExtsig libenv :: LibEnv
libenv ln :: LibName
ln refDG :: DGraph
refDG dg :: DGraph
dg name :: NodeName
name
  (ExtGenSig (GenSig imps :: MaybeNode
imps params :: [NodeSig]
params gsigmaP :: MaybeNode
gsigmaP) body :: NodeSig
body) = let
  pName :: NodeName
pName = FilePath -> NodeName -> NodeName
extName "Parameters" NodeName
name
  (dg1 :: DGraph
dg1, imps1 :: MaybeNode
imps1) = case MaybeNode
imps of
    EmptyNode _ -> (DGraph
dg, MaybeNode
imps)
    JustNode ns :: NodeSig
ns -> let
        (dg0 :: DGraph
dg0, nns :: NodeSig
nns) = LibEnv
-> LibName
-> DGraph
-> DGraph
-> (NodeName, NodeSig)
-> (DGraph, NodeSig)
refNodesig LibEnv
libenv LibName
ln DGraph
refDG DGraph
dg (FilePath -> NodeName -> NodeName
extName "Imports" NodeName
name, NodeSig
ns)
        in (DGraph
dg0, NodeSig -> MaybeNode
JustNode NodeSig
nns)
  (dg2 :: DGraph
dg2, params1 :: [NodeSig]
params1) = LibEnv
-> LibName
-> DGraph
-> DGraph
-> [(NodeName, NodeSig)]
-> (DGraph, [NodeSig])
refNodesigs LibEnv
libenv LibName
ln DGraph
refDG DGraph
dg1
      ([(NodeName, NodeSig)] -> (DGraph, [NodeSig]))
-> [(NodeName, NodeSig)] -> (DGraph, [NodeSig])
forall a b. (a -> b) -> a -> b
$ (NodeName, [(NodeName, NodeSig)]) -> [(NodeName, NodeSig)]
forall a b. (a, b) -> b
snd ((NodeName, [(NodeName, NodeSig)]) -> [(NodeName, NodeSig)])
-> (NodeName, [(NodeName, NodeSig)]) -> [(NodeName, NodeSig)]
forall a b. (a -> b) -> a -> b
$ (NodeSig
 -> (NodeName, [(NodeName, NodeSig)])
 -> (NodeName, [(NodeName, NodeSig)]))
-> (NodeName, [(NodeName, NodeSig)])
-> [NodeSig]
-> (NodeName, [(NodeName, NodeSig)])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ p :: NodeSig
p (n :: NodeName
n, l :: [(NodeName, NodeSig)]
l) -> let nn :: NodeName
nn = NodeName -> NodeName
inc NodeName
n in
              (NodeName
nn, (NodeName
nn, NodeSig
p) (NodeName, NodeSig)
-> [(NodeName, NodeSig)] -> [(NodeName, NodeSig)]
forall a. a -> [a] -> [a]
: [(NodeName, NodeSig)]
l)) (NodeName
pName, []) [NodeSig]
params
  (dg3 :: DGraph
dg3, gsigmaP1 :: MaybeNode
gsigmaP1) = case MaybeNode
gsigmaP of
    EmptyNode _ -> (DGraph
dg, MaybeNode
gsigmaP)
    JustNode ns :: NodeSig
ns -> let
        (dg0 :: DGraph
dg0, nns :: NodeSig
nns) = LibEnv
-> LibName
-> DGraph
-> DGraph
-> (NodeName, NodeSig)
-> (DGraph, NodeSig)
refNodesig LibEnv
libenv LibName
ln DGraph
refDG DGraph
dg2 (NodeName
pName, NodeSig
ns)
        in (DGraph
dg0, NodeSig -> MaybeNode
JustNode NodeSig
nns)
  (dg4 :: DGraph
dg4, body1 :: NodeSig
body1) = LibEnv
-> LibName
-> DGraph
-> DGraph
-> (NodeName, NodeSig)
-> (DGraph, NodeSig)
refNodesig LibEnv
libenv LibName
ln DGraph
refDG DGraph
dg3 (NodeName
name, NodeSig
body)
  in (DGraph
dg4, GenSig -> NodeSig -> ExtGenSig
ExtGenSig (MaybeNode -> [NodeSig] -> MaybeNode -> GenSig
GenSig MaybeNode
imps1 [NodeSig]
params1 MaybeNode
gsigmaP1) NodeSig
body1)

refViewsig :: LibEnv -> LibName -> DGraph -> DGraph -> NodeName -> ExtViewSig
           -> (DGraph, ExtViewSig)
refViewsig :: LibEnv
-> LibName
-> DGraph
-> DGraph
-> NodeName
-> ExtViewSig
-> (DGraph, ExtViewSig)
refViewsig libenv :: LibEnv
libenv ln :: LibName
ln refDG :: DGraph
refDG dg :: DGraph
dg name :: NodeName
name (ExtViewSig src :: NodeSig
src mor :: GMorphism
mor extsig :: ExtGenSig
extsig) = let
  (dg1 :: DGraph
dg1, src1 :: NodeSig
src1) = LibEnv
-> LibName
-> DGraph
-> DGraph
-> (NodeName, NodeSig)
-> (DGraph, NodeSig)
refNodesig LibEnv
libenv LibName
ln DGraph
refDG DGraph
dg (FilePath -> NodeName -> NodeName
extName "Source" NodeName
name, NodeSig
src)
  (dg2 :: DGraph
dg2, extsig1 :: ExtGenSig
extsig1) = LibEnv
-> LibName
-> DGraph
-> DGraph
-> NodeName
-> ExtGenSig
-> (DGraph, ExtGenSig)
refExtsig LibEnv
libenv LibName
ln DGraph
refDG DGraph
dg1 (FilePath -> NodeName -> NodeName
extName "Target" NodeName
name) ExtGenSig
extsig
  in (DGraph
dg2, NodeSig -> GMorphism -> ExtGenSig -> ExtViewSig
ExtViewSig NodeSig
src1 GMorphism
mor ExtGenSig
extsig1)

-- BEGIN CURIE expansion

expandCurieItemNameMap :: FilePath -> FilePath -> ItemNameMap
  -> Either (Result ()) ItemNameMap
expandCurieItemNameMap :: FilePath
-> FilePath -> ItemNameMap -> Either (Result ()) ItemNameMap
expandCurieItemNameMap fn :: FilePath
fn newFn :: FilePath
newFn (ItemNameMap i1 :: IRI
i1 mi2 :: Maybe IRI
mi2) =
    case FilePath -> IRI -> Maybe IRI
expandCurieByPath FilePath
fn IRI
i1 of
        Just i :: IRI
i -> case Maybe IRI
mi2 of
            Nothing -> ItemNameMap -> Either (Result ()) ItemNameMap
forall a b. b -> Either a b
Right (ItemNameMap -> Either (Result ()) ItemNameMap)
-> ItemNameMap -> Either (Result ()) ItemNameMap
forall a b. (a -> b) -> a -> b
$ IRI -> Maybe IRI -> ItemNameMap
ItemNameMap IRI
i Maybe IRI
mi2
            Just j :: IRI
j -> case FilePath -> IRI -> Maybe IRI
expandCurieByPath FilePath
newFn IRI
j of
                Nothing -> Result () -> Either (Result ()) ItemNameMap
forall a b. a -> Either a b
Left (Result () -> Either (Result ()) ItemNameMap)
-> Result () -> Either (Result ()) ItemNameMap
forall a b. (a -> b) -> a -> b
$ IRI -> Result ()
forall a. IRI -> Result a
prefixErrorIRI IRI
j
                mj :: Maybe IRI
mj -> ItemNameMap -> Either (Result ()) ItemNameMap
forall a b. b -> Either a b
Right (ItemNameMap -> Either (Result ()) ItemNameMap)
-> ItemNameMap -> Either (Result ()) ItemNameMap
forall a b. (a -> b) -> a -> b
$ IRI -> Maybe IRI -> ItemNameMap
ItemNameMap IRI
i Maybe IRI
mj
        Nothing -> Result () -> Either (Result ()) ItemNameMap
forall a b. a -> Either a b
Left (Result () -> Either (Result ()) ItemNameMap)
-> Result () -> Either (Result ()) ItemNameMap
forall a b. (a -> b) -> a -> b
$ IRI -> Result ()
forall a. IRI -> Result a
prefixErrorIRI IRI
i1

itemNameMapsToIRIs :: [ItemNameMap] -> [IRI]
itemNameMapsToIRIs :: [ItemNameMap] -> [IRI]
itemNameMapsToIRIs = (ItemNameMap -> [IRI]) -> [ItemNameMap] -> [IRI]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (ItemNameMap i :: IRI
i mi :: Maybe IRI
mi) -> [IRI
i | Maybe IRI -> Bool
forall a. Maybe a -> Bool
isNothing Maybe IRI
mi])

-- END CURIE expansion