{-# LANGUAGE ExistentialQuantification, DeriveDataTypeable #-}
module Proofs.FreeDefLinks where
import Static.GTheory
import Static.DevGraph
import Static.DgUtils
import Static.ComputeTheory
import Proofs.EdgeUtils
import Common.ExtSign
import Common.LibName
import Common.AS_Annotation
import qualified Common.Lib.Graph as Tree
import Logic.Logic
import Logic.Prover
import Logic.Grothendieck
import Logic.Comorphism
import Logic.Coerce
import Data.Graph.Inductive.Basic (elfilter)
import Data.Graph.Inductive.Graph
import Data.Maybe
import Data.Typeable
getCFreeDefLinks :: DGraph -> Node
-> ([[LEdge DGLinkLab]], [[LEdge DGLinkLab]])
getCFreeDefLinks :: DGraph -> Node -> ([[LEdge DGLinkLab]], [[LEdge DGLinkLab]])
getCFreeDefLinks dg :: DGraph
dg tgt :: Node
tgt =
let isGlobalOrCFreeEdge :: DGLinkType -> Bool
isGlobalOrCFreeEdge = (DGLinkType -> Bool) -> (DGLinkType -> Bool) -> DGLinkType -> Bool
forall a. (a -> Bool) -> (a -> Bool) -> a -> Bool
liftOr DGLinkType -> Bool
isGlobalEdge ((DGLinkType -> Bool) -> DGLinkType -> Bool)
-> (DGLinkType -> Bool) -> DGLinkType -> Bool
forall a b. (a -> b) -> a -> b
$ (DGLinkType -> Bool) -> (DGLinkType -> Bool) -> DGLinkType -> Bool
forall a. (a -> Bool) -> (a -> Bool) -> a -> Bool
liftOr DGLinkType -> Bool
isFreeEdge DGLinkType -> Bool
isCofreeEdge
paths :: [[LEdge DGLinkLab]]
paths = ([LEdge DGLinkLab] -> [LEdge DGLinkLab])
-> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
forall a b. (a -> b) -> [a] -> [b]
map [LEdge DGLinkLab] -> [LEdge DGLinkLab]
forall a. [a] -> [a]
reverse ([[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]])
-> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
forall a b. (a -> b) -> a -> b
$ Node -> Gr DGNodeLab DGLinkLab -> [[LEdge DGLinkLab]]
forall a b. Node -> Gr a b -> [[LEdge b]]
Tree.getAllPathsTo Node
tgt
(Gr DGNodeLab DGLinkLab -> [[LEdge DGLinkLab]])
-> Gr DGNodeLab DGLinkLab -> [[LEdge DGLinkLab]]
forall a b. (a -> b) -> a -> b
$ (DGLinkLab -> Bool)
-> Gr DGNodeLab DGLinkLab -> Gr DGNodeLab DGLinkLab
forall (gr :: * -> * -> *) b a.
DynGraph gr =>
(b -> Bool) -> gr a b -> gr a b
elfilter (DGLinkType -> Bool
isGlobalOrCFreeEdge (DGLinkType -> Bool)
-> (DGLinkLab -> DGLinkType) -> DGLinkLab -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DGLinkLab -> DGLinkType
dgl_type) (Gr DGNodeLab DGLinkLab -> Gr DGNodeLab DGLinkLab)
-> Gr DGNodeLab DGLinkLab -> Gr DGNodeLab DGLinkLab
forall a b. (a -> b) -> a -> b
$ DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dg
myfilter :: (DGLinkType -> Bool)
-> [[(a, b, DGLinkLab)]] -> [[(a, b, DGLinkLab)]]
myfilter p :: DGLinkType -> Bool
p = ([(a, b, DGLinkLab)] -> Bool)
-> [[(a, b, DGLinkLab)]] -> [[(a, b, DGLinkLab)]]
forall a. (a -> Bool) -> [a] -> [a]
filter ( \ ~((_, _, lbl :: DGLinkLab
lbl) : _) -> DGLinkType -> Bool
p (DGLinkType -> Bool) -> DGLinkType -> Bool
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> DGLinkType
dgl_type DGLinkLab
lbl)
in ((DGLinkType -> Bool) -> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
forall a b.
(DGLinkType -> Bool)
-> [[(a, b, DGLinkLab)]] -> [[(a, b, DGLinkLab)]]
myfilter DGLinkType -> Bool
isFreeEdge [[LEdge DGLinkLab]]
paths, (DGLinkType -> Bool) -> [[LEdge DGLinkLab]] -> [[LEdge DGLinkLab]]
forall a b.
(DGLinkType -> Bool)
-> [[(a, b, DGLinkLab)]] -> [[(a, b, DGLinkLab)]]
myfilter DGLinkType -> Bool
isCofreeEdge [[LEdge DGLinkLab]]
paths)
mkFreeDefMor :: [Named sentence] -> morphism -> morphism
-> FreeDefMorphism sentence morphism
mkFreeDefMor :: [Named sentence]
-> morphism -> morphism -> FreeDefMorphism sentence morphism
mkFreeDefMor sens :: [Named sentence]
sens m1 :: morphism
m1 m2 :: morphism
m2 = FreeDefMorphism :: forall sentence morphism.
morphism
-> morphism
-> [Named sentence]
-> Bool
-> FreeDefMorphism sentence morphism
FreeDefMorphism
{ freeDefMorphism :: morphism
freeDefMorphism = morphism
m1
, pathFromFreeDef :: morphism
pathFromFreeDef = morphism
m2
, freeTheory :: [Named sentence]
freeTheory = [Named sentence]
sens
, isCofree :: Bool
isCofree = Bool
False }
data GFreeDefMorphism =
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
=> GFreeDefMorphism lid (FreeDefMorphism sentence morphism)
deriving Typeable
getFreeDefMorphism :: LibEnv -> LibName -> DGraph -> [LEdge DGLinkLab]
-> Maybe GFreeDefMorphism
getFreeDefMorphism :: LibEnv
-> LibName -> DGraph -> [LEdge DGLinkLab] -> Maybe GFreeDefMorphism
getFreeDefMorphism libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg path :: [LEdge DGLinkLab]
path = case [LEdge DGLinkLab]
path of
[] -> [Char] -> Maybe GFreeDefMorphism
forall a. HasCallStack => [Char] -> a
error "getFreeDefMorphism"
(s :: Node
s, t :: Node
t, l :: DGLinkLab
l) : rp :: [LEdge DGLinkLab]
rp -> do
gmor :: GMorphism
gmor@(GMorphism cid :: cid
cid _ _ fmor :: morphism2
fmor _) <- GMorphism -> Maybe GMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return (GMorphism -> Maybe GMorphism) -> GMorphism -> Maybe GMorphism
forall a b. (a -> b) -> a -> b
$ DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
l
let tlid :: lid2
tlid = cid -> lid2
forall cid 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.
Comorphism
cid
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 =>
cid -> lid2
targetLogic cid
cid
G_theory lidth :: lid
lidth _ (ExtSign _sign :: sign
_sign _) _ axs :: ThSens sentence (AnyComorphism, BasicProof)
axs _ <-
LibEnv -> LibName -> Node -> Maybe G_theory
computeTheory LibEnv
libEnv LibName
ln Node
s
if GMorphism -> Bool
isHomogeneous GMorphism
gmor then do
[Named sentence2]
sens <- lid
-> lid2 -> [Char] -> [Named sentence] -> Maybe [Named sentence2]
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 -> [Char] -> [Named sentence1] -> m [Named sentence2]
coerceSens lid
lidth lid2
tlid "getFreeDefMorphism4" (ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (AnyComorphism, BasicProof)
axs)
case [LEdge DGLinkLab]
rp of
[] -> do
G_theory lid2 :: lid
lid2 _ (ExtSign sig :: sign
sig _) _ _ _ <-
G_theory -> Maybe G_theory
forall (m :: * -> *) a. Monad m => a -> m a
return (G_theory -> Maybe G_theory) -> G_theory -> Maybe G_theory
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> G_theory
dgn_theory (DGNodeLab -> G_theory) -> DGNodeLab -> G_theory
forall a b. (a -> b) -> a -> b
$ DGraph -> Node -> DGNodeLab
labDG DGraph
dg Node
t
sign2
sig2 <- lid -> lid2 -> [Char] -> sign -> Maybe sign2
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 -> [Char] -> sign1 -> m sign2
coercePlainSign lid
lid2 lid2
tlid "getFreeDefMorphism2" sign
sig
GFreeDefMorphism -> Maybe GFreeDefMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return (GFreeDefMorphism -> Maybe GFreeDefMorphism)
-> GFreeDefMorphism -> Maybe GFreeDefMorphism
forall a b. (a -> b) -> a -> b
$ lid2 -> FreeDefMorphism sentence2 morphism2 -> GFreeDefMorphism
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 -> FreeDefMorphism sentence morphism -> GFreeDefMorphism
GFreeDefMorphism lid2
tlid (FreeDefMorphism sentence2 morphism2 -> GFreeDefMorphism)
-> FreeDefMorphism sentence2 morphism2 -> GFreeDefMorphism
forall a b. (a -> b) -> a -> b
$ [Named sentence2]
-> morphism2 -> morphism2 -> FreeDefMorphism sentence2 morphism2
forall sentence morphism.
[Named sentence]
-> morphism -> morphism -> FreeDefMorphism sentence morphism
mkFreeDefMor [Named sentence2]
sens morphism2
fmor (morphism2 -> FreeDefMorphism sentence2 morphism2)
-> morphism2 -> FreeDefMorphism sentence2 morphism2
forall a b. (a -> b) -> a -> b
$ sign2 -> morphism2
forall object morphism.
Category object morphism =>
object -> morphism
ide sign2
sig2
_ -> do
pm :: GMorphism
pm@(GMorphism cid2 :: cid
cid2 _ _ pmor :: morphism2
pmor _) <- [LEdge DGLinkLab] -> Maybe GMorphism
calculateMorphismOfPath [LEdge DGLinkLab]
rp
if GMorphism -> Bool
isHomogeneous GMorphism
pm then do
morphism2
cpmor <- lid2 -> lid2 -> [Char] -> morphism2 -> Maybe morphism2
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 -> [Char] -> morphism1 -> m morphism2
coerceMorphism (cid -> lid2
forall cid 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.
Comorphism
cid
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 =>
cid -> lid2
targetLogic cid
cid2) lid2
tlid
"getFreeDefMorphism3" morphism2
pmor
GFreeDefMorphism -> Maybe GFreeDefMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return (GFreeDefMorphism -> Maybe GFreeDefMorphism)
-> GFreeDefMorphism -> Maybe GFreeDefMorphism
forall a b. (a -> b) -> a -> b
$ lid2 -> FreeDefMorphism sentence2 morphism2 -> GFreeDefMorphism
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 -> FreeDefMorphism sentence morphism -> GFreeDefMorphism
GFreeDefMorphism lid2
tlid (FreeDefMorphism sentence2 morphism2 -> GFreeDefMorphism)
-> FreeDefMorphism sentence2 morphism2 -> GFreeDefMorphism
forall a b. (a -> b) -> a -> b
$ [Named sentence2]
-> morphism2 -> morphism2 -> FreeDefMorphism sentence2 morphism2
forall sentence morphism.
[Named sentence]
-> morphism -> morphism -> FreeDefMorphism sentence morphism
mkFreeDefMor [Named sentence2]
sens morphism2
fmor morphism2
cpmor
else Maybe GFreeDefMorphism
forall a. Maybe a
Nothing
else Maybe GFreeDefMorphism
forall a. Maybe a
Nothing
getCFreeDefMorphs :: LibEnv -> LibName -> DGraph -> Node -> [GFreeDefMorphism]
getCFreeDefMorphs :: LibEnv -> LibName -> DGraph -> Node -> [GFreeDefMorphism]
getCFreeDefMorphs libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg node :: Node
node = let
(frees :: [[LEdge DGLinkLab]]
frees, cofrees :: [[LEdge DGLinkLab]]
cofrees) = DGraph -> Node -> ([[LEdge DGLinkLab]], [[LEdge DGLinkLab]])
getCFreeDefLinks DGraph
dg Node
node
myget :: [[LEdge DGLinkLab]] -> [GFreeDefMorphism]
myget = ([LEdge DGLinkLab] -> Maybe GFreeDefMorphism)
-> [[LEdge DGLinkLab]] -> [GFreeDefMorphism]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (LibEnv
-> LibName -> DGraph -> [LEdge DGLinkLab] -> Maybe GFreeDefMorphism
getFreeDefMorphism LibEnv
libEnv LibName
ln DGraph
dg)
mkCoFree :: GFreeDefMorphism -> GFreeDefMorphism
mkCoFree (GFreeDefMorphism lid :: lid
lid m :: FreeDefMorphism sentence morphism
m) = lid -> FreeDefMorphism sentence morphism -> GFreeDefMorphism
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 -> FreeDefMorphism sentence morphism -> GFreeDefMorphism
GFreeDefMorphism lid
lid FreeDefMorphism sentence morphism
m { isCofree :: Bool
isCofree = Bool
True }
in [[LEdge DGLinkLab]] -> [GFreeDefMorphism]
myget [[LEdge DGLinkLab]]
frees [GFreeDefMorphism] -> [GFreeDefMorphism] -> [GFreeDefMorphism]
forall a. [a] -> [a] -> [a]
++ (GFreeDefMorphism -> GFreeDefMorphism)
-> [GFreeDefMorphism] -> [GFreeDefMorphism]
forall a b. (a -> b) -> [a] -> [b]
map GFreeDefMorphism -> GFreeDefMorphism
mkCoFree ([[LEdge DGLinkLab]] -> [GFreeDefMorphism]
myget [[LEdge DGLinkLab]]
cofrees)