AnalysisStructured.hs revision 89d5b892ca2fd8eb8f72dba097759a6d54f0a78c
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder Till Mossakowski
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder Analysis of structured specifications
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder Follows the extended static semantic rules in:
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder T. Mossakowski, S. Autexier, D. Hutter, P. Hoffman:
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder CASL Proof calculus.
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder Available from http://www.informatik.uni-bremen.de/~till/calculus.ps
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder To appear in teh CASL book.
d48085f765fca838c1d972d2123601997174583dChristian Maedermodule AnalysisStructured
d48085f765fca838c1d972d2123601997174583dChristian Maederimport Grothendieck
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maederimport DevGraph
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport AS_Annotation
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederimport GlobalAnnotations
3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maederimport AS_Structured
3c5cc698b0c061209ff83eb8de027daef5ae922aChristian MaederlookupNode n dg = lab' $ context n dg
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maederana_SPEC :: GlobalAnnos -> GlobalEnv -> DGraph -> Node -> SPEC -> (Node,DGraph)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederana_SPEC gannos genv dg n sp = case dgn_sign $ lookupNode n dg of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder G_sign logid sigma ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Basic_spec (G_basic_spec logid' bspec) ->
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder case coerce logid logid' sigma of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Nothing -> error ("logic mismatch: "++language_name logid++" expected, but "
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ++language_name logid'++" found")
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Just sigma' -> case basic_analysis logid' of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Nothing -> error ("no basic analysis for logic "++language_name logid')
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder let res = b (bspec,sigma',gannos)
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder in case maybeResult res of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Nothing -> error (show (diags res))
eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder Just (sigma_local, sigma_complete, ax) ->
eab576044505ba1fbc64610323053490fbd9e82cChristian Maeder let node_contents = DGNode {
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder dgn_sign = G_sign logid' sigma_local, -- only the delta
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder dgn_sens = G_l_sentence logid' ax,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder dgn_origin = DGBasic }
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder [node] = newNodes 1 dg
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder in (node,insNode (node,node_contents) dg)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Translation asp (Renaming ren pos) ->
ce3928e71520030ad0275b72050a8f4377f9313cChristian Maeder let sp = item asp
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ren' = zip ren (tail pos)
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (n',dg') = ana_SPEC gannos genv dg n sp
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder gSigma' = dgn_sign $ lookupNode n' dg'
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder mor = foldl (ana_RENAMING dg) (g_ide gSigma') ren'
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder in undefined --case of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- G_sign logid' sigma' ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Reduction asp restr ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Union asps pos ->
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder Extension asps pos ->
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder Free_spec asp pos ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Cofree_spec asp pos ->
d48085f765fca838c1d972d2123601997174583dChristian Maeder Local_spec asp1 asp2 pos ->
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder Closed_spec asp pos ->
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder Group asp pos ->
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder Spec_inst spname afitargs ->
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder Qualified_spec logname asp pos ->
a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maederana_RENAMING = undefined