Logic_LF.hs revision 80d2ec8f37d5ddec13c14b17b1bab01e9c94630a
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
71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
7c66aeba0f28cb82027d6015405ed71afa3b6059Kay SieversModule : $Header$
c904f64d84db8c4eebedf210ba10893f19ba05edLennart PoetteringDescription : Instances of classes defined in Logic.hs for the Edinburgh
c904f64d84db8c4eebedf210ba10893f19ba05edLennart Poettering Logical Framework
f957632b960a0a42999b38ded7089fa602b41745Kay SieversCopyright : (c) Kristina Sojakova, DFKI Bremen 2009
f957632b960a0a42999b38ded7089fa602b41745Kay SieversLicense : GPLv2 or higher, see LICENSE.txt
f957632b960a0a42999b38ded7089fa602b41745Kay SieversMaintainer : k.sojakova@jacobs-university.de
9a36607584bbd1d78775353e022a51794b4e27b1Lennart PoetteringStability : experimental
9a36607584bbd1d78775353e022a51794b4e27b1Lennart PoetteringPortability : portable
2d19f95caef8668aeb5c05a18b39c6b79f710856Kay Sieversimport qualified Data.Map as Map
a4cc3e5ccc0a3033d764a9eb3ae5ee90db560682Lennart Poetteringdata LF = LF deriving Show
0028da22f194f7c0ca7169a48cf32e1bc0f9138aLennart Poetteringinstance Language LF where
a4cc3e5ccc0a3033d764a9eb3ae5ee90db560682Lennart Poettering description LF = "Edinburgh Logical Framework"
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringinstance Category Sign Morphism where
7e2c2bcf1285d124c9c656ff46cafa4db0a987c9Lennart Poettering composeMorphisms = compMorph
7b4da18c1717f811bae67ea3d39290495857c03eLennart Poettering isInclusion = Map.null . symMap . canForm
7b4da18c1717f811bae67ea3d39290495857c03eLennart Poettering legal_mor = const True
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringinstance Syntax LF BASIC_SPEC SYMB_ITEMS SYMB_MAP_ITEMS where
205b7fa46594b38901636b167b02a8725d915b79Lennart Poettering parse_basic_spec LF = Just basicSpec
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering parse_symb_items LF = Just symbItems
95b4be171988fc2ea33377b1b4450e5d410add7bLennart Poettering parse_symb_map_items LF = Just symbMapItems
81d112a8f0522a09fcfe317f420363a2b728137cLennart Poetteringinstance Sentences LF
eb124a97fb72d076014253b1acde69d428f15ecfLennart Poettering map_sen LF m = (Result []) . (translate m)
d01a73b6396f57792113c1b5df6e8492fc703e5eLennart Poettering sym_of LF = singletonList . getSymbols
eb124a97fb72d076014253b1acde69d428f15ecfLennart Poetteringinstance Logic LF
f8aeee1f1fe432924b355f48f01f09c9a552ed97Lennart Poettering SYMB_MAP_ITEMS
81d112a8f0522a09fcfe317f420363a2b728137cLennart Poetteringinstance StaticAnalysis LF
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering SYMB_MAP_ITEMS
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering basic_analysis LF = Just $ basicAnalysis
e41814846c19a48f4490169d82e359e005c4db45Lennart Poettering stat_symb_items LF _ = symbAnalysis
81d112a8f0522a09fcfe317f420363a2b728137cLennart Poettering stat_symb_map_items LF _ = symbMapAnalysis
81d112a8f0522a09fcfe317f420363a2b728137cLennart Poettering symbol_to_raw LF = symName
c0fe5db522b52f27e030655ce2c03e05cbbc1558Kay Sievers matches LF s1 s2 =
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering then symName s1 == s2 --symbols are matched by their name
e9fd44b728ff1fc0d1f24fccb87a767f6865df27Lennart Poettering else True -- expressions are checked manually hence always True
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering empty_signature LF = emptySig
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering is_subsig LF = isSubsig
3040728b6691ea2e9df3a2060e2d49a792bbaedaLennart Poettering subsig_inclusion LF = inclusionMorph
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering signature_union LF = sigUnion
8ed206517c2be381324ac5832bf34cc14024270eLennart Poettering intersection LF = sigIntersection
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering generated_sign LF syms sig = do
e6c6e7afffa80ad74efdb1ddfa815294624f1608Lennart Poettering sig'<- genSig syms sig
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering inclusionMorph sig' sig
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering cogenerated_sign LF syms sig = do
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering sig'<- coGenSig syms sig
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering inclusionMorph sig' sig
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering induced_from_to_morphism LF m (ExtSign sig1 _) (ExtSign sig2 _) =
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering inducedFromToMorphism (translMapAnalysis m sig1 sig2) sig1 sig2
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering induced_from_morphism LF m sig =
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering inducedFromMorphism (renamMapAnalysis m sig) sig
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringinstance LogicFram LF
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart Poettering SYMB_MAP_ITEMS
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering base_sig LF = baseSig
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering write_logic LF = writeLogic
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering write_syntax LF = writeSyntax