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
type LNS = Set.Set LibName
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
-> 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)
anaString :: Maybe LibName
-> LogicGraph -> HetcatsOpts -> LNS -> LibEnv -> DGraph -> String
-> FilePath -> Maybe String
-> 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
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
anaStringAux :: Maybe LibName
-> 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)
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
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
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
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"
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
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
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
(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
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'
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)
("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
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"
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)
{ 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)
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
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
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
(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
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'
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
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
(_, 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
(_, 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
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
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
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
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
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
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
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
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 :: 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 :: 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
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
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
morphism
mor2 <-
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)
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)
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)
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])