Cross Reference: /hets/LF/Analysis.hs
Analysis.hs revision ccaa75089b23c0f043cdbd4001cba4e076ca4fd3
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering{- |
7c66aeba0f28cb82027d6015405ed71afa3b6059Kay SieversModule : $Header$
7c66aeba0f28cb82027d6015405ed71afa3b6059Kay SieversDescription : Static analysis for the Edinburgh Logical Framework
c904f64d84db8c4eebedf210ba10893f19ba05edLennart PoetteringCopyright : (c) Kristina Sojakova, DFKI Bremen 2010
c904f64d84db8c4eebedf210ba10893f19ba05edLennart PoetteringLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
f957632b960a0a42999b38ded7089fa602b41745Kay Sievers
f957632b960a0a42999b38ded7089fa602b41745Kay SieversMaintainer : k.sojakova@jacobs-university.de
f957632b960a0a42999b38ded7089fa602b41745Kay SieversStability : experimental
f957632b960a0a42999b38ded7089fa602b41745Kay SieversPortability : portable
9a36607584bbd1d78775353e022a51794b4e27b1Lennart Poettering
9a36607584bbd1d78775353e022a51794b4e27b1Lennart Poettering Currently not used; requires refactoring of Twelf2DG.hs
a40593a0d0d740efa387e35411e1e456a6c5aba7Lennart Poettering-}
20ffc4c4a9226b0e45cc02ad9c0108981626c0bbKay Sievers
2d19f95caef8668aeb5c05a18b39c6b79f710856Kay Sieversmodule LF.Analysis
3679d1126bae52e02f6cd60fca196f616b9e660dLennart Poettering ( basicAnalysis
a4cc3e5ccc0a3033d764a9eb3ae5ee90db560682Lennart Poettering , symbAnalysis
a4cc3e5ccc0a3033d764a9eb3ae5ee90db560682Lennart Poettering , symbMapAnalysis
a4cc3e5ccc0a3033d764a9eb3ae5ee90db560682Lennart Poettering ) where
0028da22f194f7c0ca7169a48cf32e1bc0f9138aLennart Poettering
a4cc3e5ccc0a3033d764a9eb3ae5ee90db560682Lennart Poetteringimport LF.AS
7e2c2bcf1285d124c9c656ff46cafa4db0a987c9Lennart Poetteringimport LF.Sign
f0c15f288513aa4da012db7497a4aec3f7763ebbLennart Poetteringimport LF.Twelf2DG
7b4da18c1717f811bae67ea3d39290495857c03eLennart Poettering
81d112a8f0522a09fcfe317f420363a2b728137cLennart Poetteringimport Common.DocUtils
81d112a8f0522a09fcfe317f420363a2b728137cLennart Poetteringimport Common.ExtSign
81d112a8f0522a09fcfe317f420363a2b728137cLennart Poetteringimport Common.GlobalAnnotations
eb124a97fb72d076014253b1acde69d428f15ecfLennart Poetteringimport Common.AS_Annotation
3df82d5a8cdc510f518fd5e234ccb3233b748719Lennart Poetteringimport Common.Id
5954c07433b134694256b9989f2ad3f85a643976Lennart Poetteringimport Common.Result
5954c07433b134694256b9989f2ad3f85a643976Lennart Poettering
5954c07433b134694256b9989f2ad3f85a643976Lennart Poetteringimport qualified Data.Set as Set
5954c07433b134694256b9989f2ad3f85a643976Lennart Poetteringimport qualified Data.Map as Map
aa96c6cb44a6eeccc506ae055aae2519a7f914e1Lennart Poettering
e8a7a315391a6a07897122725cd707f4e9ce63d7Lennart Poetteringimport Static.DevGraph
ef3b5246879094e29cc99c4d24cbfeb19b7da49bLennart Poettering
ef3b5246879094e29cc99c4d24cbfeb19b7da49bLennart Poetteringimport System.FilePath
ef3b5246879094e29cc99c4d24cbfeb19b7da49bLennart Poettering
461bd8e47cafacfcd38389e7558330bfb6e902adLennart Poetteringgen_file :: String
461bd8e47cafacfcd38389e7558330bfb6e902adLennart Poetteringgen_file = "gen_twelf_file.elf"
461bd8e47cafacfcd38389e7558330bfb6e902adLennart Poettering
ab8e074ce25b9947314c69e17afe1bd2527ee26dLennart Poetteringgen_sig :: String
ab8e074ce25b9947314c69e17afe1bd2527ee26dLennart Poetteringgen_sig = "GEN_SIG"
ab8e074ce25b9947314c69e17afe1bd2527ee26dLennart Poettering
ab8e074ce25b9947314c69e17afe1bd2527ee26dLennart Poetteringgen_ax :: String
ab8e074ce25b9947314c69e17afe1bd2527ee26dLennart Poetteringgen_ax = "gen_ax"
ab8e074ce25b9947314c69e17afe1bd2527ee26dLennart Poettering
ab8e074ce25b9947314c69e17afe1bd2527ee26dLennart PoetteringsenSuf :: String -> String
ab8e074ce25b9947314c69e17afe1bd2527ee26dLennart PoetteringsenSuf sn = sn ++ "_SEN"
ab8e074ce25b9947314c69e17afe1bd2527ee26dLennart Poettering
b454b11220e87add6d0f011695c7912b009c853dLennart PoetteringnumSuf :: String -> Int -> String
b454b11220e87add6d0f011695c7912b009c853dLennart PoetteringnumSuf s i = s ++ "_" ++ show i
b454b11220e87add6d0f011695c7912b009c853dLennart Poettering
b454b11220e87add6d0f011695c7912b009c853dLennart PoetteringwrapInSig :: String -> String -> String
4a449ed73d2c1cfb91a1c773b70231b3457b3046Lennart PoetteringwrapInSig sn cont = "%sig " ++ sn ++ " = {\n" ++ cont ++ "}."
755123030a4b4c82251b49155aa0e7f523081558Harald Hoyer
4a449ed73d2c1cfb91a1c773b70231b3457b3046Lennart PoetteringwrapInIncl :: String -> String
4a449ed73d2c1cfb91a1c773b70231b3457b3046Lennart PoetteringwrapInIncl sn = "%include " ++ sn ++ " %open."
4a449ed73d2c1cfb91a1c773b70231b3457b3046Lennart Poettering
4a449ed73d2c1cfb91a1c773b70231b3457b3046Lennart PoetteringgetSentenceAnnos :: [Annoted BASIC_ITEM] ->
4ff49cb63075aba646b578f2516b37a8dfd5a65bLennart Poettering
4ff49cb63075aba646b578f2516b37a8dfd5a65bLennart Poettering-----------------------------------------------------------------
4ff49cb63075aba646b578f2516b37a8dfd5a65bLennart Poettering-----------------------------------------------------------------
4ff49cb63075aba646b578f2516b37a8dfd5a65bLennart Poettering
fff87a35d9e26c0d4ea41273a963c0eb20e18da4Zbigniew Jędrzejewski-Szmek-- basic analysis for LF
fff87a35d9e26c0d4ea41273a963c0eb20e18da4Zbigniew Jędrzejewski-SzmekbasicAnalysis :: (BASIC_SPEC, Sign, GlobalAnnos) ->
fff87a35d9e26c0d4ea41273a963c0eb20e18da4Zbigniew Jędrzejewski-Szmek Result (BASIC_SPEC, ExtSign Sign Symbol, [Named EXP])
fff87a35d9e26c0d4ea41273a963c0eb20e18da4Zbigniew Jędrzejewski-SzmekbasicAnalysis (bs, initsig, _) =
b8b4d3dddc7611dce3bf28004b0375d661120c62Lennart Poettering if initsig /= emptySig
b8b4d3dddc7611dce3bf28004b0375d661120c62Lennart Poettering then error "Structuring for LF nyi."
b8b4d3dddc7611dce3bf28004b0375d661120c62Lennart Poettering else do makeTwelfFile gen_file gen_sig bs
b8b4d3dddc7611dce3bf28004b0375d661120c62Lennart Poettering (sig,sen) <- getSigSen gen_file
b8b4d3dddc7611dce3bf28004b0375d661120c62Lennart Poettering let syms = getAllSymbols sig
3df82d5a8cdc510f518fd5e234ccb3233b748719Lennart Poettering let fs = makeNamedFormulas sen
3df82d5a8cdc510f518fd5e234ccb3233b748719Lennart Poettering return $ Just $ (bs, ExtSign sig syms, fs)
3df82d5a8cdc510f518fd5e234ccb3233b748719Lennart Poettering
3df82d5a8cdc510f518fd5e234ccb3233b748719Lennart PoetteringmakeNamedFormulas :: Sign -> [Named EXP]
5666ea6fcaaf1e829de07625b7c185949b23fecdKay SieversmakeNamedFormulas (Sign _ _ ds) =
5666ea6fcaaf1e829de07625b7c185949b23fecdKay Sievers map ( -> ds
5666ea6fcaaf1e829de07625b7c185949b23fecdKay Sievers
a9602630c64791571ca37606a0a5eabfac85820aLennart PoetteringmakeNamedFormula :: DEF -> Named EXP
b6b7d4337976eeac610b9ed2c3e1fd596a247b14Lennart PoetteringmakeNamedFormula (Def s t _) =
b6b7d4337976eeac610b9ed2c3e1fd596a247b14Lennart Poettering let isImplies = or $ map isImplies annos
b6b7d4337976eeac610b9ed2c3e1fd596a247b14Lennart Poettering isImplied = or $ map isImplied annos
b5c03638d48c07aa0eaf13b5f54000c7133e1883Lennart Poettering isTheorem = isImplies || isImplied
b5c03638d48c07aa0eaf13b5f54000c7133e1883Lennart Poettering
b5c03638d48c07aa0eaf13b5f54000c7133e1883Lennart Poettering
b5c03638d48c07aa0eaf13b5f54000c7133e1883Lennart Poettering
b5c03638d48c07aa0eaf13b5f54000c7133e1883Lennart Poettering-- converts the basic spec into a Twelf file
752beb0c8560fb7e989d2f8da5e10c4692d78422Lennart PoetteringmakeTwelfFile :: FilePath -> String -> BASIC_SPEC -> IO ()
752beb0c8560fb7e989d2f8da5e10c4692d78422Lennart PoetteringmakeTwelfFile file sn (Basic_spec items) = do
eece8c6fb5f4d354dcef6fd369e876c4f3a3f163Lennart Poettering let sig = wrapInSig sn $ printSigItems items
eece8c6fb5f4d354dcef6fd369e876c4f3a3f163Lennart Poettering let sen = wrapInSig (senSuf sn) $
eece8c6fb5f4d354dcef6fd369e876c4f3a3f163Lennart Poettering wrapInIncl sn ++ printSenItems items
d325d9bcfa8846a65767087f958a2dd11139d0e7Kay Sievers writeFile file $ sig ++ "\n\n" ++ sen
d325d9bcfa8846a65767087f958a2dd11139d0e7Kay Sievers
d325d9bcfa8846a65767087f958a2dd11139d0e7Kay SieversprintSigItems :: [Annoted BASIC_ITEM] -> String
3679d1126bae52e02f6cd60fca196f616b9e660dLennart PoetteringprintSigItems [] = ""
356ce9915ab1a4a1e6dc26954df34936a69e7c12Lennart PoetteringprintSigItems (i:is) =
356ce9915ab1a4a1e6dc26954df34936a69e7c12Lennart Poettering case i of
356ce9915ab1a4a1e6dc26954df34936a69e7c12Lennart Poettering Annoted (Decl d) _ _ _ -> d ++ ".\n" ++ printSigItems is
356ce9915ab1a4a1e6dc26954df34936a69e7c12Lennart Poettering _ -> printSigItems is
bfa00bc6c05d0f896e9632eccd47d442fea556b9Lennart Poettering
bfa00bc6c05d0f896e9632eccd47d442fea556b9Lennart PoetteringprintSenItems :: [Annoted BASIC_ITEM] -> String
3b953d68c628c6ae70adba871719ac0f16083b51Josh TriplettprintSenItems items = printSenItemsH 0 items
3b953d68c628c6ae70adba871719ac0f16083b51Josh Triplett
3b953d68c628c6ae70adba871719ac0f16083b51Josh TriplettprintSenItemsH :: Int -> [Annoted BASIC_ITEM] -> String
3b953d68c628c6ae70adba871719ac0f16083b51Josh TriplettprintSenItemsH _ [] = ""
3b953d68c628c6ae70adba871719ac0f16083b51Josh TriplettprintSenItemsH num (i:is) =
09f727eebd87661f263d3c2c1e0de7b7771acd40Lennart Poettering case i of
09f727eebd87661f263d3c2c1e0de7b7771acd40Lennart Poettering Annoted (Form f) _ _ _ ->
09f727eebd87661f263d3c2c1e0de7b7771acd40Lennart Poettering let label = getRLabel i
795607b22308f5b92073b012e43be1892fdd97c0Lennart Poettering nam = if null label then numSuf gen_ax num else label
795607b22308f5b92073b012e43be1892fdd97c0Lennart Poettering num' = if null label then num + 1 else num
795607b22308f5b92073b012e43be1892fdd97c0Lennart Poettering in nam ++ " : " ++ f ++ ".\n" ++ printSenItemsH num' is
795607b22308f5b92073b012e43be1892fdd97c0Lennart Poettering _ -> printSenItemsH num is
795607b22308f5b92073b012e43be1892fdd97c0Lennart Poettering
795607b22308f5b92073b012e43be1892fdd97c0Lennart Poettering-- retrieves the signatures containing basic spec declarations and sentences
795607b22308f5b92073b012e43be1892fdd97c0Lennart PoetteringgetSigSen :: FilePath -> String -> IO (Sign,Sign)
0be8342c04bbf129b4a21e5073eacccbbce4e896Lennart PoetteringgetSigSen fp sn = do
0be8342c04bbf129b4a21e5073eacccbbce4e896Lennart Poettering file <- resolveToCur fp
0be8342c04bbf129b4a21e5073eacccbbce4e896Lennart Poettering runTwelf file
0be8342c04bbf129b4a21e5073eacccbbce4e896Lennart Poettering (_,_,(sigmap,_)) <- buildGraph file (emptyLibEnv,emptyGrMap)
0be8342c04bbf129b4a21e5073eacccbbce4e896Lennart Poettering let base = dropExtension file
487060c2394b7703e59650ef332053645ffae2a3Lennart Poettering let sn' = senSuf sn
487060c2394b7703e59650ef332053645ffae2a3Lennart Poettering let sig1 = Map.findWithDefault (error $ sn ++ " not found.")
e5ec62c56963d997edaffa904af5dc45dac23988Lennart Poettering (base,sn) sigmap
54c31a79f72ff57ac8eba089acacc4ab482b745dLennart Poettering let sig2 = Map.findWithDefault (error $ sn' ++ " not found.")
826872b61e4857dfffe63ba84e2b005623baecd6Lennart Poettering (base,sn') sigmap
826872b61e4857dfffe63ba84e2b005623baecd6Lennart Poettering return (sig1,sig2)
54c31a79f72ff57ac8eba089acacc4ab482b745dLennart Poettering
826872b61e4857dfffe63ba84e2b005623baecd6Lennart Poettering
8973790ee6f62132b1b57de15c4edaef2c097004Lennart Poettering