Cross Reference: /hets/LF/Logic_LF.hs
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 Sievers{- |
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 Sievers
f957632b960a0a42999b38ded7089fa602b41745Kay SieversMaintainer : k.sojakova@jacobs-university.de
f957632b960a0a42999b38ded7089fa602b41745Kay SieversStability : experimental
a40593a0d0d740efa387e35411e1e456a6c5aba7Lennart PoetteringPortability : portable
20ffc4c4a9226b0e45cc02ad9c0108981626c0bbKay Sievers-}
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poettering
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poetteringmodule LF.Logic_LF where
466784c8710e5cb0e0b86a16506d992d7ec5b619Kay Sievers
55d32caf94d8df547ca763be52b0c35bb6388606Lennart Poetteringimport LF.AS
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poetteringimport LF.Parse
bafb15bab99887d1b6b8a35136531bac6c3876a6Lennart Poetteringimport LF.MorphParser (readMorphism)
f38afcd0c7f558ca5bf0854b42f8c6954f8ad7f3Lennart Poetteringimport LF.Sign
bafb15bab99887d1b6b8a35136531bac6c3876a6Lennart Poetteringimport LF.Morphism
81429136905a6204875174b60a179333b7f3c9e4Kay Sieversimport LF.ATC_LF ()
e7b4d43ec3d5eb0099a3978f98a46f3c15443b23Lennart Poetteringimport LF.Analysis
58f55364fa00a6a4706df2c4a01c6967f432e531Lennart Poetteringimport LF.Framework
58f55364fa00a6a4706df2c4a01c6967f432e531Lennart Poetteringimport LF.ComorphFram ()
81429136905a6204875174b60a179333b7f3c9e4Kay Sievers
fbe1a1a94f19112d7e5d60c40d87487ad24e2ce4Lennart Poetteringimport Logic.Logic
7f035ea56bc0b75327c54e8aa4a56d57ed00dd6dLennart Poettering
7f035ea56bc0b75327c54e8aa4a56d57ed00dd6dLennart Poetteringimport Common.Result
7f035ea56bc0b75327c54e8aa4a56d57ed00dd6dLennart Poetteringimport Common.ExtSign
7f035ea56bc0b75327c54e8aa4a56d57ed00dd6dLennart Poettering
7f035ea56bc0b75327c54e8aa4a56d57ed00dd6dLennart Poetteringimport qualified Data.Map as Map
7f035ea56bc0b75327c54e8aa4a56d57ed00dd6dLennart Poettering
9d6db739ce1eaa3eace21801fd606d523b73c8f4Lennart Poetteringdata LF = LF deriving Show
b6b63571ae3eca1741d54172922961af972b8f20Lennart Poettering
9d6db739ce1eaa3eace21801fd606d523b73c8f4Lennart Poetteringinstance Language LF where
49ee032fc3b694a1b45be9d08a2b97ab3eb93f75Lennart Poettering description LF = "Edinburgh Logical Framework"
49ee032fc3b694a1b45be9d08a2b97ab3eb93f75Lennart Poettering
49ee032fc3b694a1b45be9d08a2b97ab3eb93f75Lennart Poetteringinstance Category Sign Morphism where
bc07548926ec5ed7b13df8d3656654f238e0b9a7Lennart Poettering ide = idMorph
49ee032fc3b694a1b45be9d08a2b97ab3eb93f75Lennart Poettering dom = source
bc07548926ec5ed7b13df8d3656654f238e0b9a7Lennart Poettering cod = target
6992efee44d3affd17dd9174e8673ae63ba01ec7Lennart Poettering composeMorphisms = compMorph
6992efee44d3affd17dd9174e8673ae63ba01ec7Lennart Poettering isInclusion = Map.null . symMap . canForm
6992efee44d3affd17dd9174e8673ae63ba01ec7Lennart Poettering
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 Poettering
bc07548926ec5ed7b13df8d3656654f238e0b9a7Lennart Poetteringinstance Sentences LF
b6b63571ae3eca1741d54172922961af972b8f20Lennart Poettering Sentence
9d6db739ce1eaa3eace21801fd606d523b73c8f4Lennart Poettering Sign
e2a69298819b58f008be61d314f8ab95ccaec427Lennart Poettering Morphism
e2a69298819b58f008be61d314f8ab95ccaec427Lennart Poettering Symbol
58f55364fa00a6a4706df2c4a01c6967f432e531Lennart Poettering where
58f55364fa00a6a4706df2c4a01c6967f432e531Lennart Poettering map_sen LF m = Result [] . translate m
27f1e9ebf6f9e7ff8a898f894c1b38cbdecfa77cLennart Poettering sym_of LF = singletonList . getSymbols
27f1e9ebf6f9e7ff8a898f894c1b38cbdecfa77cLennart Poettering
27f1e9ebf6f9e7ff8a898f894c1b38cbdecfa77cLennart Poetteringinstance Logic LF
ce4a52a500965ae6c2f95787f5346112ed56bbaeLennart Poettering ()
2834ffe78d7fd8be118429aa1449ac72641638c2Lennart Poettering BASIC_SPEC
2834ffe78d7fd8be118429aa1449ac72641638c2Lennart Poettering Sentence
3a53fdaa34eded70d6f971234a9ac78891336f9eLennart Poettering SYMB_ITEMS
3a53fdaa34eded70d6f971234a9ac78891336f9eLennart Poettering SYMB_MAP_ITEMS
0b30586904d3d20dd93136917d24fe00bf6081eeLennart Poettering Sign
0b30586904d3d20dd93136917d24fe00bf6081eeLennart Poettering Morphism
fed515f0a845a2ce387cb2d1fcac1ca36b5bac46Lennart Poettering Symbol
229811628584b370e3fa7e8524d66be46c5a4661Lennart Poettering RAW_SYM
a940778fb1dd16479f455bab3ac6cbdbc5b06165Lennart Poettering ()
a940778fb1dd16479f455bab3ac6cbdbc5b06165Lennart Poettering
a01647e53727107d82382bc5c9d98c894e8f386cLennart Poetteringinstance StaticAnalysis LF
3c779fa59d1825d7db2a9516669d34ded7916913Lennart Poettering BASIC_SPEC
a940778fb1dd16479f455bab3ac6cbdbc5b06165Lennart Poettering Sentence
e8a152c62dd2003731a59e0dffef4336c63110b9Lennart Poettering SYMB_ITEMS
a01647e53727107d82382bc5c9d98c894e8f386cLennart Poettering SYMB_MAP_ITEMS
3de03738fc970496d2d3da668c72767a48ccc41bLennart Poettering Sign
3de03738fc970496d2d3da668c72767a48ccc41bLennart Poettering Morphism
3de03738fc970496d2d3da668c72767a48ccc41bLennart Poettering Symbol
3de03738fc970496d2d3da668c72767a48ccc41bLennart Poettering RAW_SYM
8891f695c71bd4c266d827c9aaedbbbbaf79d3ebLennart Poettering where
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
11fb37f16ed99c1603c9d770b60ce4953b96a58dLennart Poettering
01083ad094664e5c685060f4fb35a05ea2f212edLennart Poetteringinstance LogicFram LF
01083ad094664e5c685060f4fb35a05ea2f212edLennart Poettering ()
b107b705cc97d3033e37c44229deb37b5aa31df5Lennart Poettering BASIC_SPEC
b107b705cc97d3033e37c44229deb37b5aa31df5Lennart Poettering Sentence
edb2935c5c5b95c42b8679086f60da5eafad74cbLennart Poettering SYMB_ITEMS
edb2935c5c5b95c42b8679086f60da5eafad74cbLennart Poettering SYMB_MAP_ITEMS
769918ecd30c0f7ee6e87b9aa6226d956bd2f530Lennart Poettering Sign
769918ecd30c0f7ee6e87b9aa6226d956bd2f530Lennart Poettering Morphism
769918ecd30c0f7ee6e87b9aa6226d956bd2f530Lennart Poettering Symbol
769918ecd30c0f7ee6e87b9aa6226d956bd2f530Lennart Poettering RAW_SYM
6a3f892a23db71544d0439355f96c44350dafa8fLennart Poettering ()
2a781fc9bd33982c81e5ff75974a442a33d4f167Lennart Poettering where
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