$ insLEdgeNubDG (n, t, link) dg
-- first Parameter determines if incoming symbols shall be ignored
-- options: here we need the info: shall only the structure be analysed?
ana_SPEC :: Bool -> LogicGraph -> DGraph -> MaybeNode -> NODE_NAME ->
HetcatsOpts -> SPEC -> Result (SPEC, NodeSig, DGraph)
ana_SPEC addSyms lg dg nsig name opts sp = case sp of
Basic_spec (G_basic_spec lid bspec) pos ->
do G_sign lid' sigma' i1 <- return (getMaybeSig nsig)
sigma@(ExtSign sig sys) <-
adj $ coerceSign lid' lid "Analysis of basic spec" sigma'
(bspec', ExtSign sigma_complete sysd, ax) <- adj $
then return (bspec, mkExtSign $ empty_signature lid, [])
else do b <- maybeToMonad
("no basic analysis for logic "
b (bspec, sig, globalAnnos dg)
let (ns@(NodeSig node gsig), dg') = insGTheory dg name DGBasic
$ G_theory lid (ExtSign sigma_complete
(if addSyms then
Set.union sys sysd else sysd)
$ sym_of lid sigma_complete) 0 (toThSens ax) 0
incl <- adj $ ginclusion lg (G_sign lid sigma i1) gsig
return (Basic_spec (G_basic_spec lid bspec') pos, ns, case nsig of
JustNode (NodeSig n _) ->
insLink dg' incl GlobalDef DGExtension n node)
EmptySpec pos -> case nsig of
warning () "empty spec" pos
let (ns, dg') = insGSig dg name DGEmpty (getMaybeSig nsig)
{- ana_SPEC should be changed to return a MaybeNode!
Then this duplicate dummy node could be avoided.
Also empty unions could be treated then -}
JustNode ns -> return (sp, ns ,dg)
(sp1', NodeSig n' gsigma, dg') <-
ana_SPEC addSyms lg dg nsig (inc name) opts sp1
mor <- ana_RENAMING lg nsig gsigma opts ren
-- ??? check that mor is identity on local env
let (ns@(NodeSig node _), dg'') =
insGSig dg' name DGTranslation $ cod Grothendieck mor
-- ??? too simplistic for non-comorphism inter-logic translations
return (Translation (replaceAnnoted sp1' asp) ren, ns,
insLink dg'' mor GlobalDef DGTranslation n' node)
(sp1', NodeSig n' gsigma', dg') <-
ana_SPEC addSyms lg dg nsig (inc name) opts sp1
let gsigma = getMaybeSig nsig
(hmor, tmor) <- ana_RESTRICTION gsigma gsigma' opts restr
-- we treat hiding and revealing differently
-- in order to keep the dg as simple as possible
do let (ns@(NodeSig node _), dg'') =
insGSig dg' name DGHiding $ dom Grothendieck hmor
-- ??? too simplistic for non-comorphism inter-logic reductions
return (Reduction (replaceAnnoted sp1' asp) restr, ns,
insLink dg'' hmor HidingDef DGHiding n' node)
let gsigma1 = dom Grothendieck tmor'
gsigma'' = cod Grothendieck tmor'
-- ??? too simplistic for non-comorphism inter-logic reductions
-- the case with identity translation leads to a simpler dg
if tmor' == ide Grothendieck (dom Grothendieck tmor')
let (ns@(NodeSig node1 _), dg'') =
insGSig dg' name DGRevealing gsigma1
return (Reduction (replaceAnnoted sp1' asp) restr, ns,
insLink dg'' hmor HidingDef DGRevealing n' node1)
let (NodeSig node1 _, dg'') =
insGSig dg' (extName "T" name) DGRevealing gsigma1
(ns@(NodeSig node2 _), dg3) =
insGSig dg'' name DGRevealTranslation gsigma''
dg4 = insLink dg3 hmor HidingDef DGRevealing n' node1
return (Reduction (replaceAnnoted sp1' asp) restr, ns,
insLink dg4 tmor' GlobalDef DGRevealTranslation node1 node2)
Union [] pos -> adjustPos pos $ fail $ "empty union"
do let sps = map item asps
let ana (sps1, nsigs, dg', n) sp' = do
(sp1, nsig', dg1) <- ana_SPEC addSyms lg dg' nsig n opts sp'
return (sp1 : sps1, nsig' : nsigs, dg1, inc n)
in foldM ana ([], [], dg, extName "U" name) sps
let nsigs' = reverse nsigs
gbigSigma <- adj $ gsigManyUnion lg (map getSig nsigs')
let (ns@(NodeSig node _), dg2) = insGSig dg' name DGUnion gbigSigma
insE dgl (NodeSig n gsigma) = do
incl <- adj $ ginclusion lg gsigma gbigSigma
return $ insLink dgl incl GlobalDef DGUnion n node
dg3 <- foldM insE dg2 nsigs'
return (Union (map (uncurry replaceAnnoted)
(zip (reverse sps') asps))
(sps', nsig1', dg1, _, _, _, _) <-
foldM ana_Extension ([], nsig, dg, lg, opts, pos, addSyms) namedSps
EmptyNode _ -> fail "empty extension"
JustNode nsig1 -> return (Extension (map (uncurry replaceAnnoted)
(zip (reverse sps') asps))
namedSps = zip (reverse (name: tail (take (length asps)
(iterate inc (extName "E" name)))))
anaPlainSpec addSyms lg opts dg nsig name DGFree (FreeDef nsig)
return (Free_spec nasp poss, nsig', dg')
Cofree_spec asp poss -> do
anaPlainSpec addSyms lg opts dg nsig name DGCofree (CofreeDef nsig)
return (Cofree_spec nasp poss, nsig', dg')
Local_spec asp asp' poss ->
(sp2, nsig'@(NodeSig _ (G_sign lid' sigma' _)), dg') <-
ana_SPEC False lg dg nsig (extName "L" name) opts sp1
(sp2', NodeSig n'' (G_sign lid'' sigma'' _), dg'') <-
ana_SPEC False lg dg' (JustNode nsig') (inc name) opts sp1'
let gsigma = getMaybeSig nsig
G_sign lid sigma _ <- return gsigma
sigma1 <- coerceSign lid' lid "Analysis of local spec" sigma'
sigma2 <- coerceSign lid'' lid "Analysis of local spec" sigma''
let sys = ext_sym_of lid sigma
sys1 = ext_sym_of lid sigma1
sys2 = ext_sym_of lid sigma2
mor3 <- if isStructured opts then return (ext_ide lid sigma2)
else adjustPos poss $ ext_cogenerated_sign lid
let sigma3 = dom lid mor3
-- gsigma2 = G_sign lid sigma2
gsigma3 = G_sign lid (makeExtSign lid sigma3) 0
when (not( isStructured opts ||
"illegal use of locally declared symbols: "
let (ns@(NodeSig node _), dg2) = insGSig dg'' name DGLocal gsigma3
return (Local_spec (replaceAnnoted sp2 asp)
(replaceAnnoted sp2' asp')
insLink dg2 (gEmbed2 gsigma3 $ mkG_morphism lid mor3)
HidingDef DGLocal n'' node)
-- analyse spec with empty local env
(sp', NodeSig n' gsigma', dg') <-
ana_SPEC False lg dg (EmptyNode l) (inc name) opts sp1
let gsigma = getMaybeSig nsig
gsigma'' <- adj $ gsigUnion lg gsigma gsigma'
let (ns@(NodeSig node gsigma2), dg2) = insGSig dg' name DGClosed gsigma''
incl1 <- adj $ ginclusion lg gsigma gsigma2
incl2 <- adj $ ginclusion lg gsigma' gsigma2
let dg3 = insLink dg2 incl2 GlobalDef DGClosed n' node
return (Closed_spec (replaceAnnoted sp' asp) pos, ns, case nsig of
JustNode (NodeSig n _) ->
insLink dg3 incl1 GlobalDef DGClosedLenv n node)
Qualified_spec lognm@(Logic_name ln _) asp pos -> do
let newLG = lg { currentLogic = tokStr ln }
l <- lookupCurrentLogic "Qualified_spec" newLG
let newNSig = case nsig of
EmptyNode _ -> EmptyNode l
anaPlainSpec addSyms lg opts dg newNSig name DGLogicQual GlobalDef
return (Qualified_spec lognm nasp pos, nsig', dg')
(sp', nsig', dg') <- ana_SPEC addSyms lg dg nsig name opts (item asp)
return (Group (replaceAnnoted sp' asp) pos, nsig', dg')
Spec_inst spname afitargs pos0 -> let
pos = if null afitargs then tokPos spname else pos0
in case lookupGlobalEnvDG spname dg of
Just (SpecEntry gs@(imps, params, _, body@(NodeSig nB gsigmaB))) ->
case (\ x y -> (x , x - y)) (length afitargs) (length params) of
-- the case without parameters leads to a simpler dg
gsigma <- adj $ gsigUnion lg (getMaybeSig nsig) gsigmaB
let (fsig@(NodeSig node gsigma'), dg2) =
insGSig dg name (DGSpecInst spname) gsigma
incl <- adj $ ginclusion lg gsigmaB gsigma'
let dg3 = insLink dg2 incl GlobalDef (DGSpecInst spname) nB node
-- the subcase with empty local env leads to an even simpler dg
-- if the node shall not be named and the logic does not change,
if isInternal name && langNameSig gsigma' == langNameSig gsigmaB
-- then just return the body
then return (sp, body, dg)
-- otherwise, we need to create a new one
else return (sp, fsig, dg3)
-- the subcase with nonempty local env
JustNode (NodeSig n sigma) -> do
incl2 <- adj $ ginclusion lg sigma gsigma'
insLink dg3 incl2 GlobalDef (DGSpecInst spname) n node)
-- now the case with parameters
let fitargs = map item afitargs
(fitargs', dg', args, _) <- adj $ foldM (anaFitArg lg opts spname imps)
([], dg, [], extName "A" name) (zip params fitargs)
let actualargs = reverse args
(gsigma', morDelta) <- adj $ apply_GS lg gs actualargs
gsigmaRes <- adj $ gsigUnion lg (getMaybeSig nsig) gsigma'
let (ns@(NodeSig node gsigmaRes'), dg2) =
insGSig dg' name (DGSpecInst spname) gsigmaRes
incl1 <- adj $ ginclusion lg (getMaybeSig nsig) gsigmaRes'
incl2 <- adj $ ginclusion lg gsigma' gsigmaRes'
morDelta' <- comp Grothendieck (gEmbed morDelta) incl2
let dg3 = insLink dg2 morDelta' GlobalDef (DGSpecInst spname) nB node
JustNode (NodeSig n _) ->
insLink dg3 incl1 GlobalDef (DGSpecInst spname) n node
dg5 <- foldM (parLink lg DGFitSpec gsigmaRes' node) dg4
(map (uncurry replaceAnnoted)
(zip (reverse fitargs') afitargs))
-- finally the case with conflicting numbers of formal and actual parameters
(spstr ++ " expects " ++ show (length params) ++ " arguments"
++ " but was given " ++ show (length afitargs)) pos
("Structured specification " ++ spstr ++ " not found") pos
Data (Logic lidD) (Logic lidP) asp1 asp2 pos -> do
Comorphism cid <- adj $ logicInclusion lg (Logic lidD) (Logic lidP)
let lidD' = sourceLogic cid
(sp1', NodeSig n' (G_sign lid' sigma' _), dg') <-
ana_SPEC False lg dg (EmptyNode (Logic lidD)) (inc name) opts sp1
sigmaD <- adj $ coerceSign lid' lidD' "Analysis of data spec" sigma'
(sigmaD',sensD') <- adj $ ext_map_sign cid sigmaD
let (nsig2@(NodeSig node _), dg1) = insGTheory dg' name DGData
$ G_theory lidP' sigmaD' 0 (toThSens sensD') 0
dg2 = insLink dg1 (GMorphism cid sigmaD 0
(ext_ide lidP' sigmaD') 0)
ana_SPEC addSyms lg dg2 (JustNode nsig2) name opts sp2
return (Data (Logic lidD) (Logic lidP)
(replaceAnnoted sp1' asp1)
(replaceAnnoted sp2' asp2)
anaPlainSpec :: Bool -> LogicGraph -> HetcatsOpts -> DGraph -> MaybeNode
-> NODE_NAME -> DGOrigin -> DGLinkType -> Annoted SPEC -> Range
-> Result (Annoted SPEC, NodeSig, DGraph)
anaPlainSpec addSyms lg opts dg nsig name orig dglType asp pos = do
(sp', NodeSig n' gsigma, dg') <-
ana_SPEC addSyms lg dg nsig (inc name) opts $ item asp
let (ns@(NodeSig node gsigma'), dg2) = insGSig dg' name orig gsigma
incl <- adjustPos pos $ ginclusion lg (getMaybeSig nsig) gsigma'
return (replaceAnnoted sp' asp, ns,
insLink dg2 incl dglType orig n' node)
anaFitArg :: LogicGraph -> HetcatsOpts -> SPEC_NAME -> MaybeNode
-> ([FIT_ARG], DGraph, [(G_morphism, NodeSig)], NODE_NAME)
-> Result ([FIT_ARG], DGraph, [(G_morphism, NodeSig)], NODE_NAME)
anaFitArg lg opts spname imps (fas', dg1, args, name') (nsig', fa) = do
(fa', dg', arg) <- ana_FIT_ARG lg dg1 spname imps nsig' opts name' fa
return (fa' : fas', dg', arg : args , inc name')
parLink :: LogicGraph -> DGOrigin -> G_sign -> Node -> DGraph -> NodeSig
parLink lg orig gsigma' node dg (NodeSig nA_i sigA_i)= do
incl <- ginclusion lg sigA_i gsigma'
return $ insLink dg incl GlobalDef orig nA_i node
ana_ren :: LogicGraph -> HetcatsOpts -> MaybeNode -> Range -> GMorphism
-> G_mapping -> Result GMorphism
ana_ren lg opts lenv pos gmor@(GMorphism r sigma ind1 mor _) gmap =
let adj = adjustPos pos in case gmap of
G_symb_map (G_symb_map_items_list lid sis) ->
if isStructured opts then return gmor else do
sis1 <- adj $ coerceSymbMapItemsList lid lid2 "Analysis of renaming" sis
rmap <- adj $ stat_symb_map_items lid2 sis1
mor1 <- adj $ induced_from_morphism lid2 rmap (cod lid2 mor)
JustNode (NodeSig _ (G_sign lidLenv sigmaLenv _)) -> do
-- needs to be changed for logic translations
sigmaLenv' <- coerceSign lidLenv lid2
"Analysis of renaming: logic translations not properly handeled"
let sysLenv = ext_sym_of lid2 sigmaLenv'
when (not $
Set.null forbiddenSys) $ plain_error () (
"attempt to rename the following symbols from " ++
"the local environment:\n" ++ showDoc forbiddenSys "") pos
mor2 <- adj $ comp lid2 mor mor1
return $ GMorphism r sigma ind1 mor2 0
G_logic_translation (Logic_code tok src tar pos1) -> do
let adj1 = adjustPos $ if pos1 == nullRange then pos else pos1
G_sign srcLid srcSig ind<- return (cod Grothendieck gmor)
Comorphism cid <- lookupComorphism (tokStr ctok) lg
when (isJust src && getLogicStr (fromJust src) /=
language_name (sourceLogic cid))
(fail (getLogicStr (fromJust src) ++
"is not the source logic of "
when (isJust tar && getLogicStr (fromJust tar) /=
language_name (targetLogic cid))
(fail (getLogicStr (fromJust tar) ++
"is not the target logic of "
Just (Logic_name l _) -> do
tarL <- lookupLogic "with logic: " (tokStr l) lg
logicInclusion lg (Logic srcLid) tarL
Nothing -> fail "with logic: cannot determine comorphism"
mor1 <- adj1 $ gEmbedComorphism c (G_sign srcLid srcSig ind)
adj $ comp Grothendieck gmor mor1
where getLogicStr (Logic_name l _) = tokStr l
ana_RENAMING :: LogicGraph -> MaybeNode -> G_sign -> HetcatsOpts -> RENAMING
ana_RENAMING lg lenv gSigma opts (Renaming ren pos) =
foldM (ana_ren lg opts lenv pos) (ide Grothendieck gSigma) ren
-- analysis of restrictions
ana_restr :: G_sign -> Range -> GMorphism -> G_hiding -> Result GMorphism
ana_restr (G_sign lidLenv sigmaLenv _) pos
(GMorphism cid (ExtSign sigma1 sys1) _ mor _) gh =
G_symb_list (G_symb_items_list lid' sis') -> do
let lid1 = sourceLogic cid
sis1 <- coerceSymbItemsList lid' lid1 "Analysis of restriction" sis'
rsys <- stat_symb_items lid1 sis1
let sys = sym_of lid1 sigma1
sys' =
Set.filter (\ sy -> any (matches lid1 sy) rsys) sys
( \ sy -> matches lid1 sy rsy) sys') rsys
when (not $ null unmatched)
$ plain_error () ("attempt to hide unknown symbols:\n"
++ showDoc unmatched "") pos
-- needs to be changed when logic projections are implemented
sigmaLenv' <- coerceSign lidLenv lid1
"Analysis of restriction: logic projections not properly handeled"
let sysLenv = ext_sym_of lid1 sigmaLenv'
"attempt to hide the following symbols from the local environment:\n"
++ showDoc forbiddenSys "") pos
mor1 <- cogenerated_sign lid1 sys' sigma1
mor1' <- map_morphism cid mor1
mor2 <- comp lid2 mor1' mor
return $ GMorphism cid (ExtSign (dom lid1 mor1) $
Set.fold (\ sy ->
G_logic_projection (Logic_code _tok _src _tar pos1) ->
fatal_error "no analysis of logic projections yet" pos1
ana_RESTRICTION :: G_sign -> G_sign -> HetcatsOpts -> RESTRICTION
-> Result (GMorphism, Maybe GMorphism)
ana_RESTRICTION gSigma@(G_sign lid sigma _)
gSigma'@(G_sign lid' sigma' _) opts restr =
if isStructured opts then return (ide Grothendieck gSigma, Nothing) else
mor <- foldM (ana_restr gSigma pos) (ide Grothendieck gSigma') rstr
Revealed (G_symb_map_items_list lid1 sis) pos -> do
let sys = ext_sym_of lid sigma -- local env
sys' = ext_sym_of lid' sigma' -- "big" signature
sis' <- adj $ coerceSymbMapItemsList lid1 lid'
"Analysis of restriction" sis
rmap <- adj $ stat_symb_map_items lid' sis'
-- domain of rmap intersected with sys'
-- domain of rmap should be checked to match symbols from sys' ???
sys1 <- adj $ coerceSymbolSet lid lid' "Analysis of restriction" sys
-- ??? this is too simple in case that local env is translated
mor1 <- adj $ ext_generated_sign lid' (sys1 `
Set.union` sys'') sigma'
mor2 <- adj $ induced_from_morphism lid' rmap (dom lid' mor1)
return (gEmbed (mkG_morphism lid' mor1),
Just (gEmbed (mkG_morphism lid' mor2)))
ana_FIT_ARG :: LogicGraph -> DGraph -> SPEC_NAME -> MaybeNode
-> NodeSig -> HetcatsOpts -> NODE_NAME -> FIT_ARG
-> Result (FIT_ARG, DGraph, (G_morphism,NodeSig))
ana_FIT_ARG lg dg spname nsigI (NodeSig nP gsigmaP@(G_sign lidP sigmaP _))
opts name fv = case fv of
Fit_spec asp gsis pos -> do
(sp', nsigA@(NodeSig nA (G_sign lidA sigmaA _)), dg') <-
ana_SPEC False lg dg nsigI name opts (item asp)
G_symb_map_items_list lid sis <- homogenizeGM (Logic lidP) gsis
sigmaA' <- adj $ coerceSign lidA lidP "Analysis of fitting argument" sigmaA
mor <- adj $ if isStructured opts then return (ext_ide lidP sigmaP)
rmap <- stat_symb_map_items lid sis
else coerceRawSymbolMap lid lidP
"Analysis of fitting argument" rmap
(\ s -> matches lidP s r) $ ext_sym_of lidP sig
unknowns = filter (noMatch sigmaP) (
Map.keys rmap')
++ filter (noMatch sigmaA') (
Map.elems rmap')
ext_induced_from_to_morphism lidP rmap' sigmaP sigmaA'
else fatal_error ("unknown symbols " ++ showDoc unknowns "") pos
let symI = sym_of lidP sigmaI'
symmap_mor = symmap_of lidP mor
-- are symbols of the imports left untouched?
if
Set.all (\sy -> lookupFM symmap_mor sy == Just sy) symI
else plain_error () "Fitting morphism must not affect import" pos
-- ??? also output some symbol that is affected
let gmor = mkG_morphism lidP mor
return (Fit_spec (replaceAnnoted sp' asp) gsis pos,
insLink dg' (gEmbed gmor) (GlobalThm LeftOpen None LeftOpen)
(DGSpecInst spname) nP nA, (gmor, nsigA))
Fit_view vn afitargs pos -> let
in case lookupGlobalEnvDG vn dg of
Just (ViewEntry (src, mor, gs@(imps, params, _, target))) -> do
gsigmaI = getMaybeSig nsigI
GMorphism cid _ _ morHom ind <- return mor
let lid = targetLogic cid
when (not (language_name (sourceLogic cid) == language_name lid))
"heterogeneous fitting views not yet implemented"
case (\ x y -> (x, x - y)) (length afitargs) (length params) of
-- the case without parameters leads to a simpler dg
-- the subcase with empty import leads to a simpler dg
return (fv, insLink dg (ide Grothendieck gsigmaP)
(GlobalThm LeftOpen None LeftOpen) (DGFitView spname)
nP nSrc, (G_morphism lid morHom ind, target))
-- the subcase with nonempty import
JustNode (NodeSig nI _) -> do
gsigmaIS <- adj $ gsigUnion lg gsigmaI gsigmaS
when (not (isSubGsign lg gsigmaP gsigmaIS))
("Parameter does not match source of fittig view. "
++ "Parameter signature:\n"
"\nSource signature of fitting view (united with import):\n"
++ showDoc gsigmaIS "") pos)
G_sign lidI sigI1 _<- return gsigmaI
sigI <- adj $ coerceSign lidI lid
"Analysis of instantiation with import" sigI1
mor_I <- adj $ morphism_union lid morHom $ ext_ide lid sigI
gsigmaA <- adj $ gsigUnion lg gsigmaI gsigmaT
incl1 <- adj $ ginclusion lg gsigmaI gsigmaA
incl2 <- adj $ ginclusion lg gsigmaT gsigmaA
incl3 <- adj $ ginclusion lg gsigmaI gsigmaP
incl4 <- adj $ ginclusion lg gsigmaS gsigmaP
let (ns@(NodeSig nA _), dg1) =
insGSig dg name (DGFitViewA spname) gsigmaA
insGSig dg1 (inc name) (DGFitView spname) gsigmaP
dg3 = insLink dg2 incl1 GlobalDef (DGFitViewAImp spname) nI nA
dg4 = insLink dg3 incl3 GlobalDef (DGFitViewImp spname) nI n'
dg5 = insLink dg4 incl2 GlobalDef (DGFitViewA spname) nTar nA
dg6 = insLink dg5 incl4 GlobalDef (DGFitView spname) nSrc n'
dg7 = insLink dg6 (ide Grothendieck gsigmaP)
(GlobalThm LeftOpen None LeftOpen) (DGFitView spname) nP n'
return (fv, dg7, (mkG_morphism lid mor_I, ns))
-- now the case with parameters
let fitargs = map item afitargs
(fitargs', dg', args,_) <- foldM (anaFitArg lg opts spname imps)
([], dg, [], extName "A" name) (zip params fitargs)
let actualargs = reverse args
(gsigmaA,mor_f) <- adj $ apply_GS lg gs actualargs
let gmor_f = gEmbed mor_f
gsigmaRes <- adj $ gsigUnion lg gsigmaI gsigmaA
mor1 <- adj $ comp Grothendieck mor gmor_f
incl1 <- adj $ ginclusion lg gsigmaA gsigmaRes
mor' <- adj $ comp Grothendieck gmor_f incl1
GMorphism cid1 _ _ mor1Hom _<- return mor1
let lid1 = targetLogic cid1
when (not (language_name (sourceLogic cid1) == language_name lid1))
("heterogeneous fitting views not yet implemented")
G_sign lidI sigI1 _<- return gsigmaI
sigI <- adj $ coerceSign lidI lid1
"Analysis of instantiation with parameters" sigI1
theta <- adj $ morphism_union lid1 mor1Hom (ext_ide lid1 sigI)
incl2 <- adj $ ginclusion lg gsigmaI gsigmaRes
incl3 <- adj $ ginclusion lg gsigmaI gsigmaP
incl4 <- adj $ ginclusion lg gsigmaS gsigmaP
let (ns@(NodeSig nA _), dg1) =
insGSig dg' name (DGFitViewA spname) gsigmaRes
insGSig dg1 (extName "V" name) (DGFitView spname) gsigmaP
dg3 <- foldM (parLink lg (DGFitView spname) gsigmaRes nA) dg2
JustNode (NodeSig nI _) -> let
dg3a = insLink dg3 incl2 GlobalDef (DGFitViewAImp spname) nI nA
in insLink dg3a incl3 GlobalDef (DGFitViewImp spname) nI n'
dg5 = insLink dg4 mor' GlobalDef (DGFitViewA spname) nTar nA
dg6 = insLink dg5 incl4 GlobalDef (DGFitView spname) nSrc n'
dg7 = insLink dg6 (ide Grothendieck gsigmaP)
(GlobalThm LeftOpen None LeftOpen) (DGFitView spname) nP n'
(map (uncurry replaceAnnoted)
(zip (reverse fitargs') afitargs))
pos, dg7, (mkG_morphism lid1 theta, ns))
-- finally the case with conflicting numbers of formal and actual parameters
(spstr ++ " expects " ++ show (length params) ++ " arguments"
++ " but was given " ++ show (length afitargs)) pos
("View " ++ tokStr vn ++ " not found") pos
-- Extension of signature morphisms (for instantitations)
-- first some auxiliary functions
mapID idmap i@(Id toks comps pos1) =
compsnew <- sequence $ map (mapID idmap) comps
return (Id toks compsnew pos1)
Just ids -> if
Set.null ids then return i else
("Identifier component " ++ showId i
" can be mapped in various ways:\n"
++ showDoc ids "") $ getRange i
-> Result (EndoMap Id) -> Result (EndoMap Id)
extID1 idmap i@(Id toks comps pos1) m = do
compsnew <- sequence $ map (mapID idmap) comps
else return (
Map.insert i (Id toks compsnew pos1) m1)
extendMorphism :: G_sign -- ^ formal parameter
-> G_sign -- ^ actual parameter
-> G_morphism -- ^ fitting morphism
-> Result(G_sign,G_morphism)
extendMorphism (G_sign lid sigmaP _) (G_sign lidB sigmaB1 _)
(G_sign lidA sigmaA1 _) (G_morphism lidM fittingMor1 _) = do
-- for now, only homogeneous instantiations....
sigmaB@(ExtSign _ sysB) <-
coerceSign lidB lid "Extension of symbol map" sigmaB1
sigmaA <- coerceSign lidA lid "Extension of symbol map" sigmaA1
fittingMor <- coerceMorphism lidM lid "Extension of symbol map" fittingMor1
let symsP = ext_sym_of lid sigmaP
symsB = ext_sym_of lid sigmaB
idsB =
Set.map (sym_name lid) symsB
h = symmap_of lid fittingMor
rh = symbMapToRawSymbMap h
(\sy1 sy2 ->
Rel.setInsert (sym_name lid sy1) (sym_name lid sy2))
(id_to_raw lid id1) (id_to_raw lid id2))
-- do we need combining function catching the clashes???
mor <- ext_induced_from_morphism lid r sigmaB
let hmor = symmap_of lid mor
sigmaAD = ExtSign (cod lid mor) $
Set.map (\ sy ->
sigma <- ext_final_union lid sigmaA sigmaAD
(plain_error () ("Symbols shared between actual parameter and body"
++ "\nmust be in formal parameter:\n"
++ showDoc illShared "") nullRange)
comb2 p qs [] ++ comb1 qs
comb2 p@(a, b) ((c, d) : qs) rs =
comb2 p qs $ if b == d then (a, c) : rs else rs
newIdentifications = myKernel hmor Set.\\ myKernel h
when (not (
Set.null newIdentifications))
"Fitting morphism leads to forbidden identifications:\n"
++ showDoc newIdentifications "") nullRange)
incl <- ext_inclusion lid sigmaAD sigma
mor1 <- comp lid mor incl
return (G_sign lid sigma 0, mkG_morphism lid mor1)
apply_GS :: LogicGraph -> ExtGenSig -> [(G_morphism,NodeSig)]
-> Result(G_sign,G_morphism)
apply_GS lg (nsigI, _, gsigmaP, nsigB) args = do
gsigmaA_i = map (getSig . snd) args
gsigmaI = getMaybeSig nsigI
G_sign lidI sigmaI _<- return gsigmaI
let idI = ext_ide lidI sigmaI
gsigmaA <- gsigManyUnion lg gsigmaA_i
mor_f <- homogeneousMorManyUnion (mkG_morphism lidI idI : mor_i)
extendMorphism gsigmaP gsigmaB gsigmaA mor_f
-> Result G_symb_map_items_list
homogenizeGM (Logic lid) gsis =
foldM homogenize1 (G_symb_map_items_list lid []) gsis
homogenize1 itl2@(G_symb_map_items_list lid2 sis) sm = case sm of
sis1' <- coerceSymbMapItemsList lid1 lid2 "" sis1
return $ G_symb_map_items_list lid2 $ sis ++ sis1'
-- | check if structured analysis should be performed
isStructured :: HetcatsOpts -> Bool
isStructured a = case analysis a of
-- only consider addSyms for the first spec
:: ([SPEC], MaybeNode, DGraph, LogicGraph, HetcatsOpts, Range, Bool)
-> (NODE_NAME, Annoted SPEC)
-> Result ([SPEC], MaybeNode, DGraph, LogicGraph, HetcatsOpts, Range, Bool)
ana_Extension (sps', nsig', dg', lg, opts, pos, addSyms) (name',asp') = do
(sp1', nsig1@(NodeSig n1 sig1), dg1) <-
ana_SPEC addSyms lg dg' nsig' name' opts (item asp')
let anno = find isSemanticAnno $ l_annos asp'
-- is the extension going between real nodes?
dg2 <- case (anno, nsig') of
(Just anno0@(Semantic_anno anno1 _), JustNode (NodeSig n' sig')) -> do
-- any other semantic annotation? that's an error
when (any (\an -> isSemanticAnno an && an/=anno0) $ l_annos asp')
(plain_error () "Conflicting semantic annotations"
-- %implied should not occur here
"Annotation %implied should come after a BASIC-ITEM"
if anno1==SA_implies then do
when (not (isHomSubGsign sig1 sig')) (plain_error ()
"Signature must not be extended in presence of %implies"
-- insert a theorem link according to p. 319 of the CASL Reference Manual
return $ insLink dg1 (ide Grothendieck sig1)
(GlobalThm LeftOpen None LeftOpen) DGExtension n1 n'
let anno2 = case anno1 of
-- insert a theorem link according to p. 319 of the CASL Reference Manual
-- the theorem link is trivally proved by the parallel definition link,
-- but for clarity, we leave it open here
-- the interesting open proof obligation is anno2, of course
incl <- ginclusion lg sig' sig1
return $ insLink dg1 incl (GlobalThm LeftOpen anno2 LeftOpen)
return (sp1' : sps', JustNode nsig1, dg2, lg, opts, pos, True)