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
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederDescription : coding out subsorting
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederCopyright : (c) C. Maeder DFKI GmbH 2012
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederMaintainer : Christian.Maeder@dfki.de
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederStability : provisional
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederPortability : non-portable (imports Logic.Logic)
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederCoding out subsorting (SubPCFOL= -> PCFOL=),
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder following Chap. III:3.1 of the CASL Reference Manual
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maedermodule Comorphisms.ExtModal2ExtModalTotal where
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport qualified Data.Map as Map
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederimport qualified Data.Set as Set
683ee7dc6ecd65a50eb224cf5fa32ca39d907a8cChristian Maederimport qualified Common.Lib.MapSet as MapSet
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder-- | The identity of the comorphism
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederdata ExtModal2ExtModalTotal = ExtModal2ExtModalTotal deriving Show
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederinstance Language ExtModal2ExtModalTotal -- default definition is okay
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maederinstance Comorphism ExtModal2ExtModalTotal
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder SYMB_MAP_ITEMS ExtModalSign ExtModalMorph
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder Symbol RawSymbol ()
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder SYMB_MAP_ITEMS ExtModalSign ExtModalMorph
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder Symbol RawSymbol () where
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder sourceLogic ExtModal2ExtModalTotal = ExtModal
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder sourceSublogic ExtModal2ExtModalTotal = mkTop maxSublogic
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder targetLogic ExtModal2ExtModalTotal = ExtModal
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder mapSublogic ExtModal2ExtModalTotal sl = Just
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder $ if has_part sl then sl
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder { has_part = False -- partiality is coded out
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder , has_pred = True
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder , which_logic = max Horn $ which_logic sl
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder , has_eq = True} else sl
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder map_theory ExtModal2ExtModalTotal (sig, sens) = let
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder bsrts = emsortsWithBottom sig
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder sens1 = generateAxioms True bsrts sig
bdb38ed280979a57381ed914ef48d105b8e84fe7Christian Maeder sens2 = map (mapNamed (noCondsEMFormula . simplifyEMFormula
bdb38ed280979a57381ed914ef48d105b8e84fe7Christian Maeder . codeEMFormula bsrts)) sens
683ee7dc6ecd65a50eb224cf5fa32ca39d907a8cChristian Maeder ( emEncodeSig bsrts sig
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder , nameAndDisambiguate $ sens1 ++ sens2)
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder map_morphism ExtModal2ExtModalTotal mor@Morphism
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder {msource = src, mtarget = tar}
683ee7dc6ecd65a50eb224cf5fa32ca39d907a8cChristian Maeder mor { msource = emEncodeSig (emsortsWithBottom src) src
683ee7dc6ecd65a50eb224cf5fa32ca39d907a8cChristian Maeder , mtarget = emEncodeSig (emsortsWithBottom tar) tar
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder , op_map = Map.map (\ (i, _) -> (i, Total)) $ op_map mor }
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder map_sentence ExtModal2ExtModalTotal sig sen = let
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder bsrts = emsortsWithBottom sig
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder in return $ simplifyEMFormula $ codeEMFormula bsrts sen
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder map_symbol ExtModal2ExtModalTotal _ s =
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder Set.singleton s { symbType = totalizeSymbType $ symbType s }
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder has_model_expansion ExtModal2ExtModalTotal = True
914b90f3d6644fd464c5b26712b65d515a58c037Christian Maeder is_weakly_amalgamable ExtModal2ExtModalTotal = True
683ee7dc6ecd65a50eb224cf5fa32ca39d907a8cChristian MaederemEncodeSig :: Set.Set SORT -> Sign f EModalSign -> Sign f EModalSign
683ee7dc6ecd65a50eb224cf5fa32ca39d907a8cChristian MaederemEncodeSig bsrts sig = (encodeSig bsrts sig)
683ee7dc6ecd65a50eb224cf5fa32ca39d907a8cChristian Maeder { extendedInfo = let extInfo = extendedInfo sig in
683ee7dc6ecd65a50eb224cf5fa32ca39d907a8cChristian Maeder extInfo { flexOps = MapSet.map mkTotal $ flexOps extInfo }}
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederemsortsWithBottom :: Sign f e -> Set.Set SORT
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaederemsortsWithBottom sig = sortsWithBottom NoMembershipOrCast sig Set.empty
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaedersimplifyEM :: EM_FORMULA -> EM_FORMULA
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaedersimplifyEM = mapExtForm simplifyEMFormula
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaedersimplifyEMFormula :: FORMULA EM_FORMULA -> FORMULA EM_FORMULA
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaedersimplifyEMFormula = simplifyFormula simplifyEM
bdb38ed280979a57381ed914ef48d105b8e84fe7Christian MaedernoCondsEM :: EM_FORMULA -> EM_FORMULA
bdb38ed280979a57381ed914ef48d105b8e84fe7Christian MaedernoCondsEM = mapExtForm noCondsEMFormula
bdb38ed280979a57381ed914ef48d105b8e84fe7Christian MaedernoCondsEMFormula :: FORMULA EM_FORMULA -> FORMULA EM_FORMULA
bdb38ed280979a57381ed914ef48d105b8e84fe7Christian MaedernoCondsEMFormula = codeOutConditionalF noCondsEM
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaedercodeEM :: Set.Set SORT -> EM_FORMULA -> EM_FORMULA
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaedercodeEM = mapExtForm . codeEMFormula
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaedercodeEMFormula :: Set.Set SORT -> FORMULA EM_FORMULA -> FORMULA EM_FORMULA
914b90f3d6644fd464c5b26712b65d515a58c037Christian MaedercodeEMFormula bsrts = foldFormula (codeRecord True bsrts $ codeEM bsrts)