Basic_arch_spec udd uexpr pos ->
do (branchMap, uctx, dg', udd') <-
anaUnitDeclDefns lgraph libEnv ln dg opts eo sharedCtx udd
(nodes, usig, diag'', dg'', uexpr') <-
anaUnitExpression lgraph libEnv ln dg' opts eo uctx $ item uexpr
let (nodes', maybeRes) = case nodes of
[] -> ([], Nothing) -- don't think its possible
(n, dgI) = addNodeRT dg'' usig "ArchSpec"
in (n, addEdgesToNodeRT dgI rNodes n)
Just x -> (x, addEdgesToNodeRT dg' rNodes x)
rP = NPBranch rN branchMap
return (nodes', maybeRes, diag'',
BranchRefSig rP (usig, Just $ BranchStaticContext (ctx uctx)),
dg3, Basic_arch_spec udd'
(replaceAnnoted uexpr' uexpr) pos)
anaArchSpec lgraph libEnv ln dg opts eo sharedCtx nP (item asp)
asi <- expCurieR (globalAnnos dg) eo un'
case lookupGlobalEnvDG asi dg of
Just (ArchOrRefEntry True asig@(BranchRefSig
(NPBranch n f) (UnitSig nsList resNs _, _))) -> do
(dg0, g) = copySubTree dg n Nothing
(r1, d1) = (n0, dg0) -- TODO: this is not needed
a1 = setPointerInRef asig (NPBranch r1 $
(dg0, g) = copySubTree dg n Nothing
d1 = addRefEdgeRT dg0 x n0
a1 = setPointerInRef asig (NPBranch rN $
return ([], Nothing, snd sharedCtx, asig', dg', archSp)
(dnsigs, diag') <- foldM (\ (l, d) ns -> do
(dns, d') <- extendDiagramIncl lgraph d [] ns "Arch Sig"
([], snd sharedCtx) $ reverse nsList
extendDiagramIncl lgraph diag' dnsigs resNs "arch sig"
return (dns : dnsigs, Nothing, diag'', asig', dg', archSp)
_ -> notFoundError "architectural specification" asi
-- | Analyse a list of unit declarations and definitions
anaUnitDeclDefns :: LogicGraph -> LibEnv -> LibName -> DGraph
-> ExtStUnitCtx -> [Annoted UNIT_DECL_DEFN]
-> Result (
Map.Map IRI RTPointer, ExtStUnitCtx,
DGraph, [Annoted UNIT_DECL_DEFN])
{- ^ returns 1. extended static unit context 2. possibly modified
development graph 3. possibly modified list of unit declarations and
anaUnitDeclDefns lgraph libEnv ln dg opts eo sharedCtx =
anaUnitDeclDefns' lgraph libEnv ln dg opts eo sharedCtx
Map.emptyanaUnitDeclDefns' :: LogicGraph -> LibEnv -> LibName -> DGraph -> HetcatsOpts
-> ExtStUnitCtx ->
Map.Map IRI RTPointer
-> [Annoted UNIT_DECL_DEFN]
-> Result (
Map.Map IRI RTPointer, ExtStUnitCtx,
DGraph, [Annoted UNIT_DECL_DEFN])
anaUnitDeclDefns' lgraph libEnv ln dg opts eo uctx rNodes uds = case uds of
(rNodes1, uctx', dg', udd') <-
anaUnitDeclDefn lgraph libEnv ln dg opts eo uctx (item udd)
(rNodes2, uctx'', dg'', udds') <- anaUnitDeclDefns' lgraph libEnv ln dg' opts eo
return (rNodes2, uctx'', dg'', replaceAnnoted udd' udd : udds')
[] -> return (rNodes, uctx, dg, [])
alreadyDefinedUnit :: IRI -> String
-- | Create a node that represents a union of signatures
nodeSigUnion :: LogicGraph -> DGraph -> [MaybeNode] -> DGOrigin -> SPEC_NAME
-> Result (NodeSig, DGraph)
nodeSigUnion lgraph dg nodeSigs orig sname =
do sigUnion@(G_sign lid sigU ind) <- gsigManyUnion lgraph
$ map getMaybeSig nodeSigs
let unionName = makeName $
sname {abbrevPath = abbrevPath sname ++ "_union"}
nodeContents = newNodeLab
(unionName{extIndex = 1})
$ noSensGTheory lid sigU ind
dg' = insNodeDG (node, nodeContents) dg
JustNode (NodeSig n sig) -> do
incl <- ginclusion lgraph sig sigUnion
(n, node, globDefLink incl SeeTarget) dgv
dg'' <- foldl inslink (return dg') nodeSigs
return (NodeSig node sigUnion, dg'')
-- | Analyse unit declaration or definition
anaUnitDeclDefn :: LogicGraph -> LibEnv -> LibName -> DGraph -> HetcatsOpts
-> ExtStUnitCtx -> UNIT_DECL_DEFN
-> Result (
Map.Map IRI RTPointer, ExtStUnitCtx, DGraph, UNIT_DECL_DEFN)
{- ^ returns 1. extended static unit context 2. possibly modified
development graph 3. possibly modified UNIT_DECL_DEFN -}
anaUnitDeclDefn lgraph libEnv ln dg opts eo uctx@(buc, _) udd = case udd of
Unit_decl un' usp uts pos -> do
unIRI <- expCurieR (globalAnnos dg) eo un'
let ustr = iriToStringShortUnsecure unIRI
(dns, diag', dg', uts') <-
anaUnitImported lgraph libEnv ln dg opts eo uctx pos uts
let impSig = toMaybeNode dns
(nodes, maybeRes, mDiag, rsig', dg0, usp') <- anaRefSpec lgraph libEnv ln
dg' opts eo impSig unIRI (buc, diag') Nothing usp
usig@(UnitSig argSigs resultSig unionSig) <- getUnitSigFromRef rsig'
case getPointerFromRef rsig' of
(n', d') = addNodeRT dg0 usig ustr
r' = setPointerInRef rsig' (NPUnit n')
_ -> (refSource $ getPointerFromRef rsig', dg0, rsig')
{- is this above needed? when can rsig' have no pointer?
ANSWER: when it's just a unit sig -}
(dg'', rsig) <- case impSig of
(resultSig', dg2) <- case unionSig of
Just x -> nodeSigUnion lgraph dg1
[JustNode x, JustNode resultSig] DGImports unIRI
_ -> return (resultSig, dg1)
return (updateNodeNameRT dg2 n False ustr,
setUnitSigInRef rsig0 $ UnitSig argSigs resultSig' unionSig)
-- S -> T becomes S -> S \cup T
let dg2 = updateNodeNameRT dg1 n False ustr
-- this changes the name of the node in the RT
(argUnion, dg3) <- nodeSigUnion lgraph dg2
(map JustNode argSigs ++ [impSig])
-- union of the arguments with the imports
(resultSig', dg4) <- nodeSigUnion lgraph dg3
[JustNode resultSig, JustNode argUnion] DGImports
{- union of the arguments with the result
becomes F : M * S -> S_M \cup S \cup T -}
let dgU = updateSigRT dg4 n $ UnitSig [] resultSig' Nothing
usig' = UnitSig (ns : argSigs) resultSig' $ Just argUnion
(newN, dgU') = addNodeRT dgU usig' ""
[(simpleIdToIRI $ mkSimpleId "a", NPUnit newN)]
rUnit = UnitSig argSigs resultSig' $ Just argUnion
rSig = BranchRefSig newP (rUnit, Just $ BranchStaticContext $
return (addEdgesToNodeRT dgU' [newN] n, rSig)
let diag = fromMaybe diag' mDiag
ud' = Unit_decl unIRI usp' uts' pos
ComponentRefSig _ _ -> error $
"component refinement forbidden in arch spec: unit"
then plain_error (
Map.empty, uctx, dg'', ud')
(alreadyDefinedUnit unIRI) (iriPos unIRI)
_usigN@(UnitSig argSigsN resultSig' unionSigN) <-
(basedParUSig, diag''') <- if null argSigsN then do
(dn', diag'') <- extendDiagramIncl lgraph diag
_ -> [])) resultSig' ustr
return (Based_unit_sig dn' rsig, diag'')
else if length nodes < 2 then do
-- clarify the pointers here
UnitSig argSigsN resultSig' unionSigN)
return (Based_par_unit_sig dns rsig''
-- here we handle U : arch spec ASP with ASP parametric
let rsig'' = setPointerInRef
(setUnitSigInRef rsig usig)
return (Based_lambda_unit_sig nodes rsig'',
Unit_defn un' uexp poss -> do
un <- expCurieR (globalAnnos dg) eo un'
(nodes, usig, diag, dg'', uexp') <-
anaUnitExpression lgraph libEnv ln dg opts eo uctx uexp
let ud' = Unit_defn un uexp' poss
(alreadyDefinedUnit un) $ iriPos un
{- we can use
Map.insert as there are no mappings for
un in ps and bs (otherwise there would have been a
mapping in (ctx uctx)) -}
UnitSig args _ _ -> case args of
let bsig = Based_unit_sig dn $
_ -> error "anaUnitDeclDefn"
(Based_lambda_unit_sig nodes $
_ -> error "anaUnitDeclDefn:lambda expression"
anaUnitRef :: LogicGraph -> LibEnv -> LibName -> DGraph -> HetcatsOpts
-> ExtStUnitCtx -> Maybe RTPointer -> UNIT_REF
-> Result ((UNIT_NAME, RefSig), DGraph, UNIT_REF)
{- ^ returns 1. extended static unit context 2. possibly modified
development graph 3. possibly modified UNIT_DECL_DEFN -}
anaUnitRef lgraph libEnv ln dg opts eo _uctx@(_ggbuc, _diag') rN
(Unit_ref un' usp pos) = do
un <- expCurieR (globalAnnos dg) eo un'
(error "component not in map!") un f
(error "component not in map!") un f
curl <- lookupCurrentLogic "UNIT_REF" lgraph
let impSig = EmptyNode curl
( _, _, _, rsig, dg'', usp') <- anaRefSpec lgraph libEnv ln dg opts eo impSig un
let ud' = Unit_ref un usp' pos
return ((un, rsig), dg'', ud')
-- | Analyse unit imports
anaUnitImported :: LogicGraph -> LibEnv -> LibName -> DGraph -> HetcatsOpts
-> ExtStUnitCtx -> Range -> [Annoted UNIT_TERM]
-> Result (MaybeDiagNode, Diag, DGraph, [Annoted UNIT_TERM])
anaUnitImported lgraph libEnv ln dg opts eo uctx@(_, diag) poss terms =
curl <- lookupCurrentLogic "UnitImported" lgraph
return (EmptyDiagNode curl, diag, dg, [])
(dnsigs, diag', dg', terms') <-
anaUnitImported' lgraph libEnv ln dg opts eo uctx terms
(sig, dg'') <- nodeSigUnion lgraph dg'
(map (JustNode . getSigFromDiag) dnsigs) DGImports
(simpleIdToIRI $ mkSimpleId "imports")
let pos = getPosUnitImported poss
sink <- inclusionSink lgraph dnsigs sig
() <- assertAmalgamability opts pos diag' sink ("imports:" ++
foldl (\ x y -> x ++ " " ++ show (prettyLG lgraph y)) "" terms)
(dnsig, diag'') <- extendDiagramIncl lgraph diag' dnsigs sig
. show . sepByCommas $ map (prettyLG lgraph) terms
return (JustDiagNode dnsig, diag'', dg'', terms')
anaUnitImported' :: LogicGraph -> LibEnv -> LibName -> DGraph
-> ExtStUnitCtx -> [Annoted UNIT_TERM]
-> Result ([DiagNodeSig], Diag, DGraph, [Annoted UNIT_TERM])
anaUnitImported' lgraph libEnv ln dg opts eo uctx@(buc, diag) ts = case ts of
[] -> return ([], diag, dg, [])
(dnsig, diag', dg', ut') <-
anaUnitTerm lgraph libEnv ln dg opts eo uctx (item ut)
(dnsigs, diag'', dg'', uts') <-
anaUnitImported' lgraph libEnv ln dg' opts eo (buc, diag') uts
return (dnsig : dnsigs, diag'', dg'', replaceAnnoted ut' ut : uts')
-- | Analyse an unit expression
anaUnitExpression :: LogicGraph -> LibEnv -> LibName -> DGraph
-> ExtStUnitCtx -> UNIT_EXPRESSION
-> Result ([DiagNodeSig], UnitSig, Diag, DGraph, UNIT_EXPRESSION)
anaUnitExpression lgraph libEnv ln dg opts eo uctx@(buc, diag)
uexp@(Unit_expression ubs ut poss) = case ubs of
(dnsig@(Diag_node_sig _ ns'), diag', dg', ut') <-
anaUnitTerm lgraph libEnv ln dg opts eo uctx (item ut)
return ([dnsig], UnitSig [] ns' Nothing, diag', dg',
Unit_expression [] (replaceAnnoted ut' ut) poss)
anaUnitBindings lgraph libEnv ln dg opts eo uctx ubs
let dexp = show $ prettyLG lgraph uexp
insNodes diag0 [] buc0 = return ([], diag0, buc0)
insNodes diag0 ((un, nsig) : args0) buc0 =
do (dnsig, diag') <- extendDiagramIncl lgraph diag0 []
{- we made sure in anaUnitBindings that there's no
mapping for un in buc so we can just use
here RTNone actually makes sense -}
let rsig = BranchRefSig RTNone
(UnitSig [] nsig Nothing, Nothing)
buc' =
Map.insert un (Based_unit_sig dnsig rsig) buc0
(dnsigs, diag'', buc'') <- insNodes diag' args0 buc'
return (dnsig : dnsigs, diag'', buc'')
(pardnsigs, diag'', buc') <- insNodes diag args buc
(resnsig, _) <- nodeSigUnion lgraph dg'
(map (JustNode . snd) args) DGFormalParams
(simpleIdToIRI $ mkSimpleId "union")
(Diag_node_sig nU _, diagI) <-
extendDiagramIncl lgraph diag''
{- only add the union to ensure compatibility of
but remove afterwards to be able to check
compatibility of actual parameters: matchDiagram below -}
(p@(Diag_node_sig _ pnsig), diag''', dg''', ut') <-
anaUnitTerm lgraph libEnv ln dg' opts eo (buc', diagI) (item ut)
-- check amalgamability conditions
let pos = getPosUnitExpression uexp
checkSubSign dnsigs nsup =
all (\ dnsub -> isSubGsign lgraph (getSig $ getSigFromDiag dnsub)
-- check that signatures in pardnsigs are subsignatures of pnsig
if checkSubSign pardnsigs pnsig
sink <- inclusionSink lgraph (p : pardnsigs) pnsig
assertAmalgamability opts pos diag''' sink
("subsignature test for: " ++
show (prettyLG lgraph uexp))
-- add new node to the diagram
let (_, diag4) = matchDiagram nU diag'''
UnitSig (map snd args) pnsig $ Just resnsig,
Unit_expression ubs' (replaceAnnoted ut' ut) poss)
("The body signature does not extend the parameter signatures in\n"
{- | Analyse a list of unit bindings. Ensures that the unit names are
not present in extended static unit context and that there are no
duplicates among them. -}
anaUnitBindings :: LogicGraph -> LibEnv -> LibName -> DGraph
-> ExtStUnitCtx -> [UNIT_BINDING]
-> Result ([(IRI, NodeSig)], DGraph, [UNIT_BINDING])
anaUnitBindings lgraph libEnv ln dg opts eo uctx@(buc, _) bs = case bs of
[] -> return ([], dg, [])
Unit_binding un' usp poss : ubs -> do
un <- expCurieR (globalAnnos dg) eo un'
curl <- lookupCurrentLogic "UNIT_BINDINGS" lgraph
(BranchRefSig _ (UnitSig argSigs nsig _, _), dg', usp') <-
anaUnitSpec lgraph libEnv ln dg opts eo
un (EmptyNode curl) Nothing usp
let ub' = Unit_binding un usp' poss
_ : _ -> plain_error ([], dg', [])
++ iriToStringUnsecure un
++ " must not be parameterized") unpos
do (args, dg'', ubs') <- anaUnitBindings lgraph libEnv ln
let args' = (un, nsig) : args
then plain_error (args', dg'', ub' : ubs')
(alreadyDefinedUnit un) unpos
else case lookup un args of
plain_error (args', dg'', ub' : ubs')
(alreadyDefinedUnit un) unpos
Nothing -> return (args', dg'', ub' : ubs')
-- | Analyse a list of unit terms
anaUnitTerms :: LogicGraph -> LibEnv -> LibName -> DGraph
-> ExtStUnitCtx -> [Annoted UNIT_TERM]
-> Result ([DiagNodeSig], Diag, DGraph, [Annoted UNIT_TERM])
anaUnitTerms lgraph libEnv ln dg opts eo uctx@(buc, diag) ts = case ts of
[] -> return ([], diag, dg, [])
(dnsig, diag', dg', ut') <-
anaUnitTerm lgraph libEnv ln dg opts eo uctx (item ut)
(dnsigs, diag'', dg'', uts') <- anaUnitTerms lgraph libEnv ln
dg' opts eo (buc, diag') uts
return (dnsig : dnsigs, diag'', dg'', replaceAnnoted ut' ut : uts')
-- | Analyse an unit term
anaUnitTerm :: LogicGraph -> LibEnv -> LibName -> DGraph -> HetcatsOpts
-> ExtStUnitCtx -> UNIT_TERM -> Result (DiagNodeSig, Diag, DGraph, UNIT_TERM)
anaUnitTerm lgraph libEnv ln dg opts eo uctx@(buc, diag) utrm =
let pos = getPosUnitTerm utrm
utStr = show $ prettyLG lgraph utrm
Unit_reduction ut restr -> do
let orig = DGRestriction (Restricted restr)
Set.empty anaUnitTerm lgraph libEnv ln dg opts eo uctx (item ut)
curl <- lookupCurrentLogic "UnitTerm" lgraph
(incl, msigma) <- anaRestriction lgraph (emptyG_sign curl)
(getSig (getSigFromDiag p)) opts restr
(q@(Diag_node_sig qn _), diag', dg') <-
extendDiagramWithMorphismRevHide pos lgraph diag1 dg1 p incl utStr
{- the renaming morphism is just identity, so
there's no need to extend the diagram
Unit_reduction (replaceAnnoted ut' ut) restr)
-- check amalgamability conditions
() <- assertAmalgamability opts pos diag' sink utStr
(q', diag'', dg'') <- extendDiagramWithMorphism pos
lgraph diag' dg' q sigma utStr orig
return (q', diag'', dg'',
(replaceAnnoted ut' ut) restr)
Unit_translation ut ren -> do
(dnsig@(Diag_node_sig p _), diag1, dg1, ut') <-
anaUnitTerm lgraph libEnv ln dg opts eo uctx (item ut)
-- EmptyNode $ error ... should be replaced with local env!
gMorph <- anaRenaming lgraph
(getSig (getSigFromDiag dnsig)) opts ren
-- check amalamability conditions
() <- assertAmalgamability opts pos diag1 sink utStr
(dnsig', diag', dg') <- extendDiagramWithMorphism pos lgraph
diag1 dg1 dnsig gMorph utStr
(DGTranslation $ Renamed ren)
return (dnsig', diag', dg', Unit_translation
(replaceAnnoted ut' ut) ren)
Amalgamation uts poss -> do
(dnsigs, diag1, dg', uts') <-
anaUnitTerms lgraph libEnv ln dg opts eo uctx uts
(sig, dg'') <- nodeSigUnion lgraph dg'
(map (JustNode . getSigFromDiag) dnsigs) DGUnion
(simpleIdToIRI $ mkSimpleId "imports")
-- check amalgamability conditions
sink <- inclusionSink lgraph dnsigs sig
() <- assertAmalgamability opts poss diag1 sink utStr
(q, diag') <- extendDiagramIncl lgraph diag1 dnsigs
return (q, diag', dg'', Amalgamation uts' poss)
Local_unit udds ut poss -> do
(_, uctx', dg1, udds') <-
anaUnitDeclDefns' lgraph libEnv ln dg opts eo uctx
Map.empty udds
(dnsig, diag', dg', ut') <-
anaUnitTerm lgraph libEnv ln dg1 opts eo uctx' (item ut)
return (dnsig, diag', dg',
Local_unit udds' (replaceAnnoted ut' ut) poss)
Unit_appl un' fargus _ -> do
un <- expCurieR (globalAnnos dg) eo un'
let ustr = iriToStringUnsecure un
argStr = show . sepByCommas $ map (prettyLG lgraph) fargus
Just (Based_unit_sig dnsig _rsig) -> case fargus of
[] -> return (dnsig, diag, dg, utrm)
_ -> plain_error (dnsig, diag, dg, utrm)
(ustr ++ " is a parameterless unit, "
++ "but arguments have been given: " ++ argStr) pos
Just (Based_par_unit_sig pI
(BranchRefSig _ (UnitSig argSigs resultSig _, _))) ->
do (sigF, dg') <- nodeSigUnion lgraph dg
(toMaybeNode pI : map JustNode argSigs) DGFormalParams
(simpleIdToIRI $ mkSimpleId "sigF")
(morphSigs, dg'', diagA) <-
anaFitArgUnits lgraph libEnv ln dg' opts eo
uctx utrm pos argSigs fargus
(sigA, dg''') <- nodeSigUnion lgraph dg''
(toMaybeNode pI : map (JustNode . second) morphSigs)
(simpleIdToIRI $ mkSimpleId "sigA")
-- compute morphA (\sigma^A)
G_sign lidI sigI _ <- return (getMaybeSig (toMaybeNode pI))
let idI = mkG_morphism lidI (ext_ide sigI)
morphA <- homogeneousMorManyUnion
$ idI : map first morphSigs
-- compute sigMorExt (\sigma^A(\Delta))
(_, gSigMorExt) <- extendMorphism True (getSig sigF)
(getSig resultSig) (getSig sigA) morphA
-- check amalgamability conditions
let sigMorExt = gEmbed gSigMorExt
sink <- inclusionSink lgraph (pIL ++
map third morphSigs) sigA
() <- assertAmalgamability opts pos diagA sink utStr
(qB@(Diag_node_sig nqB _), diag') <-
extendDiagramIncl lgraph diagA pIL resultSig ""
-- insert nodes p^F_i and appropriate edges to the diagram
let ins diag0 dg0 [] = return (diag0, dg0)
ins diag0 dg0 ((fpi, (morph, _, tar)) : morphNodes) =
insertFormalParamAndVerifCond
ins diag'' dg2 morphNodes
(diag'', dg4) <- ins diag' dg''' $ zip argSigs morphSigs
-- check amalgamability conditions
(sigR, dg5) <- extendDGraph dg4 resultSig
-- make the union of sigR with all specs of arguments
let nsigs' = reverse $ map (getSigFromDiag . third) morphSigs
gbigSigma <- gsigManyUnion lgraph $ map getSig
let (ns@(NodeSig node _), dg6) = insGSig dg5 emptyNodeName
insE dgl (NodeSig n gsigma) = do
incl <- ginclusion lgraph gsigma gbigSigma
return $ insLink dgl incl globalDef SeeTarget n node
dg7 <- foldM insE dg6 $ sigR : nsigs'
incSink <- inclusionSink lgraph (map third morphSigs) sigR
let sink' = (nqB, sigMorExt) : incSink
assertAmalgamability opts pos diag'' sink' utStr
{- for lambda applications below
the node qB is not added, but only the edge from r
here we use ns instead of sigR -}
(q, diag''') <- extendDiagram diag'' qB
diag4 <- insInclusionEdges lgraph diag'''
return (q, diag4, dg7, utrm)
Just (Based_lambda_unit_sig nodes
(BranchRefSig _ (UnitSig argSigs resultSig _, _))) ->
[] -> error "error in lambda expression"
_r@(Diag_node_sig rn _) : fs ->
do let fnodes = map (\ (Diag_node_sig x _) -> x) fs
(diagC, copyFun) <- copyDiagram lgraph fnodes $ snd uctx
y = lab (diagGraph diagC) x'
Nothing -> error "node not found"
Just (DiagNode ns _) -> Diag_node_sig x' ns
(sigF, dg') <- nodeSigUnion lgraph dg
(map JustNode argSigs) DGFormalParams
(simpleIdToIRI $ mkSimpleId "sigF")
(morphSigs, dg'', diagA) <-
anaFitArgUnits lgraph libEnv ln dg' opts eo
(fst uctx, diagC) utrm pos argSigs fargus
(sigA, dg''') <- nodeSigUnion lgraph dg''
(map (JustNode . second) morphSigs)
(simpleIdToIRI $ mkSimpleId "sigA")
-- compute morphA (\sigma^A)
morphA <- homogeneousMorManyUnion
{- compute sigMorExt (\sigma^A(\Delta))
but allow sharing between body and parameter -}
(_, gSigMorExt) <- extendMorphism False (getSig sigF)
(getSig resultSig) (getSig sigA) morphA
-- check amalgamability conditions
let sigMorExt = gEmbed gSigMorExt
sink <- inclusionSink lgraph (map third morphSigs) sigA
() <- assertAmalgamability opts pos diagA sink utStr
let eI = zip fs' $ map (\ (x, _, z) -> (x, z)) morphSigs
{- insert an edge from f_i to targetNode_i
extendDiagramWithEdge does it
and then call it for pairs (f_i, targetNode_i) -}
let ins diag0 dg0 [] = return (diag0, dg0)
ins diag0 dg0 ((fI, (morph, pIA)) : eIS) =
extendDiagramWithEdge pos lgraph diag0
dg0 fI pIA (gEmbed morph) TEST
(diag', dg4) <- ins diagA dg''' eI
-- check amalgamability conditions
(sigR, dg5) <- extendDGraph dg4 resultSig
incSink <- inclusionSink lgraph (map third morphSigs) sigR
assertAmalgamability opts pos diag' incSink utStr
{- -- for lambda applications
-- the node qB is not added, but only the edge from r -}
(q, diag'') <- extendDiagram diag' r'
diag3 <- insInclusionEdges lgraph diag''
return (q, diag3, dg5, utrm)
_ -> fatal_error ("Undefined unit " ++ ustr) pos
Group_unit_term ut poss -> do
(dnsig, diag1, dg1, ut') <-
anaUnitTerm lgraph libEnv ln dg opts eo uctx (item ut)
return (dnsig, diag1, dg1, Group_unit_term (replaceAnnoted ut' ut) poss)
-- | Analyse unit arguments
anaFitArgUnits :: LogicGraph -> LibEnv -> LibName -> DGraph
-> HetcatsOpts -> ExpOverrides -> ExtStUnitCtx -> UNIT_TERM
-- ^ the whole application for diagnostic purposes
-- ^ the position of the application (for diagnostic purposes)
-- ^ the signatures of unit's formal parameters
-> [FIT_ARG_UNIT] -- ^ the arguments for the unit
-> Result ([(G_morphism, NodeSig, DiagNodeSig)], DGraph, Diag)
anaFitArgUnits lgraph libEnv ln dg opts eo uctx@(buc, diag)
appl pos nodeSigs fArgs = case (nodeSigs, fArgs) of
(nsig : nsigs, fau : faus) -> do
(gmorph, nsig', dnsig, dg1, diag1) <-
anaFitArgUnit lgraph libEnv ln dg opts eo uctx nsig fau
(morphSigs, dg', diag') <- anaFitArgUnits lgraph libEnv ln dg1 opts eo
(buc, diag1) appl pos nsigs faus
return ((gmorph, nsig', dnsig) : morphSigs, dg', diag')
([], []) -> return ([], dg, diag)
_ -> plain_error ([], dg, diag)
("non-matching number of arguments given in application\n"
++ show (prettyLG lgraph appl)) pos
-- | Analyse unit argument
anaFitArgUnit :: LogicGraph -> LibEnv -> LibName -> DGraph
-> ExtStUnitCtx -> NodeSig -> FIT_ARG_UNIT
-> Result (G_morphism, NodeSig, DiagNodeSig, DGraph, Diag)
{- ^ returns 1. the signature morphism 2. the target signature of the morphism
3. the diagram node 4. the modified DGraph 5. the modified diagram -}
anaFitArgUnit lgraph libEnv ln dg opts eo uctx nsig
(Fit_arg_unit ut symbMap poss) = adjustPos poss $ do
anaUnitTerm lgraph libEnv ln dg opts eo uctx (item ut)
let gsigmaS = getSig nsig
gsigmaT = getSig (getSigFromDiag p)
G_sign lidS sigmaS _ <- return gsigmaS
G_sign lidT sigmaT _ <- return gsigmaT
cl <- lookupCurrentLogic "anaFitArgUnit" lgraph
G_symb_map_items_list lid sis <- homogenizeGM cl symbMap
sigmaS' <- coerceSign lidS lid "anaFitArgUnit1" sigmaS
sigmaT' <- coerceSign lidT lid "anaFitArgUnit2" sigmaT
mor <- if isStructured opts then return (ext_ide sigmaS') else do
rmap <- stat_symb_map_items lid (plainSign sigmaS')
(Just $ plainSign sigmaT') sis
ext_induced_from_to_morphism lid rmap sigmaS' sigmaT'
let gMorph = mkG_morphism lid mor
(nsig', dg'') <- extendDGraph dg' nsig (gEmbed gMorph) DGFitSpec
return (gMorph, nsig', p, dg'', diag')
-- | Analyse unit specification
anaUnitSpec :: LogicGraph -> LibEnv -> LibName -> DGraph
-> HetcatsOpts -- ^ should only the structure be analysed?
-> ExpOverrides -- for expanding CURIEs
-> SPEC_NAME -- the name of the unit spec, for node names
-> MaybeNode -- ^ the signature of imports
-> Maybe RTPointer -- for building refinement trees
-> UNIT_SPEC -> Result (RefSig, DGraph, UNIT_SPEC)
{- ^ returns 1. unit signature 2. the development graph resulting from
structred specs inside the unit spec and 3. a UNIT_SPEC after possible
anaUnitSpec lgraph libEnv ln dg opts eo usName impsig rN usp = case usp of
Unit_type argSpecs resultSpec poss ->
Annoted (Spec_inst spn [] _ _) _ _ _
| case lookupGlobalEnvDG (fromMaybe spn
$ expCurie (globalAnnos dg) eo spn) dg of
Just (UnitEntry _) -> True
Just (SpecEntry _) -> True
-- this is needed because there are no REF_NAME in REF_SPEC
Just (ArchOrRefEntry False _) -> True
{- if argspecs are empty and resultspec is a name of unit spec
then this should be converted to a Spec_name -}
anaUnitSpec lgraph libEnv ln dg opts eo usName impsig rN (Spec_name spn)
_ -> do -- a trivial unit type
(resultSpec', resultSig, dg') <- anaSpec False True lgraph libEnv ln
(makeName $ usName{abbrevPath = abbrevPath usName ++ "_res"})
opts eo (item resultSpec) poss
let usig = UnitSig [] resultSig Nothing
return (mkRefSigFromUnit usig , dg', Unit_type []
(replaceAnnoted resultSpec' resultSpec) poss)
_ -> do -- a non-trivial unit type
let argsName = usName{abbrevPath = abbrevPath usName ++ "_args"}
(argSigs, dg1, argSpecs') <-
anaArgSpecs lgraph libEnv ln dg opts eo argsName argSpecs
[argSig] -> return (argSig, dg1) -- the optimization mentioned below
_ -> nodeSigUnion lgraph dg1
(impsig : map JustNode argSigs) DGFormalParams usName
{- if i have no imports, i can optimize?
in that case, an identity morphism is introduced -}
let resName = makeName $ usName{abbrevPath = abbrevPath usName ++ "_res"}
(resultSpec', resultSig, dg3) <- anaSpec True True lgraph libEnv ln
opts eo (item resultSpec) poss
let usig = UnitSig argSigs resultSig $ Just sigUnion
rsig = mkRefSigFromUnit usig
return (rsig, dg3, Unit_type argSpecs'
(replaceAnnoted resultSpec' resultSpec) poss)
usn <- expCurieR (globalAnnos dg) eo un'
case lookupGlobalEnvDG usn dg of
Just (UnitEntry usig) -> return (mkRefSigFromUnit usig, dg, usp)
Just (SpecEntry (ExtGenSig _gsig@(GenSig _ args unSig) nsig) ) -> do
return (mkRefSigFromUnit $ UnitSig args nsig uSig, dg, usp)
Just (ArchOrRefEntry False rsig) ->
p = getPointerFromRef rsig
(dg', newP) = addSubTree dg Nothing p
in return (setPointerInRef rsig newP , dg', usp)
Just p0 -> let l = refTarget p0 in
p = getPointerFromRef rsig
(dg', p') = addSubTree dg (Just l) p
np' = compPointer (NPUnit x) p'
in return (setPointerInRef rsig np', dg', usp)
p = getPointerFromRef rsig
(dg', p') = addSubTree dg (Just l) p
in return (setPointerInRef rsig np', dg', usp)
(dg', p') = addSubTree dg (Just h) p
np' = compPointer (NPUnit x) p'
in return (setPointerInRef rsig np', dg', usp)
_ -> error "can't compose signatures!"
_ -> notFoundError "unit specification" usn
Closed_unit_spec usp' _ -> do
curl <- lookupCurrentLogic "UnitSpec" lgraph
anaUnitSpec lgraph libEnv ln dg opts eo usName (EmptyNode curl) rN usp'
-- | Analyse refinement specification
anaRefSpec :: LogicGraph -> LibEnv -> LibName -> DGraph
-> HetcatsOpts -- ^ should only the structure be analysed?
-> MaybeNode -- ^ the signature of imports
-> SPEC_NAME -- for origin
-> Result ([DiagNodeSig], -- for lambda expressions
Maybe DiagNodeSig, -- for tracing between levels
Maybe Diag, RefSig, DGraph, REF_SPEC)
anaRefSpec lgraph libEnv ln dg opts eo nsig rn sharedCtx nP rsp =
anaUnitSpec lgraph libEnv ln dg opts eo rn nsig nP asp
usig <- getUnitSigFromRef rsig
let rP = getPointerFromRef rsig
(rsig', dg3) = case rP of
(n, dg'') = addNodeRT dg' usig (name asp)
r' = setPointerInRef rsig (NPUnit n)
return ([], Nothing, Just (snd sharedCtx), rsig', dg3, Unit_spec asp')
return ([], Nothing, Just (snd sharedCtx), rsig, dg', Unit_spec asp')
Arch_unit_spec asp poss ->
(nodes, maybeRes, diag, rsig, dg', asp') <-
anaArchSpec lgraph libEnv ln dg opts eo sharedCtx x $ item asp
return (nodes, maybeRes, Just diag, rsig, dg',
Arch_unit_spec (replaceAnnoted asp' asp) poss)
{- check whether it is indeed correct
to ignore the nodes of the
lambda expressions, like you do in the following -}
Compose_ref rslist range ->
(dg', anaSpecs, _) <- foldM (\ (dgr, rList, rN') rsp0 ->
(_, _, _, rsig', dgr', rsp') <-
anaRefSpec lgraph libEnv ln dgr opts eo nsig
(simpleIdToIRI $ mkSimpleId $
show rn ++ "gen_ref_name" ++
return (dgr', rList ++ [(rsig', rsp')],
Just $ getPointerFromRef rsig')
-- compose signatures in csig
let refSigs = map fst anaSpecs
csig <- foldM refSigComposition (head refSigs) $ tail refSigs
let compRef = Compose_ref (map snd anaSpecs) range
return ([], Nothing, Nothing, csig, dg', compRef)
Component_ref urlist range -> do
(dg', anaRefs, resultMap, pMap) <-
foldM (\ (dgr, rList, cx, ps) uref0 -> do
((n, rs), dgr', uref') <-
anaUnitRef lgraph libEnv ln dgr opts eo emptyExtStUnitCtx nP uref0
insert a dummy node labeled with the name of the component
insert a refinement link from the dummy node to the
return ([], Nothing, Nothing,
ComponentRefSig (NPComp pMap) resultMap, dg',
Component_ref (reverse anaRefs) range)
Refinement beh uspec gMapList rspec range ->
-- beh will be ignored for now
(_rsig@(BranchRefSig _ (usig, _)), dg', asp') <-
anaUnitSpec lgraph libEnv ln dg opts eo rn nsig nP uspec
-- TODO: is rn fine above?
(_, _, _, _rsig'@(BranchRefSig n2 (usig', bsig)), dgr', rsp') <-
anaRefSpec lgraph libEnv ln dg' opts eo nsig rn emptyExtStUnitCtx Nothing rspec
(UnitSig _ls ns _, UnitSig _ls' ns' _) -> do
dg'' <- anaSymbMapRef lgraph dgr' ns ns' gMapList rn
let (s, dg3) = case nP of
Nothing -> addNodeRT dg'' usig (name uspec)
_ -> error "can't refine to component!"
dg4 = addRefEdgeRT dg3 s (refSource n2)
return ([], Nothing, Nothing,
BranchRefSig (compPointer (NPUnit s) n2)
Refinement beh asp' gMapList rsp' range)
Spec_name x -> iriToStringShortUnsecure x
Unit_type argSpecs resultSpec _ ->
Annoted (Spec_inst spn [] _ _) _ _ _ ->
iriToStringShortUnsecure spn
anaSymbMapRef :: LogicGraph -> DGraph -> NodeSig -> NodeSig -> [G_mapping]
-> SPEC_NAME -> Result DGraph
anaSymbMapRef lg dg' ns ns' symbMap rn = do
G_sign lidS sigS _ <- return gSigS
G_sign lidT sigT _ <- return gSigT
cl <- lookupCurrentLogic "anaSymbMapRef" lg
G_symb_map_items_list lid sis <- homogenizeGM cl symbMap
sigS' <- coerceSign lidS lid "anaSymbMapRef1" sigS
sigT' <- coerceSign lidT lid "anaSymbMapRef2" sigT
rmap <- stat_symb_map_items lid (plainSign sigS')
(Just $ plainSign sigT') sis
mor <- ext_induced_from_to_morphism lid rmap sigS' sigT'
let gm = gEmbed $ mkG_morphism lid mor
-- for now we stay in the homogeneous case
linkLabel = defDGLink gm globalThm (DGLinkRefinement rn)
(_, dg'') = insLEdgeDG (nodeS, nodeT, linkLabel) dg'
-- | Analyse a list of argument specifications
anaArgSpecs :: LogicGraph -> LibEnv -> LibName -> DGraph -> HetcatsOpts
-> ExpOverrides -> SPEC_NAME
-> [Annoted SPEC] -> Result ([NodeSig], DGraph, [Annoted SPEC])
anaArgSpecs lgraph libEnv ln dg opts eo usName args = let
anaArgSpecsAux aDG x args' = case args' of
[] -> return ([], aDG, [])
l <- lookupLogic "anaArgSpecs " (currentLogic lgraph) lgraph
xName = makeName $ usName{abbrevPath = abbrevPath usName ++ show x}
(argSpec', argSig, dg') <-
anaSpec False False -- don't optimize the node out
lgraph libEnv ln aDG (EmptyNode l)
(xName{extIndex = x + 1})
(argSigs, dg'', argSpecs') <-
anaArgSpecsAux dg' (x + 1 ::Int) argSpecs
return (argSig : argSigs, dg'', replaceAnnoted argSpec' argSpec
in anaArgSpecsAux dg 0 args
{- | Check that given diagram ensures amalgamability along given set
:: HetcatsOpts -- ^ the program options
-> Range -- ^ the position (for diagnostics)
-> Diag -- ^ the diagram to be checked
-> [(Node, GMorphism)] -- ^ the sink
-> String -- ^ the unit expr as a string
assertAmalgamability opts pos diag sink uexp = do
ensAmalg <- homogeneousEnsuresAmalgamability opts pos diag sink
NoAmalgamation msg -> plain_error ()
("Amalgamability is not ensured: " ++ msg ++ "\n for " ++ uexp) pos
DontKnow msg -> warning () msg pos
-- | Check the amalgamability assuming common logic for whole diagram
homogeneousEnsuresAmalgamability
:: HetcatsOpts -- ^ the program options
-> Range -- ^ the position (for diagnostics)
-> Diag -- ^ the diagram to be checked
-> [(Node, GMorphism)] -- ^ the sink
homogeneousEnsuresAmalgamability opts pos diag sink = case sink of
[] -> plain_error defaultDontKnow
"homogeneousEnsuresAmalgamability: Empty sink" pos
G_sign lid _ _ <- return sig
hDiag <- homogeniseDiagram lid diag
hSink <- homogeniseSink lid sink
ensures_amalgamability lid (caslAmalg opts, hDiag, hSink, diagDesc diag)
-- | Get a position within the source file of a UNIT-TERM
getPosUnitTerm :: UNIT_TERM -> Range
getPosUnitTerm ut = case ut of
Unit_reduction _ restr -> case restr of
-- obtain position from RESTRICTION
Unit_translation _ (Renaming _ poss) -> poss
Amalgamation _ poss -> poss
Local_unit _ _ poss -> poss
Unit_appl u _ poss -> appRange (iriPos u) poss
Group_unit_term _ poss -> poss
-- | Get a position within the source file of UNIT-IMPORTED
getPosUnitImported :: Range -> Range
getPosUnitImported (Range ps) = Range $ case ps of
_ : qs -> if null qs then ps else qs
-- | Get a position within the source file of UNIT-EXPRESSION
getPosUnitExpression :: UNIT_EXPRESSION -> Range
getPosUnitExpression (Unit_expression _ (Annoted ut _ _ _) poss) =
appRange (getPosUnitTerm ut) poss