{- |

Module : $Header$

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 Common.Lib.Graph

freenessRule :: DGRule

freenessRule = DGRule "Freeness"

freeness :: LibName -> LibEnv -> Result LibEnv

freeness ln le = do

let dg = lookupDGraph ln le

newDg <- freenessDG le dg

return $ Map.insert ln

(groupHistory dg freenessRule newDg) le

freenessDG :: LibEnv -> DGraph -> Result DGraph

freenessDG le dgraph = do

foldM (handleEdge le) dgraph $ labEdgesDG dgraph

handleEdge :: LibEnv -> DGraph -> LEdge DGLinkLab -> Result DGraph

handleEdge libEnv dg edge@(m,n,x) = do

case dgl_type x of

FreeOrCofreeDefLink _ _ -> do

let phi = dgl_morphism x

mlab = labDG dg m

gth= case globalTheory mlab of

Nothing -> dgn_theory $ labDG dg m

Just t -> t

case gth of

G_theory lid sig _ sen _ -> do

case phi of

GMorphism cid _ _ mor1 _ -> do

mor <- coerceMorphism (targetLogic cid) lid "free" mor1

let res = quotient_term_algebra lid mor $ toNamedList sen

case maybeResult res of

Just (sigK, axK) -> do

-- success in logic lid

let thK = G_theory lid (makeExtSign lid sigK)

startSigId (toThSens axK) startThId

incl <- subsig_inclusion lid (plainSign sig) sigK

let inclM = gEmbed $ mkG_morphism lid 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 = labDG dg m

info = nodeInfo nodelab

ConsStatus c _ _ = node_cons_status info

k = (getNewNodeDG dg)

labelK = newInfoNodeLab

(extName "Freeness" $ dgn_name nodelab)

info

{ node_origin = DGNormalForm m

, node_cons_status = mkConsStatus c }

thK

insK = InsertNode (k, labelK)

insE = [ InsertEdge (m,k, globDefLink inclM DGLinkProof)

, InsertEdge (k, n, defDGLink inclM HidingDefLink

DGLinkProof)]

del = DeleteEdge edge

allChanges = del: insK : insE

newDG = changesDGH dg allChanges

labelN = labDG dg n

succs = map (\y -> (y,labDG dg y)) $ descs (dgBody dg) n

labCh = [SetNodeLab labelK (k, labelK

{ globalTheory = computeLabelTheory libEnv newDG

(k, labelK) }),

SetNodeLab labelN (n, labelN

{ globalTheory = computeLabelTheory libEnv newDG

(n, labelN)

, labelHasHiding = True })

] ++

map (\(y,ly) -> SetNodeLab ly

(y, ly{labelHasHiding = True})) succs

return $ changesDGH newDG $ labCh

_ -> return 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'

_ -> return dg

descs :: Gr a b -> Node -> [Node]

descs graph node = let

d nList descList =

case nList of

[] -> descList

_ -> let

newDescs = concatMap (\x -> suc graph x) nList

nList' = filter (\x -> not $ (x `elem` nList) ||

(x `elem` descList))

newDescs

descList' = nub $ descList ++ newDescs

in d nList' descList'

in d [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