Logic_LF.hs revision 44e934cd533a334ae00a65b83dba146c1352b0aa
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
ee9c9500ab13c1093fc3feaf2aa5a0d330d0bfadKay Sievers{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
c343be283b7152554bac0c02493a4e1759c163f7Kay SieversModule : $Header$
c343be283b7152554bac0c02493a4e1759c163f7Kay SieversDescription : Instances of classes defined in Logic.hs for the Edinburgh
b3ae710c251d0ce5cf2cef63208e325497b5e323Zbigniew Jędrzejewski-Szmek Logical Framework
b3ae710c251d0ce5cf2cef63208e325497b5e323Zbigniew Jędrzejewski-SzmekCopyright : (c) Kristina Sojakova, DFKI Bremen 2009
f957632b960a0a42999b38ded7089fa602b41745Kay SieversLicense : GPLv2 or higher, see LICENSE.txt
f957632b960a0a42999b38ded7089fa602b41745Kay SieversMaintainer : k.sojakova@jacobs-university.de
f957632b960a0a42999b38ded7089fa602b41745Kay SieversStability : experimental
a40593a0d0d740efa387e35411e1e456a6c5aba7Lennart PoetteringPortability : portable
bafb15bab99887d1b6b8a35136531bac6c3876a6Lennart Poetteringimport LF.MorphParser (readMorphism)
7f035ea56bc0b75327c54e8aa4a56d57ed00dd6dLennart Poetteringimport qualified Data.Map as Map
9d6db739ce1eaa3eace21801fd606d523b73c8f4Lennart Poetteringdata LF = LF deriving Show
9d6db739ce1eaa3eace21801fd606d523b73c8f4Lennart Poetteringinstance Language LF where
49ee032fc3b694a1b45be9d08a2b97ab3eb93f75Lennart Poettering description LF = "Edinburgh Logical Framework"
49ee032fc3b694a1b45be9d08a2b97ab3eb93f75Lennart Poetteringinstance Category Sign Morphism where
6992efee44d3affd17dd9174e8673ae63ba01ec7Lennart Poettering composeMorphisms = compMorph
6992efee44d3affd17dd9174e8673ae63ba01ec7Lennart Poettering isInclusion = Map.null . symMap . canForm
9d6db739ce1eaa3eace21801fd606d523b73c8f4Lennart Poetteringinstance Syntax LF BASIC_SPEC SYMB_ITEMS SYMB_MAP_ITEMS where
9d6db739ce1eaa3eace21801fd606d523b73c8f4Lennart Poettering parse_basic_spec LF = Just basicSpec
f1f520e8dfe2072a6d8c50d35bc9f2f145596aa5Lennart Poettering parse_symb_items LF = Just symbItems
f1f520e8dfe2072a6d8c50d35bc9f2f145596aa5Lennart Poettering parse_symb_map_items LF = Just symbMapItems
bc07548926ec5ed7b13df8d3656654f238e0b9a7Lennart Poetteringinstance Sentences LF
58f55364fa00a6a4706df2c4a01c6967f432e531Lennart Poettering map_sen LF m = Result [] . translate m
27f1e9ebf6f9e7ff8a898f894c1b38cbdecfa77cLennart Poettering sym_of LF = singletonList . getSymbols
27f1e9ebf6f9e7ff8a898f894c1b38cbdecfa77cLennart Poetteringinstance Logic LF
3a53fdaa34eded70d6f971234a9ac78891336f9eLennart Poettering SYMB_MAP_ITEMS
a01647e53727107d82382bc5c9d98c894e8f386cLennart Poetteringinstance StaticAnalysis LF
a01647e53727107d82382bc5c9d98c894e8f386cLennart Poettering SYMB_MAP_ITEMS
8891f695c71bd4c266d827c9aaedbbbbaf79d3ebLennart Poettering basic_analysis LF = Just basicAnalysis
8891f695c71bd4c266d827c9aaedbbbbaf79d3ebLennart Poettering stat_symb_items LF _ = symbAnalysis
2b1c3767515672dfd0f5e0a9c9d7ac3a16a6a361Lennart Poettering stat_symb_map_items LF _ _ = symbMapAnalysis
2b1c3767515672dfd0f5e0a9c9d7ac3a16a6a361Lennart Poettering symbol_to_raw LF = symName
81429136905a6204875174b60a179333b7f3c9e4Kay Sievers matches LF s1 s2 =
1df52dd282cd6014ace8ca2279dd90d9ea52d2a4Lennart Poettering not (isSym s2) || symName s1 == s2
37efac5ddb21fd91ed420c070ed07f375e78b3b9Lennart Poettering -- expressions are checked manually or symbols match by name
37efac5ddb21fd91ed420c070ed07f375e78b3b9Lennart Poettering empty_signature LF = emptySig
7348b3adb324614132cf376f478e883bd7de28f1Lennart Poettering is_subsig LF = isSubsig
7348b3adb324614132cf376f478e883bd7de28f1Lennart Poettering subsig_inclusion LF = inclusionMorph
f55b9bdfae46e3683c74c30f1d063642a41368a5Lennart Poettering signature_union LF = sigUnion
f55b9bdfae46e3683c74c30f1d063642a41368a5Lennart Poettering intersection LF = sigIntersection
f55b9bdfae46e3683c74c30f1d063642a41368a5Lennart Poettering generated_sign LF syms sig = do
f55b9bdfae46e3683c74c30f1d063642a41368a5Lennart Poettering sig' <- genSig syms sig
e107ed185ef08945102834234a05ec51bb438685Lennart Poettering inclusionMorph sig' sig
e107ed185ef08945102834234a05ec51bb438685Lennart Poettering cogenerated_sign LF syms sig = do
81429136905a6204875174b60a179333b7f3c9e4Kay Sievers sig' <- coGenSig syms sig
81429136905a6204875174b60a179333b7f3c9e4Kay Sievers inclusionMorph sig' sig
e107ed185ef08945102834234a05ec51bb438685Lennart Poettering induced_from_to_morphism LF m (ExtSign sig1 _) (ExtSign sig2 _) =
e30fa16e27cbd48f960113a1d72d9a15c3b2d67bLennart Poettering inducedFromToMorphism (translMapAnalysis m sig1 sig2) sig1 sig2
e30fa16e27cbd48f960113a1d72d9a15c3b2d67bLennart Poettering induced_from_morphism LF m sig =
f598ac3e28b729dd0b1d0a881df3e16465687a2bLennart Poettering inducedFromMorphism (renamMapAnalysis m sig) sig
01083ad094664e5c685060f4fb35a05ea2f212edLennart Poetteringinstance LogicFram LF
edb2935c5c5b95c42b8679086f60da5eafad74cbLennart Poettering SYMB_MAP_ITEMS
2a781fc9bd33982c81e5ff75974a442a33d4f167Lennart Poettering base_sig LF = baseSig
6a3f892a23db71544d0439355f96c44350dafa8fLennart Poettering write_logic LF = writeLogic
6a3f892a23db71544d0439355f96c44350dafa8fLennart Poettering write_syntax LF = writeSyntax
efc141b8ffbfa1e449da40ce27fccaa81428f779Lennart Poettering write_proof LF = writeProof
efc141b8ffbfa1e449da40ce27fccaa81428f779Lennart Poettering write_model LF = writeModel
d28315e4aff91560ed4c2fc9f876ec8bfc559f2dJan Engelhardt write_comorphism LF = writeComorphism
efc141b8ffbfa1e449da40ce27fccaa81428f779Lennart Poettering read_morphism LF = readMorphism