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
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 SieversMaintainer : k.sojakova@jacobs-university.de
f957632b960a0a42999b38ded7089fa602b41745Kay SieversStability : experimental
f957632b960a0a42999b38ded7089fa602b41745Kay SieversPortability : portable
9a36607584bbd1d78775353e022a51794b4e27b1Lennart Poettering Currently not used; requires refactoring of Twelf2DG.hs
3679d1126bae52e02f6cd60fca196f616b9e660dLennart Poettering ( basicAnalysis
a4cc3e5ccc0a3033d764a9eb3ae5ee90db560682Lennart Poettering , symbAnalysis
a4cc3e5ccc0a3033d764a9eb3ae5ee90db560682Lennart Poettering , symbMapAnalysis
5954c07433b134694256b9989f2ad3f85a643976Lennart Poetteringimport qualified Data.Set as Set
5954c07433b134694256b9989f2ad3f85a643976Lennart Poetteringimport qualified Data.Map as Map
461bd8e47cafacfcd38389e7558330bfb6e902adLennart Poetteringgen_file :: String
ab8e074ce25b9947314c69e17afe1bd2527ee26dLennart Poetteringgen_sig :: String
ab8e074ce25b9947314c69e17afe1bd2527ee26dLennart Poetteringgen_sig = "GEN_SIG"
ab8e074ce25b9947314c69e17afe1bd2527ee26dLennart Poetteringgen_ax :: String
ab8e074ce25b9947314c69e17afe1bd2527ee26dLennart Poetteringgen_ax = "gen_ax"
ab8e074ce25b9947314c69e17afe1bd2527ee26dLennart PoetteringsenSuf :: String -> String
ab8e074ce25b9947314c69e17afe1bd2527ee26dLennart PoetteringsenSuf sn = sn ++ "_SEN"
b454b11220e87add6d0f011695c7912b009c853dLennart PoetteringnumSuf :: String -> Int -> String
b454b11220e87add6d0f011695c7912b009c853dLennart PoetteringnumSuf s i = s ++ "_" ++ show i
b454b11220e87add6d0f011695c7912b009c853dLennart PoetteringwrapInSig :: String -> String -> String
4a449ed73d2c1cfb91a1c773b70231b3457b3046Lennart PoetteringwrapInSig sn cont = "%sig " ++ sn ++ " = {\n" ++ cont ++ "}."
4a449ed73d2c1cfb91a1c773b70231b3457b3046Lennart PoetteringwrapInIncl :: String -> String
4a449ed73d2c1cfb91a1c773b70231b3457b3046Lennart PoetteringwrapInIncl sn = "%include " ++ sn ++ " %open."
4a449ed73d2c1cfb91a1c773b70231b3457b3046Lennart PoetteringgetSentenceAnnos :: [Annoted BASIC_ITEM] ->
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 PoetteringmakeNamedFormulas :: Sign -> [Named EXP]
5666ea6fcaaf1e829de07625b7c185949b23fecdKay SieversmakeNamedFormulas (Sign _ _ ds) =
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-- 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 SieversprintSigItems :: [Annoted BASIC_ITEM] -> String
3679d1126bae52e02f6cd60fca196f616b9e660dLennart PoetteringprintSigItems [] = ""
356ce9915ab1a4a1e6dc26954df34936a69e7c12Lennart PoetteringprintSigItems (i:is) =
356ce9915ab1a4a1e6dc26954df34936a69e7c12Lennart Poettering Annoted (Decl d) _ _ _ -> d ++ ".\n" ++ printSigItems is
356ce9915ab1a4a1e6dc26954df34936a69e7c12Lennart Poettering _ -> printSigItems is
bfa00bc6c05d0f896e9632eccd47d442fea556b9Lennart PoetteringprintSenItems :: [Annoted BASIC_ITEM] -> String
3b953d68c628c6ae70adba871719ac0f16083b51Josh TriplettprintSenItems items = printSenItemsH 0 items
3b953d68c628c6ae70adba871719ac0f16083b51Josh TriplettprintSenItemsH :: Int -> [Annoted BASIC_ITEM] -> String
3b953d68c628c6ae70adba871719ac0f16083b51Josh TriplettprintSenItemsH _ [] = ""
3b953d68c628c6ae70adba871719ac0f16083b51Josh TriplettprintSenItemsH num (i:is) =
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-- 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 (_,_,(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)