a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach{- HetCATS/AnalysisStructured.hs

8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy Gimblett $Id$

e071fb22ea9923a2a4ff41184d80ca46b55ee932Till Mossakowski Till Mossakowski

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder Analysis of structured specifications

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

b4fbc96e05117839ca409f5f20f97b3ac872d1edTill Mossakowski Follows the extended static semantic rules in:

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach T. Mossakowski, S. Autexier, D. Hutter, P. Hoffman:

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach CASL Proof calculus.

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder Available from http://www.informatik.uni-bremen.de/~till/calculus.ps

8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy Gimblett To appear in the CASL book.

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach Todo:

fbb2d28086a1860850f661fbf4af531322bac405Christian Maeder Check that translations and reductions do not effect local env

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach Unions (already in the parser) need unions of logics

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach = suprema in the lattice of default logic inclusions!

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach Should we use institution independent analysis over the Grothendieck logic?

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett abstract syntax + devgraph would have to be changed to homogeneous case

cdf1545bdcd39a9d53c00761ffa42e7b1174b91eLiam O'Reilly logic translations are symbol maps in the Grothendieck logic

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett Problem with this approach: symbol functor goes into rel,

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder and induced_from_morphism gets difficult to implement

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett Unions need inclusion morphisms. Should these play a special role?

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett At least we need a function delivering the inclusion morphism

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett between two (sub)signatures.

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder In most logics, inclusions could be represented specially, such

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett that composition for them becomes fast.

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder Should we even identify an inclusion subcategory?

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder Treatment of translations and reductions along logic translations

90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett (see WADT 02 paper).

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett Open question:

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett may local env be translated, and even reduced, along logic translations?

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett if yes: how is local env linked to signature of resulting spec?

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett (important e.g. for checking that local env is not being renamed?)

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett does signature+comorphism suffice, such that c(local env)\subseteq sig?

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett if no: this means that only closed specs may be translated

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett Pushouts: only admissible within one logic?

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett-}

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblettmodule AnalysisStructured

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblettwhere

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblettimport Maybe

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maederimport Logic

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettimport LogicRepr

90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblettimport Grothendieck

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblettimport Graph

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblettimport DevGraph

90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblettimport AS_Structured

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettimport AS_Annotation

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblettimport GlobalAnnotations

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maederimport Result

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettimport Id

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettimport Set

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblettimport FiniteMap

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian MaederlookupNode n dg = lab' $ context n dg

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian MaedersetFilter p s = mkSet (filter p (setToList s))

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian MaedersetAny p s = any p (setToList s)

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeders1 `disjoint` s2 = s1 `intersect` s2 == emptySet

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy GimblettdomFM m = mkSet (keysFM m)

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettana_SPEC :: GlobalAnnos -> GlobalEnv -> DGraph -> NodeSig -> SPEC

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett -> Result (NodeSig,DGraph)

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maederana_SPEC gannos genv dg nsig sp =

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett case sp of

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett Basic_spec (G_basic_spec lid bspec) ->

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder do Logic lid' <- return (getLogic nsig)

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder sigma <- rcoerce lid' lid nullPos (getSig nsig)

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett b <- maybeToResult nullPos

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett ("no basic analysis for logic "++language_name lid)

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett (basic_analysis lid)

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett (sigma_local, sigma_complete, ax) <- b (bspec,sigma,gannos)

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder let node_contents = DGNode {

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder dgn_sign = G_sign lid sigma_local, -- only the delta

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett dgn_sens = G_l_sentence lid ax,

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett dgn_origin = DGBasic }

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder [node] = newNodes 1 dg

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett dg' = insNode (node,node_contents) dg

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder link = DGLink {

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder dgl_morphism = undefined, -- where to get it from ???

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett dgl_type = GlobalDef,

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett dgl_origin = DGExtension }

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett dg'' = case nsig of

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett EmptyNode _ -> dg'

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett NodeSig (n,_) -> insEdge (n,node,link) dg'

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett return (NodeSig (node,G_sign lid sigma_complete),dg')

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett Translation asp ren ->

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach do let sp = item asp

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett (nsig',dg') <- ana_SPEC gannos genv dg nsig sp

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett n' <- maybeToResult nullPos "Translation of empty spec" (getNode nsig')

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett mor <- ana_RENAMING dg (getSig nsig') ren

929190acb9f2b2f5857dce841c5a389710895515Andy Gimblett -- ??? check that mor is identity on local env

cdf1545bdcd39a9d53c00761ffa42e7b1174b91eLiam O'Reilly let gsigma' = cod Grothendieck mor

cdf1545bdcd39a9d53c00761ffa42e7b1174b91eLiam O'Reilly -- ??? too simplistic for non-comorphism inter-logic translations

cdf1545bdcd39a9d53c00761ffa42e7b1174b91eLiam O'Reilly G_sign lid' sigma' <- return gsigma'

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett let node_contents = DGNode {

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett dgn_sign = G_sign lid' (empty_signature lid'), -- delta is empty

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett dgn_sens = G_l_sentence lid' [],

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett dgn_origin = DGTranslation }

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett [node] = newNodes 1 dg'

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett link = DGLink {

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett dgl_morphism = mor,

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett dgl_type = GlobalDef,

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett dgl_origin = DGTranslation }

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett return (NodeSig(node,gsigma'),

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett insEdge (n',node,link) $

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett insNode (node,node_contents) dg')

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett Reduction asp restr ->

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett do let sp = item asp

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett (nsig',dg') <- ana_SPEC gannos genv dg nsig sp

eca4db63ed0bdbd93b62678feea6e3eb80aa47bbChristian Maeder let gsigma = getSig nsig

1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski gsigma' = getSig nsig'

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett n' <- maybeToResult nullPos "Reduction of empty spec" (getNode nsig')

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett (hmor,tmor) <- ana_RESTRICTION dg gsigma gsigma' restr

1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski -- we treat hiding and revealing differently

1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski -- in order to keep the dg as simple as possible

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett case tmor of

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett Nothing ->

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett do let gsigma' = dom Grothendieck hmor

41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimblett -- ??? too simplistic for non-comorphism inter-logic reductions

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett G_sign lid' sigma' <- return gsigma'

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett let node_contents = DGNode {

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder dgn_sign = G_sign lid' (empty_signature lid'),

b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski dgn_sens = G_l_sentence lid' [],

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder dgn_origin = DGHiding }

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder [node] = newNodes 1 dg'

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder link = DGLink {

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder dgl_morphism = hmor,

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder dgl_type = HidingDef,

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder dgl_origin = DGHiding }

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder return (NodeSig(node,gsigma'),

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder insEdge (n',node,link) $

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder insNode (node,node_contents) dg')

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder Just tmor' ->

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder do let gsigma1 = dom Grothendieck tmor'

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder gsigma'' = cod Grothendieck tmor'

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett -- ??? too simplistic for non-comorphism inter-logic reductions

b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski G_sign lid1 sigma1 <- return gsigma1

41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimblett G_sign lid'' sigma'' <- return gsigma''

41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimblett let [node1,node''] = newNodes 2 dg'

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder node_contents1 = DGNode {

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett dgn_sign = G_sign lid1 (empty_signature lid1),

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett dgn_sens = G_l_sentence lid1 [],

1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski dgn_origin = DGRevealing }

b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski link1 = DGLink {

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett dgl_morphism = hmor,

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett dgl_type = HidingDef,

41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimblett dgl_origin = DGRevealing }

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett node_contents'' = DGNode {

dgn_sign = G_sign lid'' (empty_signature lid''),

dgn_sens = G_l_sentence lid'' [],

dgn_origin = DGRevealTranslation }

link'' = DGLink {

dgl_morphism = tmor',

dgl_type = GlobalDef,

dgl_origin = DGRevealTranslation }

return (NodeSig(node'',gsigma''),

insEdge (node1,node'',link'') $

insNode (node'',node_contents'') $

insEdge (n',node1,link1) $

insNode (node1,node_contents1) dg')

Union [] pos -> return (nsig,dg)

Union asps pos ->

do let sps = map item asps

(nsigs,dg') <- let ana r sp = do

(nsigs,dg) <- r

(nsig,dg1) <- ana_SPEC gannos genv dg nsig sp

return (nsig:nsigs,dg1)

in foldl ana (return ([],dg)) sps

G_sign lid' sigma' <- return (getSig (head nsigs))

let nsigs' = reverse nsigs

nodes = catMaybes (map getNode nsigs')

sigmas <- let coerce_lid (G_sign lid1 sigma1) =

rcoerce lid' lid1 (head (pos++nullPosList)) sigma1

in sequence (map (coerce_lid . getSig) (tail nsigs'))

big_sigma <- let sig_union s1 s2 = do

s1' <- s1

signature_union lid' s1' s2

in foldl sig_union (return sigma') sigmas

let node_contents = DGNode {

dgn_sign = G_sign lid' (empty_signature lid'),

dgn_sens = G_l_sentence lid' [],

dgn_origin = DGUnion }

[node] = newNodes 1 dg'

link = DGLink {

dgl_morphism = undefined, -- ??? how to get it?

dgl_type = GlobalDef,

dgl_origin = DGUnion }

return (let insE dg n = insEdge (n,node,link) dg -- link should vary

in (NodeSig(node,G_sign lid' big_sigma),

foldl insE (insNode (node,node_contents) dg') nodes))

Extension asps pos ->

foldl ana (return (nsig,dg)) (map item asps)

where

ana res sp = do

(nsig,dg) <- res

ana_SPEC gannos genv dg nsig sp

Free_spec asp pos ->

ana_err "free specs"

Cofree_spec asp pos ->

ana_err "cofree specs"

Local_spec asp1 asp2 pos ->

ana_err "local specs"

Closed_spec asp pos ->

ana_err "closed specs"

Group asp pos ->

ana_SPEC gannos genv dg nsig (item asp)

Spec_inst spname afitargs ->

ana_err "spec inst"

Qualified_spec logname asp pos ->

ana_err "logic qualified specs"

-- analysis of renamings

ana_ren1 dg (GMorphism lid1 lid2 r sigma mor)

(G_symb_map (G_symb_map_items_list lid sis),pos) = do

sis1 <- rcoerce lid2 lid pos sis

rmap <- stat_symb_map_items lid2 sis1

mor1 <- induced_from_morphism lid2 rmap (cod lid2 mor)

mor2 <- maybeToResult pos

"renaming: signature morphism composition failed"

(comp lid2 mor mor1)

return (GMorphism lid1 lid2 r sigma mor2)

ana_ren1 dg mor (G_logic_translation (Logic_code tok src tar pos1),pos2) =

fatal_error "no analysis of logic translations yet" pos2

ana_ren :: DGraph -> Result GMorphism -> (G_mapping,Pos) -> Result GMorphism

ana_ren dg mor_res ren =

do mor <- mor_res

ana_ren1 dg mor ren

ana_RENAMING :: DGraph -> G_sign -> RENAMING -> Result GMorphism

ana_RENAMING dg gSigma (Renaming ren pos) =

foldl (ana_ren dg) (return (ide Grothendieck gSigma)) ren'

where

ren' = zip ren (tail (pos++nullPosList))

-- analysis of restrictions

ana_restr1 dg (G_sign lid sigma) (GMorphism lid1 lid2 r sigma1 mor)

(G_symb_list (G_symb_items_list lid' sis'),pos) = do

sis1 <- rcoerce lid1 lid' pos sis'

rsys <- stat_symb_items lid1 sis1

let sys = sym_of lid1 sigma1

let sys' = filter (\sy -> any (\rsy -> matches lid1 sy rsy) rsys)

(setToList sys)

-- if sys' `disjoint` () then return ()

-- else plain_error () "attempt to hide symbols from the local environment" pos

mor1 <- cogenerated_sign lid1 sys' sigma1

mor1' <- maybeToResult pos

("restriction: could not map morphism along" ++ repr_name r)

(map_morphism r mor1)

mor2 <- maybeToResult pos

"restriction: signature morphism composition failed"

(comp lid2 mor1' mor)

return (GMorphism lid1 lid2 r (dom lid1 mor1) mor2)

ana_restr1 dg gSigma mor

(G_logic_projection (Logic_code tok src tar pos1),pos2) =

fatal_error "no analysis of logic projections yet" pos2

ana_restr :: DGraph -> G_sign -> Result GMorphism -> (G_hiding,Pos)

-> Result GMorphism

ana_restr dg gSigma mor_res restr =

do mor <- mor_res

ana_restr1 dg gSigma mor restr

ana_RESTRICTION :: DGraph -> G_sign -> G_sign -> RESTRICTION

-> Result (GMorphism, Maybe GMorphism)

ana_RESTRICTION dg gSigma gSigma' (Hidden restr pos) =

do mor <- foldl (ana_restr dg gSigma)

(return (ide Grothendieck gSigma'))

restr'

return (mor,Nothing)

where

restr' = zip restr (tail (pos++nullPosList))

ana_RESTRICTION dg gSigma@(G_sign lid sigma) gSigma'@(G_sign lid' sigma')

(Revealed (G_symb_map_items_list lid1 sis) pos) =

do let sys = sym_of lid sigma

sys' = sym_of lid' sigma'

sis' <- rcoerce lid1 lid' (head (pos++nullPosList)) sis

rmap <- stat_symb_map_items lid' sis'

let sys'' =

mkSet

[sy | sy <- setToList sys', rsy <- keysFM rmap, matches lid' sy rsy]

sys1 <- rcoerce lid lid' (head (pos++nullPosList)) sys

-- ??? this is too simple in case that local env is translated

-- to a different logic

if sys1 `disjoint` sys'' then return ()

else plain_error () "attempt to hide symbols from the local environment" (head (pos++nullPosList))

mor1 <- generated_sign lid' (setToList (sys1 `union` sys'')) sigma'

mor2 <- induced_from_morphism lid' rmap (dom lid' mor1)

return (gEmbed (G_morphism lid' mor1),

Just (gEmbed (G_morphism lid' mor2)))

ana_GENERICITY :: GlobalAnnos -> GlobalEnv -> DGraph -> AnyLogic -> GENERICITY

-> Result (ExtGenSig,DGraph)

ana_GENERICITY gannos genv dg l

(Genericity (Params []) (Imported []) pos) =

return ((EmptyNode l,[],EmptyNode l),dg)

ana_GENERICITY gannos genv dg l (Genericity params imps pos) =

ana_err "parameterized specs"

---- helpers ---------------------------------

ana_err :: String -> a

ana_err fname =

error ("*** Analysis of \"" ++ fname ++ "\" is not yet implemented!")

----------------------------------------------