Cross Reference: /hets/LF/Logic_LF.hs
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 Sievers{- |
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 Sievers
f957632b960a0a42999b38ded7089fa602b41745Kay SieversMaintainer : k.sojakova@jacobs-university.de
9a36607584bbd1d78775353e022a51794b4e27b1Lennart PoetteringStability : experimental
9a36607584bbd1d78775353e022a51794b4e27b1Lennart PoetteringPortability : portable
a40593a0d0d740efa387e35411e1e456a6c5aba7Lennart Poettering-}
20ffc4c4a9226b0e45cc02ad9c0108981626c0bbKay Sievers
7bcd865d386d96caac83cb1c589fdb8f9ce3b081Zbigniew Jędrzejewski-Szmekmodule LF.Logic_LF where
7bcd865d386d96caac83cb1c589fdb8f9ce3b081Zbigniew Jędrzejewski-Szmek
7bcd865d386d96caac83cb1c589fdb8f9ce3b081Zbigniew Jędrzejewski-Szmekimport LF.AS
2f8d077ece024b985f2501dc8c904c2d29967acbKay Sieversimport LF.Parse
2f8d077ece024b985f2501dc8c904c2d29967acbKay Sieversimport LF.Sign
2d19f95caef8668aeb5c05a18b39c6b79f710856Kay Sieversimport LF.Morphism
2f8d077ece024b985f2501dc8c904c2d29967acbKay Sieversimport LF.ATC_LF ()
81d112a8f0522a09fcfe317f420363a2b728137cLennart Poetteringimport LF.Analysis
c0fe5db522b52f27e030655ce2c03e05cbbc1558Kay Sieversimport LF.Framework
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering
c0fe5db522b52f27e030655ce2c03e05cbbc1558Kay Sieversimport Logic.Logic
c3090674833c8bd34fbdb0e743f1c47d85dd14fbLennart Poettering
81d112a8f0522a09fcfe317f420363a2b728137cLennart Poetteringimport Common.Result
81d112a8f0522a09fcfe317f420363a2b728137cLennart Poetteringimport Common.ExtSign
2d19f95caef8668aeb5c05a18b39c6b79f710856Kay Sievers
2d19f95caef8668aeb5c05a18b39c6b79f710856Kay Sieversimport qualified Data.Map as Map
a4cc3e5ccc0a3033d764a9eb3ae5ee90db560682Lennart Poettering
a4cc3e5ccc0a3033d764a9eb3ae5ee90db560682Lennart Poetteringdata LF = LF deriving Show
a4cc3e5ccc0a3033d764a9eb3ae5ee90db560682Lennart Poettering
0028da22f194f7c0ca7169a48cf32e1bc0f9138aLennart Poetteringinstance Language LF where
a4cc3e5ccc0a3033d764a9eb3ae5ee90db560682Lennart Poettering description LF = "Edinburgh Logical Framework"
7e2c2bcf1285d124c9c656ff46cafa4db0a987c9Lennart Poettering
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringinstance Category Sign Morphism where
7e2c2bcf1285d124c9c656ff46cafa4db0a987c9Lennart Poettering ide = idMorph
7e2c2bcf1285d124c9c656ff46cafa4db0a987c9Lennart Poettering dom = source
7e2c2bcf1285d124c9c656ff46cafa4db0a987c9Lennart Poettering cod = target
7e2c2bcf1285d124c9c656ff46cafa4db0a987c9Lennart Poettering composeMorphisms = compMorph
7b4da18c1717f811bae67ea3d39290495857c03eLennart Poettering isInclusion = Map.null . symMap . canForm
7b4da18c1717f811bae67ea3d39290495857c03eLennart Poettering legal_mor = const True
788f75a0e766738c052086e856b7c1b1b676de6bLennart Poettering
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 Poettering
81d112a8f0522a09fcfe317f420363a2b728137cLennart Poetteringinstance Sentences LF
81d112a8f0522a09fcfe317f420363a2b728137cLennart Poettering Sentence
81d112a8f0522a09fcfe317f420363a2b728137cLennart Poettering Sign
eb124a97fb72d076014253b1acde69d428f15ecfLennart Poettering Morphism
990ffbe5cffe7f11a8d3ab2258a85fc52b97bf60Lennart Poettering Symbol
eb124a97fb72d076014253b1acde69d428f15ecfLennart Poettering where
eb124a97fb72d076014253b1acde69d428f15ecfLennart Poettering map_sen LF m = (Result []) . (translate m)
d01a73b6396f57792113c1b5df6e8492fc703e5eLennart Poettering sym_of LF = singletonList . getSymbols
d01a73b6396f57792113c1b5df6e8492fc703e5eLennart Poettering
eb124a97fb72d076014253b1acde69d428f15ecfLennart Poetteringinstance Logic LF
eb124a97fb72d076014253b1acde69d428f15ecfLennart Poettering ()
990ffbe5cffe7f11a8d3ab2258a85fc52b97bf60Lennart Poettering BASIC_SPEC
f8aeee1f1fe432924b355f48f01f09c9a552ed97Lennart Poettering Sentence
f8aeee1f1fe432924b355f48f01f09c9a552ed97Lennart Poettering SYMB_ITEMS
f8aeee1f1fe432924b355f48f01f09c9a552ed97Lennart Poettering SYMB_MAP_ITEMS
f8aeee1f1fe432924b355f48f01f09c9a552ed97Lennart Poettering Sign
f8aeee1f1fe432924b355f48f01f09c9a552ed97Lennart Poettering Morphism
f8aeee1f1fe432924b355f48f01f09c9a552ed97Lennart Poettering Symbol
f8aeee1f1fe432924b355f48f01f09c9a552ed97Lennart Poettering RAW_SYM
81d112a8f0522a09fcfe317f420363a2b728137cLennart Poettering ()
490b7e47093d491a2bdb1084fe92b796f4e07eefLennart Poettering
81d112a8f0522a09fcfe317f420363a2b728137cLennart Poetteringinstance StaticAnalysis LF
490b7e47093d491a2bdb1084fe92b796f4e07eefLennart Poettering BASIC_SPEC
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering Sentence
5965984d6b9f7751d6281028142ecf3ca475f156Lennart Poettering SYMB_ITEMS
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering SYMB_MAP_ITEMS
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering Sign
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering Morphism
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering Symbol
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering RAW_SYM
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering where
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 =
e9fd44b728ff1fc0d1f24fccb87a767f6865df27Lennart Poettering if (isSym 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 Poettering
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poetteringinstance LogicFram LF
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering ()
eb124a97fb72d076014253b1acde69d428f15ecfLennart Poettering BASIC_SPEC
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart Poettering Sentence
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering SYMB_ITEMS
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart Poettering SYMB_MAP_ITEMS
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering Sign
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart Poettering Morphism
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering Symbol
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart Poettering RAW_SYM
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering ()
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering where
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering base_sig LF = baseSig
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering write_logic LF = writeLogic
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering write_syntax LF = writeSyntax
b44be3ecf6326c27aa2c6c6d1fe34e22e22592a0Lennart Poettering