Cross Reference: /hets/Comorphisms/THFP_P2THFP.hs
THFP_P2THFP.hs revision ad1df93673cf323534cdfe18981ad5daae4c90c0
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
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder{- |
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von SchroederModule : $Header$
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von SchroederDescription : Comorphism from THFP_P to THFP
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von SchroederCopyright : (c) J. von Schroeder, DFKI Bremen 2012
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von SchroederLicense : GPLv2 or higher, see LICENSE.txt
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder
ad1df93673cf323534cdfe18981ad5daae4c90c0Jonathan von SchroederMaintainer : J. von Schroeder <jonathan.von_schroeder@dfki.de>
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von SchroederStability : provisional
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von SchroederPortability : non-portable (imports Logic.Logic)
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von SchroederThe comorphism from THFP to THF0.
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder-}
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroedermodule Comorphisms.THFP_P2THFP where
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroederimport Logic.Logic as Logic
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroederimport Logic.Comorphism
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroederimport Common.ProofTree
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroederimport Common.Result
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroederimport Common.AS_Annotation (Named)
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroederimport THF.Logic_THF
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroederimport THF.Cons
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroederimport THF.Sign
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroederimport qualified THF.Sublogic as SL
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroederimport THF.As
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroederimport THF.Utils
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroederimport THF.Poly
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroederdata THFP_P2THFP = THFP_P2THFP deriving Show
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroederinstance Language THFP_P2THFP
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroederinstance Comorphism THFP_P2THFP
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder THF SL.THFSl
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder BasicSpecTHF THFFormula () ()
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder SignTHF MorphismTHF SymbolTHF () ProofTree
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder THF SL.THFSl
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder BasicSpecTHF THFFormula () ()
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder SignTHF MorphismTHF SymbolTHF () ProofTree where
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder sourceLogic THFP_P2THFP = THF
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder sourceSublogic THFP_P2THFP = SL.tHFP_P
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder targetLogic THFP_P2THFP = THF
fee6e355c164d9248e0512436812a476ad0c2e99Jonathan von Schroeder mapSublogic THFP_P2THFP sl = Just $ sl { SL.ext_Poly = False }
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder map_theory THFP_P2THFP = trans_theory
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder has_model_expansion THFP_P2THFP = True
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroedertrans_theory :: (SignTHF,[Named THFFormula])
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder -> Result (SignTHF,[Named THFFormula])
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroedertrans_theory (sig, sentences1) = do
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder (cs,sentences) <- infer (consts sig) sentences1
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder let sig1 = sig {consts = cs}
880945fae9c3f61341f1cd94439c802b7a0af194Jonathan von Schroeder return (recreateSymbols sig1,sentences)