{- |

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 Data.Maybe (fromMaybe)

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 = foldM (handleEdge le) dgraph $ labEdgesDG dgraph

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

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

case dgl_type x of

FreeOrCofreeDefLink _ _ -> do

let phi = dgl_morphism x

mlab = labDG dg m

gth = fromMaybe (dgn_theory $ labDG dg m) $ globalTheory mlab

case gth of

G_theory lid syn sig _ sen _ ->

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 syn (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 (suc graph) 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 -}