{- |
Module      :  ./Proofs/Freeness.hs
Description :  normalization of freeness
Copyright   :  (c) Mihai Codescu, DFKI GmbH 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Mihai.Codescu@dfki.de
Stability   :  provisional
Portability :  non-portable(Logic)

compute normal forms
-}

module Proofs.Freeness
    ( freeness
    ) where

import Logic.Logic
import Logic.Grothendieck
import Logic.Coerce
import Logic.Comorphism
import Logic.Prover (toNamedList, toThSens)
import Logic.ExtSign

import Static.ComputeTheory
import Static.GTheory
import Static.DevGraph
import Static.DgUtils
import Static.History

import Common.ExtSign
import Common.LibName
import Common.Result

import Data.Graph.Inductive.Graph as Graph
import qualified Data.Map as Map
import Control.Monad

import Data.List (nub)
import Data.Maybe (fromMaybe)
import Common.Lib.Graph

freenessRule :: DGRule
freenessRule :: DGRule
freenessRule = String -> DGRule
DGRule "Freeness"

freeness :: LibName -> LibEnv -> Result LibEnv
freeness :: LibName -> LibEnv -> Result LibEnv
freeness ln :: LibName
ln le :: LibEnv
le = do
  let dg :: DGraph
dg = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
le
  DGraph
newDg <- LibEnv -> LibName -> DGraph -> Result DGraph
freenessDG LibEnv
le LibName
ln DGraph
dg
  LibEnv -> Result LibEnv
forall (m :: * -> *) a. Monad m => a -> m a
return (LibEnv -> Result LibEnv) -> LibEnv -> Result 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 -> DGRule -> DGraph -> DGraph
groupHistory DGraph
dg DGRule
freenessRule DGraph
newDg) LibEnv
le

freenessDG :: LibEnv -> LibName -> DGraph -> Result DGraph
freenessDG :: LibEnv -> LibName -> DGraph -> Result DGraph
freenessDG le :: LibEnv
le ln :: LibName
ln dgraph :: DGraph
dgraph = (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 (LibEnv -> LibName -> DGraph -> LEdge DGLinkLab -> Result DGraph
handleEdge LibEnv
le LibName
ln) DGraph
dgraph ([LEdge DGLinkLab] -> Result DGraph)
-> [LEdge DGLinkLab] -> Result DGraph
forall a b. (a -> b) -> a -> b
$ DGraph -> [LEdge DGLinkLab]
labEdgesDG DGraph
dgraph

handleEdge :: LibEnv -> LibName -> DGraph -> LEdge DGLinkLab -> Result DGraph
handleEdge :: LibEnv -> LibName -> DGraph -> LEdge DGLinkLab -> Result DGraph
handleEdge libEnv :: LibEnv
libEnv ln :: LibName
ln dg :: DGraph
dg edge :: LEdge DGLinkLab
edge@(m :: Node
m, n :: Node
n, x :: DGLinkLab
x) =
    case DGLinkLab -> DGLinkType
dgl_type DGLinkLab
x of
     FreeOrCofreeDefLink _ _ -> do
      let phi :: GMorphism
phi = DGLinkLab -> GMorphism
dgl_morphism DGLinkLab
x
          mlab :: DGNodeLab
mlab = DGraph -> Node -> DGNodeLab
labDG DGraph
dg Node
m
          gth :: G_theory
gth = G_theory -> Maybe G_theory -> G_theory
forall a. a -> Maybe a -> a
fromMaybe (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
m) (Maybe G_theory -> G_theory) -> Maybe G_theory -> G_theory
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> Maybe G_theory
globalTheory DGNodeLab
mlab
      case G_theory
gth of
       G_theory lid :: lid
lid syn :: Maybe IRI
syn sig :: ExtSign sign symbol
sig _ sen :: ThSens sentence (AnyComorphism, BasicProof)
sen _ ->
        case GMorphism
phi of
         GMorphism cid :: cid
cid _ _ mor1 :: morphism2
mor1 _ -> do
          morphism
mor <- lid2 -> lid -> String -> morphism2 -> Result morphism
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 -> String -> 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
cid) lid
lid "free" morphism2
mor1
          let res :: Result (sign, [Named sentence])
res = lid
-> morphism -> [Named sentence] -> Result (sign, [Named sentence])
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
-> morphism -> [Named sentence] -> Result (sign, [Named sentence])
quotient_term_algebra lid
lid morphism
mor ([Named sentence] -> Result (sign, [Named sentence]))
-> [Named sentence] -> Result (sign, [Named sentence])
forall a b. (a -> b) -> a -> b
$ ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (AnyComorphism, BasicProof)
sen
          case Result (sign, [Named sentence]) -> Maybe (sign, [Named sentence])
forall a. Result a -> Maybe a
maybeResult Result (sign, [Named sentence])
res of
           Just (sigK :: sign
sigK, axK :: [Named sentence]
axK) -> do
               -- success in logic lid
            let thK :: G_theory
thK = 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
lid Maybe IRI
syn (lid -> sign -> ExtSign sign 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 -> sign -> ExtSign sign symbol
makeExtSign lid
lid sign
sigK)
                             SigId
startSigId ([Named sentence] -> ThSens sentence (AnyComorphism, BasicProof)
forall a b. Ord a => [Named a] -> ThSens a b
toThSens [Named sentence]
axK) ThId
startThId
            morphism
incl <- lid -> sign -> sign -> 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 -> sign -> sign -> Result morphism
subsig_inclusion lid
lid (ExtSign sign symbol -> sign
forall sign symbol. ExtSign sign symbol -> sign
plainSign ExtSign sign symbol
sig) sign
sigK
            let inclM :: GMorphism
inclM = G_morphism -> GMorphism
gEmbed (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
lid morphism
incl
      {- remove x
      add nodes
      k  with signature = sigK, sentences axK
      global def link from m to k, labeled with inclusion
      hiding def link from k to n, labeled with inclusion
              m' = getNewNodeDG dg -- new node -}
                nodelab :: DGNodeLab
nodelab = DGraph -> Node -> DGNodeLab
labDG DGraph
dg Node
m
                info :: DGNodeInfo
info = DGNodeLab -> DGNodeInfo
nodeInfo DGNodeLab
nodelab
                ConsStatus c :: Conservativity
c _ _ = DGNodeInfo -> ConsStatus
node_cons_status DGNodeInfo
info
                k :: Node
k = DGraph -> Node
getNewNodeDG DGraph
dg
                labelK :: DGNodeLab
labelK = NodeName -> DGNodeInfo -> G_theory -> DGNodeLab
newInfoNodeLab
                   (String -> NodeName -> NodeName
extName "Freeness" (NodeName -> NodeName) -> NodeName -> NodeName
forall a b. (a -> b) -> a -> b
$ DGNodeLab -> NodeName
dgn_name DGNodeLab
nodelab)
                   DGNodeInfo
info
                   { node_origin :: DGOrigin
node_origin = Node -> DGOrigin
DGNormalForm Node
m
                  , node_cons_status :: ConsStatus
node_cons_status = Conservativity -> ConsStatus
mkConsStatus Conservativity
c }
                  G_theory
thK
                insK :: DGChange
insK = LNode DGNodeLab -> DGChange
InsertNode (Node
k, DGNodeLab
labelK)
                insE :: [DGChange]
insE = [ LEdge DGLinkLab -> DGChange
InsertEdge (Node
m, Node
k, GMorphism -> DGLinkOrigin -> DGLinkLab
globDefLink GMorphism
inclM DGLinkOrigin
DGLinkProof)
                       , LEdge DGLinkLab -> DGChange
InsertEdge (Node
k, Node
n, GMorphism -> DGLinkType -> DGLinkOrigin -> DGLinkLab
defDGLink GMorphism
inclM DGLinkType
HidingDefLink
                                      DGLinkOrigin
DGLinkProof)]
                del :: DGChange
del = LEdge DGLinkLab -> DGChange
DeleteEdge LEdge DGLinkLab
edge
                allChanges :: [DGChange]
allChanges = DGChange
del DGChange -> [DGChange] -> [DGChange]
forall a. a -> [a] -> [a]
: DGChange
insK DGChange -> [DGChange] -> [DGChange]
forall a. a -> [a] -> [a]
: [DGChange]
insE
                newDG :: DGraph
newDG = DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dg [DGChange]
allChanges
                labelN :: DGNodeLab
labelN = DGraph -> Node -> DGNodeLab
labDG DGraph
dg Node
n
                succs :: [LNode DGNodeLab]
succs = (Node -> LNode DGNodeLab) -> [Node] -> [LNode DGNodeLab]
forall a b. (a -> b) -> [a] -> [b]
map (\ y :: Node
y -> (Node
y, DGraph -> Node -> DGNodeLab
labDG DGraph
dg Node
y)) ([Node] -> [LNode DGNodeLab]) -> [Node] -> [LNode DGNodeLab]
forall a b. (a -> b) -> a -> b
$ Gr DGNodeLab DGLinkLab -> Node -> [Node]
forall a b. Gr a b -> Node -> [Node]
descs (DGraph -> Gr DGNodeLab DGLinkLab
dgBody DGraph
dg) Node
n
                labCh :: [DGChange]
labCh = [DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab DGNodeLab
labelK (Node
k, DGNodeLab
labelK
                          { globalTheory :: Maybe G_theory
globalTheory = LibEnv -> LibName -> DGraph -> LNode DGNodeLab -> Maybe G_theory
computeLabelTheory LibEnv
libEnv LibName
ln DGraph
newDG
                               (Node
k, DGNodeLab
labelK) }),
                         DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab DGNodeLab
labelN (Node
n, DGNodeLab
labelN
                          { globalTheory :: Maybe G_theory
globalTheory = LibEnv -> LibName -> DGraph -> LNode DGNodeLab -> Maybe G_theory
computeLabelTheory LibEnv
libEnv LibName
ln DGraph
newDG
                               (Node
n, DGNodeLab
labelN)
                            , labelHasHiding :: Bool
labelHasHiding = Bool
True })
                         ] [DGChange] -> [DGChange] -> [DGChange]
forall a. [a] -> [a] -> [a]
++
                         (LNode DGNodeLab -> DGChange) -> [LNode DGNodeLab] -> [DGChange]
forall a b. (a -> b) -> [a] -> [b]
map (\ (y :: Node
y, ly :: DGNodeLab
ly) -> DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab DGNodeLab
ly
                                         (Node
y, DGNodeLab
ly {labelHasHiding :: Bool
labelHasHiding = Bool
True})) [LNode DGNodeLab]
succs
            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 -> [DGChange] -> DGraph
changesDGH DGraph
newDG [DGChange]
labCh
           _ -> DGraph -> Result DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return DGraph
dg
              {- do
              -- failed in logic lid, look for comorphism and translate
              -- then recursive call
              let look = lookupQTA_in_LG $ language_name lid
              case maybeResult look of
              Nothing -> return dg
              -- can't translate to a logic where qta is implemented
              Just com -> do
              (m', dgM) <- translateFree libEnv dg edge com
              foldM (handleEdge libEnv) dgM $ out (dgBody dgM) m' -}
     _ -> DGraph -> Result DGraph
forall (m :: * -> *) a. Monad m => a -> m a
return DGraph
dg

descs :: Gr a b -> Node -> [Node]
descs :: Gr a b -> Node -> [Node]
descs graph :: Gr a b
graph node :: Node
node = let
   d :: [Node] -> [Node] -> [Node]
d nList :: [Node]
nList descList :: [Node]
descList =
    case [Node]
nList of
      [] -> [Node]
descList
      _ -> let
             newDescs :: [Node]
newDescs = (Node -> [Node]) -> [Node] -> [Node]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Gr a b -> Node -> [Node]
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Node -> [Node]
suc Gr a b
graph) [Node]
nList
             nList' :: [Node]
nList' = (Node -> Bool) -> [Node] -> [Node]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ x :: Node
x -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (Node
x Node -> [Node] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Node]
nList) Bool -> Bool -> Bool
||
                                          (Node
x Node -> [Node] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Node]
descList))
                      [Node]
newDescs
             descList' :: [Node]
descList' = [Node] -> [Node]
forall a. Eq a => [a] -> [a]
nub ([Node] -> [Node]) -> [Node] -> [Node]
forall a b. (a -> b) -> a -> b
$ [Node]
descList [Node] -> [Node] -> [Node]
forall a. [a] -> [a] -> [a]
++ [Node]
newDescs
           in [Node] -> [Node] -> [Node]
d [Node]
nList' [Node]
descList'
 in [Node] -> [Node] -> [Node]
d [Node
node] []


{- translateFree :: LibEnv -> DGraph -> LEdge DGLinkLab -> AnyComorphism ->
Result (Node, DGraph)
translateFree le dg edge@(m,n,x) com = do
(m', dg') <- translateNode le dg m (dgn_theory $ labDG dg m) com
(n', dg'') <- translateNode le dg' n (dgn_theory $ labDG dg n) com
dg''' <- translateEdge dg'' edge (dgl_morphism x) com m' n'
return (m', dg''') -}

{- translateEdge :: DGraph -> LEdge DGLinkLab -> GMorphism -> AnyComorphism ->
Node -> Node -> Result DGraph
translateEdge dg _edge (GMorphism cid _sig _i1 mor1 _i2)
(Comorphism cid') m n = do
let
lidS = sourceLogic cid'
lidT = targetLogic cid'
mor2 <- coerceMorphism (targetLogic cid) lidS "" mor1
mor3 <- map_morphism cid' mor2
let
gm = gEmbed $ mkG_morphism lidT mor3
--del = DeleteEdge edge
edge' = defDGLink gm
(FreeOrCofreeDefLink Free $ EmptyNode $ Logic lidT)  DGLinkProof
ins = InsertEdge (m, n, edge')
return $ changesDGH dg  [ins] -}

{- translateNode :: LibEnv -> DGraph -> Node -> G_theory -> AnyComorphism ->
Result (Node, DGraph)
translateNode libEnv dg n s@(G_theory lid sig _ _ _) com@(Comorphism cid) = do
let
m' = getNewNodeDG dg -- new node
nodelab = labDG dg n
info = nodeInfo nodelab
ConsStatus cs _ _ = node_cons_status info
lidS = sourceLogic cid
lidT = targetLogic cid
sig' <- coerceSign lid lidS "" sig
(sig'',sen'') <- wrapMapTheory cid (plainSign sig', [])
let
gth = G_theory lidT (mkExtSign sig'') startSigId
(toThSens sen'') startThId
labelM' = newInfoNodeLab
(extName "Freeness" $ dgn_name nodelab)
info
{ node_origin = DGNormalForm n
, node_cons_status = mkConsStatus cs }
gth
insM' = InsertNode (m', labelM')
gMor <- gEmbedComorphism com (signOf s)
let insE = InsertEdge (n,m', globDefLink gMor DGLinkProof)
changeLabel = SetNodeLab nodelab
(n, nodelab{dgn_freenf = Just m', dgn_phi = Just gMor})
newDG = changesDGH dg [insM', insE, changeLabel]
return $ (m', changeDGH newDG $ SetNodeLab labelM' (m', labelM'
{ globalTheory = computeLabelTheory libEnv newDG
(m', labelM') })) -}

{- thmFreeShift :: DGRule
thmFreeShift = DGRule "TheoremFreeShift" -}

{- ----------------------------------------------
Theorem free shift and  auxiliaries
moves theorem links to nodes with incoming free dfn links
to their freeness normal form (must be computed before)
--------------------------------------------- -}

{- theoremFreeShift :: LibName -> LibEnv -> Result LibEnv
theoremFreeShift ln  = return .
Map.adjust (\ dg -> theoremFreeShiftAux (labNodesDG dg) dg) ln -}

{- -- | assume that the normal forms a commputed already.
-- return Nothing if nothing changed
theoremFreeShiftAux :: [LNode DGNodeLab] -> DGraph -> DGraph
theoremFreeShiftAux  ns dg = let
nodesWFree = map fst $ filter
(\ (_, lbl) -> labelHasFree lbl && isJust (dgn_freenf lbl)
&& isJust (dgn_phi lbl)) ns
-- all nodes with incoming hiding links
-- all the theorem links entering these nodes
-- have to replaced by theorem links with the same origin
-- but pointing to the normal form of the former target node
ingoingEdges = concatMap (getInComingGlobalUnprovenEdges dg) nodesWFree
in foldl theoremFreeShiftForEdge
dg ingoingEdges -}

{- theoremFreeShiftForEdge :: DGraph -> LEdge DGLinkLab -> DGraph
theoremFreeShiftForEdge dg edge@(source, target, edgeLab) =
case maybeResult $ theoremFreeShiftForEdgeAux dg edge of
Nothing -> error "theoremFreeShiftForEdgeAux"
Just (dg', pbasis) -> let
provenEdge = (source, target, edgeLab
{ dgl_type = setProof (Proven thmFreeShift pbasis) $ dgl_type edgeLab
, dgl_origin = DGLinkProof
, dgl_id = defaultEdgeId })
in insertDGLEdge provenEdge $ changeDGH dg' $ DeleteEdge edge -}

{- theoremFreeShiftForEdgeAux :: DGraph -> LEdge DGLinkLab
-> Result (DGraph, ProofBasis)
theoremFreeShiftForEdgeAux dg (sn, tn, llab) = do
let tlab = labDG dg tn
Just nfNode = dgn_freenf tlab
phi = dgl_morphism llab
Just muN = dgn_phi tlab
let cmor1  = composeMorphisms phi muN
case maybeResult cmor1 of
Nothing -> error "composition"
Just cmor -> do
let newEdge =(sn, nfNode, defDGLink cmor globalThm DGLinkProof)
case tryToGetEdge newEdge dg of
Nothing -> let
newGraph = changeDGH dg $ InsertEdge newEdge
finalEdge = case getLastChange newGraph of
InsertEdge final_e -> final_e
_ -> error "Proofs.Global.globDecompForOneEdgeAux"
in return
(newGraph, addEdgeId emptyProofBasis $ getEdgeId finalEdge)
Just e -> return (dg, addEdgeId emptyProofBasis $ getEdgeId e) -}

{- theoremFreeShiftFromList :: LibName -> [LNode DGNodeLab] -> LibEnv
-> Result LibEnv
theoremFreeShiftFromList ln ls =
return . Map.adjust (theoremFreeShiftAux ls) ln -}